| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed '_new' sufffix in SMT2 solver names (in some cases)
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 11:38:53 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 17:34:26 +0200 |
blanchet |
split replay and proof parsing for Z3
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:57:45 +0200 |
blanchet |
renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
|
file |
diff |
annotate
|
| Thu, 01 May 2014 22:57:34 +0200 |
boehmes |
use internal proof-producing SAT solver for more efficient SMT proof replay
|
file |
diff |
annotate
|
| 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
|
| Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
adapted to renamed ML files
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
|
file |
diff |
annotate
|