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

4 files changed, 19 insertions, 52 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 689f231e6..a367b8599 100644
--- 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 10e255535..9b3f37d31 100644
--- 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 c863bf3c5..fd6f04ca8 100644
--- 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 e23262137..1d89c02d4 100644
--- 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