| #
21fef7de |
|
07-Jun-2019 |
blanchet <none@none> |
handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
7110473f |
|
30-Oct-2018 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
add reconstruction by veriT in method smt
|
| #
ea4853ba |
|
28-Jan-2018 |
wenzelm <none@none> |
clarified take/drop/chop prefix/suffix;
|
| #
038835b6 |
|
11-Jan-2018 |
wenzelm <none@none> |
uniform use of Standard ML op-infix -- eliminated warnings;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
f9beda92 |
|
29-Aug-2017 |
blanchet <none@none> |
towards support for HO SMT-LIB
|
| #
0ce7501d |
|
04-Nov-2016 |
blanchet <none@none> |
disable CVC4 statistics, and hence crashes upon user interruptions
|
| #
af6f1e98 |
|
19-May-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
better handling of veriT's 'unknown' status
|
| #
7d38a922 |
|
10-Nov-2015 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
fixing premises in veriT proof reconstruction
|
| #
7e139616 |
|
05-Nov-2015 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
updating options to verit
|
| #
2c86cbbc |
|
08-Apr-2015 |
blanchet <none@none> |
updated SMT module and Sledgehammer to fully open source Z3
|
| #
28085c4a |
|
23-Nov-2014 |
blanchet <none@none> |
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
|
| #
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
|
| #
d31246b6 |
|
30-Sep-2014 |
blanchet <none@none> |
give more facts to veriT -- it seems to be able to cope with them
|
| #
f678ba5a |
|
30-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
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
|