19 months ago blanchet 2017-10-01 properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
21 months ago blanchet 2017-08-29 towards support for HO SMT-LIB
22 months ago blanchet 2017-07-28 introduced option for nat-as-int in SMT
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2015-05-30 wenzelm 2015-05-30 tuned message;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2014-12-29 boehmes 2014-12-29 optionally display statistics for Z3 proof reconstruction
2014-12-29 boehmes 2014-12-29 avoid more than one data slot per module
2014-12-29 boehmes 2014-12-29 limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2013-10-02 blanchet 2013-10-02 make SMT integration slacker w.r.t. bad apples (facts)
2013-07-18 wenzelm 2013-07-18 tuned signature;
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2013-03-28 boehmes 2013-03-28 new, simpler implementation of monomorphization; old monomorphization code is still available as Legacy_Monomorphization; modified SMT integration to use the new monomorphization code
2012-12-03 wenzelm 2012-12-03 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic); clarified signature -- cache init is unsynchronized and hopefully used at most once per file;
2012-05-30 boehmes 2012-05-30 introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
2012-03-27 blanchet 2012-03-27 renamed "smt_fixed" to "smt_read_only_certificates"
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-02-29 boehmes 2012-02-29 SMT fails if the chosen SMT solver is not installed
2011-12-29 wenzelm 2011-12-29 comments;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-01 boehmes 2011-04-01 make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-02-14 boehmes 2011-02-14 limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops); updated SMT certificate
2011-02-14 boehmes 2011-02-14 more explicit errors to inform users about problems related to SMT solvers; fall back to remote SMT solver (if local version does not exist); extend the Z3 proof parser to accommodate for slight changes introduced by Z3 2.18
2011-01-10 boehmes 2011-01-10 be more precise: also merge option values
2011-01-10 boehmes 2011-01-10 only print warning in a visible context (previously, the warning was printed more than once)
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2011-01-07 boehmes 2011-01-07 shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)
2011-01-07 boehmes 2011-01-07 made SML/NJ happy
2011-01-06 boehmes 2011-01-06 differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface
2010-12-15 boehmes 2010-12-15 added option to enable trigger inference; better documentation of triggers and SMT available options
2010-12-15 boehmes 2010-12-15 moved SMT classes and dictionary functions to SMT_Utils
2010-12-15 boehmes 2010-12-15 added option to modify the random seed of SMT solvers
2010-12-07 boehmes 2010-12-07 centralized handling of built-in types and constants; also store types and constants which are rewritten during preprocessing; interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols); removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)
2010-11-17 boehmes 2010-11-17 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
2010-11-12 boehmes 2010-11-12 look for certificates relative to the theory
2010-11-08 boehmes 2010-11-08 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)