| Mon, 19 Jun 2023 22:28:09 +0200 |
Mathias Fleury |
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
|
file |
diff |
annotate
|
| Mon, 07 Feb 2022 15:26:22 +0100 |
blanchet |
added possibility of extra options to SMT slices
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
run all installed provers by default
|
file |
diff |
annotate
|
| Wed, 17 Nov 2021 15:09:10 +0100 |
fleury |
generate problems with correct logic for veriT
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Fri, 05 Mar 2021 20:52:08 +0100 |
wenzelm |
more direct unlimited smt_timeout;
|
file |
diff |
annotate
|
| Fri, 05 Mar 2021 20:38:55 +0100 |
wenzelm |
clarified smt: support Timeout.ignored and Timeout.scale_time;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2020 21:02:57 +0100 |
Mathias Fleury |
improve and activate compression for veriT proof reconstruction
|
file |
diff |
annotate
|
| Tue, 27 Oct 2020 22:34:37 +0100 |
wenzelm |
clarified signature: overloaded "+" for Path.append;
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 18:59:44 +0200 |
Mathias Fleury |
add reconstruction for the SMT solver veriT
|
file |
diff |
annotate
|
| Wed, 30 Sep 2020 18:37:22 +0200 |
desharna |
Effectively disable timeout for smt method/tactic
|
file |
diff |
annotate
|
| 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
|