twee 2.5 → 2.6.1
raw patch · 14 files changed
+619/−284 lines, 14 filesdep ~jukeboxdep ~twee-lib
Dependency ranges changed: jukebox, twee-lib
Files
- executable/SequentialMain.hs +362/−262
- misc/BestTwee.hs +14/−10
- tests/KLE125+1.p +47/−0
- tests/ROB001-1-a.p +42/−0
- tests/ROB007-1-b.p +12/−0
- tests/aim.p +7/−7
- tests/nicomachus-tptp-2.p +19/−0
- tests/nicomachus-tptp.p +20/−0
- tests/nicomachus2.p +36/−0
- tests/rob.p +7/−0
- tests/rob2.p +7/−0
- tests/sum.p +30/−0
- tests/wos.p +6/−0
- twee.cabal +10/−5
executable/SequentialMain.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass, RankNTypes #-}+{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass, RankNTypes, ApplicativeDo #-} {-# OPTIONS_GHC -flate-specialise #-} module SequentialMain(main) where @@ -32,7 +32,7 @@ import System.IO import System.Exit import qualified Data.Set as Set-import qualified Data.Label as Label+import qualified Data.Intern as Intern import System.Console.ANSI import Data.Symbol import Twee.Profile@@ -40,6 +40,7 @@ data MainFlags = MainFlags { flags_proof :: Bool,+ flags_proof_on_saturation :: Bool, flags_trace :: Maybe (String, String), flags_formal_proof :: Bool, flags_explain_encoding :: Bool,@@ -56,197 +57,234 @@ flags_equals_transformation :: Bool, flags_distributivity_heuristic :: Bool, flags_kbo_weight0 :: Bool,+ flags_kbo_weight0_unary :: Bool, flags_goal_heuristic :: Bool } parseMainFlags :: OptionParser MainFlags-parseMainFlags =- MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenNonGround <*> flattenLightly <*> flattenAll <*> flattenRegeneralise <*> eliminate <*> backwardsGoal <*> flattenBackwardsGoal <*> equalsTransformation <*> distributivityHeuristic <*> kboWeight0 <*> goalHeuristic- where- proof =- inGroup "Output options" $- bool "proof" ["Produce proofs (on by default)."]- True- trace =- expert $- inGroup "Output options" $- flag "trace"- ["Write a Prolog-format execution trace to this file (off by default)."]- Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule)- formal =- expert $- inGroup "Output options" $- bool "formal-proof" ["Print proof as formal TSTP derivation (requires --tstp; off by default)."] False- explain =- expert $- inGroup "Output options" $- bool "explain-encoding" ["In CASC mode, explain the conditional encoding (off by default)."] False- flipOrdering =- expert $- inGroup "Term order options" $- bool "flip-ordering" ["Make more common function symbols smaller (off by default)."] False- kboWeight0 =- expert $- inGroup "Term order options" $- bool "kbo-weight0" ["Give functions of arity >= 2 a weight of 0."] False- giveUp =- expert $- inGroup "Output options" $- bool "give-up-on-saturation" ["Report SZS status GiveUp rather than Unsatisfiable on saturation (off by default)."] False- flatten =- expert $- inGroup "Completion heuristics" $- bool "flatten-goal" ["Flatten goal by adding new axioms (on by default)."] True- flattenNonGround =- expert $- inGroup "Completion heuristics" $- bool "flatten-nonground" ["Flatten even non-ground clauses (off by default)."] False- flattenLightly =- expert $- inGroup "Completion heuristics" $- bool "flatten-goal-lightly" ["Flatten goal non-recursively by adding new axioms (off by default)."] False- flattenAll =- expert $- inGroup "Completion heuristics" $- bool "flatten" ["Flatten all clauses by adding new axioms (off by default)."] False- flattenRegeneralise =- expert $- inGroup "Completion heuristics" $- bool "flatten-regeneralise" ["Regeneralise rules involving flattened goal terms (off by default)."] False- backwardsGoal =- expert $- inGroup "Completion heuristics" $- flag "backwards-goal" ["Try rewriting backwards from the goal this many times (0 by default)."] 0 argNum- flattenBackwardsGoal =- expert $- inGroup "Completion heuristics" $- flag "flatten-backwards-goal" ["Try rewriting backwards from the goal this many times when flattening (0 by default)."] 0 argNum- equalsTransformation =- expert $- inGroup "Completion heuristics" $- bool "equals-transformation" ["Apply the 'equals transformation' even to ground goals (off by default)."] False- distributivityHeuristic =- expert $- inGroup "Completion heuristics" $- bool "distributivity-heuristic" ["Treat distributive operators specially (off by default)."] False- goalHeuristic =- expert $- inGroup "Completion heuristics" $- bool "goal-heuristic" ["Use the CP weighting heuristic from Anantharaman and Andrianarievelo (off by default)."] False- eliminate =- inGroup "Proof presentation" $- concat <$>- manyFlags "eliminate"- ["Treat these axioms as definitions and eliminate them from the proof.",- "The axiom must have the shape f(x1...xn) = t, where x1...xn are",- "distinct variables. The term f must not otherwise appear in the problem!",- "This is not checked."]- (splitOn "," <$> arg "<axioms>" "expected a list of axiom names" Just)+parseMainFlags = do+ let argModule = arg "<module>" "expected a Prolog module name" Just+ flags_proof <-+ inGroup "Output options" $+ bool "proof" ["Produce proofs (on by default)."]+ True+ flags_proof_on_saturation <-+ expert $+ inGroup "Output options" $+ bool "proof-on-saturation" ["Produce proofs of all rewrite rules on saturation (off by default)."]+ False+ flags_trace <-+ expert $+ inGroup "Output options" $+ flag "trace"+ ["Write a Prolog-format execution trace to this file (off by default)."]+ Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule)+ flags_formal_proof <-+ expert $+ inGroup "Output options" $+ bool "formal-proof" ["Print proof as formal TSTP derivation (requires --tstp; off by default)."] False+ flags_explain_encoding <-+ expert $+ inGroup "Output options" $+ bool "explain-encoding" ["In CASC mode, explain the conditional encoding (off by default)."] False+ flags_flip_ordering <-+ expert $+ inGroup "Term order options" $+ bool "flip-ordering" ["Make more common function symbols smaller (off by default)."] False+ flags_kbo_weight0 <-+ expert $+ inGroup "Term order options" $+ bool "kbo-weight0" ["Give functions of arity >= 2 a weight of 0."] False+ flags_kbo_weight0_unary <-+ expert $+ inGroup "Term order options" $+ bool "kbo-weight0-unary" ["Give one function of arity 1 a weight of 0."] True+ flags_give_up_on_saturation <-+ expert $+ inGroup "Output options" $+ bool "give-up-on-saturation" ["Report SZS status GiveUp rather than Unsatisfiable on saturation (off by default)."] False+ flags_flatten_goals <-+ expert $+ inGroup "Completion heuristics" $+ bool "flatten-goal" ["Flatten goal by adding new axioms (on by default)."] True+ flags_flatten_nonground <-+ expert $+ inGroup "Completion heuristics" $+ bool "flatten-nonground" ["Flatten even non-ground clauses (off by default)."] False+ flags_flatten_goals_lightly <-+ expert $+ inGroup "Completion heuristics" $+ bool "flatten-goal-lightly" ["Flatten goal non-recursively by adding new axioms (off by default)."] False+ flags_flatten_all <-+ expert $+ inGroup "Completion heuristics" $+ bool "flatten" ["Flatten all clauses by adding new axioms (off by default)."] False+ flags_flatten_regeneralise <-+ expert $+ inGroup "Completion heuristics" $+ bool "flatten-regeneralise" ["Regeneralise rules involving flattened goal terms (off by default)."] False+ flags_backwards_goal <-+ expert $+ inGroup "Completion heuristics" $+ flag "backwards-goal" ["Try rewriting backwards from the goal this many times (0 by default)."] 0 argNum+ flags_flatten_backwards_goal <-+ expert $+ inGroup "Completion heuristics" $+ flag "flatten-backwards-goal" ["Try rewriting backwards from the goal this many times when flattening (0 by default)."] 0 argNum+ flags_equals_transformation <-+ expert $+ inGroup "Completion heuristics" $+ bool "equals-transformation" ["Apply the 'equals transformation' even to ground goals (off by default)."] False+ flags_distributivity_heuristic <-+ expert $+ inGroup "Completion heuristics" $+ bool "distributivity-heuristic" ["Treat distributive operators specially (off by default)."] False+ flags_goal_heuristic <-+ expert $+ inGroup "Completion heuristics" $+ bool "goal-heuristic" ["Use the CP weighting heuristic from Anantharaman and Andrianarievelo (off by default)."] False+ flags_eliminate <-+ inGroup "Proof presentation" $+ concat <$>+ manyFlags "eliminate"+ ["Treat these axioms as definitions and eliminate them from the proof.",+ "The axiom must have the shape f(x1...xn) = t, where x1...xn are",+ "distinct variables. The term f must not otherwise appear in the problem!",+ "This is not checked."]+ (splitOn "," <$> arg "<axioms>" "expected a list of axiom names" Just) - argModule = arg "<module>" "expected a Prolog module name" Just+ return MainFlags{..} parseConfig :: OptionParser (Config Constant)-parseConfig =- Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> maxRules <*> simplify <*> normPercent <*> cpSampleSize <*> cpRenormaliseThreshold <*> set_join_goals <*> always_simplify <*> complete_subsets <*>- pure undefined <*> -- scoring function - filled in later, in runTwee- (Join.Config <$> ground_join <*> connectedness <*> ground_connectedness <*> set_join) <*>- (Proof.Config <$> all_lemmas <*> flat_proof <*> ground_proof <*> show_instances <*> colour <*> show_axiom_uses) <*> pure [] <*> randomMode <*> randomModeGoalDirected <*> randomModeSimple <*> randomModeBestOf <*> alwaysComplete- where- maxSize =- inGroup "Resource limits" $- flag "max-term-size" ["Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default)."] Nothing (Just <$> checkSize <$> argNum)- checkSize n t = KBO.size t <= n- maxCPs =- inGroup "Resource limits" $- flag "max-cps" ["Give up after considering this many critical pairs (unlimited by default)."] maxBound argNum- maxCPDepth =- inGroup "Resource limits" $- flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum- maxRules =- inGroup "Resource limits" $- flag "max-rules" ["Give up after generating this many rules (unlimited by default)."] maxBound argNum- simplify =- expert $- inGroup "Completion heuristics" $- bool "simplify"- ["Simplify rewrite rules with respect to one another (on by default)."]- True- normPercent =- expert $- inGroup "Completion heuristics" $- defaultFlag "normalise-queue-percent" "Percent of time spent renormalising queued critical pairs" cfg_renormalise_percent argNum- cpSampleSize =- expert $- inGroup "Completion heuristics" $- defaultFlag "cp-sample-size" "Size of random CP sample used to trigger renormalisation" cfg_cp_sample_size argNum- cpRenormaliseThreshold =- expert $- inGroup "Completion heuristics" $- defaultFlag "cp-renormalise-threshold" "Trigger renormalisation when this percentage of CPs can be simplified" cfg_renormalise_threshold argNum- ground_join =+parseConfig = do+ cfg_accept_term <-+ let checkSize n t = KBO.size (t :: Term Constant) <= n in+ inGroup "Resource limits" $+ flag "max-term-size" ["Discard rewrite rules whose left-hand side is bigger than this limit (unlimited by default)."] Nothing (Just <$> checkSize <$> argNum)+ cfg_max_critical_pairs <-+ inGroup "Resource limits" $+ flag "max-cps" ["Give up after considering this many critical pairs (unlimited by default)."] maxBound argNum+ cfg_max_cp_depth <-+ inGroup "Resource limits" $+ flag "max-cp-depth" ["Only consider critical pairs up to this depth (unlimited by default)."] maxBound argNum+ cfg_max_rules <-+ inGroup "Resource limits" $+ flag "max-rules" ["Give up after generating this many rules (unlimited by default)."] maxBound argNum+ cfg_max_time <-+ inGroup "Resource limits" $+ flag "max-time" ["Give up after running for this long in seconds (unlimited by default)."] Nothing (Just <$> argNum)+ cfg_simplify <-+ expert $+ inGroup "Completion heuristics" $+ bool "simplify"+ ["Simplify rewrite rules with respect to one another (on by default)."]+ True+ cfg_renormalise_percent <-+ expert $+ inGroup "Completion heuristics" $+ defaultFlag "normalise-queue-percent" "Percent of time spent renormalising queued critical pairs" cfg_renormalise_percent argNum+ cfg_cp_sample_size <-+ expert $+ inGroup "Completion heuristics" $+ defaultFlag "cp-sample-size" "Size of random CP sample used to trigger renormalisation" cfg_cp_sample_size argNum+ cfg_renormalise_threshold <-+ expert $+ inGroup "Completion heuristics" $+ defaultFlag "cp-renormalise-threshold" "Trigger renormalisation when this percentage of CPs can be simplified" cfg_renormalise_threshold argNum+ cfg_set_join_goals <-+ expert $+ inGroup "Critical pair joining heuristics" $+ bool "set-join-goals"+ ["Compute all normal forms when joining goal terms (on by default)."]+ True+ cfg_always_simplify <-+ expert $+ inGroup "Debugging options" $+ bool "always-simplify"+ ["Interreduce rules after every step."]+ False+ cfg_complete_subsets <-+ expert $+ inGroup "Critical pair joining heuristics" $+ bool "complete-subsets"+ ["Identify and exploit complete subsets of the axioms in joining (off by default)."]+ False+ let cfg_score_cp = undefined -- filled in later, in runTwee++ cfg_join <- do+ cfg_ground_join <- expert $ inGroup "Critical pair joining heuristics" $ bool "ground-joining" ["Test terms for ground joinability (on by default)."] True- connectedness =+ cfg_use_connectedness_standalone <- expert $ inGroup "Critical pair joining heuristics" $ bool "connectedness" ["Test terms for subconnectedness, as a separate check (on by default)."] True- ground_connectedness =+ cfg_use_connectedness_in_ground_joining <- expert $ inGroup "Critical pair joining heuristics" $ bool "ground-connectedness" ["Test terms for subconnectedness, as part of ground joinability testing (off by default)."] False- complete_subsets =- expert $- inGroup "Critical pair joining heuristics" $- bool "complete-subsets"- ["Identify and exploit complete subsets of the axioms in joining (off by default)."]- False- set_join =+ cfg_set_join <- expert $ inGroup "Critical pair joining heuristics" $ bool "set-join" ["Compute all normal forms when joining critical pairs (off by default)."] False- set_join_goals =- expert $+ cfg_ground_join_limit <- inGroup "Critical pair joining heuristics" $- bool "set-join-goals"- ["Compute all normal forms when joining goal terms (on by default)."]- True- always_simplify =- expert $- inGroup "Debugging options" $- bool "always-simplify"- ["Interreduce rules after every step."]- False- all_lemmas =+ flag "ground-joining-limit" ["Assume not ground joinable after considering this many orderings (unlimited by default)."] maxBound argNum+ cfg_ground_join_incomplete_limit <-+ inGroup "Critical pair joining heuristics" $+ flag "ground-joining-incomplete-limit" ["Assume ground joinable after considering this many orderings (unlimited by default)."] maxBound argNum+ return Join.Config{..}++ cfg_proof_presentation <- do+ cfg_all_lemmas <- inGroup "Proof presentation" $ bool "all-lemmas" ["Produce a proof with one lemma for each critical pair (off by default)."] False- flat_proof =+ cfg_no_lemmas <- inGroup "Proof presentation" $ bool "no-lemmas" ["Produce a proof with no lemmas (off by default).", "May lead to exponentially large proofs."] False- ground_proof =+ cfg_ground_proof <- inGroup "Proof presentation" $ bool "ground-proof" ["Produce a ground proof (off by default).", "May lead to exponentially large proofs."] False- show_instances =+ cfg_show_instances <- inGroup "Proof presentation" $ bool "show-instances" ["Show which instance of a lemma or axiom each rewrite step uses (off by default)."] False- show_axiom_uses =+ cfg_use_colour <-+ let+ colourFlag =+ inGroup "Proof presentation" $+ primFlag "(no-)colour"+ ["Produce output in colour (on by default if writing output to a terminal)."]+ (`elem` map fst colourFlags)+ (\_ y -> return y)+ Nothing+ (pure (`lookup` colourFlags))+ colourFlags = [("--colour", True), ("--no-colour", False),+ ("--color", True), ("--no-color", False)]+ colourSupported =+ liftM2 (&&) (hSupportsANSIColor stdout)+ (return (setSGRCode [] /= "")) -- Check for Windows terminal not supporting ANSI+ in fromMaybe <$> io colourSupported <*> colourFlag++ cfg_show_uses_of_axioms <-+ let interpret xss ax = axiom_name ax `elem` xss || "all" `elem` xss in inGroup "Proof presentation" $ interpret <$> concat <$>@@ -255,49 +293,68 @@ "Separate multiple axiom names with commas.", "Use --show-uses-of all to show uses of all axioms."] (splitOn "," <$> arg "<axioms>" "expected a list of axiom names" Just)- where- interpret xss ax = axiom_name ax `elem` xss || "all" `elem` xss- randomMode =- expert $- inGroup "Completion heuristics" $- bool "random-mode"- ["Use random testing to find suitable CPs (doesn't work yet!) (off by default)."]- False- randomModeGoalDirected =- expert $- inGroup "Completion heuristics" $- bool "random-mode-goal-directed"- ["Use goal-direction in --random-mode (off by default)."]- False- randomModeSimple =- expert $- inGroup "Completion heuristics" $- bool "random-mode-simple"- ["Use simple version of --random-mode (off by default)."]- False- randomModeBestOf =- inGroup "Completion heuristics" $- defaultFlag "random-mode-best-of" "Generate this many critical pairs at a time and pick the best one" cfg_random_mode_best_of argNum- alwaysComplete =- inGroup "Input and clausifier options" $- bool "complete"- ["Don't stop until the rewrite system is confluent"]++ cfg_show_peaks <-+ inGroup "Proof presentation" $+ bool "show-peaks"+ ["Show peak terms in a proof (off by default)."] False- colour = fromMaybe <$> io colourSupported <*> colourFlag- colourFlag =+ cfg_eliminate_existentials_coding <- inGroup "Proof presentation" $- primFlag "(no-)colour"- ["Produce output in colour (on by default if writing output to a terminal)."]- (`elem` map fst colourFlags)- (\_ y -> return y)- Nothing- (pure (`lookup` colourFlags))- colourFlags = [("--colour", True), ("--no-colour", False),- ("--color", True), ("--no-color", False)]- colourSupported =- liftM2 (&&) (hSupportsANSIColor stdout)- (return (setSGRCode [] /= "")) -- Check for Windows terminal not supporting ANSI+ bool "eliminate-existentials-coding"+ ["Eliminate $equals from proofs (on by default)."]+ True+ cfg_show_subterms <-+ inGroup "Proof presentation" $+ bool "show-subterms"+ ["Show which subterm is rewritten at each step (off by default)."]+ False + return Proof.Config{..}++ let cfg_eliminate_axioms = [] -- filled in later++ cfg_random_mode <-+ expert $+ inGroup "Completion heuristics" $+ bool "random-mode"+ ["Use random testing to find suitable CPs (doesn't work yet!) (off by default)."]+ False+ cfg_random_mode_goal_directed <-+ expert $+ inGroup "Completion heuristics" $+ bool "random-mode-goal-directed"+ ["Use goal-direction in --random-mode (off by default)."]+ False+ cfg_random_mode_simple <-+ expert $+ inGroup "Completion heuristics" $+ bool "random-mode-simple"+ ["Use simple version of --random-mode (off by default)."]+ False+ cfg_random_mode_best_of <-+ inGroup "Completion heuristics" $+ defaultFlag "random-mode-best-of" "Generate this many critical pairs at a time and pick the best one" cfg_random_mode_best_of argNum+ cfg_always_complete <-+ inGroup "Input and clausifier options" $+ bool "complete"+ ["Don't stop until the rewrite system is confluent"]+ False+ cfg_hint_skel_cost <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "hint-skel-cost" "Size of hint skeletons" cfg_hint_skel_cost argNum+ cfg_hint_skel_factor <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "hint-skel-factor" "Size factor of hint skeletons" cfg_hint_skel_factor argNum+ cfg_print_score <-+ expert $+ inGroup "Output options" $+ bool "print-score" ["Print score of each generated rule (off by default)."] False++ return Config{..}+ where defaultFlag :: Show a => String -> String -> (Config Constant -> a) -> ArgParser a -> OptionParser a defaultFlag name desc field parser = flag name [desc ++ " (" ++ show def ++ " by default)."] def parser@@ -305,38 +362,41 @@ def = field defaultConfig parseCPConfig :: OptionParser CP.Config-parseCPConfig =- CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor+parseCPConfig = do+ cfg_lhsweight <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "lhs-weight" "Weight given to LHS of critical pair" CP.cfg_lhsweight argNum+ cfg_rhsweight <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "rhs-weight" "Weight given to RHS of critical pair" CP.cfg_rhsweight argNum+ cfg_funweight <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "fun-weight" "Weight given to function symbols" CP.cfg_funweight argNum+ cfg_varweight <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "var-weight" "Weight given to variable symbols" CP.cfg_varweight argNum+ cfg_depthweight <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "depth-weight" "Weight given to critical pair depth" CP.cfg_depthweight argNum+ cfg_dupcost <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "dup-cost" "Cost of duplicate subterms" CP.cfg_dupcost argNum+ cfg_dupfactor <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ defaultFlag "dup-factor" "Size factor of duplicate subterms" CP.cfg_dupfactor argNum+ cfg_resonance <-+ expert $+ inGroup "Critical pair weighting heuristics" $+ bool "resonance" ["Interpret hints as resonators by only allowing substitutions which map variables to variables (off by default)."] False+ return CP.Config{..} where- lweight =- expert $- inGroup "Critical pair weighting heuristics" $- defaultFlag "lhs-weight" "Weight given to LHS of critical pair" CP.cfg_lhsweight argNum- rweight =- expert $- inGroup "Critical pair weighting heuristics" $- defaultFlag "rhs-weight" "Weight given to RHS of critical pair" CP.cfg_rhsweight argNum- funweight =- expert $- inGroup "Critical pair weighting heuristics" $- defaultFlag "fun-weight" "Weight given to function symbols" CP.cfg_funweight argNum- varweight =- expert $- inGroup "Critical pair weighting heuristics" $- defaultFlag "var-weight" "Weight given to variable symbols" CP.cfg_varweight argNum- depthweight =- expert $- inGroup "Critical pair weighting heuristics" $- defaultFlag "depth-weight" "Weight given to critical pair depth" CP.cfg_depthweight argNum- dupcost =- expert $- inGroup "Critical pair weighting heuristics" $- defaultFlag "dup-cost" "Cost of duplicate subterms" CP.cfg_dupcost argNum- dupfactor =- expert $- inGroup "Critical pair weighting heuristics" $- defaultFlag "dup-factor" "Size factor of duplicate subterms" CP.cfg_dupfactor argNum- defaultFlag name desc field parser = flag name [desc ++ " (" ++ show def ++ " by default)."] def parser where@@ -351,6 +411,7 @@ data Constant = Minimal |+ Skolem Int | Constant { con_prec :: {-# UNPACK #-} !Precedence, con_id :: {-# UNPACK #-} !Jukebox.Function,@@ -358,20 +419,23 @@ con_size :: !Integer, con_weight :: !Integer, con_bonus :: !Bool }- deriving (Eq, Ord, Labelled)+ deriving (Eq, Ord) -data Precedence = Precedence !Bool !Bool !(Maybe Int) !Int+data Precedence = Precedence !Bool !Bool !Bool !(Maybe Int) !Int deriving (Eq, Ord) instance KBO.Sized Constant where size Minimal = 1+ size Skolem{} = 1 size Constant{..} = con_size instance KBO.Weighted Constant where argWeight Minimal = 1+ argWeight Skolem{} = 1 argWeight Constant{..} = con_weight instance Pretty Constant where pPrint Minimal = text "?"+ pPrint (Skolem n) = text ("sk" ++ show n) pPrint Constant{..} = text (removePostfix (base con_id)) where removePostfix ('_':x:xs) | con_arity == 1 = x:xs@@ -379,6 +443,7 @@ instance PrettyTerm Constant where termStyle Minimal = uncurried+ termStyle Skolem{} = uncurried termStyle Constant{..} | hasLabel "type_tag" con_id = invisible | "_" `isPrefixOf` base con_id && con_arity == 1 = postfix@@ -390,7 +455,8 @@ _ -> uncurried instance Minimal Constant where- minimal = fun Minimal+ minimal = Sym Minimal+ skolem = Sym . Skolem instance Ordered Constant where lessEq t u = KBO.lessEq t u@@ -399,12 +465,16 @@ instance EqualsBonus Constant where hasEqualsBonus Minimal = False+ hasEqualsBonus Skolem{} = False hasEqualsBonus c = con_bonus c isEquals Minimal = False+ isEquals Skolem{} = False isEquals c = SequentialMain.isEquals (con_id c) isTrue Minimal = False+ isTrue Skolem{} = False isTrue c = SequentialMain.isTrue (con_id c) isFalse Minimal = False+ isFalse Skolem{} = False isFalse c = SequentialMain.isFalse (con_id c) data TweeContext =@@ -425,13 +495,16 @@ con_prec = prec, con_id = fun, con_arity = Jukebox.arity fun,- con_size = if flags_kbo_weight0 && Jukebox.arity fun >= 2 then 0 else 1,+ con_size = if flags_kbo_weight0 && Jukebox.arity fun >= 2 then 0 else if flags_kbo_weight0_unary && isInv then 0 else 1, con_weight = 1, con_bonus = bonus fun } where bonus fun = (isIfeq fun && encoding flags /= Asymmetric2) || SequentialMain.isEquals fun+ isInv =+ case prec of+ Precedence _ x _ _ _ -> x isType :: Jukebox.Function -> Bool isType fun =@@ -461,20 +534,20 @@ tweeTerm flags horn ctx prec t = build (tm t) where tm (Jukebox.Var (x ::: _)) =- var (V (fromIntegral (Label.labelNum (Label.label x))))+ var (V (Intern.symId (Intern.intern x))) tm (f :@: ts) =- app (fun (tweeConstant flags horn ctx (prec f) f)) (map tm ts)+ app (Sym (tweeConstant flags horn ctx (prec f) f)) (map tm ts) jukeboxTerm :: TweeContext -> Term Constant -> Jukebox.Term jukeboxTerm TweeContext{..} (Var (V x)) = Jukebox.Var (Unique (fromIntegral x) (intern "X") Nothing defaultRenamer ::: ctx_type)-jukeboxTerm ctx@TweeContext{..} (App f t) =- jukeboxFunction ctx (fun_value f) :@: map (jukeboxTerm ctx) ts+jukeboxTerm ctx@TweeContext{..} (App (Sym f) t) =+ jukeboxFunction ctx f :@: map (jukeboxTerm ctx) ts where ts = unpack t -makeContext :: Problem Clause -> TweeContext-makeContext prob = run prob $ \prob -> do+makeContext :: [Jukebox.Term] -> Problem Clause -> TweeContext+makeContext hints prob = run (hints, prob) $ \(_, prob) -> do let ty = case types' prob of@@ -495,9 +568,9 @@ ctx_equals = equals, ctx_type = ty } -flattenGoals :: Int -> Bool -> Bool -> Bool -> Problem Clause -> Problem Clause-flattenGoals backwardsGoal flattenNonGround flattenAll full prob =- run prob $ \prob -> do+flattenGoals :: Int -> Bool -> Bool -> Bool -> [Jukebox.Term] -> Problem Clause -> Problem Clause+flattenGoals backwardsGoal flattenNonGround flattenAll full hints prob =+ run (hints, prob) $ \(_, prob) -> do let ts = usort $ extraTerms prob cs <- mapM define ts return (prob ++ cs)@@ -525,7 +598,7 @@ let vs = Jukebox.vars ts g = name ::: FunType (map typ vs) (typ f) c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: f :@: ts)]- return Input{tag = "flattening", kind = Jukebox.Ax Definition,+ return Input{ident = Nothing, tag = "flattening", kind = Jukebox.Ax Definition, what = c, source = Unknown } backwards 0 _ t = [t]@@ -540,9 +613,9 @@ ground u, v <- backwards (n-1) cs u ] -addDistributivityHeuristic :: Problem Clause -> Problem Clause-addDistributivityHeuristic prob =- run prob $ \prob -> do+addDistributivityHeuristic :: [Jukebox.Term] -> Problem Clause -> Problem Clause+addDistributivityHeuristic hints prob =+ run (hints, prob) $ \(_, prob) -> do cs <- mapM add prob return (prob ++ catMaybes cs) @@ -579,7 +652,7 @@ let vs = Jukebox.vars t g = name ::: FunType (map typ vs) (typ t) c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: t)]- return Input{tag = "distributivity_heuristic", kind = Jukebox.Ax Definition,+ return Input{ident = Nothing, tag = "distributivity_heuristic", kind = Jukebox.Ax Definition, what = c, source = Unknown } -- Encode existentials so that all goals are ground.@@ -587,7 +660,9 @@ addNarrowing alwaysNarrow TweeContext{..} prob = unchanged ++ equalityClauses where- (unchanged, nonGroundGoals) = partitionEithers (map f prob)+ prob' = [inp { ident = Just (variant "addNarrowing" [i :: Int]) } | (i, inp) <- zip [0..] prob]++ (unchanged, nonGroundGoals) = partitionEithers (map f prob') where f inp@Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])} | not (ground x) || not (ground y) || alwaysNarrow =@@ -613,6 +688,7 @@ -- Equisatisfiable to the input clauses justification = Input {+ ident = Just (name "addNarrowing2"), tag = "new_negated_conjecture", kind = Jukebox.Ax NegatedConjecture, what =@@ -622,15 +698,16 @@ inference "encode_existential" "esa" (map (fmap toForm . fst) nonGroundGoals) } - input tag form =+ input tag form i = Input {+ ident = Just (variant "addNarrowing3" [i :: Int]), tag = tag,- kind = Conj Conjecture,+ kind = Jukebox.Ax NegatedConjecture, what = clause [form], source = inference "split_conjunct" "thm" [justification] } - in [input tag form | (tag, form) <- equalityLiterals]+ in [input tag form i | ((tag, form), i) <- zip equalityLiterals [0..]] data PreEquation = PreEquation {@@ -662,19 +739,19 @@ return $ Left (pre inp (Jukebox.Var ctx_var, ctx_minimal :@: [])) identify inp = Left inp -runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> CP.Config -> MainFlags -> (IO () -> IO ()) -> Problem Clause -> IO Answer-runTwee globals (TSTPFlags tstp) horn precedence config0 cpConfig flags@MainFlags{..} later obligs = {-# SCC runTwee #-} do+runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> CP.Config -> MainFlags -> (IO () -> IO ()) -> [Jukebox.Term] -> Problem Clause -> IO Answer+runTwee globals (TSTPFlags tstp) horn precedence config0 cpConfig flags@MainFlags{..} later hints obligs = {-# SCC runTwee #-} do let -- Encode whatever needs encoding in the problem obligs1- | flags_flatten_goals_lightly = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False False obligs- | flags_flatten_all = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground True True obligs- | flags_flatten_goals = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False True obligs+ | flags_flatten_goals_lightly = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False False hints obligs+ | flags_flatten_all = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground True True hints obligs+ | flags_flatten_goals = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False True hints obligs | otherwise = obligs obligs2- | flags_distributivity_heuristic = addDistributivityHeuristic obligs1+ | flags_distributivity_heuristic = addDistributivityHeuristic hints obligs1 | otherwise = obligs1- ctx = makeContext obligs2+ ctx = makeContext hints obligs2 lowercaseSkolem x | hasLabel "skolem" x = withRenamer x $ \s i ->@@ -682,7 +759,7 @@ Renaming xss xs -> Renaming (map (map toLower) xss) (map toLower xs) | otherwise = x- prob = prettyNames (mapName lowercaseSkolem (addNarrowing flags_equals_transformation ctx obligs2))+ (hints', prob) = prettyNames (mapName lowercaseSkolem (hints, addNarrowing flags_equals_transformation ctx obligs2)) (unsortedAxioms0, goals0) <- case identifyProblem ctx prob of@@ -699,23 +776,31 @@ prec c = Precedence (isType c)+ (Just c == maxUnary) (isNothing (elemIndex (base c) precedence)) (fmap negate (elemIndex (base c) precedence)) (maybeNegate (Map.findWithDefault 0 c funOccs)) maybeNegate = if flags_flip_ordering then negate else id funOccs = funsOcc prob+ maxUnary =+ case filter (\(f, _) -> arity f == 1 && not (isType f)) (Map.toList funOccs) of+ [] -> Nothing+ xs -> Just (fst (maximumBy (comparing snd) xs)) -- Translate everything to Twee.- toEquation (t, u) =- canonicalise (tweeTerm flags horn ctx prec t :=: tweeTerm flags horn ctx prec u)+ toTerm t = tweeTerm flags horn ctx prec t+ toEquation (t, u) = canonicalise (toTerm t :=: toTerm u) axiomCompare ax1 ax2+ | isEquality ax1' && not (isEquality ax2') = GT+ | isEquality ax2' && not (isEquality ax1') = LT | ax1' `simplerThan` ax2' = LT | ax2' `simplerThan` ax1' = GT | otherwise = EQ where ax1' = toEquation (pre_eqn ax1) ax2' = toEquation (pre_eqn ax2)+ isEquality ax = isJust (decodeEquality (eqn_lhs ax)) || isJust (decodeEquality (eqn_rhs ax)) axioms0 = sortBy axiomCompare unsortedAxioms0 goals =@@ -735,15 +820,15 @@ let goalNests = nests (map goal_eqn goals) goalOccs = occs (map goal_eqn goals)- score depth eqn+ score depth hints eqn | flags_goal_heuristic =- fromIntegral (CP.score cpConfig depth eqn) *+ CP.score cpConfig depth hints eqn * product [ pos (IntMap.findWithDefault 0 f eqnNests - IntMap.findWithDefault 0 f goalNests) * pos (IntMap.findWithDefault 0 f eqnOccs - IntMap.findWithDefault 0 f goalOccs) | f <- IntMap.keys eqnNests ] -- skip constants | otherwise = - fromIntegral (CP.score cpConfig depth eqn)+ CP.score cpConfig depth hints eqn where eqnNests = nests eqn eqnOccs = occs eqn@@ -753,7 +838,8 @@ config = config0 { cfg_score_cp = score, cfg_eliminate_axioms = if flags_flatten_regeneralise then defs else [] } let- withGoals = foldl' (addGoal config) (initialState config) goals+ withHints = foldl' (addHint config) (initialState config) (map toTerm hints')+ withGoals = foldl' (addGoal config) withHints goals withAxioms = foldl' (addAxiom config) withGoals axioms withBackwardsGoal = foldn rewriteGoalsBackwards withAxioms flags_backwards_goal @@ -781,7 +867,7 @@ say (prettyShow msg) sayTrace (show (traceMsg msg)) } - traceMsg (NewActive active) =+ traceMsg (NewActive _ active) = step "add" [traceActive active] traceMsg (NewEquation eqn) = step "hard" [traceEqn eqn]@@ -839,7 +925,7 @@ (cfg_proof_presentation config){cfg_all_lemmas = True} | otherwise = cfg_proof_presentation config- pres = present cfg_present $ map (eliminateDefinitionsFromGoal defs) $ solutions state+ pres = present cfg_present [] $ map (eliminateDefinitionsFromGoal defs) $ solutions state sayTrace "" forM_ (pres_axioms pres) $ \p ->@@ -926,7 +1012,7 @@ print $ pPrintProof $ map pre_form axioms0 ++ map pre_form goals0 ++- [ Input "rule" (Jukebox.Ax Jukebox.Axiom) Unknown $+ [ Input Nothing "rule" (Jukebox.Ax Jukebox.Axiom) Unknown $ toForm $ clause [Pos (jukeboxTerm ctx (lhs rule) Jukebox.:=: jukeboxTerm ctx (rhs rule))] | rule <- rules state ]@@ -941,6 +1027,10 @@ forM_ actives $ \active -> putStrLn (" " ++ prettyShow (canonicalise (active_rule active))) putStrLn ""+ + when flags_proof_on_saturation $ do+ let pres = present (cfg_proof_presentation config) (map active_proof actives) []+ print $ pPrintPresentation (cfg_proof_presentation config) pres return $ if solved state then Unsat Unsatisfiable Nothing@@ -959,6 +1049,7 @@ Problem Form presentToJukebox ctx toEquation axioms goals Presentation{..} = [ Input {+ ident = Nothing, tag = pg_name, kind = Jukebox.Ax Jukebox.Axiom, what = false,@@ -973,11 +1064,15 @@ where axiom_proofs = Map.fromList- [ (axiom_number, fromJust (lookup axiom_number axioms))+ [ (axiom_number, (fromJust (lookup axiom_number axioms)) { ident = Just (ident axiom_number) }) | Axiom{..} <- pres_axioms ]+ where+ ident i = variant "axiom" [i] lemma_proofs =- Map.fromList [(p, tstp p) | p <- pres_lemmas]+ Map.fromList [(p, (tstp p) { ident = Just (ident i) }) | (i, p) <- zip [0..] pres_lemmas]+ where+ ident i = variant "lemma" [i :: Int] goal_proofs = Map.fromList [(pg_number, tstp pg_proof) | ProvedGoal{..} <- pres_goals]@@ -988,6 +1083,7 @@ deriv :: Derivation Constant -> Input Form deriv p = Input {+ ident = Nothing, tag = "step", kind = Jukebox.Ax Jukebox.Axiom, what = jukeboxEquation (equation (certify p)),@@ -1062,8 +1158,12 @@ (runTwee <$> globalFlags <*> tstpFlags <*> expert hornFlags <*> parsePrecedence))) profile where+ getHint Input{what = Clause (Bind _ [Pos (Tru (hint :@: [t]))])}+ | base (name hint) == "$hint" = Left t+ getHint c = Right c combine horn config cpConfig main encode prove later prob0 = do- res <- horn prob0+ let (hints, nonHints) = partitionEithers (map getHint prob0)+ res <- horn nonHints case res of Left ans -> return ans Right prob -> do@@ -1073,4 +1173,4 @@ isUnitEquality _ = False isUnit = all isUnitEquality (map (toLiterals . what) prob0) main' = if isUnit then main{flags_explain_encoding = False} else main{flags_formal_proof = False}- encode prob >>= prove config cpConfig main' later+ encode prob >>= prove config cpConfig main' later hints
misc/BestTwee.hs view
@@ -83,24 +83,24 @@ bonuses :: [(String, (Int, Int, Int, Int, Int, Int))] bonuses = [("no bonus", (1, 1, 1, 1, 1, 1)),- ("low bonus", (1, 1, 2, 3, 5, 10)),- --("medium bonus", (1, 2, 4, 6, 8, 10)),+ --("low bonus", (1, 1, 2, 3, 5, 10)),+ ("medium bonus", (1, 2, 4, 6, 8, 10)), --("high bonus", (0, 1, 2, 3, 4, 5)), --("big fish", (0, 0, 0, 0, 1, 1)), ("rating 1", (0, 0, 0, 0, 0, 1))] readResults ok = do- filenames <- glob "/home/nick/writing/twee/times/*-twee-casc-extra-*"+ filenames <- glob "/home/nick/twee-out/*/times" fmap (filter (\(x, _) -> x `notElem` banned)) $ forM filenames $ \filename -> do- let name = takeFileName filename+ let name = takeFileName (takeDirectory filename) let unpack xs = (takeBaseName name, read time :: Double) where [name, time] = words xs solved <- filter (ok . fst) . map unpack . lines <$> readFile filename let solvedInTime t = [name | (name, time) <- solved, time < t] -- fast <- filterM (solvedInTime 120 directory) solved -- med <- filterM (solvedInTime 240 directory) solved -- slow <- filterM (solvedInTime 600 directory) solved- let fast = solvedInTime 210- let med = solvedInTime 300+ let fast = solvedInTime 120+ let med = solvedInTime 210 let slow = solvedInTime (1/0) return (name, (fast, med, slow))@@ -117,8 +117,8 @@ find x = fromJust (lookup x results) main = do- probs <- lines <$> readFile "unsat"- results <- readResults (`elem` probs)+ --probs <- lines <$> readFile "unsat"+ results <- readResults (const True) -- `elem` probs) let options = [("fast", \(fast, _, _) -> (fast, [], [])),@@ -140,7 +140,7 @@ best = greedy results1 putStrLn (option ++ "/" ++ bonus ++ ":")- forM_ (take 6 $ zip3 [1..] best (inits best)) $ \(i, name, names) -> do+ forM_ (take 8 $ zip3 [1..] best (inits best)) $ \(i, name, names) -> do putStrLn (show i ++ ". " ++ name ++ " " ++ show (score results1 (name:names)) ++ ", useful at levels " ++ show (drop (length fixed) $ levels results1 name names)) putStrLn ""@@ -167,7 +167,11 @@ Nothing -> Left (length probs) fixed :: [String]-fixed = fixed_new+fixed = [+ "twee-250707-casc---lhs-weight-1---flip-ordering---normalise-queue-percent-10---cp-renormalise-threshold-10---complete-subsets---ground-joining-incomplete-limit-15",+ "twee-250707-casc---no-flatten-goal---ground-joining-incomplete-limit-15"+ ]+ fixed_new = take 6 [ "twee-210619-twee-casc-extra-lhsnormal-flatten", "twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0",
+ tests/KLE125+1.p view
@@ -0,0 +1,47 @@+%------------------------------------------------------------------------------+% File : KLE125+1 : TPTP v9.0.0. Released v4.0.0.+% Domain : Kleene Algebra (Modal with Divergence)+% Problem : Quasicommutation theorem+% Version : [Hoe08] axioms.+% English : If x quasicommutes over y, then x+y terminates if x and y+% individually do.++% Refs : [BD86] Bachmair & Dershowitz (1986), Commutation, Transformat+% : [Str07] Struth (2007), Reasoning Automatically about Terminati+% : [Hoe08] Hoefner (2008), Email to G. Sutcliffe+% Source : [Hoe08]+% Names :++% Status : Theorem+% Rating : 1.00 v4.0.0+% Syntax : Number of formulae : 29 ( 26 unt; 0 def)+% Number of atoms : 33 ( 32 equ)+% Maximal formula atoms : 3 ( 1 avg)+% Number of connectives : 4 ( 0 ~; 0 |; 0 &)+% ( 2 <=>; 2 =>; 0 <=; 0 <~>)+% Maximal formula depth : 5 ( 3 avg)+% Maximal term depth : 6 ( 2 avg)+% Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)+% Number of functors : 16 ( 16 usr; 2 con; 0-2 aty)+% Number of variables : 49 ( 49 !; 0 ?)+% SPC : FOF_THM_RFO_SEQ++% Comments : An abstract version of a theorem in [BD86].+% : Equational encoding+%------------------------------------------------------------------------------+%---Include axioms for modal Kleene algebra with divergence+include('Axioms/KLE001+0.ax').+%---Include axioms for Boolean domain/codomain+include('Axioms/KLE001+4.ax').+%---Include axioms for diamond and boxes+include('Axioms/KLE001+6.ax').+%---Include axioms for divergence+include('Axioms/KLE001+7.ax').+%------------------------------------------------------------------------------+fof(goals,conjecture,+ ! [X0,X1] :+ ( addition(multiplication(X0,X1),multiplication(X1,star(addition(X1,X0)))) = multiplication(X1,star(addition(X1,X0)))+ => ( divergence(addition(X1,X0)) = zero+ <= addition(divergence(X1),divergence(X0)) = zero ) ) ).++%------------------------------------------------------------------------------
+ tests/ROB001-1-a.p view
@@ -0,0 +1,42 @@+%------------------------------------------------------------------------------+% File : ROB001-1 : TPTP v9.0.0. Released v1.0.0.+% Domain : Robbins Algebra+% Problem : Is every Robbins algebra Boolean?+% Version : [Win90] (equality) axioms.+% English :++% Refs : [HMT71] Henkin et al. (1971), Cylindrical Algebras+% : [Win90] Winker (1990), Robbins Algebra: Conditions that make a+% Source : [TPTP]+% Names :++% Status : Unsatisfiable+% Rating : 1.00 v2.0.0+% Syntax : Number of clauses : 4 ( 4 unt; 0 nHn; 1 RR)+% Number of literals : 4 ( 4 equ; 1 neg)+% Maximal clause size : 1 ( 1 avg)+% Maximal term depth : 6 ( 2 avg)+% Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)+% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)+% Number of variables : 7 ( 0 sgn)+% SPC : CNF_UNS_RFO_PEQ_UEQ++% Comments : Commutativity, associativity, and Huntington's axiom axiomatize +% Boolean algebra.+%------------------------------------------------------------------------------+%----Include axioms for Robbins algebra+include('Axioms/ROB001-0.ax').+%------------------------------------------------------------------------------+cnf(prove_huntingtons_axiom,negated_conjecture,+ add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b ).++%------------------------------------------------------------------------------++cnf(sos04,axiom,(+ g(A) = inv(add(A,inv(A))) )).++%----Definition of h+%cnf(sos05,axiom,(+% h(A) = add(A,add(A,add(A,inv(add(A,inv(A)))))))).+cnf(sos05,axiom,(+ $hint(add(A,add(A,add(A,g(A))))))).
+ tests/ROB007-1-b.p view
@@ -0,0 +1,12 @@+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).+cnf(associativity_of_add, axiom, add(add(X, Y), Z)=add(X, add(Y, Z))).+cnf(robbins_axiom, axiom, inv(add(inv(add(X, Y)), inv(add(X, inv(Y)))))=X).+cnf(condition, hypothesis, inv(add(a, b))=inv(b)).+cnf(prove_huntingtons_axiom, negated_conjecture, add(inv(add(a, inv(b))), inv(add(inv(a), inv(b))))!=b).++cnf(sos04,axiom,(+ $hint(inv(add(A,inv(A)))) )).++%----Definition of h+cnf(sos05,axiom,(+ $hint(add(A,add(A,add(A,inv(add(A,inv(A))))))))).
tests/aim.p view
@@ -35,21 +35,21 @@ % aK (or "single-a") goals cnf(ka, conjecture,- k(a(X,Y,Z),U) = '1').+ k(a(x,y,z),u) = '1'). cnf(aK1, conjecture,- a(k(X,Y),Z,U) = '1').+ a(k(x,y),z,u) = '1'). cnf(aK2, conjecture,- a(X,k(Y,Z),U) = '1').+ a(x,k(y,z),u) = '1'). cnf(aK3, conjecture,- a(X,Y,k(Z,U)) = '1').+ a(x,y,k(z,u)) = '1'). % aa (or "double-a") goals cnf(aa1, conjecture,- a(a(X,Y,Z),U,W) = '1').+ a(a(x,y,z),u,w) = '1'). cnf(aa2, conjecture,- a(X,a(Y,Z,U),W) = '1').+ a(x,a(y,z,u),w) = '1'). cnf(aa3, conjecture,- a(X,Y,a(Z,U,W)) = '1').+ a(x,y,a(z,u,w)) = '1'). %cnf(everything, conjecture, % k(a(X,Y,Z),U) = '1' |
+ tests/nicomachus-tptp-2.p view
@@ -0,0 +1,19 @@+cnf(plus_comm, axiom, plus(X, Y)=plus(Y, X)).+cnf(plus_assoc, axiom, plus(X, plus(Y, Z))=plus(plus(X, Y), Z)).+cnf(times_comm, axiom, times(X, Y)=times(Y, X)).+cnf(times_assoc, axiom, times(X, times(Y, Z))=times(times(X, Y), Z)).+cnf(plus_zero, axiom, plus(X, zero)=X).+cnf(times_zero, axiom, times(X, zero)=zero).+cnf(times_one, axiom, times(X, one)=X).+cnf(distr, axiom, times(X, plus(Y, Z))=plus(times(X, Y), times(X, Z))).+cnf(distr, axiom, times(plus(X, Y), Z)=plus(times(X, Z), times(Y, Z))).+cnf(plus_s, axiom, plus(s(X), Y)=s(plus(X, Y))).+cnf(times_s, axiom, times(s(X), Y)=plus(Y, times(X, Y))).+cnf(sum_zero, axiom, sum(zero)=zero).+cnf(sum_s, axiom, sum(s(N))=plus(s(N), sum(N))).+cnf(cubes_zero, axiom, cubes(zero)=zero).+cnf(cubes_s, axiom, cubes(s(N))=plus(times(s(N), times(s(N), s(N))), cubes(N))).+cnf(plus_sum_step_1, axiom, plus(sum(zero), sum(zero))!=times(zero, s(zero)) | plus(sum(ih_a), sum(ih_a))=times(ih_a, s(ih_a))).+cnf(plus_sum, axiom, plus(sum(zero), sum(zero))!=times(zero, s(zero)) | plus(sum(s(ih_a)), sum(s(ih_a)))!=times(s(ih_a), s(s(ih_a))) | plus(sum(N), sum(N))=times(N, s(N))).+cnf(ih, axiom, times(sum(a), sum(a))=cubes(a)).+cnf(conjecture, negated_conjecture, times(sum(s(a)), sum(s(a)))!=cubes(s(a))).
+ tests/nicomachus-tptp.p view
@@ -0,0 +1,20 @@+cnf(plus_comm, axiom, plus(X, Y)=plus(Y, X)).+cnf(plus_assoc, axiom, plus(X, plus(Y, Z))=plus(plus(X, Y), Z)).+cnf(times_comm, axiom, times(X, Y)=times(Y, X)).+cnf(times_assoc, axiom, times(X, times(Y, Z))=times(times(X, Y), Z)).+cnf(plus_zero, axiom, plus(X, zero)=X).+cnf(times_zero, axiom, times(X, zero)=zero).+cnf(times_one, axiom, times(X, one)=X).+cnf(distr, axiom, times(X, plus(Y, Z))=plus(times(X, Y), times(X, Z))).+cnf(distr, axiom, times(plus(X, Y), Z)=plus(times(X, Z), times(Y, Z))).+cnf(plus_s, axiom, plus(s(X), Y)=s(plus(X, Y))).+cnf(times_s, axiom, times(s(X), Y)=plus(Y, times(X, Y))).+cnf(sum_zero, axiom, sum(zero)=zero).+cnf(sum_s, axiom, sum(s(N))=plus(s(N), sum(N))).+cnf(cubes_zero, axiom, cubes(zero)=zero).+cnf(cubes_s, axiom, cubes(s(N))=plus(times(s(N), times(s(N), s(N))), cubes(N))).+%cnf(plus_sum, axiom, plus(sum(N), sum(N))=times(N, s(N))).+cnf(plus_sum_step_1, axiom, plus(sum(zero), sum(zero)) = times(zero, s(zero)) => plus(sum(ih_a), sum(ih_a)) = times(ih_a, s(ih_a))).+cnf(plus_sum, axiom, (plus(sum(zero), sum(zero)) = times(zero, s(zero)) & plus(sum(s(ih_a)), sum(s(ih_a))) = times(s(ih_a), s(s(ih_a)))) => plus(sum(N),sum(N))=times(N,s(N))).+cnf(ih, axiom, times(sum(a), sum(a))=cubes(a)).+cnf(conjecture, negated_conjecture, times(sum(s(a)), sum(s(a)))!=cubes(s(a))).
+ tests/nicomachus2.p view
@@ -0,0 +1,36 @@+cnf(plus_comm, axiom,+ X + Y = Y + X).+cnf(plus_assoc, axiom,+ X + (Y + Z) = (X + Y) + Z).+cnf(times_comm, axiom,+ X * Y = Y * X).+cnf(times_assoc, axiom,+ X * (Y * Z) = (X * Y) * Z).+cnf(plus_zero, axiom,+ X + zero = X).+cnf(times_zero, axiom,+ X * zero = zero).+cnf(times_one, axiom,+ X * one = X).+cnf(distr, axiom,+ X * (Y + Z) = (X * Y) + (X * Z)).+cnf(distr, axiom,+ (X + Y) * Z = (X * Z) + (Y * Z)).+cnf(plus_s, axiom,+ s(X) + Y = s(X+Y)).+cnf(times_s, axiom,+ s(X)*Y = Y + (X*Y)).+cnf(sum_zero, axiom,+ sum(zero) = zero).+cnf(sum_s, axiom,+ sum(s(N)) = s(N) + sum(N)).+cnf(cubes_zero, axiom,+ cubes(zero) = zero).+cnf(cubes_s, axiom,+ cubes(s(N)) = (s(N) * (s(N) * s(N))) + cubes(N)).+cnf(plus_sum, axiom,+ sum(N) + sum(N) = N * s(N)).+cnf(ih, axiom,+ sum(a) * sum(a) = cubes(a)).+cnf(conjecture, conjecture,+ sum(s(a)) * sum(s(a)) = cubes(s(a))).
+ tests/rob.p view
@@ -0,0 +1,7 @@+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).+cnf(associativity_of_add, axiom,+ add(add(X, Y), Z)=add(X, add(Y, Z))).+cnf(robbins_axiom, axiom,+ negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).+cnf(winker_specialised, conjecture,+ add(add(x,x), negate(add(negate(add(x,add(x,x))),x))) = add(x,x)).
+ tests/rob2.p view
@@ -0,0 +1,7 @@+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).+cnf(associativity_of_add, axiom,+ add(add(X, Y), Z)=add(X, add(Y, Z))).+cnf(robbins_axiom, axiom,+ negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).+fof(winker, conjecture,+ ?[X,Y]: add(X,Y) = X).
+ tests/sum.p view
@@ -0,0 +1,30 @@+cnf(plus_comm, axiom,+ X + Y = Y + X).+cnf(plus_assoc, axiom,+ X + (Y + Z) = (X + Y) + Z).+cnf(times_comm, axiom,+ X * Y = Y * X).+cnf(times_assoc, axiom,+ X * (Y * Z) = (X * Y) * Z).+cnf(plus_zero, axiom,+ X + zero = X).+cnf(times_zero, axiom,+ X * zero = zero).+cnf(times_one, axiom,+ X * one = X).+cnf(distr, axiom,+ X * (Y + Z) = (X * Y) + (X * Z)).+cnf(distr, axiom,+ (X + Y) * Z = (X * Z) + (Y * Z)).+cnf(plus_s, axiom,+ s(X) + Y = s(X+Y)).+cnf(times_s, axiom,+ s(X)*Y = Y + (X*Y)).+cnf(sum_zero, axiom,+ sum(zero) = zero).+cnf(sum_s, axiom,+ sum(s(N)) = s(N) + sum(N)).+cnf(ih, axiom,+ sum(a) + sum(a) = a * s(a)).+cnf(conjecture, conjecture,+ sum(s(a)) + sum(s(a)) = s(a) * s(s(a))).
+ tests/wos.p view
@@ -0,0 +1,6 @@+cnf(a, axiom,+ prod(inv(prod(inv(prod(inv(prod(Xl,X2)),prod(X2,Xl))),prod(inv(prod(Z,Y)), prod(Z,inv(prod(prod(V,inv(X)),inv(Y))))))),X) = V).++%fof(associativity, conjecture, prod(a,prod(b,c)) = prod(prod(a,b),c)).+fof(identity_and_inverse, conjecture, ?[X]: (![Y]: prod(X,Y)=Y & ![Y]: prod(Y, inv(Y)) = X)).+%fof(commutativity, conjecture, prod(a,b) = prod(b,a)).
twee.cabal view
@@ -1,5 +1,5 @@ name: twee-version: 2.5+version: 2.6.1 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3@@ -25,7 +25,7 @@ source-repository head type: git- location: git://github.com/nick8325/twee.git+ location: https://github.com/nick8325/twee.git branch: master flag static@@ -44,17 +44,22 @@ manual: True executable twee+ --if flag(parallel)+ -- main-is: ParallelMain.hs+ -- build-depends: async, unix+ -- c-sources: executable/link.c+ --else main-is: Main.hs hs-source-dirs: executable other-modules: SequentialMain default-language: Haskell2010 build-depends: base < 5,- twee-lib == 2.5,+ twee-lib == 2.6.1, containers, pretty, split,- jukebox >= 0.5.4,+ jukebox >= 0.5.9, ansi-terminal >= 0.9, symbol ghc-options: -W -fno-warn-incomplete-patterns@@ -71,7 +76,7 @@ hs-source-dirs: misc main-is: Test.hs- build-depends: base < 5, QuickCheck, twee-lib == 2.5, containers, pretty+ build-depends: base < 5, QuickCheck, twee-lib == 2.6.1, containers, pretty ghc-options: -threaded -rtsopts