diff options
author | Tim King <taking@cs.nyu.edu> | 2011-02-24 20:36:35 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-02-24 20:36:35 +0000 |
commit | 1d64c07f3eb160d297e786b31dac6ed05cd05a1a (patch) | |
tree | da0c29ebb94a6fcbdcce8355308560d5f59eea3e /src/theory/arith/simplex.cpp | |
parent | d21fc6157aa190944d9e3181de883c080cb6ce3f (diff) |
- Adds an additional mode to ArithPriorityQueue, Collection. Collection is a mode where the heap structure is not maintained. There is just a list of variables that may be inconsistent. This is used up until the simplex procedure is invoked.
- Misc. cleanup and renaming in ArithPriorityQueue.
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 4efa5fa43..ced76c843 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -342,7 +342,7 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ ArithVar slack = ARITHVAR_SENTINEL; uint32_t numRows = std::numeric_limits<uint32_t>::max(); - bool pivotStage = d_queue.usingGriggioRule(); + bool pivotStage = d_queue.inDifferenceMode(); for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); nbi != end; ++nbi){ @@ -410,10 +410,10 @@ Node SimplexDecisionProcedure::selectInitialConflict() { TimerStat::CodeTimer codeTimer(d_statistics.d_selectInitialConflictTime); int conflictChanges = 0; - ArithPriorityQueue::GriggioPQueue::const_iterator i = d_queue.queueAsListBegin(); - ArithPriorityQueue::GriggioPQueue::const_iterator end = d_queue.queueAsListEnd(); + ArithPriorityQueue::const_iterator i = d_queue.begin(); + ArithPriorityQueue::const_iterator end = d_queue.end(); for(; i != end; ++i){ - ArithVar x_i = (*i).variable(); + ArithVar x_i = *i; if(d_tableau.isBasic(x_i)){ Node possibleConflict = checkBasicForConflict(x_i); @@ -441,6 +441,8 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ d_foundAConflict = false; d_pivotsSinceConflict = 0; + d_queue.transitionToDifferenceMode(); + Node possibleConflict = Node::null(); if(d_queue.size() > 1){ possibleConflict = selectInitialConflict(); @@ -450,7 +452,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ } if(!d_queue.empty() && possibleConflict.isNull()){ - d_queue.useBlandQueue(); + d_queue.transitionToVariableOrderMode(); possibleConflict = searchForFeasibleSolution<false>(0); } @@ -460,10 +462,11 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ // means that the assignment we can always empty these queues. d_queue.clear(); - if(!d_queue.usingGriggioRule()){ - d_queue.useGriggioQueue(); - } - Assert(d_queue.usingGriggioRule()); + Assert(!d_queue.inCollectionMode()); + d_queue.transitionToCollectionMode(); + + + Assert(d_queue.inCollectionMode()); return possibleConflict; } |