Tue, 15 Jul 2014 00:21:32 +0200 |
blanchet |
don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic
|
file |
diff |
annotate
|
Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
don't ask proof-disabled solvers to do proofs
|
file |
diff |
annotate
|
Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 10 Jun 2014 19:15:14 +0200 |
blanchet |
generate ':named' attributes in SMT-LIB 2 problems, to facilitate reconstruction
|
file |
diff |
annotate
|
Tue, 03 Jun 2014 11:43:07 +0200 |
blanchet |
removed SMT weights -- their impact was very inconclusive anyway
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
simplified solution parsing
|
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 |
reintroduced old model reconstruction code -- still needs to be ported
|
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
|