From eefe0b63e564320eb135eb66d6c02c9dc6e9e8de Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 28 Feb 2012 21:26:35 +0000 Subject: This commit merges in branches/arithmetic/internalbb up to revision 2831. This is a significant refactoring of code. - r2820 -- Refactors Simplex so that it does significantly fewer functions. -- Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model. -- Some of the code for propagation has moved to TheoryArith. -r2826 -- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound(). - r2827 -- Adds isZero() to Rational. Adds cmp to DeltaRational. - r2831 -- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp. -- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases. --- src/theory/arith/theory_arith.cpp | 378 +++++++++++++++++++++++++++++++------- 1 file changed, 312 insertions(+), 66 deletions(-) (limited to 'src/theory/arith/theory_arith.cpp') diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b10fc964d..1137ca7b7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -56,6 +56,7 @@ using namespace CVC4::theory::arith; static 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), d_hasDoneWorkSinceCut(false), @@ -65,9 +66,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_constantIntegerVariables(c), d_CivIterator(c,0), d_varsInDioSolver(c), - d_partialModel(c, d_differenceManager), d_diseq(c), + d_partialModel(c, d_differenceManager), d_tableau(), + d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack), d_diosolver(c), d_pbSubstitutions(u), d_restartsCounter(0), @@ -77,7 +79,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_atomDatabase(c, out), d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation), d_differenceManager(c, d_propManager), - d_simplex(d_propManager, d_partialModel, d_tableau), + d_simplex(d_propManager, d_linEq), + d_basicVarModelUpdateCallBack(d_simplex), d_DELTA_ZERO(0), d_statistics() {} @@ -85,6 +88,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha TheoryArith::~TheoryArith(){} TheoryArith::Statistics::Statistics(): + d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), + d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), d_statUserVariables("theory::arith::UserVariables", 0), d_statSlackVariables("theory::arith::SlackVariables", 0), d_statDisequalitySplits("theory::arith::DisequalitySplits", 0), @@ -97,8 +102,14 @@ TheoryArith::Statistics::Statistics(): d_initialTableauSize("theory::arith::initialTableauSize", 0), d_currSetToSmaller("theory::arith::currSetToSmaller", 0), d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0), - d_restartTimer("theory::arith::restartTimer") + d_restartTimer("theory::arith::restartTimer"), + d_boundComputationTime("theory::arith::bound::time"), + d_boundComputations("theory::arith::bound::boundComputations",0), + d_boundPropagations("theory::arith::bound::boundPropagations",0) { + StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); + StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); + StatisticsRegistry::registerStat(&d_statUserVariables); StatisticsRegistry::registerStat(&d_statSlackVariables); StatisticsRegistry::registerStat(&d_statDisequalitySplits); @@ -115,9 +126,16 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_currSetToSmaller); StatisticsRegistry::registerStat(&d_smallerSetToCurr); StatisticsRegistry::registerStat(&d_restartTimer); + + StatisticsRegistry::registerStat(&d_boundComputationTime); + StatisticsRegistry::registerStat(&d_boundComputations); + StatisticsRegistry::registerStat(&d_boundPropagations); } TheoryArith::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); + StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); + StatisticsRegistry::unregisterStat(&d_statUserVariables); StatisticsRegistry::unregisterStat(&d_statSlackVariables); StatisticsRegistry::unregisterStat(&d_statDisequalitySplits); @@ -134,6 +152,186 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_currSetToSmaller); StatisticsRegistry::unregisterStat(&d_smallerSetToCurr); StatisticsRegistry::unregisterStat(&d_restartTimer); + + StatisticsRegistry::unregisterStat(&d_boundComputationTime); + StatisticsRegistry::unregisterStat(&d_boundComputations); + StatisticsRegistry::unregisterStat(&d_boundPropagations); +} + +/* procedure AssertLower( x_i >= c_i ) */ +Node TheoryArith::AssertLower(ArithVar x_i, DeltaRational& c_i, TNode original){ + Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; + + if(isInteger(x_i)){ + c_i = DeltaRational(c_i.ceiling()); + } + + //TODO Relax to less than? + if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){ + return Node::null(); + } + + int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i); + if(cmpToUB > 0){ // c_i < \lowerbound(x_i) + Node ubc = d_partialModel.getUpperConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); + //d_out->conflict(conflict); + Debug("arith") << "AssertLower conflict " << conflict << endl; + ++(d_statistics.d_statAssertLowerConflicts); + return conflict; + }else if(cmpToUB == 0){ + if(isInteger(x_i)){ + d_constantIntegerVariables.push_back(x_i); + } + //check to make sure x_i != c_i has not been asserted + Node left = d_arithvarNodeMap.asNode(x_i); + + // if lowerbound and upperbound are equal, then the infinitesimal must be 0 + Assert(c_i.getInfinitesimalPart().isZero()); + Node right = mkRationalNode(c_i.getNoninfinitesimalPart()); + + Node diseq = left.eqNode(right).notNode(); + if (d_diseq.find(diseq) != d_diseq.end()) { + Node lb = d_partialModel.getLowerConstraint(x_i); + return disequalityConflict(diseq, lb , original); + } + } + + d_partialModel.setLowerConstraint(x_i,original); + d_partialModel.setLowerBound(x_i, c_i); + + d_updatedBounds.softAdd(x_i); + + if(!d_tableau.isBasic(x_i)){ + if(d_partialModel.getAssignment(x_i) < c_i){ + d_linEq.update(x_i, c_i); + } + }else{ + d_simplex.updateBasic(x_i); + } + + if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } + + return Node::null(); +} + +/* procedure AssertUpper( x_i <= c_i) */ +Node TheoryArith::AssertUpper(ArithVar x_i, DeltaRational& c_i, TNode original){ + Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; + + if(isInteger(x_i)){ + c_i = DeltaRational(c_i.floor()); + } + + Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; + + if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i + return Node::null(); //sat + } + + // cmpToLb = \lowerbound(x_i).cmp(c_i) + int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i); + if( cmpToLB < 0 ){ // \upperbound(x_i) < \lowerbound(x_i) + Node lbc = d_partialModel.getLowerConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); + Debug("arith") << "AssertUpper conflict " << conflict << endl; + ++(d_statistics.d_statAssertUpperConflicts); + return conflict; + }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i) + if(isInteger(x_i)){ + d_constantIntegerVariables.push_back(x_i); + } + + //check to make sure x_i != c_i has not been asserted + Node left = d_arithvarNodeMap.asNode(x_i); + + // if lowerbound and upperbound are equal, then the infinitesimal must be 0 + Assert(c_i.getInfinitesimalPart().isZero()); + Node right = mkRationalNode(c_i.getNoninfinitesimalPart()); + + Node diseq = left.eqNode(right).notNode(); + if (d_diseq.find(diseq) != d_diseq.end()) { + Node lb = d_partialModel.getLowerConstraint(x_i); + return disequalityConflict(diseq, lb , original); + } + } + + d_partialModel.setUpperConstraint(x_i,original); + d_partialModel.setUpperBound(x_i, c_i); + + d_updatedBounds.softAdd(x_i); + + if(!d_tableau.isBasic(x_i)){ + if(d_partialModel.getAssignment(x_i) > c_i){ + d_linEq.update(x_i, c_i); + } + }else{ + d_simplex.updateBasic(x_i); + } + + if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } + + return Node::null(); +} + + +/* procedure AssertLower( x_i == c_i ) */ +Node TheoryArith::AssertEquality(ArithVar x_i, DeltaRational& c_i, TNode original){ + + Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; + + int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i); + int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i); + + // u_i <= c_i <= l_i + // This can happen if both c_i <= x_i and x_i <= c_i are in the system. + if(cmpToUB >= 0 && cmpToLB <= 0){ + return Node::null(); //sat + } + + if(cmpToUB > 0){ + Node ubc = d_partialModel.getUpperConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); + Debug("arith") << "AssertLower conflict " << conflict << endl; + return conflict; + } + + if(cmpToLB < 0){ + Node lbc = d_partialModel.getLowerConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); + Debug("arith") << "AssertUpper conflict " << conflict << endl; + return conflict; + } + + Assert(cmpToUB <= 0); + Assert(cmpToLB >= 0); + Assert(cmpToUB < 0 || cmpToLB > 0); + + + if(isInteger(x_i)){ + d_constantIntegerVariables.push_back(x_i); + } + + // Don't bother to check whether x_i != c_i is in d_diseq + // The a and (not a) should never be on the fact queue + + d_partialModel.setLowerConstraint(x_i,original); + d_partialModel.setLowerBound(x_i, c_i); + + d_partialModel.setUpperConstraint(x_i,original); + d_partialModel.setUpperBound(x_i, c_i); + + + d_updatedBounds.softAdd(x_i); + + if(!d_tableau.isBasic(x_i)){ + if(!(d_partialModel.getAssignment(x_i) == c_i)){ + d_linEq.update(x_i, c_i); + } + }else{ + d_simplex.updateBasic(x_i); + } + return Node::null(); } @@ -482,8 +680,8 @@ void TheoryArith::setupInitialValue(ArithVar x){ //This can go away if the tableau creation is done at preregister //time instead of register - DeltaRational safeAssignment = d_simplex.computeRowValue(x, true); - DeltaRational assignment = d_simplex.computeRowValue(x, false); + DeltaRational safeAssignment = d_linEq.computeRowValue(x, true); + DeltaRational assignment = d_linEq.computeRowValue(x, false); d_partialModel.initialize(x,safeAssignment); d_partialModel.setAssignment(x,assignment); } @@ -634,69 +832,33 @@ Node TheoryArith::assertionCases(TNode assertion){ ArithVar x_i = determineLeftVariable(assertion, simpleKind); DeltaRational c_i = determineRightConstant(assertion, simpleKind); - bool tightened = false; + // bool tightened = false; - //If the variable is an integer tighen the constraint. - if(isInteger(x_i)){ - if(simpleKind == LT){ - tightened = true; - c_i = DeltaRational(c_i.floor()); - }else if(simpleKind == GT){ - tightened = true; - c_i = DeltaRational(c_i.ceiling()); - } - } + // //If the variable is an integer tighen the constraint. + // if(isInteger(x_i)){ + // if(simpleKind == LT){ + // tightened = true; + // c_i = DeltaRational(c_i.floor()); + // }else if(simpleKind == GT){ + // tightened = true; + // c_i = DeltaRational(c_i.ceiling()); + // } + // } Debug("arith::assertions") << "arith assertion @" << getContext()->getLevel() <<"(" << assertion - << " \\-> " - << x_i<<" "<< simpleKind <<" "<< c_i << ")" << std::endl; + << " \\-> " + << x_i<<" "<< simpleKind <<" "<< c_i << ")" << std::endl; switch(simpleKind){ case LEQ: case LT: - if(simpleKind == LEQ || (simpleKind == LT && tightened)){ - if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) { - //If equal - TNode left = getSide(assertion, simpleKind); - TNode right = getSide(assertion, simpleKind); - - Node diseq = left.eqNode(right).notNode(); - if (d_diseq.find(diseq) != d_diseq.end()) { - Node lb = d_partialModel.getLowerConstraint(x_i); - return disequalityConflict(diseq, lb , assertion); - } - - if(isInteger(x_i)){ - d_constantIntegerVariables.push_back(x_i); - } - } - } - return d_simplex.AssertUpper(x_i, c_i, assertion); + return AssertUpper(x_i, c_i, assertion); case GEQ: case GT: - if(simpleKind == GEQ || (simpleKind == GT && tightened)){ - if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) { - //If equal - TNode left = getSide(assertion, simpleKind); - TNode right = getSide(assertion, simpleKind); - - Node diseq = left.eqNode(right).notNode(); - if (d_diseq.find(diseq) != d_diseq.end()) { - Node ub = d_partialModel.getUpperConstraint(x_i); - return disequalityConflict(diseq, assertion, ub); - } - if(isInteger(x_i)){ - d_constantIntegerVariables.push_back(x_i); - } - } - } - return d_simplex.AssertLower(x_i, c_i, assertion); + return AssertLower(x_i, c_i, assertion); case EQUAL: - if(isInteger(x_i)){ - d_constantIntegerVariables.push_back(x_i); - } - return d_simplex.AssertEquality(x_i, c_i, assertion); + return AssertEquality(x_i, c_i, assertion); case DISTINCT: { d_diseq.insert(assertion); @@ -760,7 +922,7 @@ void TheoryArith::check(Effort effortLevel){ if(!possibleConflict.isNull()){ d_partialModel.revertAssignmentChanges(); Debug("arith::conflict") << "conflict " << possibleConflict << endl; - d_simplex.clearUpdates(); + clearUpdates(); d_out->conflict(possibleConflict); return; } @@ -771,10 +933,10 @@ void TheoryArith::check(Effort effortLevel){ } bool emmittedConflictOrSplit = false; - Node possibleConflict = d_simplex.updateInconsistentVars(); + Node possibleConflict = d_simplex.findModel(); if(possibleConflict != Node::null()){ d_partialModel.revertAssignmentChanges(); - d_simplex.clearUpdates(); + clearUpdates(); Debug("arith::conflict") << "conflict " << possibleConflict << endl; d_out->conflict(possibleConflict); @@ -818,7 +980,7 @@ void TheoryArith::check(Effort effortLevel){ } }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel() - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } if(Debug.isOn("arith::print_model")) { debugPrintModel(); } Debug("arith") << "TheoryArith::check end" << std::endl; } @@ -958,10 +1120,10 @@ Node flattenAnd(Node n){ void TheoryArith::propagate(Effort e) { if(quickCheckOrMore(e)){ bool propagated = false; - if(Options::current()->arithPropagation && d_simplex.hasAnyUpdates()){ - d_simplex.propagateCandidates(); + if(Options::current()->arithPropagation && hasAnyUpdates()){ + propagateCandidates(); }else{ - d_simplex.clearUpdates(); + clearUpdates(); } while(d_propManager.hasMorePropagations()){ @@ -1106,7 +1268,7 @@ void TheoryArith::notifyEq(TNode lhs, TNode rhs) { void TheoryArith::notifyRestart(){ TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer); - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } ++d_restartsCounter; @@ -1225,7 +1387,7 @@ void TheoryArith::presolve(){ d_statistics.d_initialTableauSize.setData(d_tableau.size()); - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } static CVC4_THREADLOCAL(unsigned) callCount = 0; if(Debug.isOn("arith::presolve")) { @@ -1245,3 +1407,87 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) { } } + +bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){ + ++d_statistics.d_boundComputations; + + DeltaRational bound = upperBound ? + d_linEq.computeUpperBound(basic): + d_linEq.computeLowerBound(basic); + + if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) || + (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){ + Node bestImplied = upperBound ? + d_propManager.getBestImpliedUpperBound(basic, bound): + d_propManager.getBestImpliedLowerBound(basic, bound); + + if(!bestImplied.isNull()){ + bool asserted = d_propManager.isAsserted(bestImplied); + bool propagated = d_propManager.isPropagated(bestImplied); + if( !asserted && !propagated){ + + NodeBuilder<> nb(kind::AND); + if(upperBound){ + d_linEq.explainNonbasicsUpperBound(basic, nb); + }else{ + d_linEq.explainNonbasicsLowerBound(basic, nb); + } + Node explanation = nb; + d_propManager.propagate(bestImplied, explanation, false); + return true; + }else{ + Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl; + } + } + } + return false; +} + +void TheoryArith::propagateCandidate(ArithVar basic){ + bool success = false; + if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasLowerBounds(basic)){ + success |= propagateCandidateLowerBound(basic); + } + if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasUpperBounds(basic)){ + success |= propagateCandidateUpperBound(basic); + } + if(success){ + ++d_statistics.d_boundPropagations; + } +} + +void TheoryArith::propagateCandidates(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime); + + Assert(d_candidateBasics.empty()); + + if(d_updatedBounds.empty()){ return; } + + PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin(); + PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end(); + for(; i != end; ++i){ + ArithVar var = *i; + if(d_tableau.isBasic(var) && + d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){ + d_candidateBasics.softAdd(var); + }else{ + Tableau::ColIterator basicIter = d_tableau.colIterator(var); + for(; !basicIter.atEnd(); ++basicIter){ + const TableauEntry& entry = *basicIter; + ArithVar rowVar = entry.getRowVar(); + Assert(entry.getColVar() == var); + Assert(d_tableau.isBasic(rowVar)); + if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){ + d_candidateBasics.softAdd(rowVar); + } + } + } + } + d_updatedBounds.purge(); + + while(!d_candidateBasics.empty()){ + ArithVar candidate = d_candidateBasics.pop_back(); + Assert(d_tableau.isBasic(candidate)); + propagateCandidate(candidate); + } +} -- cgit v1.2.3