projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 60f6d09) | patch
Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Enable...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 21 Aug 2015 08:07:12 +0000 (10:07 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 21 Aug 2015 08:07:19 +0000 (10:07 +0200)
commitfb746fdd4e60e7d166b0fa1e5788bea925d22ee7
tree1a8b8dc8c2b4f57352ab10365e2b2765c06285c9tree
parent60f6d09d7ad9e37f5a23e6a2b0e47a7b0e47df81commit | diff
Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi.  Enable redundant ITE branch elimination in quantifiers rewriter.
12 files changed:
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quant_util.cpp 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/theory_engine.h diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
test/regress/regress0/quantifiers/006-cbqi-ite.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/Makefile.am diff | blob | history