diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 19:35:58 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 20:07:39 -0400 |
commit | 0a3422299da7e882bae22c5fa3e5ec3c80b42046 (patch) | |
tree | d00f31a33f03f11608ee046b851f4c63e194fe87 /src/theory/arith/arith_rewriter.cpp | |
parent | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (diff) |
Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 95 |
1 files changed, 90 insertions, 5 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index aa5049ed4..247c09294 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -29,7 +29,8 @@ namespace theory { namespace arith { bool ArithRewriter::isAtom(TNode n) { - return arith::isRelationOperator(n.getKind()); + Kind k = n.getKind(); + return arith::isRelationOperator(k) || k == kind::IS_INTEGER || k == kind::DIVISIBLE; } RewriteResponse ArithRewriter::rewriteConstant(TNode t){ @@ -98,11 +99,28 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ return preRewritePlus(t); case kind::MULT: return preRewriteMult(t); - //case kind::INTS_DIVISION: - //case kind::INTS_MODULUS: + case kind::INTS_DIVISION: + case kind::INTS_MODULUS: + return RewriteResponse(REWRITE_DONE, t); case kind::INTS_DIVISION_TOTAL: case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t,true); + case kind::ABS: + if(t[0].isConst()) { + const Rational& rat = t[0].getConst<Rational>(); + if(rat >= 0) { + return RewriteResponse(REWRITE_DONE, t[0]); + } else { + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(-rat)); + } + } + return RewriteResponse(REWRITE_DONE, t); + case kind::IS_INTEGER: + case kind::TO_INTEGER: + return RewriteResponse(REWRITE_DONE, t); + case kind::TO_REAL: + return RewriteResponse(REWRITE_DONE, t[0]); default: Unhandled(k); } @@ -126,11 +144,44 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ return postRewritePlus(t); case kind::MULT: return postRewriteMult(t); - //case kind::INTS_DIVISION: - //case kind::INTS_MODULUS: + case kind::INTS_DIVISION: + case kind::INTS_MODULUS: + return RewriteResponse(REWRITE_DONE, t); case kind::INTS_DIVISION_TOTAL: case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, false); + case kind::ABS: + if(t[0].isConst()) { + const Rational& rat = t[0].getConst<Rational>(); + if(rat >= 0) { + return RewriteResponse(REWRITE_DONE, t[0]); + } else { + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(-rat)); + } + } + case kind::TO_REAL: + return RewriteResponse(REWRITE_DONE, t[0]); + case kind::TO_INTEGER: + if(t[0].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor()))); + } + if(t[0].getType().isInteger()) { + return RewriteResponse(REWRITE_DONE, t[0]); + } + //Unimplemented("TO_INTEGER, nonconstant"); + //return rewriteToInteger(t); + return RewriteResponse(REWRITE_DONE, t); + case kind::IS_INTEGER: + if(t[0].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(t[0].getConst<Rational>().getDenominator() == 1)); + } + if(t[0].getType().isInteger()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + //Unimplemented("IS_INTEGER, nonconstant"); + //return rewriteIsInteger(t); + return RewriteResponse(REWRITE_DONE, t); default: Unreachable(); } @@ -190,6 +241,25 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ } RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ + if(atom.getKind() == kind::IS_INTEGER) { + if(atom[0].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(atom[0].getConst<Rational>().isIntegral())); + } + if(atom[0].getType().isInteger()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + // not supported, but this isn't the right place to complain + return RewriteResponse(REWRITE_DONE, atom); + } else if(atom.getKind() == kind::DIVISIBLE) { + if(atom[0].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(bool((atom[0].getConst<Rational>() / atom.getOperator().getConst<Divisible>().k).isIntegral()))); + } + if(atom.getOperator().getConst<Divisible>().k.isOne()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkNode(kind::INTS_MODULUS_TOTAL, atom[0], NodeManager::currentNM()->mkConst(Rational(atom.getOperator().getConst<Divisible>().k))), NodeManager::currentNM()->mkConst(Rational(0)))); + } + // left |><| right TNode left = atom[0]; TNode right = atom[1]; @@ -217,6 +287,14 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ }else if(atom.getKind() == kind::LT){ Node geq = currNM->mkNode(kind::GEQ, atom[0], atom[1]); return RewriteResponse(REWRITE_DONE, currNM->mkNode(kind::NOT, geq)); + }else if(atom.getKind() == kind::IS_INTEGER){ + if(atom[0].getType().isInteger()){ + return RewriteResponse(REWRITE_DONE, currNM->mkConst(true)); + } + }else if(atom.getKind() == kind::DIVISIBLE){ + if(atom.getOperator().getConst<Divisible>().k.isOne()){ + return RewriteResponse(REWRITE_DONE, currNM->mkConst(true)); + } } return RewriteResponse(REWRITE_DONE, atom); @@ -329,6 +407,13 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL); return RewriteResponse(REWRITE_AGAIN, n); } + }else if(dIsConstant && d.getConst<Rational>().isNegativeOne()){ + if(k == kind::INTS_MODULUS || k == kind::INTS_MODULUS_TOTAL){ + return RewriteResponse(REWRITE_DONE, mkRationalNode(0)); + }else{ + Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL); + return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::UMINUS, n)); + } }else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){ Assert(d.getConst<Rational>().isIntegral()); Assert(n.getConst<Rational>().isIntegral()); |