diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-22 15:09:03 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-22 15:09:03 +0000 |
commit | 52c5c282f47448856e0dec8a7d4e5de612a8dcc3 (patch) | |
tree | b6eac07d1c91aeab8fbfa4d6bd03981939614e77 /src/theory | |
parent | 6ce8f5cc5d7767d5ff9e74bc08d3c8a364ad8bf1 (diff) |
This commit merges in the branch arithmetic/cprop.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/constraint.cpp | 241 | ||||
-rw-r--r-- | src/theory/arith/constraint.h | 32 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 138 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 25 |
5 files changed, 388 insertions, 50 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index d2a0d9bfa..d451e9597 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -66,7 +66,11 @@ ConstraintValue::ConstraintValue(ArithVar x, ConstraintType t, const DeltaRatio std::ostream& operator<<(std::ostream& o, const Constraint c){ - return o << *c; + if(c == NullConstraint){ + return o << "NullConstraint"; + }else{ + return o << *c; + } } std::ostream& operator<<(std::ostream& o, const ConstraintType t){ @@ -530,6 +534,19 @@ ConstraintDatabase::~ConstraintDatabase(){ Assert(d_nodetoConstraintMap.empty()); } +ConstraintDatabase::Statistics::Statistics(): + d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0), + d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0) +{ + StatisticsRegistry::registerStat(&d_unatePropagateCalls); + StatisticsRegistry::registerStat(&d_unatePropagateImplications); + +} +ConstraintDatabase::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_unatePropagateCalls); + StatisticsRegistry::unregisterStat(&d_unatePropagateImplications); +} + void ConstraintDatabase::addVariable(ArithVar v){ Assert(v == d_varDatabases.size()); d_varDatabases.push_back(new PerVariableDatabase(v)); @@ -1050,29 +1067,15 @@ void mutuallyExclusive(std::vector<Node>& out, Constraint a, Constraint b){ out.push_back(orderOr); } -void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& out, ArithVar v) const{ +void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& out, ArithVar v) const{ SortedConstraintMap& scm = getVariableSCM(v); - - SortedConstraintMapConstIterator outer; + SortedConstraintMapConstIterator scm_iter = scm.begin(); SortedConstraintMapConstIterator scm_end = scm.end(); - - vector<Constraint> equalities; - for(outer = scm.begin(); outer != scm_end; ++outer){ - const ValueCollection& vc = outer->second; - if(vc.hasEquality()){ - Constraint eq = vc.getEquality(); - if(eq->hasLiteral()){ - equalities.push_back(eq); - } - } - } - Constraint prev = NullConstraint; //get transitive unates //Only lower bounds or upperbounds should be done. - for(outer = scm.begin(); outer != scm_end; ++outer){ - const ValueCollection& vc = outer->second; - + for(; scm_iter != scm_end; ++scm_iter){ + const ValueCollection& vc = scm_iter->second; if(vc.hasUpperBound()){ Constraint ub = vc.getUpperBound(); if(ub->hasLiteral()){ @@ -1083,6 +1086,26 @@ void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& out, ArithVar v } } } +} + +void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& out, ArithVar v) const{ + + vector<Constraint> equalities; + + SortedConstraintMap& scm = getVariableSCM(v); + SortedConstraintMapConstIterator scm_iter = scm.begin(); + SortedConstraintMapConstIterator scm_end = scm.end(); + + for(; scm_iter != scm_end; ++scm_iter){ + const ValueCollection& vc = scm_iter->second; + if(vc.hasEquality()){ + Constraint eq = vc.getEquality(); + if(eq->hasLiteral()){ + equalities.push_back(eq); + } + } + } + vector<Constraint>::const_iterator i, j, eq_end = equalities.end(); for(i = equalities.begin(); i != eq_end; ++i){ Constraint at_i = *i; @@ -1116,14 +1139,190 @@ void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& out, ArithVar v implies(out, eq, ub); } } +} + +void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& lemmas) const{ + for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){ + outputUnateEqualityLemmas(lemmas, v); } +} -void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& lemmas) const{ +void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& lemmas) const{ for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){ - outputAllUnateLemmas(lemmas, v); + outputUnateInequalityLemmas(lemmas, v); } } +void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ + Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl; + Assert(curr != prev); + Assert(curr != NullConstraint); + bool hasPrev = ! (prev == NullConstraint); + Assert(!hasPrev || curr->getValue() > prev->getValue()); + + ++d_statistics.d_unatePropagateCalls; + + const SortedConstraintMap& scm = curr->constraintSet(); + const SortedConstraintMapConstIterator scm_begin = scm.begin(); + SortedConstraintMapConstIterator scm_i = curr->d_variablePosition; + + //Ignore the first ValueCollection + // NOPE: (>= p c) then (= p c) NOPE + // NOPE: (>= p c) then (not (= p c)) NOPE + + while(scm_i != scm_begin){ + --scm_i; // move the iterator back + + const ValueCollection& vc = scm_i->second; + + //If it has the previous element, do nothing and stop! + if(hasPrev && + vc.hasConstraintOfType(prev->getType()) + && vc.getConstraintOfType(prev->getType()) == prev){ + break; + } + + //Don't worry about implying the negation of upperbound. + //These should all be handled by propagating the LowerBounds! + if(vc.hasLowerBound()){ + Constraint lb = vc.getLowerBound(); + if(!lb->isTrue()){ + ++d_statistics.d_unatePropagateImplications; + Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << lb << endl; + lb->impliedBy(curr); + } + } + if(vc.hasDisequality()){ + Constraint dis = vc.getDisequality(); + if(!dis->isTrue()){ + ++d_statistics.d_unatePropagateImplications; + Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << dis << endl; + dis->impliedBy(curr); + } + } + } +} + +void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ + Debug("arith::unate") << "unatePropUpperBound " << curr << " " << prev << endl; + Assert(curr != prev); + Assert(curr != NullConstraint); + bool hasPrev = ! (prev == NullConstraint); + Assert(!hasPrev || curr->getValue() < prev->getValue()); + + ++d_statistics.d_unatePropagateCalls; + + const SortedConstraintMap& scm = curr->constraintSet(); + const SortedConstraintMapConstIterator scm_end = scm.end(); + SortedConstraintMapConstIterator scm_i = curr->d_variablePosition; + ++scm_i; + for(; scm_i != scm_end; ++scm_i){ + const ValueCollection& vc = scm_i->second; + + //If it has the previous element, do nothing and stop! + if(hasPrev && + vc.hasConstraintOfType(prev->getType()) && + vc.getConstraintOfType(prev->getType()) == prev){ + break; + } + //Don't worry about implying the negation of upperbound. + //These should all be handled by propagating the UpperBounds! + if(vc.hasUpperBound()){ + Constraint ub = vc.getUpperBound(); + if(!ub->isTrue()){ + ++d_statistics.d_unatePropagateImplications; + Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << ub << endl; + ub->impliedBy(curr); + } + } + if(vc.hasDisequality()){ + Constraint dis = vc.getDisequality(); + if(!dis->isTrue()){ + Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl; + ++d_statistics.d_unatePropagateImplications; + dis->impliedBy(curr); + } + } + } +} + +void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB){ + Debug("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " " << prevUB << endl; + Assert(curr != prevLB); + Assert(curr != prevUB); + Assert(curr != NullConstraint); + bool hasPrevLB = ! (prevLB == NullConstraint); + bool hasPrevUB = ! (prevUB == NullConstraint); + Assert(!hasPrevLB || curr->getValue() >= prevLB->getValue()); + Assert(!hasPrevUB || curr->getValue() <= prevUB->getValue()); + + ++d_statistics.d_unatePropagateCalls; + + const SortedConstraintMap& scm = curr->constraintSet(); + SortedConstraintMapConstIterator scm_curr = curr->d_variablePosition; + SortedConstraintMapConstIterator scm_last = hasPrevUB ? prevUB->d_variablePosition : scm.end(); + SortedConstraintMapConstIterator scm_i; + if(hasPrevLB){ + scm_i = prevLB->d_variablePosition; + if(scm_i != scm_curr){ // If this does not move this past scm_curr, move it one forward + ++scm_i; + } + }else{ + scm_i = scm.begin(); + } + + for(; scm_i != scm_curr; ++scm_i){ + // between the previous LB and the curr + const ValueCollection& vc = scm_i->second; + + //Don't worry about implying the negation of upperbound. + //These should all be handled by propagating the LowerBounds! + if(vc.hasLowerBound()){ + Constraint lb = vc.getLowerBound(); + if(!lb->isTrue()){ + ++d_statistics.d_unatePropagateImplications; + Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << lb << endl; + lb->impliedBy(curr); + } + } + if(vc.hasDisequality()){ + Constraint dis = vc.getDisequality(); + if(!dis->isTrue()){ + ++d_statistics.d_unatePropagateImplications; + Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl; + dis->impliedBy(curr); + } + } + } + Assert(scm_i == scm_curr); + if(!hasPrevUB || scm_i != scm_last){ + ++scm_i; + } // hasPrevUB implies scm_i != scm_last + + for(; scm_i != scm_last; ++scm_i){ + // between the curr and the previous UB imply the upperbounds and disequalities. + const ValueCollection& vc = scm_i->second; + + //Don't worry about implying the negation of upperbound. + //These should all be handled by propagating the UpperBounds! + if(vc.hasUpperBound()){ + Constraint ub = vc.getUpperBound(); + if(!ub->isTrue()){ + ++d_statistics.d_unatePropagateImplications; + Debug("arith::unate") << "unateProp " << curr << " implies " << ub << endl; + ub->impliedBy(curr); + } + } + if(vc.hasDisequality()){ + Constraint dis = vc.getDisequality(); + if(!dis->isTrue()){ + ++d_statistics.d_unatePropagateImplications; + Debug("arith::unate") << "unateProp " << curr << " implies " << dis << endl; + dis->impliedBy(curr); + } + } + } +} }/* arith namespace */ }/* theory namespace */ diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index fe10ecc4a..5b49dd54d 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -828,14 +828,38 @@ public: */ Constraint getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r); + /** + * Outputs a minimal set of unate implications onto the vector for the variable. + * This outputs lemmas of the general forms + * (= p c) implies (<= p d) for c < d, or + * (= p c) implies (not (= p d)) for c != d. + */ + void outputUnateEqualityLemmas(std::vector<Node>& lemmas) const; + void outputUnateEqualityLemmas(std::vector<Node>& lemmas, ArithVar v) const; /** - * Outputs a minimal set of unate implications on the output channel - * for all variables. + * Outputs a minimal set of unate implications onto the vector for the variable. + * + * If ineqs is true, this outputs lemmas of the general form + * (<= p c) implies (<= p d) for c < d. */ - void outputAllUnateLemmas(std::vector<Node>& lemmas) const; + void outputUnateInequalityLemmas(std::vector<Node>& lemmas) const; + void outputUnateInequalityLemmas(std::vector<Node>& lemmas, ArithVar v) const; + + + void unatePropLowerBound(Constraint curr, Constraint prev); + void unatePropUpperBound(Constraint curr, Constraint prev); + void unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB); + +private: + class Statistics { + public: + IntStat d_unatePropagateCalls; + IntStat d_unatePropagateImplications; - void outputAllUnateLemmas(std::vector<Node>& lemmas, ArithVar v) const; + Statistics(); + ~Statistics(); + } d_statistics; }; /* ConstraintDatabase */ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 31187afd1..b5475586a 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -44,7 +44,7 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, d_pivotsInRound(), d_DELTA_ZERO(0,0) { - switch(Options::ArithPivotRule rule = Options::current()->pivotRule) { + switch(Options::ArithPivotRule rule = Options::current()->arithPivotRule) { case Options::MINIMUM: d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); break; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 524079938..ac9796986 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -92,6 +92,7 @@ TheoryArith::Statistics::Statistics(): d_simplifyTimer("theory::arith::simplifyTimer"), d_staticLearningTimer("theory::arith::staticLearningTimer"), d_presolveTime("theory::arith::presolveTime"), + d_newPropTime("::newPropTimer"), d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0), d_initialTableauSize("theory::arith::initialTableauSize", 0), d_currSetToSmaller("theory::arith::currSetToSmaller", 0), @@ -112,6 +113,7 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_staticLearningTimer); StatisticsRegistry::registerStat(&d_presolveTime); + StatisticsRegistry::registerStat(&d_newPropTime); StatisticsRegistry::registerStat(&d_externalBranchAndBounds); @@ -137,6 +139,7 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_staticLearningTimer); StatisticsRegistry::unregisterStat(&d_presolveTime); + StatisticsRegistry::unregisterStat(&d_newPropTime); StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds); @@ -150,6 +153,16 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_boundPropagations); } +void TheoryArith::revertOutOfConflict(){ + d_partialModel.revertAssignmentChanges(); + clearUpdates(); + d_currentPropagationList.clear(); +} + +void TheoryArith::clearUpdates(){ + d_updatedBounds.purge(); +} + void TheoryArith::zeroDifferenceDetected(ArithVar x){ Assert(d_congruenceManager.isWatchedVariable(x)); Assert(d_partialModel.upperBoundIsZero(x)); @@ -223,6 +236,9 @@ Node TheoryArith::AssertLower(Constraint constraint){ } } + d_currentPropagationList.push_back(constraint); + d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i)); + d_partialModel.setLowerBoundConstraint(constraint); if(d_congruenceManager.isWatchedVariable(x_i)){ @@ -306,6 +322,10 @@ Node TheoryArith::AssertUpper(Constraint constraint){ } + d_currentPropagationList.push_back(constraint); + d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i)); + //It is fine if this is NullConstraint + d_partialModel.setUpperBoundConstraint(constraint); if(d_congruenceManager.isWatchedVariable(x_i)){ @@ -380,6 +400,9 @@ Node TheoryArith::AssertEquality(Constraint constraint){ // 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_currentPropagationList.push_back(constraint); + d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i)); + d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i)); d_partialModel.setUpperBoundConstraint(constraint); d_partialModel.setLowerBoundConstraint(constraint); @@ -1128,6 +1151,7 @@ bool TheoryArith::hasIntegerModel(){ void TheoryArith::check(Effort effortLevel){ + Assert(d_currentPropagationList.empty()); Debug("arith") << "TheoryArith::check begun" << std::endl; d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done(); @@ -1137,17 +1161,16 @@ void TheoryArith::check(Effort effortLevel){ Node possibleConflict = assertionCases(assertion); if(!possibleConflict.isNull()){ - d_partialModel.revertAssignmentChanges(); + revertOutOfConflict(); + Debug("arith::conflict") << "conflict " << possibleConflict << endl; - clearUpdates(); d_out->conflict(possibleConflict); return; } if(d_congruenceManager.inConflict()){ Node c = d_congruenceManager.conflict(); - d_partialModel.revertAssignmentChanges(); + revertOutOfConflict(); Debug("arith::conflict") << "difference manager conflict " << c << endl; - clearUpdates(); d_out->conflict(c); return; } @@ -1162,38 +1185,84 @@ void TheoryArith::check(Effort effortLevel){ Assert(d_conflicts.empty()); bool foundConflict = d_simplex.findModel(); if(foundConflict){ - d_partialModel.revertAssignmentChanges(); - clearUpdates(); + revertOutOfConflict(); Assert(!d_conflicts.empty()); for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){ Node conflict = d_conflicts[i]; Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl; - d_out->conflict(conflict); + d_out->conflict(conflict); } emmittedConflictOrSplit = true; }else{ d_partialModel.commitAssignmentChanges(); } + if(!emmittedConflictOrSplit && + (Options::current()->arithPropagationMode == Options::UNATE_PROP || + Options::current()->arithPropagationMode == Options::BOTH_PROP)){ + TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); + + while(!d_currentPropagationList.empty()){ + Constraint curr = d_currentPropagationList.front(); + d_currentPropagationList.pop_front(); + + ConstraintType t = curr->getType(); + Assert(t != Disequality, "Disequalities are not allowed in d_currentPropagation"); + + + switch(t){ + case LowerBound: + { + Constraint prev = d_currentPropagationList.front(); + d_currentPropagationList.pop_front(); + d_constraintDatabase.unatePropLowerBound(curr, prev); + break; + } + case UpperBound: + { + Constraint prev = d_currentPropagationList.front(); + d_currentPropagationList.pop_front(); + d_constraintDatabase.unatePropUpperBound(curr, prev); + break; + } + case Equality: + { + Constraint prevLB = d_currentPropagationList.front(); + d_currentPropagationList.pop_front(); + Constraint prevUB = d_currentPropagationList.front(); + d_currentPropagationList.pop_front(); + d_constraintDatabase.unatePropEquality(curr, prevLB, prevUB); + break; + } + default: + Unhandled(curr->getType()); + } + } + }else{ + TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); + d_currentPropagationList.clear(); + } + Assert( d_currentPropagationList.empty()); + if(!emmittedConflictOrSplit && fullEffort(effortLevel)){ emmittedConflictOrSplit = splitDisequalities(); } - Node possibleConflict = Node::null(); if(!emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()){ - - if(!emmittedConflictOrSplit && Options::current()->dioSolver){ + Node possibleConflict = Node::null(); + if(!emmittedConflictOrSplit && Options::current()->arithDioSolver){ possibleConflict = callDioSolver(); if(possibleConflict != Node::null()){ + revertOutOfConflict(); Debug("arith::conflict") << "dio conflict " << possibleConflict << endl; d_out->conflict(possibleConflict); emmittedConflictOrSplit = true; } } - if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->dioSolver){ + if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->arithDioSolver){ Node possibleLemma = dioCutting(); if(!possibleLemma.isNull()){ Debug("arith") << "dio cut " << possibleLemma << endl; @@ -1358,7 +1427,9 @@ Node TheoryArith::explain(TNode n) { void TheoryArith::propagate(Effort e) { - if(Options::current()->arithPropagation && hasAnyUpdates()){ + if((Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP || + Options::current()->arithPropagationMode == Options::BOTH_PROP) + && hasAnyUpdates()){ propagateCandidates(); }else{ clearUpdates(); @@ -1616,17 +1687,42 @@ void TheoryArith::presolve(){ callCount = callCount + 1; } - if(Options::current()->arithPropagation ){ - vector<Node> lemmas; - d_constraintDatabase.outputAllUnateLemmas(lemmas); - vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end(); - for(; i != i_end; ++i){ - Node lem = *i; - Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl; - d_out->lemma(lem); - } + vector<Node> lemmas; + switch(Options::current()->arithUnateLemmaMode){ + case Options::NO_PRESOLVE_LEMMAS: + break; + case Options::INEQUALITY_PRESOLVE_LEMMAS: + d_constraintDatabase.outputUnateInequalityLemmas(lemmas); + break; + case Options::EQUALITY_PRESOLVE_LEMMAS: + d_constraintDatabase.outputUnateEqualityLemmas(lemmas); + break; + case Options::ALL_PRESOLVE_LEMMAS: + d_constraintDatabase.outputUnateInequalityLemmas(lemmas); + d_constraintDatabase.outputUnateEqualityLemmas(lemmas); + break; + default: + Unhandled(Options::current()->arithUnateLemmaMode); } + vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end(); + for(; i != i_end; ++i){ + Node lem = *i; + Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl; + d_out->lemma(lem); + } + + // if(Options::current()->arithUnateLemmaMode == Options::ALL_UNATE){ + // vector<Node> lemmas; + // d_constraintDatabase.outputAllUnateLemmas(lemmas); + // vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end(); + // for(; i != i_end; ++i){ + // Node lem = *i; + // Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl; + // d_out->lemma(lem); + // } + // } + d_learner.clear(); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 431c82476..ebc131b60 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -160,11 +160,26 @@ private: Comparison mkIntegerEqualityFromAssignment(ArithVar v); /** - * List of all of the inequalities asserted in the current context. + * List of all of the disequalities asserted in the current context that are not known + * to be satisfied. */ - //context::CDHashSet<Node, NodeHashFunction> d_diseq; context::CDQueue<Constraint> d_diseqQueue; + /** + * Constraints that have yet to be processed by proagation work list. + * All of the elements have type of LowerBound, UpperBound, or + * Equality. + * + * This is empty at the beginning of every check call. + * + * If head()->getType() == LowerBound or UpperBound, + * then d_cPL[1] is the previous constraint in d_partialModel for the + * corresponding bound. + * If head()->getType() == Equality, + * then d_cPL[1] is the previous lowerBound in d_partialModel, + * and d_cPL[2] is the previous upperBound in d_partialModel. + */ + std::deque<Constraint> d_currentPropagationList; /** * Manages information about the assignment and upper and lower bounds on @@ -380,7 +395,9 @@ private: DenseSet d_candidateBasics; bool hasAnyUpdates() { return !d_updatedBounds.empty(); } - void clearUpdates(){ d_updatedBounds.purge(); } + void clearUpdates(); + + void revertOutOfConflict(); void propagateCandidates(); void propagateCandidate(ArithVar basic); @@ -445,6 +462,8 @@ private: TimerStat d_presolveTime; + TimerStat d_newPropTime; + IntStat d_externalBranchAndBounds; IntStat d_initialTableauSize; |