projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f1dfab1) | patch
Implement virtual term substitution for non-nested quantifiers. Fix soundness bug...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 30 Jul 2015 15:18:10 +0000 (17:18 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 30 Jul 2015 15:18:24 +0000 (17:18 +0200)
commitf2da7296ff76920528c0e9edc35f96a715b85078
tree21c7b56ab3f0216f1444b454d2671a5e60c9a0d4tree
parentf1dfab159ff9b29bfe86e976ae9953d77eefa308commit | diff
Implement virtual term substitution for non-nested quantifiers.  Fix soundness bug in strings related to explaining length terms.
14 files changed:
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.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.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/delta-simp.smt2 [new file with mode: 0644] blob