projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2f11cfd) | patch
CBQI BV: Add ULT/SLT inverse handling. (#1268)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 24 Oct 2017 05:46:50 +0000 (22:46 -0700)
committerGitHub <noreply@github.com>
Tue, 24 Oct 2017 05:46:50 +0000 (22:46 -0700)
commit00e75cb0c6aedab34740b7feadb512ea3c0c7f3d
treee046bca9e8f04be0028811682f4c4b0f6dfa475btree
parent2f11cfd563ef96402042e9a3b0086712de660ae6commit | diff
CBQI BV: Add ULT/SLT inverse handling. (#1268)

This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit.
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
src/theory/quantifiers/bv_inverter.h diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 [new file with mode: 0644] blob