| Sun, 19 Jan 2014 22:38:17 +0100 |
boehmes |
removed obsolete remote_cvc3 and remote_z3
|
file |
diff |
annotate
|
| Wed, 15 Jan 2014 16:57:29 +0100 |
wenzelm |
fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
|
file |
diff |
annotate
|
| Mon, 13 Jan 2014 20:20:44 +0100 |
wenzelm |
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 23:07:21 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2013 11:35:22 +0100 |
blanchet |
Z3's soft timeout is expressed in ms, not in s -- this explains the frequenty "error code 112" failures we had recently
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
soft SMT timeout
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 13:03:29 +0200 |
wenzelm |
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
get rid of redundant "xxx_INSTALLED" environment variabl
|
file |
diff |
annotate
|
| Mon, 04 Jun 2012 09:07:23 +0200 |
boehmes |
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
|
file |
diff |
annotate
|
| Wed, 30 May 2012 23:10:42 +0200 |
boehmes |
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
|
file |
diff |
annotate
|
| Thu, 17 May 2012 13:36:23 +0200 |
blanchet |
robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 11:15:49 +0200 |
blanchet |
tuned "max_relevant" defaults for SMT solvers based on Judgment Day
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 16:04:29 +0200 |
wenzelm |
more hints on Z3 configuration;
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 15:33:17 +0100 |
boehmes |
Z3 non-commercial usage may explicitly be declined
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 14:29:29 +0100 |
boehmes |
export status function to query whether Z3 has been activated for usage within Isabelle
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 14:02:07 +0100 |
blanchet |
better fudge factors for CVC3 and Yices based on Judgment Day
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:03:48 +0100 |
blanchet |
comments to find fudge factors easily
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 15:44:52 +0100 |
blanchet |
better fudge factors for Sledgehammer
|
file |
diff |
annotate
|
| Mon, 14 Feb 2011 10:40:43 +0100 |
boehmes |
more explicit errors to inform users about problems related to SMT solvers;
|
file |
diff |
annotate
|
| Mon, 17 Jan 2011 17:45:52 +0100 |
boehmes |
made Z3 the default SMT solver again
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 17:51:56 +0100 |
boehmes |
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 15:30:00 +0100 |
boehmes |
fixed the command-line syntax for setting Yices' random seed
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 10:12:48 +0100 |
boehmes |
adapted the Z3 proof parser to recent changes in Z3's proof format;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to modify the random seed of SMT solvers
|
file |
diff |
annotate
|
| 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?
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:06 +0200 |
boehmes |
clarified error message
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 08:58:03 +0200 |
boehmes |
made SML/NJ happy
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|