#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
7110473f |
|
30-Oct-2018 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
add reconstruction by veriT in method smt
|
#
19ef2e2e |
|
30-Oct-2018 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
split SMT reconstruction into library
|
#
cc37beb1 |
|
24-Sep-2018 |
nipkow <none@none> |
Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
|
#
eee54cc2 |
|
11-Apr-2018 |
boehmes <none@none> |
avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
fd2471a9 |
|
08-Oct-2017 |
haftmann <none@none> |
euclidean rings need no normalization --HG-- extra : rebase_source : 7f2e3f676b513d6c59f526f099be30240183bf05
|
#
4bbb98d7 |
|
30-Aug-2017 |
blanchet <none@none> |
added options to make veriT more complete
|
#
f9beda92 |
|
29-Aug-2017 |
blanchet <none@none> |
towards support for HO SMT-LIB
|
#
29d6296c |
|
03-Aug-2017 |
blanchet <none@none> |
pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
|
#
1d8a8be4 |
|
28-Jul-2017 |
blanchet <none@none> |
introduced option for nat-as-int in SMT
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
9efe9f85 |
|
10-Nov-2015 |
wenzelm <none@none> |
recovered from a9c0572109af;
|
#
7d38a922 |
|
10-Nov-2015 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
fixing premises in veriT proof reconstruction
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
2c86cbbc |
|
08-Apr-2015 |
blanchet <none@none> |
updated SMT module and Sledgehammer to fully open source Z3
|
#
e2f81425 |
|
16-Jan-2015 |
boehmes <none@none> |
more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
|
#
9d42f93b |
|
23-Nov-2014 |
blanchet <none@none> |
added one more CVC4 option that helps Judgment Day (10 theory version)
|
#
f9d27b43 |
|
23-Nov-2014 |
blanchet <none@none> |
added Z3 reconstruction rule suggested by F. Maric
|
#
e0edc073 |
|
23-Nov-2014 |
blanchet <none@none> |
one more CVC4 option that helps
|
#
28085c4a |
|
23-Nov-2014 |
blanchet <none@none> |
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
|
#
ea9ef2a8 |
|
20-Nov-2014 |
blanchet <none@none> |
added CVC4 option that helps on JD
|
#
d13e746e |
|
20-Nov-2014 |
blanchet <none@none> |
removed explicit '--quant-cf' option to CVC4, now that it's the default
|
#
22da81d0 |
|
19-Nov-2014 |
blanchet <none@none> |
parse CVC4 unsat cores
|
#
f6662567 |
|
25-Apr-2015 |
blanchet <none@none> |
made CVC4 support work also without unsat cores
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
2227b563 |
|
24-Oct-2014 |
hoelzl <none@none> |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
#
76d9d199 |
|
06-Oct-2014 |
blanchet <none@none> |
strengthened 'moura' method
|
#
ef3b9997 |
|
29-Sep-2014 |
blanchet <none@none> |
made 'moura' tactic more powerful
|
#
f4f8c25c |
|
17-Sep-2014 |
blanchet <none@none> |
added interface for CVC4 extensions
|
#
62fda0f2 |
|
25-Sep-2014 |
blanchet <none@none> |
added useful options to CVC4
|
#
d6b129f0 |
|
28-Aug-2014 |
blanchet <none@none> |
tuned method description
|
#
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
|
#
b9f5418a |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems; modernized setup; tuned;
|
#
d4fd6e53 |
|
11-Jun-2014 |
blanchet <none@none> |
reduces Sledgehammer dependencies
|
#
466e1b30 |
|
11-Jun-2014 |
blanchet <none@none> |
tuning
|
#
321ad186 |
|
11-Jun-2014 |
blanchet <none@none> |
use 'ctr_sugar' abstraction in SMT(2)
|
#
e0f968f4 |
|
11-Jun-2014 |
blanchet <none@none> |
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
|
#
6b4f08d8 |
|
13-Mar-2014 |
blanchet <none@none> |
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
|
#
8ad44d7e |
|
11-Mar-2014 |
blanchet <none@none> |
full path
|
#
b92f6b52 |
|
19-Jan-2014 |
boehmes <none@none> |
removed obsolete remote_cvc3 and remote_z3
|
#
115c1df3 |
|
13-Jan-2014 |
wenzelm <none@none> |
activation of Z3 via "z3_non_commercial" system option (without requiring restart);
|
#
b5be22e7 |
|
03-Dec-2012 |
wenzelm <none@none> |
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;
|
#
7cbe0f37 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
429ef7fe |
|
23-Apr-2012 |
wenzelm <none@none> |
more standard method setup;
|
#
b24a20db |
|
27-Mar-2012 |
blanchet <none@none> |
renamed "smt_fixed" to "smt_read_only_certificates"
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
90b55d45 |
|
07-Nov-2011 |
boehmes <none@none> |
replace higher-order matching against schematic theorem with dedicated reconstruction method
|
#
a7d08ecf |
|
25-Aug-2011 |
boehmes <none@none> |
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
|
#
70c7dd0c |
|
09-Aug-2011 |
blanchet <none@none> |
load lambda-lifting structure earlier, so it can be used in Metis
|
#
4e6b21f6 |
|
19-Jul-2011 |
boehmes <none@none> |
generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
|
#
25a19c92 |
|
20-Jul-2011 |
boehmes <none@none> |
moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)
|
#
3eee5111 |
|
20-Jul-2011 |
boehmes <none@none> |
removed old (unused) SMT monomorphizer
|
#
8baae062 |
|
07-Jun-2011 |
boehmes <none@none> |
clarified meaning of monomorphization configuration option by renaming it
|
#
54cdd3ea |
|
13-Feb-2011 |
boehmes <none@none> |
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
|
#
560edaea |
|
17-Jan-2011 |
boehmes <none@none> |
made Z3 the default SMT solver again
|
#
01a0cde7 |
|
07-Jan-2011 |
boehmes <none@none> |
tuned text
|
#
0ea3f73f |
|
07-Jan-2011 |
boehmes <none@none> |
added hints about licensing restrictions and how to enable Z3
|
#
5dd62dd8 |
|
06-Jan-2011 |
boehmes <none@none> |
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
|
#
ead8ec93 |
|
03-Jan-2011 |
boehmes <none@none> |
re-implemented support for datatypes (including records and typedefs); added test cases for datatypes, records and typedefs
|
#
06e58f50 |
|
20-Dec-2010 |
boehmes <none@none> |
avoid ML structure aliases (especially single-letter abbreviations)
|
#
abf72b42 |
|
19-Dec-2010 |
boehmes <none@none> |
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions); removed odd retyping during folify (instead, keep all terms well-typed)
|
#
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
|
#
2526badf |
|
15-Dec-2010 |
boehmes <none@none> |
fixed trigger inference: testing if a theorem already has a trigger was too strict; fixed monomorphization with respect to triggers (which might occur schematically)
|
#
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)
|
#
a6d5970d |
|
15-Dec-2010 |
boehmes <none@none> |
added option to enable trigger inference; better documentation of triggers and SMT available options
|
#
4b0c0402 |
|
15-Dec-2010 |
boehmes <none@none> |
moved SMT classes and dictionary functions to SMT_Utils
|
#
681fd023 |
|
15-Dec-2010 |
boehmes <none@none> |
added option to modify the random seed of SMT solvers
|
#
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)
|
#
a93cbb2d |
|
29-Nov-2010 |
boehmes <none@none> |
also support higher-order rules for Z3 proof reconstruction
|
#
86580571 |
|
24-Nov-2010 |
boehmes <none@none> |
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
|
#
6bf2d026 |
|
22-Nov-2010 |
boehmes <none@none> |
added support for quantifier weight annotations
|
#
0b013a0d |
|
22-Nov-2010 |
boehmes <none@none> |
added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions
|
#
b1d1d667 |
|
07-Nov-2010 |
boehmes <none@none> |
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)
|
#
65656432 |
|
29-Oct-2010 |
boehmes <none@none> |
added crafted list of SMT built-in constants
|
#
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
|
#
191468cb |
|
17-Sep-2010 |
boehmes <none@none> |
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
|
#
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
|
#
225699c2 |
|
14-Jul-2010 |
haftmann <none@none> |
load cache_io before code generator; moved adhoc-overloading to generic tools --HG-- rename : src/HOL/Library/Adhoc_Overloading.thy => src/Tools/Adhoc_Overloading.thy rename : src/HOL/Library/adhoc_overloading.ML => src/Tools/adhoc_overloading.ML
|
#
f3971002 |
|
27-May-2010 |
boehmes <none@none> |
added function update examples and set examples
|
#
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
|
#
1ac49a6a |
|
26-May-2010 |
boehmes <none@none> |
hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns
|
#
3c1b8ad5 |
|
12-May-2010 |
huffman <none@none> |
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
|
#
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
|