projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2482b19) | patch
Merging the arithmetic theory draft (lra-init) back into the main trunk. This should...
authorTim King <taking@cs.nyu.edu>
Wed, 28 Apr 2010 20:14:17 +0000 (20:14 +0000)
committerTim King <taking@cs.nyu.edu>
Wed, 28 Apr 2010 20:14:17 +0000 (20:14 +0000)
commitc59fe5b21c218d3d6048cc5c34a7e27b3643ae78
treebfd3c1d1eb975989b0ef4afa4e88da4eae84ba62tree
parent2482b19ea90183d5040390b87877b7593021032ccommit | diff
Merging the arithmetic theory draft (lra-init) back into the main trunk.  This should not affect other parts of the system. This code is untested, and is volatile.  It is going to be improved in the future so don't pick on it too much.  I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.
15 files changed:
src/theory/arith/Makefile.am diff | blob | history
src/theory/arith/arith_constants.h [new file with mode: 0644] blob
src/theory/arith/arith_rewriter.cpp [new file with mode: 0644] blob
src/theory/arith/arith_rewriter.h [new file with mode: 0644] blob
src/theory/arith/arith_utilities.h [new file with mode: 0644] blob
src/theory/arith/basic.h [new file with mode: 0644] blob
src/theory/arith/delta_rational.h [new file with mode: 0644] blob
src/theory/arith/normal.h [new file with mode: 0644] blob
src/theory/arith/normal_form_notes.txt [new file with mode: 0644] blob
src/theory/arith/partial_model.h [new file with mode: 0644] blob
src/theory/arith/slack.h [new file with mode: 0644] blob
src/theory/arith/tableau.h [new file with mode: 0644] blob
src/theory/arith/theory_arith.cpp [new file with mode: 0644] blob
src/theory/arith/theory_arith.h diff | blob | history
src/util/rational.h diff | blob | history