| Wed, 12 May 2010 23:53:57 +0200 |
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 |
| Wed, 07 Apr 2010 20:40:42 +0200 |
buffered output (faster than direct output)
|
file | diff | annotate |
| Wed, 07 Apr 2010 20:40:42 +0200 |
shortened interface (do not export unused options and functions)
|
file | diff | annotate |
| Wed, 07 Apr 2010 20:40:42 +0200 |
always unfold definitions of specific constants (including special binders)
|
file | diff | annotate |
| Tue, 16 Feb 2010 16:20:34 +0100 |
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
|
file | diff | annotate |
| Thu, 05 Nov 2009 15:24:49 +0100 |
handle let expressions inside terms by unfolding (instead of raising an exception),
|
file | diff | annotate |
| Tue, 03 Nov 2009 14:51:55 +0100 |
added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),
|
file | diff | annotate |
| Fri, 30 Oct 2009 11:26:38 +0100 |
pattern are separated only by spaces (no comma)
|
file | diff | annotate |
| Tue, 20 Oct 2009 14:22:02 +0200 |
eliminated extraneous wrapping of public records,
|
file | diff | annotate |
| Fri, 18 Sep 2009 18:13:19 +0200 |
added new method "smt": an oracle-based connection to external SMT solvers
|
file | diff | annotate |