| 2013-04-18 |
wenzelm |
2013-04-18 |
simplifier uses proper Proof.context instead of historic type simpset;
|
file | diff | annotate |
| 2012-10-31 |
blanchet |
2012-10-31 |
soft SMT timeout
|
file | diff | annotate |
| 2012-02-15 |
wenzelm |
2012-02-15 |
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 |
| 2012-02-14 |
wenzelm |
2012-02-14 |
normalized aliases;
|
file | diff | annotate |
| 2011-11-07 |
boehmes |
2011-11-07 |
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
|
file | diff | annotate |
| 2011-11-07 |
boehmes |
2011-11-07 |
replace higher-order matching against schematic theorem with dedicated reconstruction method
|
file | diff | annotate |
| 2011-10-28 |
wenzelm |
2011-10-28 |
tuned Named_Thms: proper binding;
|
file | diff | annotate |
| 2011-09-12 |
nipkow |
2011-09-12 |
new fastforce replacing fastsimp - less confusing name
|
file | diff | annotate |
| 2011-08-25 |
boehmes |
2011-08-25 |
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
|
file | diff | annotate |
| 2011-08-08 |
wenzelm |
2011-08-08 |
misc tuning -- eliminated old-fashioned rep_thm;
|
file | diff | annotate |
| 2011-07-18 |
boehmes |
2011-07-18 |
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
|
file | diff | annotate |
| 2011-05-26 |
boehmes |
2011-05-26 |
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
|
file | diff | annotate |
| 2011-05-13 |
wenzelm |
2011-05-13 |
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
|
file | diff | annotate |
| 2011-04-16 |
wenzelm |
2011-04-16 |
modernized structure Proof_Context;
|
file | diff | annotate |
| 2011-04-08 |
boehmes |
2011-04-08 |
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
|
file | diff | annotate |
| 2011-04-01 |
boehmes |
2011-04-01 |
save reflexivity steps in discharging Z3 Skolemization hypotheses
|
file | diff | annotate |
| 2011-04-01 |
boehmes |
2011-04-01 |
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
|
file | diff | annotate |
| 2011-03-09 |
boehmes |
2011-03-09 |
finished and tested Z3 proof reconstruction for injective functions;
only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)
|
file | diff | annotate |
| 2011-01-03 |
boehmes |
2011-01-03 |
re-implemented support for datatypes (including records and typedefs);
added test cases for datatypes, records and typedefs
|
file | diff | annotate |
| 2010-12-20 |
boehmes |
2010-12-20 |
avoid ML structure aliases (especially single-letter abbreviations)
|
file | diff | annotate |
| 2010-12-15 |
boehmes |
2010-12-15 |
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 |
| 2010-12-15 |
boehmes |
2010-12-15 |
fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
|
file | diff | annotate |
| 2010-12-15 |
boehmes |
2010-12-15 |
adapted the Z3 proof parser to recent changes in Z3's proof format;
keep the proof steps in an ordered list instead of in an Inttab (simplifies proof reconstruction code)
|
file | diff | annotate |
| 2010-12-15 |
boehmes |
2010-12-15 |
re-implemented eta-expansion, lambda-lifting, 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);
built-in functions carry additionally their arity and their most general type;
slightly generalized the definition of fun_app
|
file | diff | annotate |
| 2010-11-24 |
boehmes |
2010-11-24 |
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
|
file | diff | annotate |
| 2010-11-24 |
boehmes |
2010-11-24 |
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
|
file | diff | annotate |
| 2010-11-22 |
boehmes |
2010-11-22 |
added support for quantifier weight annotations
|
file | diff | annotate |
| 2010-11-22 |
boehmes |
2010-11-22 |
share and use more utility functions;
slightly reduced complexity for Z3 proof rule 'rewrite'
|
file | diff | annotate |
| 2010-11-22 |
boehmes |
2010-11-22 |
added prove reconstruction for injective functions;
added SMT_Utils to collect frequently used functions
|
file | diff | annotate |
| 2010-11-17 |
boehmes |
2010-11-17 |
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 |
| 2010-11-12 |
boehmes |
2010-11-12 |
preliminary support for newer versions of Z3
|
file | diff | annotate |
| 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)
|
file | diff | annotate |
| 2010-10-29 |
boehmes |
2010-10-29 |
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
|
file | diff | annotate |
| 2010-10-26 |
boehmes |
2010-10-26 |
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
|
file | diff | annotate |
| 2010-10-26 |
boehmes |
2010-10-26 |
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
|
file | diff | annotate |
| 2010-10-26 |
boehmes |
2010-10-26 |
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 |
| 2010-09-20 |
wenzelm |
2010-09-20 |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file | diff | annotate |
| 2010-09-01 |
haftmann |
2010-09-01 |
replaced Table.map' by Table.map
|
file | diff | annotate |
| 2010-08-27 |
haftmann |
2010-08-27 |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file | diff | annotate |
| 2010-05-26 |
boehmes |
2010-05-26 |
try logical and theory abstraction before full abstraction (avoids warnings of linarith)
|
file | diff | annotate |
| 2010-05-15 |
wenzelm |
2010-05-15 |
incorporated further conversions and conversionals, after some minor tuning;
|
file | diff | annotate |
| 2010-05-12 |
boehmes |
2010-05-12 |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file | diff | annotate |
| 2010-05-12 |
boehmes |
2010-05-12 |
integrated SMT into the HOL image
|
file | diff | annotate |