| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2018 16:24:04 +0100 |
fleury |
add reconstruction by veriT in method smt
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Fri, 22 Sep 2017 13:46:11 -0300 |
blanchet |
real oracle
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 16:03:30 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 20 May 2016 07:54:54 +0200 |
fleury |
better handling of veriT's 'unknown' status
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 21:09:28 +0100 |
wenzelm |
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 22:36:09 +0200 |
blanchet |
generate proper error instead of exception if goal cannot be atomized
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 21:33:00 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 19:28:43 +0200 |
wenzelm |
Variable.focus etc.: optional bindings provided by user;
|
file |
diff |
annotate
|
| Sat, 25 Apr 2015 09:48:06 +0200 |
blanchet |
made CVC4 support work also without unsat cores
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:44:57 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
| base
|
| Wed, 02 Oct 2013 22:54:42 +0200 |
blanchet |
make SMT integration slacker w.r.t. bad apples (facts)
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 03:47:02 +0100 |
blanchet |
made MaSh evaluation driver work with SMT solvers
|
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
|
| Thu, 26 Jul 2012 11:08:16 +0200 |
blanchet |
Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
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)
|
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
|
| Mon, 23 Apr 2012 21:44:36 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
renamed "smt_fixed" to "smt_read_only_certificates"
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 10:12:58 +0100 |
boehmes |
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
|
file |
diff |
annotate
|
| Wed, 29 Feb 2012 17:43:41 +0100 |
boehmes |
SMT fails if the chosen SMT solver is not installed
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 19:18:57 +0100 |
wenzelm |
normalized aliases;
|
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
|
| Fri, 08 Apr 2011 19:04:08 +0200 |
boehmes |
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
|
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
|
| Mon, 10 Jan 2011 17:39:54 +0100 |
boehmes |
dropped superfluous error message
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
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
|
| Mon, 20 Dec 2010 22:02:57 +0100 |
boehmes |
avoid ML structure aliases (especially single-letter abbreviations)
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 08:17:23 +0100 |
boehmes |
perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 15:30:43 +0100 |
blanchet |
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 12:10:08 +0100 |
blanchet |
make timeout part of the SMT filter's tail
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 12:02:46 +0100 |
blanchet |
split "smt_filter" into head and tail
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 10:12:48 +0100 |
boehmes |
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
|
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 |
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
moved SMT classes and dictionary functions to SMT_Utils
|
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
|
| Tue, 07 Dec 2010 15:55:35 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 15:01:37 +0100 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 09:58:52 +0100 |
blanchet |
make SML/NJ happy
|
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, 06 Dec 2010 10:32:39 +0100 |
blanchet |
return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 18:27:21 +0100 |
blanchet |
export more information about available SMT solvers
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 18:22:43 +0100 |
boehmes |
split up Z3 models into constraints on free variables and constant definitions;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 22:23:28 +0100 |
boehmes |
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
|
file |
diff |
annotate
|
| Mon, 15 Nov 2010 22:23:26 +0100 |
boehmes |
honour timeouts which are not rounded to full seconds
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|