From 79b80442e5df070fe838de3fe4c09b235f6bddf5 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 12 Nov 2012 23:50:29 +0000 Subject: [PATCH] Improved error reporting for improperly using non-linear division in linear arithmetic. --- src/theory/arith/arith_rewriter.cpp | 64 ++++++------------------- src/theory/arith/arith_rewriter.h | 1 - src/theory/arith/normal_form.cpp | 2 +- src/theory/arith/theory_arith.cpp | 4 +- test/regress/regress0/arith/Makefile.am | 1 + test/regress/regress0/arith/div.09.smt2 | 11 +++++ 6 files changed, 31 insertions(+), 52 deletions(-) create mode 100644 test/regress/regress0/arith/div.09.smt2 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()); + 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(); - - 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(); - - Assert(!den.isZero()); - - const Rational& num = left.getConst(); - 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(); 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 diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 12aa0eecd..38e7e6f4e 100644 --- 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 index 000000000..2f1bca63a --- /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) -- 2.30.2