projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 07e1a16) | patch
Significant revision to theory/arith. The new draft has a lot of small bug fixes...
authorTim King <taking@cs.nyu.edu>
Wed, 19 May 2010 21:20:54 +0000 (21:20 +0000)
committerTim King <taking@cs.nyu.edu>
Wed, 19 May 2010 21:20:54 +0000 (21:20 +0000)
commitff70395fd3dcde9f68eda1c6a8bd70e6491f7458
treed0cf52a5e6cb98a0aa6c15ca4c4fe4d258cb626ftree
parent07e1a1668a27e90563f23bcf5abb5cb7fe30da86commit | diff
Significant revision to theory/arith.  The new draft has a lot of small bug fixes and organizational changes.  The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.
22 files changed:
src/expr/attribute.h diff | blob | history
src/expr/node.h diff | blob | history
src/theory/arith/Makefile.am diff | blob | history
src/theory/arith/arith_constants.h diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/arith_utilities.h diff | blob | history
src/theory/arith/basic.h diff | blob | history
src/theory/arith/delta_rational.cpp [new file with mode: 0644] blob
src/theory/arith/delta_rational.h diff | blob | history
src/theory/arith/normal.h diff | blob | history
src/theory/arith/normal_form_notes.txt diff | blob | history
src/theory/arith/partial_model.cpp [new file with mode: 0644] blob
src/theory/arith/partial_model.h diff | blob | history
src/theory/arith/tableau.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/theory_engine.h diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/ineq_basic.smt [new file with mode: 0644] blob
test/regress/regress0/ineq_slack.smt [new file with mode: 0644] blob
test/unit/expr/node_black.h diff | blob | history