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 */
d_propManager(propManager),
d_numVariables(0),
d_delayedLemmas(),
+ d_pivotsInRound(),
d_ZERO(0),
d_DELTA_ZERO(0,0)
{
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);
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);
+ }
}
}
}
while(!d_candidateBasics.empty()){
ArithVar candidate = d_candidateBasics.pop_back();
Assert(d_tableau.isBasic(candidate));
- propagateCandidate(candidate);
+ propagateCandidate(candidate);
}
}
}
}
-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){
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()){
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()){
// 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();
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);
}
}
//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);
--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
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
PermissiveBackArithVarSet d_updatedBounds;
PermissiveBackArithVarSet d_candidateBasics;
+ ArithVarMultiset d_pivotsInRound;
+
Rational d_ZERO;
DeltaRational d_DELTA_ZERO;
*/
Node updateInconsistentVars();
private:
- template <PreferenceFunction> Node searchForFeasibleSolution(uint32_t maxIterations);
+ Node searchForFeasibleSolution(uint32_t maxIterations);
enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch};
* - !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
arithPropagation(false),
satRandomFreq(0.0),
satRandomSeed(91648253),// Minisat's default value
- pivotRule(MINIMUM)
+ pivotRule(MINIMUM),
+ arithPivotThreshold(10),
+ arithPropagateMaxLength(10)
{
}
--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\
RANDOM_FREQUENCY,
RANDOM_SEED,
ENABLE_VARIABLE_REMOVAL,
- ARITHMETIC_PROPAGATION
+ ARITHMETIC_PROPAGATION,
+ ARITHMETIC_PIVOT_THRESHOLD,
+ ARITHMETIC_PROP_MAX_LENGTH
};/* enum OptionValue */
/**
{ "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 },
}
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");
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();
/**
projects / cvc5.git / commitdiff