src/HOL/Tools/SMT/smt_solver.ML
2015-08-27 blanchet 2015-08-27 generate proper error instead of exception if goal cannot be atomized
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-08 wenzelm 2015-07-08 clarified context;
2015-07-08 wenzelm 2015-07-08 Variable.focus etc.: optional bindings provided by user; Subgoal.focus command: more careful treatment of user-provided bindings;
2015-04-25 blanchet 2015-04-25 made CVC4 support work also without unsat cores
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2013-10-02 blanchet 2013-10-02 make SMT integration slacker w.r.t. bad apples (facts)
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2012-12-12 blanchet 2012-12-12 made MaSh evaluation driver work with SMT solvers
2012-08-23 wenzelm 2012-08-23 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
2012-07-26 blanchet 2012-07-26 Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here
2012-07-26 blanchet 2012-07-26 Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
2012-05-30 boehmes 2012-05-30 introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
2012-04-23 wenzelm 2012-04-23 more standard method setup;
2012-03-27 blanchet 2012-03-27 renamed "smt_fixed" to "smt_read_only_certificates"
2012-03-01 boehmes 2012-03-01 fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
2012-02-29 boehmes 2012-02-29 SMT fails if the chosen SMT solver is not installed
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2012-02-14 wenzelm 2012-02-14 normalized aliases;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-08 boehmes 2011-04-08 check if negating the goal is possible (avoids CTERM exception for Pure propositions)
2011-02-14 boehmes 2011-02-14 more explicit errors to inform users about problems related to SMT solvers; fall back to remote SMT solver (if local version does not exist); extend the Z3 proof parser to accommodate for slight changes introduced by Z3 2.18
2011-01-17 boehmes 2011-01-17 made Z3 the default SMT solver again
2011-01-10 boehmes 2011-01-10 dropped superfluous error message
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
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-20 boehmes 2010-12-20 avoid ML structure aliases (especially single-letter abbreviations)
2010-12-20 boehmes 2010-12-20 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
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-15 boehmes 2010-12-15 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
2010-12-15 boehmes 2010-12-15 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure); abolished SMT interface concept in favor of solver classes (now also the translation configuration is stored in the context); proof reconstruction is now expected to return a theorem stating False (and hence needs to discharge all hypothetical definitions); built-in functions carry additionally their arity and their most general type; slightly generalized the definition of fun_app
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-15 boehmes 2010-12-15 moved SMT classes and dictionary functions to SMT_Utils
2010-12-15 boehmes 2010-12-15 added option to modify the random seed of SMT solvers
2010-12-07 boehmes 2010-12-07 merged
2010-12-07 boehmes 2010-12-07 tuned
2010-12-07 boehmes 2010-12-07 centralized handling of built-in types and constants; also store types and constants which are rewritten during preprocessing; interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols); removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)
2010-12-07 blanchet 2010-12-07 make SML/NJ happy
2010-12-06 blanchet 2010-12-06 have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
2010-12-06 blanchet 2010-12-06 return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
2010-12-03 blanchet 2010-12-03 export more information about available SMT solvers
2010-11-30 boehmes 2010-11-30 split up Z3 models into constraints on free variables and constant definitions; reduce Z3 models by replacing unknowns with free variables and constants from the goal; remove occurrences of the hidden constant fun_app from Z3 models
2010-11-23 blanchet 2010-11-23 try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
2010-11-17 boehmes 2010-11-17 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
2010-11-17 boehmes 2010-11-17 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
2010-11-15 boehmes 2010-11-15 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
2010-11-15 boehmes 2010-11-15 honour timeouts which are not rounded to full seconds
2010-11-15 boehmes 2010-11-15 trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
2010-11-12 boehmes 2010-11-12 check the return code of the SMT solver and raise an exception if the prover failed
2010-11-12 boehmes 2010-11-12 turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
2010-11-08 boehmes 2010-11-08 return the process return code along with the process outputs
2010-11-08 boehmes 2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-04 boehmes 2010-11-04 simulate more closely the behaviour of the tactic
2010-11-03 boehmes 2010-11-03 standardize timeout value based on reals
2010-10-29 boehmes 2010-10-29 optionally drop assumptions which cannot be preprocessed
2010-10-29 boehmes 2010-10-29 clarified error message