This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and DIVISION...

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 6ac2338f3ab478fdf38e8b5bf6192292ec0ea4c3..427ebbbd396dba32f74206bdc2c51994fd6cab29 100644 (file)
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -45,7 +45,13 @@ inline Node mkBoolNode(bool b){
   return NodeManager::currentNM()->mkConst<bool>(b);
 }
 
+inline Node mkIntSkolem(const std::string& name){
+  return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType());
+}
 
+inline Node mkRealSkolem(const std::string& name){
+  return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType());
+}
 
 /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
 inline bool isRelationOperator(Kind k){

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index c90be63b980e6ba91225858c4a60a865c19adb4c..39618d49854d1fb667ca46cc996f39be1abc7a5a 100644 (file)
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -27,6 +27,17 @@ namespace CVC4 {
 namespace theory{
 namespace arith {
 
+bool Variable::isDivMember(Node n){
+  switch(n.getKind()){
+  case kind::DIVISION:
+  case kind::INTS_DIVISION:
+  case kind::INTS_MODULUS:
+    return Polynomial::isMember(n[0]) && Polynomial::isMember(n[1]);
+  default:
+    return false;
+  }
+}
+
 bool VarList::isSorted(iterator start, iterator end) {
   return __gnu_cxx::is_sorted(start, end);
 }

diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 33fc42cea484f419ca71c48cc81414f77023e249..3184deec582345542efa73eebe3ef9c346920871 100644 (file)
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -211,7 +211,6 @@ namespace arith {
  *      | (+ [monomial]) -> [monomial]
  */
 
-
 /**
  * A NodeWrapper is a class that is a thinly veiled container of a Node object.
  */
@@ -232,9 +231,17 @@ public:
 
   // TODO: check if it's a theory leaf also
   static bool isMember(Node n) {
-    if (n.getKind() == kind::CONST_RATIONAL) return false;
-    if (isRelationOperator(n.getKind())) return false;
-    return Theory::isLeafOf(n, theory::THEORY_ARITH);
+    Kind k = n.getKind();
+    if (k == kind::CONST_RATIONAL) return false;
+    if (isRelationOperator(k)) return false;
+    if (Theory::isLeafOf(n, theory::THEORY_ARITH)) return true;
+    if (k == kind::INTS_DIVISION || k == kind::INTS_MODULUS || k == kind::DIVISION) return isDivMember(n);
+    return false;
+  }
+
+  static bool isDivMember(Node n);
+  bool isDivLike() const{
+    return isDivMember(getNode());
   }
 
   bool isNormalForm() { return isMember(getNode()); }

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e159c0e42ed552c48c40376e48cd60906589586c..e552ae5a06cee79d8f39b6d95634532cd8190a36 100644 (file)
--- 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 {

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index c98c759f7a5b215ccb109b8823b287be2273563b..1c2c942fd2082c6e4f4bcd42a2226f31b9fd2e9f 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -64,6 +64,8 @@ class InstantiatorTheoryArith;
 class TheoryArith : public Theory {
   friend class InstantiatorTheoryArith;
 private:
+  context::CDO<bool> d_nlIncomplete;
+
   enum Result::Sat d_qflraStatus;
   // check()
   //   !done() -> d_qflraStatus = Unknown
@@ -105,6 +107,8 @@ private:
     d_setupNodes.insert(n);
   }
 
+  void interpretDivLike(const Variable& x);
+
   void setupVariable(const Variable& x);
   void setupVariableList(const VarList& vl);
   void setupPolynomial(const Polynomial& poly);
@@ -310,6 +314,9 @@ private:
   /** Internal model value for the node */
   DeltaRational getDeltaValue(TNode n);
 
+  /** TODO : get rid of this. */ 
+  DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed);
+
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   virtual ~TheoryArith();