diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/constraint.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 17 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 4 |
4 files changed, 17 insertions, 16 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 460877a23..3cb5464da 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -325,7 +325,7 @@ Constraint ConstraintValue::getCeiling() { DeltaRational ceiling(getValue().ceiling()); -#warning "Optimize via the iterator" + // TODO: "Optimize via the iterator" return d_database->getConstraint(getVariable(), getType(), ceiling); } @@ -334,7 +334,7 @@ Constraint ConstraintValue::getFloor() { DeltaRational floor(Rational(getValue().floor())); -#warning "Optimize via the iterator" + // TODO: "Optimize via the iterator" return d_database->getConstraint(getVariable(), getType(), floor); } diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 1b3a5cac7..613ce8368 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -504,7 +504,7 @@ SumPair DioSolver::processEquationsForCut(){ SumPair DioSolver::purifyIndex(TrailIndex i){ -#warning "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient." + // TODO: "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient." SumPair curr = d_trail[i].d_eq; @@ -612,7 +612,10 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::solveIndex(DioS Debug("arith::dio") << "before solveIndex("<<i<<":"<<si.getNode()<< ")" << endl; +#ifdef CVC4_ASSERTIONS const Polynomial& p = si.getPolynomial(); +#endif + Assert(p.isIntegral()); Assert(p.selectAbsMinimum() == d_trail[i].d_minimalMonomial); @@ -644,7 +647,10 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::decomposeIndex( Debug("arith::dio") << "before decomposeIndex("<<i<<":"<<si.getNode()<< ")" << endl; +#ifdef CVC4_ASSERTIONS const Polynomial& p = si.getPolynomial(); +#endif + Assert(p.isIntegral()); Assert(p.selectAbsMinimum() == d_trail[i].d_minimalMonomial); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e183e0e1b..7f0088f5b 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -53,8 +53,8 @@ namespace arith { const uint32_t RESET_START = 2; -TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : - Theory(THEORY_ARITH, c, u, out, valuation), +TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_ARITH, c, u, out, valuation, logicInfo), d_hasDoneWorkSinceCut(false), d_learner(d_pbSubstitutions), d_setupLiteralCallback(this), @@ -904,7 +904,7 @@ Comparison TheoryArith::mkIntegerEqualityFromAssignment(ArithVar v){ } Node TheoryArith::dioCutting(){ - context::Context::ScopedPush speculativePush(getContext()); + context::Context::ScopedPush speculativePush(getSatContext()); //DO NOT TOUCH THE OUTPUTSTREAM //TODO: Improve this @@ -1043,7 +1043,7 @@ Node TheoryArith::assertionCases(TNode assertion){ //Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind)); Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion); - Debug("arith::assertions") << "arith assertion @" << getContext()->getLevel() + Debug("arith::assertions") << "arith assertion @" << getSatContext()->getLevel() <<"(" << assertion << " \\-> " //<< determineLeftVariable(assertion, simpleKind) @@ -1352,7 +1352,7 @@ void TheoryArith::debugPrintModel(){ Node TheoryArith::explain(TNode n) { - Debug("arith::explain") << "explain @" << getContext()->getLevel() << ": " << n << endl; + Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl; Constraint c = d_constraintDatabase.lookup(n); if(c != NullConstraint){ @@ -1387,7 +1387,7 @@ void TheoryArith::propagate(Effort e) { }else if(!c->assertedToTheTheory()){ Node literal = c->getLiteral(); - Debug("arith::prop") << "propagating @" << getContext()->getLevel() << " " << literal << endl; + Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl; d_out->propagate(literal); }else{ @@ -1578,9 +1578,6 @@ Node TheoryArith::getValue(TNode n) { } } -void TheoryArith::notifyEq(TNode lhs, TNode rhs) { -} - void TheoryArith::notifyRestart(){ TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer); @@ -1674,7 +1671,7 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){ if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) || (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){ -#warning "Policy point" + // TODO: "Policy point" //We are only going to recreate the functionality for now. //In the future this can be improved to generate a temporary constraint //if none exists. diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index aa7740c37..59653b62d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -259,7 +259,7 @@ private: DeltaRational getDeltaValue(TNode n); public: - TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); + TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); virtual ~TheoryArith(); /** @@ -271,8 +271,6 @@ public: void propagate(Effort e); Node explain(TNode n); - void notifyEq(TNode lhs, TNode rhs); - Node getValue(TNode n); void shutdown(){ } |