Tue, 30 Oct 2018 16:24:04 +0100 |
fleury |
add reconstruction by veriT in method smt
|
file |
diff |
annotate
|
Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
Sun, 01 Oct 2017 15:01:39 +0200 |
blanchet |
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
|
file |
diff |
annotate
|
Tue, 29 Aug 2017 18:30:23 +0200 |
blanchet |
towards support for HO SMT-LIB
|
file |
diff |
annotate
|
Fri, 28 Jul 2017 15:36:32 +0100 |
blanchet |
introduced option for nat-as-int in SMT
|
file |
diff |
annotate
|
Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
Sat, 30 May 2015 19:29:21 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
Mon, 29 Dec 2014 22:14:13 +0100 |
boehmes |
optionally display statistics for Z3 proof reconstruction
|
file |
diff |
annotate
|
Mon, 29 Dec 2014 16:21:33 +0100 |
boehmes |
avoid more than one data slot per module
|
file |
diff |
annotate
|
Mon, 29 Dec 2014 14:57:13 +0100 |
boehmes |
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
|
file |
diff |
annotate
|
Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
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, 26 Mar 2014 14:41:52 +0100 |
wenzelm |
prefer Context_Position where a context is available;
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
|
Wed, 02 Oct 2013 22:54:42 +0200 |
blanchet |
make SMT integration slacker w.r.t. bad apples (facts)
|
file |
diff |
annotate
|
Thu, 18 Jul 2013 21:20:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
Thu, 28 Mar 2013 23:44:41 +0100 |
boehmes |
new, simpler implementation of monomorphization;
|
file |
diff |
annotate
|
Mon, 03 Dec 2012 16:07:28 +0100 |
wenzelm |
synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
|
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
|
Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
renamed "smt_fixed" to "smt_read_only_certificates"
|
file |
diff |
annotate
|
Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
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
|
Thu, 29 Dec 2011 15:54:37 +0100 |
wenzelm |
comments;
|
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, 01 Apr 2011 11:54:51 +0200 |
boehmes |
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
|
file |
diff |
annotate
|
Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
Mon, 14 Feb 2011 12:25:26 +0100 |
boehmes |
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
|
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, 10 Jan 2011 18:58:54 +0100 |
boehmes |
be more precise: also merge option values
|
file |
diff |
annotate
|
Mon, 10 Jan 2011 17:41:45 +0100 |
boehmes |
only print warning in a visible context (previously, the warning was printed more than once)
|
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
|
Fri, 07 Jan 2011 13:24:09 +0100 |
boehmes |
shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 09:26:27 +0100 |
boehmes |
made SML/NJ happy
|
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
|
Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to enable trigger inference;
|
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 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
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
|
Fri, 12 Nov 2010 15:56:07 +0100 |
boehmes |
look for certificates relative to the theory
|
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
|