This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and DIVISION. Improves support for non-linear monomials in getEqualityStatus(). Fixes bug 405.

1 files changed, 165 insertions, 11 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e159c0e42..e552ae5a0 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -58,6 +58,7 @@ const uint32_t RESET_START = 2;
 
 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
+  d_nlIncomplete(u, false),
   d_qflraStatus(Result::SAT_UNKNOWN),
   d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
@@ -653,6 +654,7 @@ Node TheoryArith::ppRewrite(TNode atom) {
                                << a << endl;
   }
 
+
   if (a.getKind() == kind::EQUAL  && options::arithRewriteEq()) {
     Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1];
     Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1];
@@ -792,6 +794,12 @@ void TheoryArith::setupVariable(const Variable& x){
   setupInitialValue(varN);
 
   markSetup(n);
+
+
+  if(x.isDivLike()){
+    interpretDivLike(x);
+  }
+
 }
 
 void TheoryArith::setupVariableList(const VarList& vl){
@@ -813,6 +821,7 @@ void TheoryArith::setupVariableList(const VarList& vl){
     // vl is the product of at least 2 variables
     // vl : (* v1 v2 ...)
     d_out->setIncomplete();
+    d_nlIncomplete = true;
 
     ++(d_statistics.d_statUserVariables);
     ArithVar av = requestArithVar(vlNode, false);
@@ -826,6 +835,68 @@ void TheoryArith::setupVariableList(const VarList& vl){
    * See the comment in setupPolynomail for more.
    */
 }
+void TheoryArith::interpretDivLike(const Variable& v){
+  Assert(v.isDivLike());
+  Node vnode = v.getNode();
+  Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion
+    Polynomial m = Polynomial::parsePolynomial(vnode[0]);
+    Polynomial n = Polynomial::parsePolynomial(vnode[1]);
+	    
+    NodeManager* currNM = NodeManager::currentNM();
+	      
+    Node nNeq0 = currNM->mkNode(EQUAL, n.getNode(), mkRationalNode(0)).notNode();
+    if(vnode.getKind() == INTS_DIVISION || vnode.getKind() == INTS_MODULUS){
+      // (for all ((m Int) (n Int))
+      //   (=> (distinct n 0)
+      //       (let ((q (div m n)) (r (mod m n)))
+      //         (and (= m (+ (* n q) r))
+      //              (<= 0 r (- (abs n) 1))))))
+
+      Node q = (vnode.getKind() == INTS_DIVISION) ? vnode : currNM->mkNode(INTS_DIVISION, m.getNode(), n.getNode());
+      Node r = (vnode.getKind() == INTS_MODULUS) ? vnode : currNM->mkNode(INTS_MODULUS, m.getNode(), n.getNode());
+
+
+      Polynomial rp = Polynomial::parsePolynomial(r);
+      Polynomial qp = Polynomial::parsePolynomial(q);
+
+      Node abs_n;
+      Node zero = mkRationalNode(0);
+
+      if(n.isConstant()){
+	abs_n = n.getHead().getConstant().abs().getNode();
+      }else{
+	abs_n = mkIntSkolem("abs_$$");
+	Polynomial abs_np = Polynomial::parsePolynomial(abs_n);
+	Node absCnd = currNM->mkNode(ITE, 
+				currNM->mkNode(LEQ, n.getNode(), zero),
+				Comparison::mkComparison(EQUAL, abs_np, -rp).getNode(),
+				Comparison::mkComparison(EQUAL, abs_np, rp).getNode());
+	
+	d_out->lemma(absCnd);
+      }
+
+      Node eq = Comparison::mkComparison(EQUAL, m, n * qp + rp).getNode();
+      Node leq0 = currNM->mkNode(LEQ,  zero, r);
+      Node leq1 = currNM->mkNode(LT, r, abs_n);
+
+      Node andE = currNM->mkNode(AND, eq, leq0, leq1);
+      Node nNeq0ImpliesandE = currNM->mkNode(IMPLIES, nNeq0, andE);
+
+      d_out->lemma(nNeq0ImpliesandE);
+    }else{
+      // DIVISION (/ q r)
+      // (=> (distinct 0 n) (= m (* d n)))
+	      
+      Assert(vnode.getKind() == DIVISION);
+      Node d = mkRealSkolem("division_$$");
+	      
+      Node eq = Comparison::mkComparison(EQUAL, m, n * Polynomial::parsePolynomial(d)).getNode();
+      Node nNeq0ImpliesEq = currNM->mkNode(IMPLIES, nNeq0, eq);
+	      
+      d_out->lemma(nNeq0ImpliesEq);
+    }
+  
+}
 
 void TheoryArith::setupPolynomial(const Polynomial& poly) {
   Assert(!poly.containsConstant());
@@ -923,7 +994,9 @@ void TheoryArith::preRegisterTerm(TNode n) {
 
 
 ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
-  Assert(isLeaf(x) || x.getKind() == PLUS);
+  //TODO : The VarList trick is good enough?
+  Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS);
+  Assert(!Variable::isDivMember(x) || !getLogicInfo().isLinear());
   Assert(!d_arithvarNodeMap.hasArithVar(x));
   Assert(x.getType().isReal());// real or integer
 
@@ -966,20 +1039,23 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs,
 
     Debug("rewriter") << "should be var: " << n << endl;
 
-    Assert(isLeaf(n));
+    // TODO: This VarList::isMember(n) can be stronger
+    Assert(isLeaf(n) || VarList::isMember(n));
     Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n));
 
     Assert(d_arithvarNodeMap.hasArithVar(n));
     ArithVar av;
-    if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) {
-      // The only way not to get it through pre-register is if it's a foreign term
-      ++(d_statistics.d_statUserVariables);
-      av = requestArithVar(n,false);
-      setupInitialValue(av);
-    } else {
-      // Otherwise, we already have it's variable
-      av = d_arithvarNodeMap.asArithVar(n);
-    }
+    // The first if is likely dead is likely dead code:
+    // if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) {
+    //   // The only way not to get it through pre-register is if it's a foreign term
+    //   ++(d_statistics.d_statUserVariables);
+    //   av = requestArithVar(n,false);
+    //   setupInitialValue(av);
+    // } else {
+    //   // Otherwise, we already have it's variable
+    //   av = d_arithvarNodeMap.asArithVar(n);
+    // }
+    av = d_arithvarNodeMap.asArithVar(n);
 
     coeffs.push_back(constant.getValue());
     variables.push_back(av);
