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.

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;