src/HOL/Tools/SMT/smt_solver.ML
20 months ago blanchet 2017-09-22 real oracle
2016-10-18 wenzelm 2016-10-18 clarified modules;
2016-05-20 fleury 2016-05-20 better handling of veriT's 'unknown' status
2016-03-07 wenzelm 2016-03-07 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; clarified treatment of whitespace in some bash scripts;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.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