diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 32 |
1 files changed, 13 insertions, 19 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bf5f285a5..b9c983215 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -53,15 +53,14 @@ using namespace CVC4::theory::arith; struct SlackAttrID; typedef expr::Attribute<SlackAttrID, Node> Slack; -TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : - Theory(id, c, out), +TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : + Theory(THEORY_ARITH, c, out), d_constants(NodeManager::currentNM()), d_partialModel(c), d_basicManager(), d_activityMonitor(), d_diseq(c), d_tableau(d_activityMonitor, d_basicManager), - d_rewriter(&d_constants), d_propagator(c, out), d_simplex(d_constants, d_partialModel, d_basicManager, d_out, d_activityMonitor, d_tableau), d_statistics() @@ -116,7 +115,7 @@ void TheoryArith::preRegisterTerm(TNode n) { d_out->setIncomplete(); } - if(isTheoryLeaf(n) || isStrictlyVarList){ + if(isLeaf(n) || isStrictlyVarList){ ++(d_statistics.d_statUserVariables); ArithVar varN = requestArithVar(n,false); setupInitialValue(varN); @@ -144,13 +143,8 @@ void TheoryArith::preRegisterTerm(TNode n) { } - -bool TheoryArith::isTheoryLeaf(TNode x) const{ - return x.getMetaKind() == kind::metakind::VARIABLE; -} - ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ - Assert(isTheoryLeaf(x)); + Assert(isLeaf(x)); Assert(!hasArithVar(x)); ArithVar varX = d_variables.size(); @@ -179,7 +173,9 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v Node n = variable.getNode(); - Assert(isTheoryLeaf(n)); + Debug("rewriter") << "should be var: " << n << endl; + + Assert(isLeaf(n)); Assert(hasArithVar(n)); ArithVar av = asArithVar(n); @@ -191,8 +187,6 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v void TheoryArith::setupSlack(TNode left){ - - ++(d_statistics.d_statSlackVariables); TypeNode real_type = NodeManager::currentNM()->realType(); Node slack = NodeManager::currentNM()->mkVar(real_type); @@ -242,10 +236,6 @@ void TheoryArith::setupInitialValue(ArithVar x){ Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl; }; -RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { - return d_rewriter.preRewrite(n); -} - void TheoryArith::registerTerm(TNode tn){ Debug("arith") << "registerTerm(" << tn << ")" << endl; } @@ -270,7 +260,7 @@ TNode getSide(TNode assertion, Kind simpleKind){ ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){ TNode left = getSide<true>(assertion, simpleKind); - if(isTheoryLeaf(left)){ + if(isLeaf(left)){ return asArithVar(left); }else{ Assert(left.hasAttribute(Slack())); @@ -457,7 +447,7 @@ void TheoryArith::check(Effort effortLevel){ } } -void TheoryArith::explain(TNode n, Effort e) { +void TheoryArith::explain(TNode n) { // Node explanation = d_propagator.explain(n); // Debug("arith") << "arith::explain("<<explanation<<")->" // << explanation << endl; @@ -552,3 +542,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { Unhandled(n.getKind()); } } + +void TheoryArith::notifyEq(TNode lhs, TNode rhs) { + +} |