diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-12 23:50:29 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-12 23:50:29 +0000 |
commit | 79b80442e5df070fe838de3fe4c09b235f6bddf5 (patch) | |
tree | 7aed459a84a1ab94b7a6e90f2d308cd24488430b /src | |
parent | 8c325a4bf6888e33fb8fdc1e071a8aab4aa20b6f (diff) |
Improved error reporting for improperly using non-linear division in linear arithmetic.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 64 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 1 | ||||
-rw-r--r-- | src/theory/arith/normal_form.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
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 |