| Mon, 02 May 2011 16:33:21 +0200 |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file | diff | annotate |
| Fri, 01 Apr 2011 11:54:51 +0200 |
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
|
file | diff | annotate |
| Sun, 13 Mar 2011 16:01:00 +0100 |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file | diff | annotate |
| Mon, 14 Feb 2011 12:25:26 +0100 |
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
|
file | diff | annotate |
| Mon, 14 Feb 2011 10:40:43 +0100 |
more explicit errors to inform users about problems related to SMT solvers;
|
file | diff | annotate |
| Mon, 10 Jan 2011 18:58:54 +0100 |
be more precise: also merge option values
|
file | diff | annotate |
| Mon, 10 Jan 2011 17:41:45 +0100 |
only print warning in a visible context (previously, the warning was printed more than once)
|
file | diff | annotate |
| Sat, 08 Jan 2011 17:14:48 +0100 |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file | diff | annotate |
| Fri, 07 Jan 2011 13:24:09 +0100 |
shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)
|
file | diff | annotate |
| Fri, 07 Jan 2011 09:26:27 +0100 |
made SML/NJ happy
|
file | diff | annotate |
| Thu, 06 Jan 2011 17:51:56 +0100 |
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
|
file | diff | annotate |
| Wed, 15 Dec 2010 08:39:24 +0100 |
added option to enable trigger inference;
|
file | diff | annotate |
| Wed, 15 Dec 2010 08:39:24 +0100 |
moved SMT classes and dictionary functions to SMT_Utils
|
file | diff | annotate |
| Wed, 15 Dec 2010 08:39:24 +0100 |
added option to modify the random seed of SMT solvers
|
file | diff | annotate |
| Tue, 07 Dec 2010 14:53:12 +0100 |
centralized handling of built-in types and constants;
|
file | diff | annotate |
| Wed, 17 Nov 2010 08:14:55 +0100 |
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
|
file | diff | annotate |
| Fri, 12 Nov 2010 15:56:07 +0100 |
look for certificates relative to the theory
|
file | diff | annotate |
| Mon, 08 Nov 2010 12:13:44 +0100 |
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
|
file | diff | annotate |