#
c93a1841 |
|
13-Apr-2019 |
wenzelm <none@none> |
tuned signature;
|
#
dead1326 |
|
13-Apr-2019 |
wenzelm <none@none> |
tuned signature -- more ctyp operations;
|
#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
f9beda92 |
|
29-Aug-2017 |
blanchet <none@none> |
towards support for HO SMT-LIB
|
#
3c2b07e1 |
|
25-Sep-2016 |
haftmann <none@none> |
syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div --HG-- extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4
|
#
f2ba2c03 |
|
01-Jun-2015 |
haftmann <none@none> |
separate class for division operator, with particular syntax added in more specific classes
|
#
904e2f2f |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
5f318eee |
|
04-Mar-2015 |
wenzelm <none@none> |
clarified signature;
|
#
f4f8c25c |
|
17-Sep-2014 |
blanchet <none@none> |
added interface for CVC4 extensions
|
#
ac75f5e7 |
|
27-Aug-2014 |
blanchet <none@none> |
renamed new SMT module from 'SMT2' to 'SMT' --HG-- rename : src/HOL/SMT2.thy => src/HOL/SMT.thy rename : src/HOL/Tools/SMT2/smt2_builtin.ML => src/HOL/Tools/SMT/smt_builtin.ML rename : src/HOL/Tools/SMT2/smt2_config.ML => src/HOL/Tools/SMT/smt_config.ML rename : src/HOL/Tools/SMT2/smt2_datatypes.ML => src/HOL/Tools/SMT/smt_datatypes.ML rename : src/HOL/Tools/SMT2/smt2_failure.ML => src/HOL/Tools/SMT/smt_failure.ML rename : src/HOL/Tools/SMT2/smt2_normalize.ML => src/HOL/Tools/SMT/smt_normalize.ML rename : src/HOL/Tools/SMT2/smt2_real.ML => src/HOL/Tools/SMT/smt_real.ML rename : src/HOL/Tools/SMT2/smt2_solver.ML => src/HOL/Tools/SMT/smt_solver.ML rename : src/HOL/Tools/SMT2/smt2_systems.ML => src/HOL/Tools/SMT/smt_systems.ML rename : src/HOL/Tools/SMT2/smt2_translate.ML => src/HOL/Tools/SMT/smt_translate.ML rename : src/HOL/Tools/SMT2/smt2_util.ML => src/HOL/Tools/SMT/smt_util.ML rename : src/HOL/Tools/SMT2/smtlib2.ML => src/HOL/Tools/SMT/smtlib.ML rename : src/HOL/Tools/SMT2/smtlib2_interface.ML => src/HOL/Tools/SMT/smtlib_interface.ML rename : src/HOL/Tools/SMT2/smtlib2_isar.ML => src/HOL/Tools/SMT/smtlib_isar.ML rename : src/HOL/Tools/SMT2/smtlib2_proof.ML => src/HOL/Tools/SMT/smtlib_proof.ML rename : src/HOL/Tools/SMT2/verit_isar.ML => src/HOL/Tools/SMT/verit_isar.ML rename : src/HOL/Tools/SMT2/verit_proof.ML => src/HOL/Tools/SMT/verit_proof.ML rename : src/HOL/Tools/SMT2/verit_proof_parse.ML => src/HOL/Tools/SMT/verit_proof_parse.ML rename : src/HOL/Tools/SMT2/z3_new_interface.ML => src/HOL/Tools/SMT/z3_interface.ML rename : src/HOL/Tools/SMT2/z3_new_isar.ML => src/HOL/Tools/SMT/z3_isar.ML rename : src/HOL/Tools/SMT2/z3_new_proof.ML => src/HOL/Tools/SMT/z3_proof.ML rename : src/HOL/Tools/SMT2/z3_new_real.ML => src/HOL/Tools/SMT/z3_real.ML rename : src/HOL/Tools/SMT2/z3_new_replay.ML => src/HOL/Tools/SMT/z3_replay.ML rename : src/HOL/Tools/SMT2/z3_new_replay_literals.ML => src/HOL/Tools/SMT/z3_replay_literals.ML rename : src/HOL/Tools/SMT2/z3_new_replay_methods.ML => src/HOL/Tools/SMT/z3_replay_methods.ML rename : src/HOL/Tools/SMT2/z3_new_replay_rules.ML => src/HOL/Tools/SMT/z3_replay_rules.ML rename : src/HOL/Tools/SMT2/z3_new_replay_util.ML => src/HOL/Tools/SMT/z3_replay_util.ML rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML rename : src/HOL/Word/Tools/smt2_word.ML => src/HOL/Word/Tools/smt_word.ML
|
#
f16a71f4 |
|
05-Oct-2012 |
blanchet <none@none> |
newer versions of Z3 call it "Bool" not "bool"
|
#
8da40e1c |
|
23-May-2012 |
boehmes <none@none> |
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
|
#
0d27b506 |
|
15-Feb-2012 |
wenzelm <none@none> |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
436f6b2f |
|
14-Feb-2011 |
boehmes <none@none> |
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
|
#
231109ad |
|
02-Feb-2011 |
boehmes <none@none> |
avoid ML structure aliases (especially single-letter abbreviations)
|
#
97693234 |
|
08-Jan-2011 |
wenzelm <none@none> |
Ord_List.merge convenience;
|
#
c0705135 |
|
20-Dec-2010 |
boehmes <none@none> |
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
|
#
104b9a3d |
|
19-Dec-2010 |
boehmes <none@none> |
only linear occurrences of multiplication are treated as built-in (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
|
#
58e355b7 |
|
15-Dec-2010 |
boehmes <none@none> |
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
|
#
d15f02bb |
|
15-Dec-2010 |
boehmes <none@none> |
re-ordered SMT normalization code (eta-normalization, 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 eta-normalization part); normalization now unfolds abs/min/max (not SMT-LIB-specific); 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 nat-int coercions); normalizations are now managed in a class-based manner (similar to built-in symbols)
|
#
4b0c0402 |
|
15-Dec-2010 |
boehmes <none@none> |
moved SMT classes and dictionary functions to SMT_Utils
|
#
842af847 |
|
08-Dec-2010 |
boehmes <none@none> |
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
|
#
1e323d7a |
|
07-Dec-2010 |
boehmes <none@none> |
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)
|
#
86580571 |
|
24-Nov-2010 |
boehmes <none@none> |
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
|
#
0b013a0d |
|
22-Nov-2010 |
boehmes <none@none> |
added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions
|
#
c982ee42 |
|
17-Nov-2010 |
boehmes <none@none> |
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)
|
#
0c41d352 |
|
12-Nov-2010 |
boehmes <none@none> |
preliminary support for newer versions of Z3
|
#
f110f01e |
|
29-Oct-2010 |
boehmes <none@none> |
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
|
#
393b826c |
|
26-Oct-2010 |
boehmes <none@none> |
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
|
#
d3020384 |
|
26-Oct-2010 |
boehmes <none@none> |
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
|
#
86bc1118 |
|
24-Sep-2010 |
wenzelm <none@none> |
modernized structure Ord_List;
|
#
d03d84c6 |
|
12-Sep-2010 |
boehmes <none@none> |
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
|
#
b11705e1 |
|
28-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix equality now named HOL.eq
|
#
c91cbd4e |
|
27-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
#
5f258a36 |
|
26-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix impliciation now named HOL.implies
|
#
806451a7 |
|
27-May-2010 |
boehmes <none@none> |
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
|
#
a61b5494 |
|
27-May-2010 |
boehmes <none@none> |
use Z3's builtin support for div and mod
|
#
5d3ecda1 |
|
12-May-2010 |
boehmes <none@none> |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
#
8cfb9a3f |
|
12-May-2010 |
boehmes <none@none> |
integrated SMT into the HOL image
|