Improved error reporting for improperly using non-linear division in linear arithmetic.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 689f231e6cfa9317cdd8f05eaaa65978b25f3910..a367b8599fdf6ec1b689ea9546b881e1c38943c5 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -68,6 +68,11 @@ RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){
 RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){
   Assert(t.getKind()== kind::UMINUS);
 
+  if(t[0].getKind() == kind::CONST_RATIONAL){
+    Rational neg = -(t[0].getConst<Rational>());
+    return RewriteResponse(REWRITE_DONE, mkRationalNode(neg));
+  }
+
   Node noUminus = makeUnaryMinusNode(t[0]);
   if(pre)
     return RewriteResponse(REWRITE_DONE, noUminus);
@@ -87,9 +92,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::UMINUS:
       return rewriteUMinus(t, true);
     case kind::DIVISION:
-      return rewriteDiv(t,true);
     case kind::DIVISION_TOTAL:
-      return rewriteDivTotal(t,true);
+      return rewriteDiv(t,true);
     case kind::PLUS:
       return preRewritePlus(t);
     case kind::MULT:
@@ -116,9 +120,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     case kind::UMINUS:
       return rewriteUMinus(t, false);
     case kind::DIVISION:
-      return rewriteDiv(t, false);
     case kind::DIVISION_TOTAL:
-      return rewriteDivTotal(t, false);
+      return rewriteDiv(t, false);
     case kind::PLUS:
       return postRewritePlus(t);
     case kind::MULT:
@@ -260,51 +263,9 @@ Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
 
   return diff;
 }
-RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre){
-  Assert(t.getKind()== kind::DIVISION);
-
-  Node left = t[0];
-  Node right = t[1];
-
-  if(right.getKind() == kind::CONST_RATIONAL &&
-     left.getKind() != kind::CONST_RATIONAL){
-
-    const Rational& den = right.getConst<Rational>();
-
-    Assert(!den.isZero());
-
-    Rational div = den.inverse();
-    Node result =  mkRationalNode(div);
-    Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result);
-    if(pre){
-      return RewriteResponse(REWRITE_DONE, mult);
-    }else{
-      return RewriteResponse(REWRITE_AGAIN, mult);
-    }
-  }
-
-  if(pre){
-    if(right.getKind() != kind::CONST_RATIONAL ||
-       left.getKind() != kind::CONST_RATIONAL){
-      return RewriteResponse(REWRITE_DONE, t);
-    }
-  }
-
-  Assert(right.getKind() == kind::CONST_RATIONAL);
-  Assert(left.getKind() == kind::CONST_RATIONAL);
-
-  const Rational& den = right.getConst<Rational>();
-
-  Assert(!den.isZero());
-
-  const Rational& num = left.getConst<Rational>();
-  Rational div = num / den;
-  Node result =  mkRationalNode(div);
-  return RewriteResponse(REWRITE_DONE, result);
-}
 
-RewriteResponse ArithRewriter::rewriteDivTotal(TNode t, bool pre){
-  Assert(t.getKind() == kind::DIVISION_TOTAL);
+RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre){
+  Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind()== kind::DIVISION);
 
 
   Node left = t[0];
@@ -313,7 +274,12 @@ RewriteResponse ArithRewriter::rewriteDivTotal(TNode t, bool pre){
     const Rational& den = right.getConst<Rational>();
 
     if(den.isZero()){
-      return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+      if(t.getKind() == kind::DIVISION_TOTAL){
+        return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+      }else{
+        // This is unsupported, but this is not a good place to complain
+        return RewriteResponse(REWRITE_DONE, t);
+      }
     }
     Assert(den != Rational(0));
 

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 10e2555358598b187ae034a02f6cc4b065ca3fdb..9b3f37d31c0e49d302279aff0088394ed1ccdac7 100644 (file)
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -50,7 +50,6 @@ private:
   static RewriteResponse rewriteMinus(TNode t, bool pre);
   static RewriteResponse rewriteUMinus(TNode t, bool pre);
   static RewriteResponse rewriteDiv(TNode t, bool pre);
-  static RewriteResponse rewriteDivTotal(TNode t, bool pre);
   static RewriteResponse rewriteIntsDivModTotal(TNode t, bool pre);
 
   static RewriteResponse preRewritePlus(TNode t);

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index c863bf3c5b27c4bf8c43dcb3c476e876266d1e65..fd6f04ca88e75d4837226030f43279cdb82983a2 100644 (file)
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -27,7 +27,7 @@ namespace arith {
 
 bool Variable::isDivMember(Node n){
   switch(n.getKind()){
-    //case kind::DIVISION:
+  case kind::DIVISION:
     //case kind::INTS_DIVISION:
     //case kind::INTS_MODULUS:
   case kind::DIVISION_TOTAL:

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e23262137043d9af32d515eeefafe0e416295186..1d89c02d4f4230ba5904246b83e895ed10992043 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1134,7 +1134,9 @@ void TheoryArith::preRegisterTerm(TNode n) {
 ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
   //TODO : The VarList trick is good enough?
   Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS);
-  Assert(!Variable::isDivMember(x) || !getLogicInfo().isLinear());
+  if(getLogicInfo().isLinear() && Variable::isDivMember(x)){
+    throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+  }
   Assert(!d_arithvarNodeMap.hasArithVar(x));
   Assert(x.getType().isReal());// real or integer
 

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 12aa0eecde47350a00d7f7fea10f6f0d3ff8ccc3..38e7e6f4ee492e6c7aded8c221e183144b283654 100644 (file)
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -36,6 +36,7 @@ TESTS =       \
        div.06.smt2 \
        div.07.smt2 \
        div.08.smt2 \
+       div.09.smt2 \
        mult.01.smt2 \
        mult.02.smt2 \
        bug443.delta01.smt

diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2
new file mode 100644 (file)
index 0000000..2f1bca6
--- /dev/null
+++ b/test/regress/regress0/arith/div.09.smt2
@@ -0,0 +1,11 @@
+; EXPECT: (error "Non-linear term was asserted to arithmetic in a linear logic.")
+; EXIT: 1
+(set-logic QF_LRA)
+(set-info :status unknown)
+(declare-fun n () Real)
+
+; This example is test that LRA rejects multiplication terms
+
+(assert (= (/ n n) 1))
+
+(check-sat)