diff options
author | Tim King <taking@cs.nyu.edu> | 2011-06-30 18:40:29 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-06-30 18:40:29 +0000 |
commit | e0926408ef5113bf261d6205c218e5d529040108 (patch) | |
tree | a55db2781e4decbf3857d9a04a3b092b7c4984e9 /src/theory/arith | |
parent | 29cf5a3812f1edafc3c233483c65f0cc4b125295 (diff) |
Merging the playground branch upto r1957 into trunk.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arithvar_set.h | 145 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 42 | ||||
-rw-r--r-- | src/theory/arith/simplex.h | 14 |
3 files changed, 183 insertions, 18 deletions
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index 4cd205172..f8a23fee0 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -179,6 +179,151 @@ public: typedef ArithVarSetImpl<false> ArithVarSet; typedef ArithVarSetImpl<true> PermissiveBackArithVarSet; + +/** + * ArithVarMultiset + */ +class ArithVarMultiset { +public: + typedef std::vector<ArithVar> VarList; +private: + //List of the ArithVars in the multi set. + VarList d_list; + + //Each ArithVar in the set is mapped to its position in d_list. + //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL + std::vector<unsigned> d_posVector; + + //Count of the number of elements in the array + std::vector<unsigned> d_counts; + +public: + typedef VarList::const_iterator const_iterator; + + ArithVarMultiset() : d_list(), d_posVector() {} + + size_t size() const { + return d_list.size(); + } + + bool empty() const { + return d_list.empty(); + } + + size_t allocated() const { + Assert(d_posVector.size() == d_counts.size()); + return d_posVector.size(); + } + + void purge() { + for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end(); i!= endIter; ++i){ + d_posVector[*i] = ARITHVAR_SENTINEL; + d_counts[*i] = 0; + } + d_list.clear(); + Assert(empty()); + } + + void increaseSize(ArithVar max){ + Assert(max >= allocated()); + d_posVector.resize(max+1, ARITHVAR_SENTINEL); + d_counts.resize(max+1, 0); + } + + void increaseSize(){ + increaseSize(allocated()); + } + + bool isMember(ArithVar x) const{ + if( x >= allocated()){ + return false; + }else{ + Assert(x < allocated()); + return d_posVector[x] != ARITHVAR_SENTINEL; + } + } + + /** Invalidates iterators */ + /* void init(ArithVar x, bool val) { */ + /* Assert(x >= allocated()); */ + /* increaseSize(x); */ + /* if(val){ */ + /* add(x); */ + /* } */ + /* } */ + + /** + * Invalidates iterators. + */ + void addMultiset(ArithVar x){ + if( x >= allocated()){ + increaseSize(x); + } + if(d_counts[x] == 0){ + d_posVector[x] = size(); + d_list.push_back(x); + } + d_counts[x]++; + } + + unsigned count(ArithVar x){ + if( x >= allocated()){ + return 0; + }else{ + return d_counts[x]; + } + } + + const_iterator begin() const{ return d_list.begin(); } + const_iterator end() const{ return d_list.end(); } + + const VarList& getList() const{ + return d_list; + } + + /** Invalidates iterators */ + void remove(ArithVar x){ + Assert(isMember(x)); + swapToBack(x); + Assert(d_list.back() == x); + pop_back(); + } + + ArithVar pop_back() { + Assert(!empty()); + ArithVar atBack = d_list.back(); + d_posVector[atBack] = ARITHVAR_SENTINEL; + d_counts[atBack] = 0; + d_list.pop_back(); + return atBack; + } + + private: + + /** This should be true of all x < allocated() after every operation. */ + bool wellFormed(ArithVar x){ + if(d_posVector[x] == ARITHVAR_SENTINEL){ + return true; + }else{ + return d_list[d_posVector[x]] == x; + } + } + + /** Swaps a member x to the back of d_list. */ + void swapToBack(ArithVar x){ + Assert(isMember(x)); + + unsigned currentPos = d_posVector[x]; + ArithVar atBack = d_list.back(); + + d_list[currentPos] = atBack; + d_posVector[atBack] = currentPos; + + d_list[size() - 1] = x; + d_posVector[x] = size() - 1; + } +}; + }; /* namespace arith */ }; /* namespace theory */ }; /* namespace CVC4 */ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 113e80c27..3e2d90674 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -23,6 +23,7 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager d_propManager(propManager), d_numVariables(0), d_delayedLemmas(), + d_pivotsInRound(), d_ZERO(0), d_DELTA_ZERO(0,0) { @@ -377,7 +378,8 @@ void SimplexDecisionProcedure::propagateCandidates(){ PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end(); for(; i != end; ++i){ ArithVar var = *i; - if(d_tableau.isBasic(var)){ + if(d_tableau.isBasic(var) && + d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){ d_candidateBasics.softAdd(var); }else{ Tableau::ColIterator basicIter = d_tableau.colIterator(var); @@ -386,7 +388,9 @@ void SimplexDecisionProcedure::propagateCandidates(){ ArithVar rowVar = entry.getRowVar(); Assert(entry.getColVar() == var); Assert(d_tableau.isBasic(rowVar)); - d_candidateBasics.softAdd(rowVar); + if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){ + d_candidateBasics.softAdd(rowVar); + } } } } @@ -395,7 +399,7 @@ void SimplexDecisionProcedure::propagateCandidates(){ while(!d_candidateBasics.empty()){ ArithVar candidate = d_candidateBasics.pop_back(); Assert(d_tableau.isBasic(candidate)); - propagateCandidate(candidate); + propagateCandidate(candidate); } } @@ -521,8 +525,8 @@ ArithVar SimplexDecisionProcedure::minBoundAndRowCount(const SimplexDecisionProc } } -template <bool above, SimplexDecisionProcedure::PreferenceFunction pref> -ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ +template <bool above> +ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, SimplexDecisionProcedure::PreferenceFunction pref){ ArithVar slack = ARITHVAR_SENTINEL; for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){ @@ -616,7 +620,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ possibleConflict.isNull() && pivotsRemaining > 0){ uint32_t pivotsToDo = min(pivotsPerCheck, pivotsRemaining); - possibleConflict = searchForFeasibleSolution<minBoundAndRowCount>(pivotsToDo); + possibleConflict = searchForFeasibleSolution(pivotsToDo); pivotsRemaining -= pivotsToDo; //Once every CHECK_PERIOD examine the entire queue for conflicts if(possibleConflict.isNull()){ @@ -631,7 +635,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ d_queue.transitionToVariableOrderMode(); while(!d_queue.empty() && possibleConflict.isNull()){ - possibleConflict = searchForFeasibleSolution<minVarOrder>(VARORDER_CHECK_PERIOD); + possibleConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD); //Once every CHECK_PERIOD examine the entire queue for conflicts if(possibleConflict.isNull()){ @@ -647,6 +651,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ // Curiously the invariant that we always do a full check // means that the assignment we can always empty these queues. d_queue.clear(); + d_pivotsInRound.purge(); Assert(!d_queue.inCollectionMode()); d_queue.transitionToCollectionMode(); @@ -666,12 +671,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ const DeltaRational& beta = d_partialModel.getAssignment(basic); if(d_partialModel.belowLowerBound(basic, beta, true)){ - ArithVar x_j = selectSlackUpperBound<minVarOrder>(basic); + ArithVar x_j = selectSlackUpperBound(basic); if(x_j == ARITHVAR_SENTINEL ){ return generateConflictBelowLowerBound(basic); } }else if(d_partialModel.aboveUpperBound(basic, beta, true)){ - ArithVar x_j = selectSlackLowerBound<minVarOrder>(basic); + ArithVar x_j = selectSlackLowerBound(basic); if(x_j == ARITHVAR_SENTINEL ){ return generateConflictAboveUpperBound(basic); } @@ -680,7 +685,7 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ } //corresponds to Check() in dM06 -template <SimplexDecisionProcedure::PreferenceFunction pf> +//template <SimplexDecisionProcedure::PreferenceFunction pf> Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ Debug("arith") << "updateInconsistentVars" << endl; Assert(remainingIterations > 0); @@ -697,11 +702,24 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera --remainingIterations; + bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= Options::current()->arithPivotThreshold; + if(!useVarOrderPivot){ + d_pivotsInRound.addMultiset(x_i); + } + + + Debug("playground") << "pivots in rounds: " << d_pivotsInRound.count(x_i) + << " use " << useVarOrderPivot + << " threshold " << Options::current()->arithPivotThreshold + << endl; + + PreferenceFunction pf = useVarOrderPivot ? minVarOrder : minBoundAndRowCount; + DeltaRational beta_i = d_partialModel.getAssignment(x_i); ArithVar x_j = ARITHVAR_SENTINEL; if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ - x_j = selectSlackUpperBound<pf>(x_i); + x_j = selectSlackUpperBound(x_i, pf); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictBelowLowerBound(x_i); //unsat @@ -710,7 +728,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera pivotAndUpdate(x_i, x_j, l_i); }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ - x_j = selectSlackLowerBound<pf>(x_i); + x_j = selectSlackLowerBound(x_i, pf); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictAboveUpperBound(x_i); //unsat diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index f0dc5d62e..b3f43baf1 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -43,6 +43,8 @@ private: PermissiveBackArithVarSet d_updatedBounds; PermissiveBackArithVarSet d_candidateBasics; + ArithVarMultiset d_pivotsInRound; + Rational d_ZERO; DeltaRational d_DELTA_ZERO; @@ -139,7 +141,7 @@ public: */ Node updateInconsistentVars(); private: - template <PreferenceFunction> Node searchForFeasibleSolution(uint32_t maxIterations); + Node searchForFeasibleSolution(uint32_t maxIterations); enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch}; @@ -159,12 +161,12 @@ private: * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j) * */ - template <bool lowerBound, PreferenceFunction> ArithVar selectSlack(ArithVar x_i); - template <PreferenceFunction pf> ArithVar selectSlackLowerBound(ArithVar x_i) { - return selectSlack<true, pf>(x_i); + template <bool lowerBound> ArithVar selectSlack(ArithVar x_i, PreferenceFunction pf); + ArithVar selectSlackLowerBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) { + return selectSlack<true>(x_i, pf); } - template <PreferenceFunction pf> ArithVar selectSlackUpperBound(ArithVar x_i) { - return selectSlack<false, pf>(x_i); + ArithVar selectSlackUpperBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) { + return selectSlack<false>(x_i, pf); } /** * Returns the smallest basic variable whose assignment is not consistent |