| Wed, 12 May 2010 23:54:00 +0200 |
boehmes |
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:53:58 +0200 |
boehmes |
added tracing of reconstruction data
|
file |
diff |
annotate
|
| 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
|
| Wed, 12 May 2010 23:53:55 +0200 |
boehmes |
move the addition of extra facts into a separate module
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 20:40:42 +0200 |
boehmes |
buffered output (faster than direct output)
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 20:40:42 +0200 |
boehmes |
shortened interface (do not export unused options and functions)
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 20:38:11 +0200 |
boehmes |
fail for problems containg the universal sort (as those problems cannot be atomized)
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 19:48:58 +0200 |
boehmes |
renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 16:20:34 +0100 |
boehmes |
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 15:25:36 +0100 |
boehmes |
added Cache_IO: cache for output of external tools,
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 11:01:47 +0100 |
boehmes |
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
|
file |
diff |
annotate
|
| Sat, 06 Feb 2010 14:50:55 +0100 |
wenzelm |
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 23:38:41 +0100 |
boehmes |
capture error messages (of SMT solvers)
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 18:10:41 +0100 |
boehmes |
collect certificates in a single file
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:47:37 +0100 |
boehmes |
removed unused code and unused arguments,
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 11:34:22 +0100 |
boehmes |
follow standard theory merge behaviour: do not change already selected solver
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 08:57:07 +0100 |
boehmes |
made theory merge deterministic wrt. the selected solver
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:22 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
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
|
| Thu, 15 Oct 2009 21:28:39 +0200 |
wenzelm |
normalized aliases of Output operations;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 16:15:22 +0200 |
wenzelm |
sort_strings (cf. Pure/library.ML);
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 15:45:50 +0200 |
wenzelm |
exported File.shell_quote;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 16:06:52 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 11:15:21 +0200 |
boehmes |
corrected remote SMT solver invocation
|
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
|