projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9bc8fe0) | patch
CBQI BV: Add inverse for more operators. (#1213)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 10 Oct 2017 00:06:30 +0000 (17:06 -0700)
committerGitHub <noreply@github.com>
Tue, 10 Oct 2017 00:06:30 +0000 (17:06 -0700)
commit3b0ce95e7b7d1cbc351df9a7d2acbf3b6e13f9e7
treef442287bef2e1fcfa070cd03c04650191b9c0d81tree
parent9bc8fe0ea33a280f2a24cca0b2c6f08b962a8f8dcommit | diff
CBQI BV: Add inverse for more operators. (#1213)

This implements side conditions and the instantiation via word-level inversion for operators BITVECTOR_AND, BITVECTOR_OR, BITVECTOR_UREM (Index=1), BITVECTOR_LSHR (index=0).
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 diff | blob | history