git.libre-soc.org Git - cvc5.git/commit

author	Aina Niemetz <aina.niemetz@gmail.com>
	Thu, 21 Dec 2017 02:27:39 +0000 (18:27 -0800)
committer	GitHub <noreply@github.com>
	Thu, 21 Dec 2017 02:27:39 +0000 (18:27 -0800)
commit	f9149d3b3e785950a846fb195bf9fa9cb1a2d94a
tree	c69c90377a6c24abbc9c608a767507740abfd3b6	tree
parent	13cc0e94ac8892fa1cefa53ff1c884d154894b58	commit \| diff

Add explicit disequality handling when generating side condition for CBQI BV. (#1447)

This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.

49 files changed:

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
src/theory/quantifiers/ceg_t_instantiator.h		diff \| blob \| history
test/regress/regress0/quantifiers/Makefile.am		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-disequality3.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-inequality2.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-simp.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.h		diff \| blob \| history

RSS Atom