Wed, 12 May 2010 23:53:57 +0200 |
boehmes |
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
|
file |
diff |
annotate
|
Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
Wed, 25 Nov 2009 12:29:37 +0100 |
boehmes |
more generic explosion of options (also accept newlines, etc.)
|
file |
diff |
annotate
|
Fri, 06 Nov 2009 17:52:57 +0100 |
boehmes |
added documentation for local SMT solver setup and available SMT options,
|
file |
diff |
annotate
|
Tue, 03 Nov 2009 14:51:55 +0100 |
boehmes |
added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 10:52:05 +0100 |
boehmes |
simplified method syntax of "smt",
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 14:22:02 +0200 |
boehmes |
eliminated extraneous wrapping of public records,
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 10:11:30 +0200 |
boehmes |
added proof reconstructon for Z3,
|
file |
diff |
annotate
|
Fri, 18 Sep 2009 18:13:19 +0200 |
boehmes |
added new method "smt": an oracle-based connection to external SMT solvers
|
file |
diff |
annotate
|