20120523 
boehmes 
20120523 
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0

file  diff  annotate 
20120215 
wenzelm 
20120215 
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

file  diff  annotate 
20110416 
wenzelm 
20110416 
modernized structure Proof_Context;

file  diff  annotate 
20110214 
boehmes 
20110214 
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

file  diff  annotate 
20110202 
boehmes 
20110202 
avoid ML structure aliases (especially singleletter abbreviations)

file  diff  annotate 
20110108 
wenzelm 
20110108 
Ord_List.merge convenience;

file  diff  annotate 
20101220 
boehmes 
20101220 
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)

file  diff  annotate 
20101219 
boehmes 
20101219 
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
hide internal constants z3div and z3mod;
rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod

file  diff  annotate 
20101215 
boehmes 
20101215 
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
abolished SMT interface concept in favor of solver classes (now also the translation configuration is stored in the context);
proof reconstruction is now expected to return a theorem stating False (and hence needs to discharge all hypothetical definitions);
builtin functions carry additionally their arity and their most general type;
slightly generalized the definition of fun_app

file  diff  annotate 
20101215 
boehmes 
20101215 
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
added simple trigger inference mechanism;
added syntactic checks for triggers and quantifier weights;
factored out the normalization of special quantifiers (used to be in the etanormalization part);
normalization now unfolds abs/min/max (not SMTLIBspecific);
rules for pairs and function update are not anymore added automatically to the problem;
more aggressive rewriting of natural number operations into integer operations (minimizes the number of remaining natint coercions);
normalizations are now managed in a classbased manner (similar to builtin symbols)

file  diff  annotate 
20101215 
boehmes 
20101215 
moved SMT classes and dictionary functions to SMT_Utils

file  diff  annotate 
20101208 
boehmes 
20101208 
be more flexible: store SMT builtin symbols in generic contexts (not in theory contexts)

file  diff  annotate 
20101207 
boehmes 
20101207 
centralized handling of builtin 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 builtin symbols);
removed term_eq in favor of type replacements: termlevel occurrences of type bool are replaced by type term_bool (only for the translation)

file  diff  annotate 
20101124 
boehmes 
20101124 
be more precise: only treat constant 'distinct' applied to an explicit list as builtin

file  diff  annotate 
20101122 
boehmes 
20101122 
added prove reconstruction for injective functions;
added SMT_Utils to collect frequently used functions

file  diff  annotate 
20101117 
boehmes 
20101117 
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)

file  diff  annotate 
20101112 
boehmes 
20101112 
preliminary support for newer versions of Z3

file  diff  annotate 
20101029 
boehmes 
20101029 
introduced SMT.distinct as a representation of the solvers' builtin predicate; check that SMT.distinct is always applied to an explicit list

file  diff  annotate 
20101026 
boehmes 
20101026 
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface

file  diff  annotate 
20101026 
boehmes 
20101026 
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs

file  diff  annotate 
20100924 
wenzelm 
20100924 
modernized structure Ord_List;

file  diff  annotate 
20100913 
boehmes 
20100913 
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet

file  diff  annotate 
20100828 
haftmann 
20100828 
formerly unnamed infix equality now named HOL.eq

file  diff  annotate 
20100827 
haftmann 
20100827 
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

file  diff  annotate 
20100826 
haftmann 
20100826 
formerly unnamed infix impliciation now named HOL.implies

file  diff  annotate 
20100527 
boehmes 
20100527 
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")

file  diff  annotate 
20100527 
boehmes 
20100527 
use Z3's builtin support for div and mod

file  diff  annotate 
20100512 
boehmes 
20100512 
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable

file  diff  annotate 
20100512 
boehmes 
20100512 
integrated SMT into the HOL image

file  diff  annotate 