diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 79 |
1 files changed, 9 insertions, 70 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 157c45160..8f17b01a9 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -33,10 +33,12 @@ #include "theory/arith/basic.h" #include "theory/arith/arith_activity.h" -#include "theory/arith/arith_rewriter.h" +#include "theory/arith/next_arith_rewriter.h" #include "theory/arith/arith_propagator.h" #include "theory/arith/theory_arith.h" +#include "theory/arith/normal_form.h" + #include <map> #include <stdint.h> @@ -55,7 +57,7 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : d_constants(NodeManager::currentNM()), d_partialModel(c), d_diseq(c), - d_rewriter(&d_constants), + d_nextRewriter(&d_constants), d_propagator(c), d_statistics() { @@ -109,22 +111,9 @@ bool isBasicSum(TNode n){ bool isNormalAtom(TNode n){ - if(!(n.getKind() == LEQ|| n.getKind() == GEQ || n.getKind() == EQUAL)){ - return false; - } - TNode left = n[0]; - TNode right = n[1]; - if(right.getKind() != CONST_RATIONAL){ - return false; - } - if(left.getMetaKind() == metakind::VARIABLE){ - return true; - }else if(isBasicSum(left)){ - return true; - }else{ - return false; - } + Comparison parse = Comparison::parseNormalForm(n); + return parse.isNormalForm(); } @@ -213,7 +202,6 @@ void TheoryArith::preRegisterTerm(TNode n) { if(left.getKind() == PLUS){ //We may need to introduce a slack variable. Assert(left.getNumChildren() >= 2); - Assert(isBasicSum(left)); if(!left.hasAttribute(Slack())){ setupSlack(left); } @@ -229,11 +217,9 @@ void TheoryArith::setupSlack(TNode left){ left.setAttribute(Slack(), slack); makeBasic(slack); - Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left); - - Debug("slack") << "slack " << slackEqLeft << endl; + Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, slack, left); - d_tableau.addRow(slackEqLeft); + d_tableau.addRow(eq); setupVariable(slack); } @@ -316,56 +302,9 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){ } RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { - // ensure a hard link to the node we're returning - Node out; - - // Look for multiplications with a 0 argument and rewrite the whole - // thing as 0 - if(n.getKind() == MULT) { - Rational ratZero; - Integer intZero; - for(TNode::iterator i = n.begin(); i != n.end(); ++i) { - if((*i).getKind() == CONST_RATIONAL) { - if((*i).getConst<Rational>() == ratZero) { - out = NodeManager::currentNM()->mkConst(ratZero); - break; - } - } else if((*i).getKind() == CONST_INTEGER) { - if((*i).getConst<Integer>() == intZero) { - if(n.getType().isInteger()) { - out = NodeManager::currentNM()->mkConst(intZero); - break; - } else { - out = NodeManager::currentNM()->mkConst(ratZero); - break; - } - } - } - } - } else if(n.getKind() == EQUAL) { - if(n[0] == n[1]) { - out = NodeManager::currentNM()->mkConst(true); - } - } - - if(out.isNull()) { - // no preRewrite to perform - return RewriteComplete(Node(n)); - } else { - // out is always a constant, so doesn't need to be rewritten again - return RewriteComplete(out); - } + return d_nextRewriter.preRewrite(n); } -Node TheoryArith::rewrite(TNode n){ - Debug("arith") << "rewrite(" << n << ")" << endl; - - Node result = d_rewriter.rewrite(n); - Debug("arith-rewrite") << "rewrite(" << n << ") -> " << result << endl; - return result; -} - - void TheoryArith::registerTerm(TNode tn){ Debug("arith") << "registerTerm(" << tn << ")" << endl; } |