20110714 
blanchet 
20110714 
allow lambdalifting without triggers

file  diff  annotate 
20110626 
boehmes 
20110626 
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
maintain extralogical information when introducing explicit application;
handle letexpressions properly

file  diff  annotate 
20110622 
boehmes 
20110622 
export lambdalifting code as there is potential use for it within Sledgehammer

file  diff  annotate 
20110614 
boehmes 
20110614 
slightly more general treatment of mutually recursive datatypes;
treat datatype constructors and selectors similarly to builtin constants wrt. introduction of explicit application (in the same way as what is already done for etaexpansion)

file  diff  annotate 
20110605 
boehmes 
20110605 
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)

file  diff  annotate 
20110408 
boehmes 
20110408 
fixed etaexpansion: use correct order to apply new bound variables

file  diff  annotate 
20110408 
boehmes 
20110408 
unfold and etacontract let expressions before lambdalifting to avoid bad terms

file  diff  annotate 
20110221 
boehmes 
20110221 
wrap occurrences of quantifiers in firstorder terms (i.e., outside firstorder formulas) in Ifexpressions

file  diff  annotate 
20110103 
boehmes 
20110103 
reimplemented support for datatypes (including records and typedefs);
added test cases for datatypes, records and typedefs

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

file  diff  annotate 
20101219 
boehmes 
20101219 
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
removed odd retyping during folify (instead, keep all terms welltyped)

file  diff  annotate 
20101217 
wenzelm 
20101217 
merged

file  diff  annotate 
20101217 
boehmes 
20101217 
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
fixed introduction of explicit application: use explicit application for every additional argument (grouping of arguments caused confusion when translating into the intermediate format)

file  diff  annotate 
20101217 
wenzelm 
20101217 
tuned;

file  diff  annotate 
20101216 
boehmes 
20101216 
merged

file  diff  annotate 
20101216 
boehmes 
20101216 
fix lambdalifting: take level of bound variables into account and also apply bound variables from outer scope

file  diff  annotate 
20101216 
boehmes 
20101216 
fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term

file  diff  annotate 
20101216 
boehmes 
20101216 
fixed etaexpansion: introduce a couple of abstractions at once

file  diff  annotate 
20101216 
paulson 
20101216 
merged

file  diff  annotate 
20101216 
paulson 
20101216 
made sml/nj happy

file  diff  annotate 
20101215 
boehmes 
20101215 
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)

file  diff  annotate 
20101215 
boehmes 
20101215 
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils

file  diff  annotate 
20101215 
blanchet 
20101215 
workaround for bug in weight handling  sometimes numerals got replaced by Vars and this confused the weight extractor

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 
tuned

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 
20101206 
boehmes 
20101206 
tuned

file  diff  annotate 
20101125 
blanchet 
20101125 
etareduce on the fly to prevent an exception

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 support for quantifier weight annotations

file  diff  annotate 
20101122 
boehmes 
20101122 
share and use more utility functions;
slightly reduced complexity for Z3 proof rule 'rewrite'

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 
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 
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 
20100919 
boehmes 
20100919 
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)

file  diff  annotate 
20100917 
boehmes 
20100917 
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions

file  diff  annotate 
20100916 
boehmes 
20100916 
reverse order of datatype declarations so that declarations only depend on already declared datatypes

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 
20100526 
boehmes 
20100526 
hide constants and types introduced by SMT,
simplified SMT patterns syntax,
added examples for SMT patterns

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 