* improving arithmetic getEqualityStatus

* some sharing improvements based on model

4 files changed, 133 insertions, 1 deletions

diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index c004a681f..a46dde1cf 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -89,6 +89,18 @@ public:
     return *(this) + (a * negOne);
   }
 
+  DeltaRational operator/(const Rational& a) const{
+    CVC4::Rational tmpC = c/a;
+    CVC4::Rational tmpK = k/a;
+    return DeltaRational(tmpC, tmpK);
+  }
+
+  DeltaRational operator/(const Integer& a) const{
+    CVC4::Rational tmpC = c/a;
+    CVC4::Rational tmpK = k/a;
+    return DeltaRational(tmpC, tmpK);
+  }
+
   bool operator==(const DeltaRational& other) const{
     return (k == other.k) && (c == other.c);
   }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 3760e233d..590a9f1cf 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -334,6 +334,17 @@ Node TheoryArith::AssertEquality(ArithVar x_i, DeltaRational& c_i, TNode origina
 
 void TheoryArith::addSharedTerm(TNode n){
   d_differenceManager.addSharedTerm(n);
+  if(!n.isConst() && !isSetup(n)){
+    Polynomial poly = Polynomial::parsePolynomial(n);
+    Polynomial::iterator it = poly.begin();
+    Polynomial::iterator it_end = poly.end();
+    for (; it != it_end; ++ it) {
+      Monomial m = *it;
+      if (!m.isConstant() && !isSetup(m.getVarList().getNode())) {
+        setupVariableList(m.getVarList());
+      }
+    }
+  }
 }
 
 Node TheoryArith::ppRewrite(TNode atom) {
@@ -1170,6 +1181,95 @@ void TheoryArith::propagate(Effort e) {
   }
 }
 
+bool TheoryArith::getDeltaAtomValue(TNode n) {
+
+  switch (n.getKind()) {
+    case kind::EQUAL: // 2 args
+      return getDeltaValue(n[0]) == getDeltaValue(n[1]);
+    case kind::LT: // 2 args
+      return getDeltaValue(n[0]) < getDeltaValue(n[1]);
+    case kind::LEQ: // 2 args
+      return getDeltaValue(n[0]) <= getDeltaValue(n[1]);
+    case kind::GT: // 2 args
+      return getDeltaValue(n[0]) > getDeltaValue(n[1]);
+    case kind::GEQ: // 2 args
+      return getDeltaValue(n[0]) >= getDeltaValue(n[1]);
+    default:
+      Unreachable();
+  }
+}
+
+
+DeltaRational TheoryArith::getDeltaValue(TNode n) {
+
+  Debug("arith::value") << n << std::endl;
+
+  switch(n.getKind()) {
+
+  case kind::CONST_INTEGER:
+    return Rational(n.getConst<Integer>());
+
+  case kind::CONST_RATIONAL:
+    return n.getConst<Rational>();
+
+  case kind::PLUS: { // 2+ args
+    DeltaRational value(0);
+    for(TNode::iterator i = n.begin(),
+            iend = n.end();
+          i != iend;
+          ++i) {
+      value = value + getDeltaValue(*i);
+    }
+    return value;
+  }
+
+  case kind::MULT: { // 2+ args
+    Assert(n.getNumChildren() == 2 && n[0].isConst());
+    DeltaRational value(1);
+    if (n[0].getKind() == kind::CONST_INTEGER) {
+      return getDeltaValue(n[1]) * n[0].getConst<Integer>();
+    }
+    if (n[0].getKind() == kind::CONST_RATIONAL) {
+      return getDeltaValue(n[1]) * n[0].getConst<Rational>();
+    }
+    Unreachable();
+  }
+
+  case kind::MINUS: // 2 args
+    // should have been rewritten
+    Unreachable();
+
+  case kind::UMINUS: // 1 arg
+    // should have been rewritten
+    Unreachable();
+
+  case kind::DIVISION: // 2 args
+    Assert(n[1].isConst());
+    if (n[1].getKind() == kind::CONST_RATIONAL) {
+      return getDeltaValue(n[0]) / n[0].getConst<Rational>();
+    }
+    if (n[1].getKind() == kind::CONST_INTEGER) {
+      return getDeltaValue(n[0]) / n[0].getConst<Integer>();
+    }
+    Unreachable();
+
+
+  default:
+  {
+    ArithVar var = d_arithvarNodeMap.asArithVar(n);
+
+    if(d_removedRows.find(var) != d_removedRows.end()){
+      Node eq = d_removedRows.find(var)->second;
+      Assert(n == eq[0]);
+      Node rhs = eq[1];
+      return getDeltaValue(rhs);
+    }
+
+    return d_partialModel.getAssignment(var);
+  }
+  }
+}
+
 Node TheoryArith::getValue(TNode n) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
@@ -1389,7 +1489,7 @@ void TheoryArith::presolve(){
 }
 
 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
-  if (getValue(a) == getValue(b)) {
+  if (getDeltaValue(a) == getDeltaValue(b)) {
     return EQUALITY_TRUE_IN_MODEL;
   } else {
     return EQUALITY_FALSE_IN_MODEL;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 929ef1173..ec2df3e17 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -249,6 +249,13 @@ private:
 
   /** This implements the Simplex decision procedure. */
   SimplexDecisionProcedure d_simplex;
+
+  /** Internal model value for the atom */
+  bool getDeltaAtomValue(TNode n);
+
+  /** Internal model value for the node */
+  DeltaRational getDeltaValue(TNode n);
+
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
   virtual ~TheoryArith();
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f0694462d..a3e347b90 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -488,6 +488,19 @@ void TheoryUF::computeCareGraph() {
           TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x);
           TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y);
 
+          EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
+          switch (eqStatusDomain) {
+          case EQUALITY_FALSE_AND_PROPAGATED:
+          case EQUALITY_FALSE:
+          case EQUALITY_FALSE_IN_MODEL:
+            somePairIsDisequal = true;
+            continue;
+            break;
+          default:
+            break;
+            // nothing
+          }
+
           // Otherwise, we need to figure it out
           Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
           currentPairs.push_back(make_pair(x_shared, y_shared));