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

author	Tim King <taking@cs.nyu.edu>
	Wed, 13 Jun 2012 20:37:43 +0000 (20:37 +0000)
committer	Tim King <taking@cs.nyu.edu>
	Wed, 13 Jun 2012 20:37:43 +0000 (20:37 +0000)
commit	d0b33af0cf910ca7adb0357dad13e7e88baedebc
tree	fc9c1fae8b7c4e9a26656e81314800852996e2f6	tree
parent	6acb8e96739df11859d3bca8a9e67bdaff5600c6	commit \| diff

- Added a loop to internally assert constraints that are marked as true.
- Changes how CongruenceManager reports conflicts.
- ConstraintDatabase can now detect and raise conflicts when doing unate propagation.

src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
test/regress/regress0/uflia/Makefile.am		diff \| blob \| history
test/regress/regress0/uflia/error1.smt	[new file with mode: 0644]	blob
test/regress/regress0/uflra/Makefile.am		diff \| blob \| history
test/regress/regress0/uflra/error1.smt	[new file with mode: 0644]	blob

RSS Atom