diff options
author | Tim King <taking@cs.nyu.edu> | 2012-02-28 21:26:35 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-02-28 21:26:35 +0000 |
commit | eefe0b63e564320eb135eb66d6c02c9dc6e9e8de (patch) | |
tree | 14d9643427fadab3e1c064d5528fa02e46f6bef7 /src/theory/arith/delta_rational.h | |
parent | 9450e5841a08db3a9529c25e03fc5cea16a8f1f5 (diff) |
This commit merges in branches/arithmetic/internalbb up to revision 2831. This is a significant refactoring of code.
- r2820
-- Refactors Simplex so that it does significantly fewer functions.
-- Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model.
-- Some of the code for propagation has moved to TheoryArith.
-r2826
-- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound().
- r2827
-- Adds isZero() to Rational. Adds cmp to DeltaRational.
- r2831
-- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp.
-- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.
Diffstat (limited to 'src/theory/arith/delta_rational.h')
-rw-r--r-- | src/theory/arith/delta_rational.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 682d13720..c004a681f 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -63,6 +63,15 @@ public: } } + int cmp(const DeltaRational& other) const{ + int cmp = c.cmp(other.c); + if(cmp == 0){ + return k.cmp(other.k); + }else{ + return cmp; + } + } + DeltaRational operator+(const DeltaRational& other) const{ CVC4::Rational tmpC = c+other.c; CVC4::Rational tmpK = k+other.k; |