src/HOL/Tools/SMT/smt_solver.ML
Tue, 07 Dec 2010 15:01:37 +0100 boehmes tuned
Tue, 07 Dec 2010 14:53:12 +0100 boehmes centralized handling of built-in types and constants;
Tue, 07 Dec 2010 09:58:52 +0100 blanchet make SML/NJ happy
Mon, 06 Dec 2010 11:25:21 +0100 blanchet 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?
Mon, 06 Dec 2010 10:32:39 +0100 blanchet return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
Fri, 03 Dec 2010 18:27:21 +0100 blanchet export more information about available SMT solvers
Tue, 30 Nov 2010 18:22:43 +0100 boehmes split up Z3 models into constraints on free variables and constant definitions;
Tue, 23 Nov 2010 18:28:09 +0100 blanchet try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
Wed, 17 Nov 2010 08:14:56 +0100 boehmes 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)
Wed, 17 Nov 2010 08:14:55 +0100 boehmes keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
Mon, 15 Nov 2010 22:23:28 +0100 boehmes renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
Mon, 15 Nov 2010 22:23:26 +0100 boehmes honour timeouts which are not rounded to full seconds
Mon, 15 Nov 2010 17:35:57 +0100 boehmes trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
Fri, 12 Nov 2010 17:28:43 +0100 boehmes check the return code of the SMT solver and raise an exception if the prover failed
Fri, 12 Nov 2010 15:56:10 +0100 boehmes 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
Mon, 08 Nov 2010 12:13:51 +0100 boehmes return the process return code along with the process outputs
Mon, 08 Nov 2010 12:13:44 +0100 boehmes 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)
Thu, 04 Nov 2010 18:01:55 +0100 boehmes simulate more closely the behaviour of the tactic
Wed, 03 Nov 2010 16:44:38 +0100 boehmes standardize timeout value based on reals
Fri, 29 Oct 2010 18:17:09 +0200 boehmes optionally drop assumptions which cannot be preprocessed
Fri, 29 Oct 2010 18:17:06 +0200 boehmes clarified error message
Tue, 26 Oct 2010 17:35:54 +0200 boehmes use proper context
Tue, 26 Oct 2010 17:35:52 +0200 boehmes trace assumptions before giving them to the SMT solver
Tue, 26 Oct 2010 17:35:51 +0200 boehmes capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
Tue, 26 Oct 2010 17:35:49 +0200 boehmes honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
Tue, 26 Oct 2010 11:51:09 +0200 boehmes optionally force the remote version of an SMT solver to be executed
Tue, 26 Oct 2010 11:49:36 +0200 boehmes tuned
Tue, 26 Oct 2010 11:49:23 +0200 boehmes added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
Tue, 26 Oct 2010 11:45:12 +0200 boehmes joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
Tue, 26 Oct 2010 11:39:26 +0200 boehmes keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
Fri, 01 Oct 2010 10:25:36 +0200 haftmann chop_while replace drop_while and take_while
Thu, 30 Sep 2010 18:37:29 +0200 haftmann take_while, drop_while
Fri, 17 Sep 2010 10:52:35 +0200 boehmes add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
Fri, 27 Aug 2010 17:59:40 +0200 wenzelm more antiquotations;
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sat, 15 May 2010 16:20:54 +0200 blanchet make SML/NJ happy
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Wed, 12 May 2010 23:54:02 +0200 boehmes integrated SMT into the HOL image
less more (0) tip