projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f70674c) | patch
Add infrastructure for tracking instantiation lemmas (for proofs, and minimization...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 19 Jul 2016 15:32:37 +0000 (10:32 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 19 Jul 2016 15:32:37 +0000 (10:32 -0500)
commit06d91e9121ecdadfc96d6175792992395833329f
tree15a969c7c044279c3677ded69465add67ea96fadtree
parentf70674c2f0c6c1c55e3d7c5fed916fc1e7721ffecommit | diff
Add infrastructure for tracking instantiation lemmas (for proofs, and minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
src/options/quantifiers_options diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 [new file with mode: 0644] blob