@@ -1870,6 +1946,7 @@ bool TheoryArith::getDeltaAtomValue(TNode n) {
 
 DeltaRational TheoryArith::getDeltaValue(TNode n) {
   Assert(d_qflraStatus != Result::SAT_UNKNOWN);
+  Assert(!d_nlIncomplete);
   Debug("arith::value") << n << std::endl;
 
   switch(n.getKind()) {
@@ -1925,8 +2002,76 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
   }
 }
 
+DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) {
+  Assert(d_qflraStatus != Result::SAT_UNKNOWN);
+  Assert(d_nlIncomplete);
+
+  Debug("arith::value") << n << std::endl;
+
+  switch(n.getKind()) {
+
+  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 && !failed;
+        ++i) {
+      value = value + getDeltaValueWithNonlinear(*i, failed);
+    }
+    return value;
+  }
+
+  case kind::MULT: { // 2+ args
+    DeltaRational value(1);
+    if (n[0].getKind() == kind::CONST_RATIONAL) {
+      return getDeltaValueWithNonlinear(n[1], failed) * n[0].getConst<Rational>();
+    }else{
+      failed = true;
+      return value;
+    }
+  }
+
+  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 getDeltaValueWithNonlinear(n[0], failed) / n[0].getConst<Rational>();
+    }else{
+      failed = true;
+      return DeltaRational();
+    }
+    //fall through
+  case kind::INTS_DIVISION:
+  case kind::INTS_MODULUS:
+    //a bit strict
+    failed = true;
+    return DeltaRational();
+
+  default:
+    {
+      if(isSetup(n)){
+        ArithVar var = d_arithvarNodeMap.asArithVar(n);
+        return d_partialModel.getAssignment(var);
+      }else{
+        Unreachable();
+      }
+    }
+  }
+}
+
 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(d_qflraStatus ==  Result::SAT);
+  Assert(!d_nlIncomplete);
 
   Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
 
@@ -2110,6 +2255,15 @@ void TheoryArith::presolve(){
 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
   if(d_qflraStatus == Result::SAT_UNKNOWN){
     return EQUALITY_UNKNOWN;
+  }else if(d_nlIncomplete){
+    bool failed = false;
+    DeltaRational amod = getDeltaValueWithNonlinear(a, failed);
+    DeltaRational bmod = getDeltaValueWithNonlinear(b, failed);
+    if(failed){
+      return EQUALITY_UNKNOWN;
+    }else{
+      return amod == bmod ? EQUALITY_TRUE_IN_MODEL : EQUALITY_FALSE_IN_MODEL;
+    }
   }else if (getDeltaValue(a) == getDeltaValue(b)) {
     return EQUALITY_TRUE_IN_MODEL;
   } else {