diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
commit | ccd77233892ace44fd4852999e66534d1c2283ea (patch) | |
tree | a856cacd24508a5839fcdbe728583ff055b64e34 /src/theory/arith/simplex.cpp | |
parent | 9644b6e12fbd3b649daafa43c5400d272e27bfb4 (diff) |
Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Below is a highlight of the changes:
- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
Roughly speaking this means: (= x (+ y z)) is in normal form.
(See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 137 |
1 files changed, 73 insertions, 64 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 7fce748dc..5837d4793 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -33,15 +33,13 @@ static const uint32_t NUM_CHECKS = 10; static const bool CHECK_AFTER_PIVOT = true; static const uint32_t VARORDER_CHECK_PERIOD = 200; -SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager, - LinearEqualityModule& linEq) : +SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel) : d_linEq(linEq), d_partialModel(d_linEq.getPartialModel()), d_tableau(d_linEq.getTableau()), d_queue(d_partialModel, d_tableau), - d_propManager(propManager), d_numVariables(0), - d_delayedLemmas(), + d_conflictChannel(conflictChannel), d_pivotsInRound(), d_DELTA_ZERO(0,0) { @@ -77,7 +75,7 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_weakeningSuccesses("theory::arith::weakening::success",0), d_weakenings("theory::arith::weakening::total",0), d_weakenTime("theory::arith::weakening::time"), - d_delayedConflicts("theory::arith::delayedConflicts",0) + d_simplexConflicts("theory::arith::simplexConflicts",0) { StatisticsRegistry::registerStat(&d_statUpdateConflicts); @@ -99,7 +97,7 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_weakenings); StatisticsRegistry::registerStat(&d_weakenTime); - StatisticsRegistry::registerStat(&d_delayedConflicts); + StatisticsRegistry::registerStat(&d_simplexConflicts); } SimplexDecisionProcedure::Statistics::~Statistics(){ @@ -123,7 +121,7 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_weakenings); StatisticsRegistry::unregisterStat(&d_weakenTime); - StatisticsRegistry::unregisterStat(&d_delayedConflicts); + StatisticsRegistry::unregisterStat(&d_simplexConflicts); } @@ -203,7 +201,7 @@ Node betterConflict(TNode x, TNode y){ else return y; } -Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool returnFirst) { +bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime); switch(type){ @@ -215,7 +213,6 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re } bool success = false; - Node firstConflict = Node::null(); ArithPriorityQueue::const_iterator i = d_queue.begin(); ArithPriorityQueue::const_iterator end = d_queue.end(); for(; i != end; ++i){ @@ -225,11 +222,7 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re Node possibleConflict = checkBasicForConflict(x_i); if(!possibleConflict.isNull()){ success = true; - if(returnFirst && firstConflict.isNull()){ - firstConflict = possibleConflict; - }else{ - delayConflictAsLemma(possibleConflict); - } + reportConflict(possibleConflict); } } } @@ -242,13 +235,14 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re case AfterVarOrderSearch: ++(d_statistics.d_successAfterVarOrderSearch); break; } } - return firstConflict; + return success; } -Node SimplexDecisionProcedure::findModel(){ +bool SimplexDecisionProcedure::findModel(){ if(d_queue.empty()){ - return Node::null(); + return false; } + bool foundConflict = false; static CVC4_THREADLOCAL(unsigned int) instance = 0; instance = instance + 1; @@ -256,45 +250,44 @@ Node SimplexDecisionProcedure::findModel(){ d_queue.transitionToDifferenceMode(); - Node possibleConflict = Node::null(); if(d_queue.size() > 1){ - possibleConflict = findConflictOnTheQueue(BeforeDiffSearch); + foundConflict = findConflictOnTheQueue(BeforeDiffSearch); } - if(possibleConflict.isNull()){ + if(!foundConflict){ uint32_t numHueristicPivots = d_numVariables + 1; uint32_t pivotsRemaining = numHueristicPivots; uint32_t pivotsPerCheck = (numHueristicPivots/NUM_CHECKS) + (NUM_CHECKS-1); while(!d_queue.empty() && - possibleConflict.isNull() && + !foundConflict && pivotsRemaining > 0){ uint32_t pivotsToDo = min(pivotsPerCheck, pivotsRemaining); - possibleConflict = searchForFeasibleSolution(pivotsToDo); + foundConflict = searchForFeasibleSolution(pivotsToDo); pivotsRemaining -= pivotsToDo; //Once every CHECK_PERIOD examine the entire queue for conflicts - if(possibleConflict.isNull()){ - possibleConflict = findConflictOnTheQueue(DuringDiffSearch); + if(!foundConflict){ + foundConflict = findConflictOnTheQueue(DuringDiffSearch); }else{ - findConflictOnTheQueue(AfterDiffSearch, false); + findConflictOnTheQueue(AfterDiffSearch); } } } - if(!d_queue.empty() && possibleConflict.isNull()){ + if(!d_queue.empty() && !foundConflict){ d_queue.transitionToVariableOrderMode(); - while(!d_queue.empty() && possibleConflict.isNull()){ - possibleConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD); + while(!d_queue.empty() && !foundConflict){ + foundConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD); //Once every CHECK_PERIOD examine the entire queue for conflicts - if(possibleConflict.isNull()){ - possibleConflict = findConflictOnTheQueue(DuringVarOrderSearch); - }else{ - findConflictOnTheQueue(AfterVarOrderSearch, false); + if(!foundConflict){ + foundConflict = findConflictOnTheQueue(DuringVarOrderSearch); + } else{ + findConflictOnTheQueue(AfterVarOrderSearch); } } } - Assert(!possibleConflict.isNull() || d_queue.empty()); + Assert(foundConflict || d_queue.empty()); // Curiously the invariant that we always do a full check // means that the assignment we can always empty these queues. @@ -309,7 +302,7 @@ Node SimplexDecisionProcedure::findModel(){ Debug("arith::findModel") << "end findModel() " << instance << endl; - return possibleConflict; + return foundConflict; } Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ @@ -333,7 +326,7 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ //corresponds to Check() in dM06 //template <SimplexDecisionProcedure::PreferenceFunction pf> -Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ +bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ Debug("arith") << "searchForFeasibleSolution" << endl; Assert(remainingIterations > 0); @@ -344,7 +337,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl; if(x_i == ARITHVAR_SENTINEL){ Debug("arith_update") << "No inconsistent variables" << endl; - return Node::null(); //sat + return false; //sat } --remainingIterations; @@ -369,7 +362,9 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera x_j = selectSlackUpperBound(x_i, pf); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); - return generateConflictBelowLowerBound(x_i); //unsat + Node conflict = generateConflictBelowLowerBound(x_i); //unsat + reportConflict(conflict); + return true; } DeltaRational l_i = d_partialModel.getLowerBound(x_i); d_linEq.pivotAndUpdate(x_i, x_j, l_i); @@ -378,7 +373,9 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera x_j = selectSlackLowerBound(x_i, pf); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); - return generateConflictAboveUpperBound(x_i); //unsat + Node conflict = generateConflictAboveUpperBound(x_i); //unsat + reportConflict(conflict); + return true; } DeltaRational u_i = d_partialModel.getUpperBound(x_i); d_linEq.pivotAndUpdate(x_i, x_j, u_i); @@ -389,38 +386,50 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera if(CHECK_AFTER_PIVOT){ Node possibleConflict = checkBasicForConflict(x_j); if(!possibleConflict.isNull()){ - return possibleConflict; + reportConflict(possibleConflict); + return true; // unsat } } } Assert(remainingIterations == 0); - return Node::null(); + return false; } -TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){ +Constraint SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){ int sgn = coeff.sgn(); bool ub = aboveUpper?(sgn < 0) : (sgn > 0); - TNode exp = ub ? - d_partialModel.getUpperConstraint(v) : - d_partialModel.getLowerConstraint(v); - DeltaRational bound = ub? - d_partialModel.getUpperBound(v) : - d_partialModel.getLowerBound(v); + + Constraint c = ub ? + d_partialModel.getUpperBoundConstraint(v) : + d_partialModel.getLowerBoundConstraint(v); + +// #warning "revisit" +// Node exp = ub ? +// d_partialModel.explainUpperBound(v) : +// d_partialModel.explainLowerBound(v); bool weakened; do{ + const DeltaRational& bound = c->getValue(); + weakened = false; - Node weaker = ub? - d_propManager.strictlyWeakerAssertedUpperBound(v, bound): - d_propManager.strictlyWeakerAssertedLowerBound(v, bound); + Constraint weaker = ub? + c->getStrictlyWeakerUpperBound(true, true): + c->getStrictlyWeakerLowerBound(true, true); + + // Node weaker = ub? + // d_propManager.strictlyWeakerAssertedUpperBound(v, bound): + // d_propManager.strictlyWeakerAssertedLowerBound(v, bound); - if(!weaker.isNull()){ - DeltaRational weakerBound = asDeltaRational(weaker); + if(weaker != NullConstraint){ + //if(!weaker.isNull()){ + const DeltaRational& weakerBound = weaker->getValue(); + //DeltaRational weakerBound = asDeltaRational(weaker); DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound; //if var == basic, @@ -438,24 +447,16 @@ TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRationa Debug("weak") << " basic: "; } Debug("weak") << " " << surplus << " "<< diff << endl - << " " << bound << exp << endl + << " " << bound << c << endl << " " << weakerBound << weaker << endl; - if(exp.getKind() == AND){ - Debug("weak") << "VICTORY" << endl; - } - Assert(diff > d_DELTA_ZERO); - exp = weaker; - bound = weakerBound; + c = weaker; } } }while(weakened); - if(exp.getKind() == AND){ - Debug("weak") << "boo: " << exp << endl; - } - return exp; + return c; } Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar){ @@ -479,7 +480,15 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar const TableauEntry& entry = *i; ArithVar v = entry.getColVar(); const Rational& coeff = entry.getCoefficient(); - conflict << weakestExplanation(aboveUpper, surplus, v, coeff, anyWeakenings, basicVar); + bool weakening = false; + Constraint c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar); + Debug("weak") << "weak : " << weakening << " " << c->assertedToTheTheory() + << c << endl + << c->explainForConflict() << endl; + anyWeakenings = anyWeakenings || weakening; + + Debug("weak") << "weak : " << c->explainForConflict() << endl; + c->explainForConflict(conflict); } ++d_statistics.d_weakeningAttempts; if(anyWeakenings){ |