src/HOL/Tools/SMT/smt_setup_solvers.ML
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Wed, 23 Mar 2011 15:33:17 +0100 boehmes Z3 non-commercial usage may explicitly be declined
Wed, 23 Mar 2011 14:29:29 +0100 boehmes export status function to query whether Z3 has been activated for usage within Isabelle
Mon, 21 Feb 2011 14:02:07 +0100 blanchet better fudge factors for CVC3 and Yices based on Judgment Day
Mon, 21 Feb 2011 10:03:48 +0100 blanchet comments to find fudge factors easily
Fri, 18 Feb 2011 15:44:52 +0100 blanchet better fudge factors for Sledgehammer
Mon, 14 Feb 2011 10:40:43 +0100 boehmes more explicit errors to inform users about problems related to SMT solvers;
Mon, 17 Jan 2011 17:45:52 +0100 boehmes made Z3 the default SMT solver again
Thu, 06 Jan 2011 17:51:56 +0100 boehmes differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
Fri, 17 Dec 2010 15:30:00 +0100 boehmes fixed the command-line syntax for setting Yices' random seed
Wed, 15 Dec 2010 10:12:48 +0100 boehmes adapted the Z3 proof parser to recent changes in Z3's proof format;
Wed, 15 Dec 2010 10:12:44 +0100 boehmes re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
Wed, 15 Dec 2010 08:39:24 +0100 boehmes added option to modify the random seed of SMT solvers
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, 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)
Fri, 29 Oct 2010 18:17:06 +0200 boehmes clarified error message
Wed, 27 Oct 2010 08:58:03 +0200 boehmes made SML/NJ happy
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 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
less more (0) tip