diff options
author | Tim King <taking@cs.nyu.edu> | 2010-10-23 21:47:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-10-23 21:47:47 +0000 |
commit | 237995ce0e7f47b826e26c0afb317cf5e3174879 (patch) | |
tree | ddeec96c8880ff186d350979f2a151179ae2d73f /src/theory/arith/arith_rewriter.cpp | |
parent | 0a3ecb598dac9e5e7416f88403dbf73d558c8739 (diff) |
Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more general ArithVarDenseSet. Renamed NextArithRewriter to ArithRewriter.
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 326 |
1 files changed, 326 insertions, 0 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp new file mode 100644 index 000000000..9f4388b54 --- /dev/null +++ b/src/theory/arith/arith_rewriter.cpp @@ -0,0 +1,326 @@ +/********************* */ +/*! \file arith_rewriter.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + + +#include "theory/theory.h" +#include "theory/arith/normal_form.h" +#include "theory/arith/arith_rewriter.h" +#include "theory/arith/arith_utilities.h" + +#include <vector> +#include <set> +#include <stack> + + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::arith; + +bool isVariable(TNode t){ + return t.getMetaKind() == kind::metakind::VARIABLE; +} + +RewriteResponse ArithRewriter::rewriteConstant(TNode t){ + Assert(t.getMetaKind() == kind::metakind::CONSTANT); + Node val = coerceToRationalNode(t); + + return RewriteComplete(val); +} + +RewriteResponse ArithRewriter::rewriteVariable(TNode t){ + Assert(isVariable(t)); + + return RewriteComplete(t); +} + +RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){ + Assert(t.getKind()== kind::MINUS); + + if(t[0] == t[1]) return RewriteComplete(d_constants->d_ZERO_NODE); + + Node noMinus = makeSubtractionNode(t[0],t[1]); + if(pre){ + return RewriteComplete(noMinus); + }else{ + return FullRewriteNeeded(noMinus); + } +} + +RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){ + Assert(t.getKind()== kind::UMINUS); + + Node noUminus = makeUnaryMinusNode(t[0]); + if(pre) + return RewriteComplete(noUminus); + else + return RewriteAgain(noUminus); +} + +RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ + if(t.getMetaKind() == kind::metakind::CONSTANT){ + return rewriteConstant(t); + }else if(isVariable(t)){ + return rewriteVariable(t); + }else if(t.getKind() == kind::MINUS){ + return rewriteMinus(t, true); + }else if(t.getKind() == kind::UMINUS){ + return rewriteUMinus(t, true); + }else if(t.getKind() == kind::DIVISION){ + if(t[0].getKind()== kind::CONST_RATIONAL){ + return rewriteDivByConstant(t, true); + }else{ + return RewriteComplete(t); + } + }else if(t.getKind() == kind::PLUS){ + return preRewritePlus(t); + }else if(t.getKind() == kind::MULT){ + return preRewriteMult(t); + }else{ + Unreachable(); + } +} +RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ + if(t.getMetaKind() == kind::metakind::CONSTANT){ + return rewriteConstant(t); + }else if(isVariable(t)){ + return rewriteVariable(t); + }else if(t.getKind() == kind::MINUS){ + return rewriteMinus(t, false); + }else if(t.getKind() == kind::UMINUS){ + return rewriteUMinus(t, false); + }else if(t.getKind() == kind::DIVISION){ + return rewriteDivByConstant(t, false); + }else if(t.getKind() == kind::PLUS){ + return postRewritePlus(t); + }else if(t.getKind() == kind::MULT){ + return postRewriteMult(t); + }else{ + Unreachable(); + } +} + +RewriteResponse ArithRewriter::preRewriteMult(TNode t){ + Assert(t.getKind()== kind::MULT); + + // Rewrite multiplications with a 0 argument and to 0 + Integer intZero; + + for(TNode::iterator i = t.begin(); i != t.end(); ++i) { + if((*i).getKind() == kind::CONST_RATIONAL) { + if((*i).getConst<Rational>() == d_constants->d_ZERO) { + return RewriteComplete(d_constants->d_ZERO_NODE); + } + } else if((*i).getKind() == kind::CONST_INTEGER) { + if((*i).getConst<Integer>() == intZero) { + if(t.getType().isInteger()) { + return RewriteComplete(NodeManager::currentNM()->mkConst(intZero)); + } else { + return RewriteComplete(d_constants->d_ZERO_NODE); + } + } + } + } + return RewriteComplete(t); +} +RewriteResponse ArithRewriter::preRewritePlus(TNode t){ + Assert(t.getKind()== kind::PLUS); + + return RewriteComplete(t); +} + +RewriteResponse ArithRewriter::postRewritePlus(TNode t){ + Assert(t.getKind()== kind::PLUS); + + Polynomial res = Polynomial::mkZero(); + + for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){ + Node curr = *i; + Polynomial currPoly = Polynomial::parsePolynomial(curr); + + res = res + currPoly; + } + + return RewriteComplete(res.getNode()); +} + +RewriteResponse ArithRewriter::postRewriteMult(TNode t){ + Assert(t.getKind()== kind::MULT); + + Polynomial res = Polynomial::mkOne(); + + for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){ + Node curr = *i; + Polynomial currPoly = Polynomial::parsePolynomial(curr); + + res = res * currPoly; + } + + return RewriteComplete(res.getNode()); +} + +RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){ + TNode left = t[0]; + TNode right = t[1]; + + + Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right)); + + if(cmp.isBoolean()){ + return RewriteComplete(cmp.getNode()); + } + + if(cmp.getLeft().containsConstant()){ + Monomial constantHead = cmp.getLeft().getHead(); + Assert(constantHead.isConstant()); + + Constant constant = constantHead.getConstant(); + + Constant negativeConstantHead = -constant; + + cmp = cmp.addConstant(negativeConstantHead); + } + Assert(!cmp.getLeft().containsConstant()); + + if(!cmp.getLeft().getHead().coefficientIsOne()){ + Monomial constantHead = cmp.getLeft().getHead(); + Assert(!constantHead.isConstant()); + Constant constant = constantHead.getConstant(); + + Constant inverse = Constant::mkConstant(constant.getValue().inverse()); + + cmp = cmp.multiplyConstant(inverse); + } + Assert(cmp.getLeft().getHead().coefficientIsOne()); + + Assert(cmp.isBoolean() || cmp.isNormalForm()); + return RewriteComplete(cmp.getNode()); +} + +RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ + // left |><| right + TNode left = atom[0]; + TNode right = atom[1]; + + if(right.getMetaKind() == kind::metakind::CONSTANT){ + return postRewriteAtomConstantRHS(atom); + }else{ + //Transform this to: (left - right) |><| 0 + Node diff = makeSubtractionNode(left, right); + Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE); + return FullRewriteNeeded(reduction); + } +} + +RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ + Assert(isAtom(atom)); + NodeManager* currNM = NodeManager::currentNM(); + + if(atom.getKind() == kind::EQUAL) { + if(atom[0] == atom[1]) { + return RewriteComplete(currNM->mkConst(true)); + } + } + + Node reduction = atom; + + if(atom[1].getMetaKind() != kind::metakind::CONSTANT){ + // left |><| right + TNode left = atom[0]; + TNode right = atom[1]; + + //Transform this to: (left - right) |><| 0 + Node diff = makeSubtractionNode(left, right); + reduction = currNM->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE); + } + + if(reduction.getKind() == kind::GT){ + Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]); + reduction = currNM->mkNode(kind::NOT, leq); + }else if(reduction.getKind() == kind::LT){ + Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]); + reduction = currNM->mkNode(kind::NOT, geq); + } + + return RewriteComplete(reduction); +} + +RewriteResponse ArithRewriter::postRewrite(TNode t){ + if(isTerm(t)){ + RewriteResponse response = postRewriteTerm(t); + if(Debug.isOn("arith::rewriter") && response.isDone()) { + Polynomial::parsePolynomial(response.getNode()); + } + return response; + }else if(isAtom(t)){ + RewriteResponse response = postRewriteAtom(t); + if(Debug.isOn("arith::rewriter") && response.isDone()) { + Comparison::parseNormalForm(response.getNode()); + } + return response; + }else{ + Unreachable(); + return RewriteComplete(Node::null()); + } +} + +RewriteResponse ArithRewriter::preRewrite(TNode t){ + if(isTerm(t)){ + return preRewriteTerm(t); + }else if(isAtom(t)){ + return preRewriteAtom(t); + }else{ + Unreachable(); + return RewriteComplete(Node::null()); + } +} + +Node ArithRewriter::makeUnaryMinusNode(TNode n){ + return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n); +} + +Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){ + Node negR = makeUnaryMinusNode(r); + Node diff = NodeManager::currentNM()->mkNode(kind::PLUS, l, negR); + + return diff; +} + +RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){ + Assert(t.getKind()== kind::DIVISION); + + Node left = t[0]; + Node right = t[1]; + Assert(right.getKind()== kind::CONST_RATIONAL); + + + const Rational& den = right.getConst<Rational>(); + + Assert(den != d_constants->d_ZERO); + + Rational div = den.inverse(); + + Node result = mkRationalNode(div); + + Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result); + if(pre){ + return RewriteComplete(mult); + }else{ + return RewriteAgain(mult); + } +} |