src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
2011-04-22 blanchet 2011-04-22 automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
2011-04-21 blanchet 2011-04-21 automatically retry with full-types upon unsound proof
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-21 blanchet 2011-04-21 tuning -- local semicolon consistency
2011-04-21 blanchet 2011-04-21 tuning
2011-04-21 blanchet 2011-04-21 fixed interaction between monomorphization and slicing for ATPs
2011-04-21 blanchet 2011-04-21 cleanup: get rid of "may_slice" arguments without changing semantics
2011-04-21 blanchet 2011-04-21 implemented general slicing for ATPs, especially E 1.2w and above
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-01 blanchet 2011-04-01 remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
2011-04-01 boehmes 2011-04-01 make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
2011-03-31 boehmes 2011-03-31 provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
2011-03-31 blanchet 2011-03-31 start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
2011-03-31 blanchet 2011-03-31 temporary workaround: filter out spurious monomorphic instances
2011-03-31 blanchet 2011-03-31 added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-03-24 blanchet 2011-03-24 more precise failure reporting in Sledgehammer/SMT
2011-03-22 blanchet 2011-03-22 let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
2011-03-22 blanchet 2011-03-22 make Minimizer honor "verbose" and "debug" options better
2011-03-17 blanchet 2011-03-17 add option to function to keep trivial ATP formulas, needed for some experiments
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-02-21 blanchet 2011-02-21 exit code 127 can mean many things -- not just (and probably not) Perl missing
2011-02-21 blanchet 2011-02-21 give more weight to Frees than to Consts in relevance filter
2011-02-10 blanchet 2011-02-10 make minimizer verbose
2011-02-09 blanchet 2011-02-09 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
2011-02-09 blanchet 2011-02-09 renamed field
2011-02-08 blanchet 2011-02-08 available_provers ~> supported_provers (for clarity)
2011-02-08 blanchet 2011-02-08 enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
2011-01-06 boehmes 2011-01-06 differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface
2010-12-21 blanchet 2010-12-21 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction
2010-12-21 blanchet 2010-12-21 added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)
2010-12-20 blanchet 2010-12-20 run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
2010-12-20 blanchet 2010-12-20 remove spurious line
2010-12-20 blanchet 2010-12-20 optionally supply constant weights to E -- turned off by default until properly parameterized
2010-12-17 blanchet 2010-12-17 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
2010-12-17 blanchet 2010-12-17 put the SMT weights back where they belong, so that they're also used by Mirabelle
2010-12-17 blanchet 2010-12-17 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
2010-12-17 blanchet 2010-12-17 make timeout part of the SMT filter's tail
2010-12-17 blanchet 2010-12-17 split "smt_filter" into head and tail
2010-12-17 blanchet 2010-12-17 trap one more Z3 error
2010-12-17 blanchet 2010-12-17 more precise/correct SMT error handling
2010-12-16 blanchet 2010-12-16 discriminate SMT errors a bit better
2010-12-16 blanchet 2010-12-16 no need to do a super-duper atomization if Metis fails afterwards anyway
2010-12-16 blanchet 2010-12-16 robustly handle SMT exceptions in Sledgehammer
2010-12-16 blanchet 2010-12-16 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
2010-12-15 blanchet 2010-12-15 facilitate debugging
2010-12-15 blanchet 2010-12-15 clean up fudge factors a little bit
2010-12-15 blanchet 2010-12-15 added weights to SMT problems
2010-12-15 blanchet 2010-12-15 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
2010-12-15 blanchet 2010-12-15 crank up Metis's timeout for SMT solvers, since users love Metis
2010-12-15 blanchet 2010-12-15 generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
2010-12-15 blanchet 2010-12-15 added Sledgehammer support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
2010-12-15 blanchet 2010-12-15 implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
2010-12-15 blanchet 2010-12-15 added "type_sys" option to Sledgehammer
2010-12-15 boehmes 2010-12-15 re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level); added simple trigger inference mechanism; added syntactic checks for triggers and quantifier weights; factored out the normalization of special quantifiers (used to be in the eta-normalization part); normalization now unfolds abs/min/max (not SMT-LIB-specific); rules for pairs and function update are not anymore added automatically to the problem; more aggressive rewriting of natural number operations into integer operations (minimizes the number of remaining nat-int coercions); normalizations are now managed in a class-based manner (similar to built-in symbols)
2010-12-10 krauss 2010-12-10 made smlnj happy
2010-12-08 blanchet 2010-12-08 lower fudge factor
2010-12-08 blanchet 2010-12-08 implicitly call the minimizer for SMT solvers that don't return an unsat core
2010-12-08 blanchet 2010-12-08 renamings
2010-12-08 blanchet 2010-12-08 moved function to later module