diff options
author | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
commit | e9198d9b99c6037165362870436b45826674303f (patch) | |
tree | b5e8d01a53d38d353dae7c16351ff9206e1f96c6 /src/theory/arith/delta_rational.h | |
parent | 8b202bab8442c927e9ac18a35c71a82444acf63b (diff) |
Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
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 c8a5e39a7..fdc3bee3b 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -54,6 +54,15 @@ public: return c; } + int sgn() const { + int x = getNoninfinitesimalPart().sgn(); + if(x == 0){ + return getInfinitesimalPart().sgn(); + }else{ + return x; + } + } + DeltaRational operator+(const DeltaRational& other) const{ CVC4::Rational tmpC = c+other.c; CVC4::Rational tmpK = k+other.k; |