From e0926408ef5113bf261d6205c218e5d529040108 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 30 Jun 2011 18:40:29 +0000 Subject: [PATCH] Merging the playground branch upto r1957 into trunk. --- src/theory/arith/arithvar_set.h | 145 ++++++++++++++++++++++++++++++++ src/theory/arith/simplex.cpp | 42 ++++++--- src/theory/arith/simplex.h | 14 +-- src/util/options.cpp | 20 ++++- src/util/options.h | 11 +++ 5 files changed, 212 insertions(+), 20 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 ArithVarSet; typedef ArithVarSetImpl PermissiveBackArithVarSet; + +/** + * ArithVarMultiset + */ +class ArithVarMultiset { +public: + typedef std::vector 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 d_posVector; + + //Count of the number of elements in the array + std::vector 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 -ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ +template +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(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(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(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(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 +//template 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(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(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 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 ArithVar selectSlack(ArithVar x_i); - template ArithVar selectSlackLowerBound(ArithVar x_i) { - return selectSlack(x_i); + template ArithVar selectSlack(ArithVar x_i, PreferenceFunction pf); + ArithVar selectSlackLowerBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) { + return selectSlack(x_i, pf); } - template ArithVar selectSlackUpperBound(ArithVar x_i) { - return selectSlack(x_i); + ArithVar selectSlackUpperBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) { + return selectSlack(x_i, pf); } /** * Returns the smallest basic variable whose assignment is not consistent diff --git a/src/util/options.cpp b/src/util/options.cpp index 32be9d6c9..e49ed77e9 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -86,7 +86,9 @@ Options::Options() : arithPropagation(false), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value - pivotRule(MINIMUM) + pivotRule(MINIMUM), + arithPivotThreshold(10), + arithPropagateMaxLength(10) { } @@ -121,6 +123,8 @@ static const string optionsDescription = "\ --replay=file replay decisions from file\n\ --replay-log=file log decisions and propagations to file\n\ --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ + --pivot-threshold=N sets the number of heuristic pivots per variable per simplex instance\n\ + --prop-row-length=N sets the maximum row length to be used in propagation\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ --enable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ @@ -214,7 +218,9 @@ enum OptionValue { RANDOM_FREQUENCY, RANDOM_SEED, ENABLE_VARIABLE_REMOVAL, - ARITHMETIC_PROPAGATION + ARITHMETIC_PROPAGATION, + ARITHMETIC_PIVOT_THRESHOLD, + ARITHMETIC_PROP_MAX_LENGTH };/* enum OptionValue */ /** @@ -280,6 +286,8 @@ static struct option cmdlineOptions[] = { { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING }, { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING }, { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, + { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD }, + { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, { "enable-variable-removal", no_argument, NULL, ENABLE_VARIABLE_REMOVAL }, @@ -574,6 +582,14 @@ throw(OptionException) { } break; + case ARITHMETIC_PIVOT_THRESHOLD: + arithPivotThreshold = atoi(optarg); + break; + + case ARITHMETIC_PROP_MAX_LENGTH: + arithPropagateMaxLength = atoi(optarg); + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); diff --git a/src/util/options.h b/src/util/options.h index b8d21f2b0..a5e03d21b 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -181,6 +181,17 @@ struct CVC4_PUBLIC Options { typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; ArithPivotRule pivotRule; + /** + * The number of pivots before Bland's pivot rule is used on a basic + * variable in arithmetic. + */ + uint16_t arithPivotThreshold; + + /** + * The maximum row length that arithmetic will use for propagation. + */ + uint16_t arithPropagateMaxLength; + Options(); /** -- 2.30.2