projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d58d78b) | patch
inequality reasoning works on small examples added to regressions (not incremental...
authorLiana Hadarean <lianahady@gmail.com>
Wed, 20 Mar 2013 01:54:22 +0000 (21:54 -0400)
committerLiana Hadarean <lianahady@gmail.com>
Wed, 20 Mar 2013 01:54:22 +0000 (21:54 -0400)
commit4cd63abf2ab901ad8d1b1c2cc2e84707736b5659
treeb45789d51329bbfdf0043f9fcb577ea0fb2c38bctree
parentd58d78b3ac3e5abfaa4e01d87bb351c0268239dfcommit | diff
inequality reasoning works on small examples added to regressions (not incremental); currently disabled though
src/theory/bv/bv_inequality_graph.cpp diff | blob | history
src/theory/bv/bv_inequality_graph.h diff | blob | history
src/theory/bv/bv_subtheory_inequality.cpp diff | blob | history
src/theory/bv/bv_subtheory_inequality.h diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history
test/regress/regress0/bv/inequality00.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/inequality01.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/inequality02.smt2 [new file with mode: 0644] blob