From 52c5c282f47448856e0dec8a7d4e5de612a8dcc3 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 22 May 2012 15:09:03 +0000 Subject: [PATCH] This commit merges in the branch arithmetic/cprop. --- src/theory/arith/constraint.cpp | 241 +++++++++++++++++++++++--- src/theory/arith/constraint.h | 32 +++- src/theory/arith/simplex.cpp | 2 +- src/theory/arith/theory_arith.cpp | 138 ++++++++++++--- src/theory/arith/theory_arith.h | 25 ++- src/util/options.cpp | 207 ++++++++++++++++------ src/util/options.h | 40 +++-- test/unit/theory/theory_arith_white.h | 20 ++- 8 files changed, 581 insertions(+), 124 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& out, Constraint a, Constraint b){ out.push_back(orderOr); } -void ConstraintDatabase::outputAllUnateLemmas(std::vector& out, ArithVar v) const{ +void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& out, ArithVar v) const{ SortedConstraintMap& scm = getVariableSCM(v); - - SortedConstraintMapConstIterator outer; + SortedConstraintMapConstIterator scm_iter = scm.begin(); SortedConstraintMapConstIterator scm_end = scm.end(); - - vector 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& out, ArithVar v } } } +} + +void ConstraintDatabase::outputUnateEqualityLemmas(std::vector& out, ArithVar v) const{ + + vector 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::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& out, ArithVar v implies(out, eq, ub); } } +} + +void ConstraintDatabase::outputUnateEqualityLemmas(std::vector& lemmas) const{ + for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){ + outputUnateEqualityLemmas(lemmas, v); } +} -void ConstraintDatabase::outputAllUnateLemmas(std::vector& lemmas) const{ +void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& 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& lemmas) const; + void outputUnateEqualityLemmas(std::vector& 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& lemmas) const; + void outputUnateInequalityLemmas(std::vector& lemmas) const; + void outputUnateInequalityLemmas(std::vector& 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& 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 lemmas; - d_constraintDatabase.outputAllUnateLemmas(lemmas); - vector::const_iterator i = lemmas.begin(), i_end = lemmas.end(); - for(; i != i_end; ++i){ - Node lem = *i; - Debug("arith::oldprop") << " lemma lemma duck " <lemma(lem); - } + vector 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::const_iterator i = lemmas.begin(), i_end = lemmas.end(); + for(; i != i_end; ++i){ + Node lem = *i; + Debug("arith::oldprop") << " lemma lemma duck " <lemma(lem); + } + + // if(Options::current()->arithUnateLemmaMode == Options::ALL_UNATE){ + // vector lemmas; + // d_constraintDatabase.outputAllUnateLemmas(lemmas); + // vector::const_iterator i = lemmas.begin(), i_end = lemmas.end(); + // for(; i != i_end; ++i){ + // Node lem = *i; + // Debug("arith::oldprop") << " lemma lemma duck " <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 d_diseq; context::CDQueue 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 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; diff --git a/src/util/options.cpp b/src/util/options.cpp index e41959da2..a510f35f8 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -101,21 +101,22 @@ Options::Options() : replayFilename(""), replayStream(NULL), replayLog(NULL), - arithPropagation(true), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value satVarDecay(0.95), satClauseDecay(0.999), satRestartFirst(25), satRestartInc(3.0), - pivotRule(MINIMUM), + arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS), + arithPropagationMode(BOTH_PROP), + arithPivotRule(MINIMUM), arithPivotThreshold(16), arithPropagateMaxLength(16), - ufSymmetryBreaker(false), - ufSymmetryBreakerSetByUser(false), - dioSolver(true), + arithDioSolver(true), arithRewriteEq(false), arithRewriteEqSetByUser(false), + ufSymmetryBreaker(false), + ufSymmetryBreakerSetByUser(false), lemmaOutputChannel(NULL), lemmaInputChannel(NULL), threads(2),// default should be 1 probably, but say 2 for now @@ -134,8 +135,10 @@ static const string mostCommonOptionsDescription = "\ Most commonly-used CVC4 options:\n\ --version | -V identify this CVC4 binary\n\ --help | -h full command line reference\n\ - --lang | -L force input language (default is `auto'; see --lang help)\n\ - --output-lang force output language (default is `auto'; see --lang help)\n\ + --lang | -L force input language\n\ + (default is `auto'; see --lang help)\n\ + --output-lang force output language\n\ + (default is `auto'; see --lang help)\n\ --verbose | -v increase verbosity (may be repeated)\n\ --quiet | -q decrease verbosity (may be repeated)\n\ --stats give statistics on exit\n\ @@ -165,7 +168,8 @@ Additional CVC4 options:\n\ --mmap memory map file input\n\ --segv-nospin don't spin on segfault waiting for gdb\n\ --lazy-type-checking type check expressions only when necessary (default)\n\ - --eager-type-checking type check expressions immediately on creation (debug builds only)\n\ + --eager-type-checking type check expressions immediately on creation\n\ + (debug builds only)\n\ --no-type-checking never type check expressions\n\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ @@ -185,18 +189,35 @@ Additional CVC4 options:\n\ --no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ --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\ + SAT:\n\ + --random-freq=P frequency of random decisions in the sat solver\n\ + (P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ - --restart-int-base=I sets the base restart interval for the sat solver (I=25 by default)\n\ - --restart-int-inc=F sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\ - --disable-arithmetic-propagation turns on arithmetic propagation\n\ - --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ + --restart-int-base=I sets the base restart interval for the sat solver\n\ + (I=25 by default)\n\ + --restart-int-inc=F restart interval increase factor for the sat solver\n\ + (F=3.0 by default)\n\ + ARITHMETIC:\n\ + --arith-presolve-lemmas=MODE determines which lemmas to add before solving\n\ + (default is 'all', see --arith-presolve-lemmas=help)\n\ + --arith-prop=MODE turns on arithmetic propagation\n\ + (default is 'old', see --arith-prop=help)\n\ + --pivot-rule=RULE change the pivot rule for the basic variable\n\ + (default is 'min', see --pivot-rule help)\n\ + --pivot-threshold=N sets the number of pivots using --pivot-rule\n\ + per basic variable per simplex instance before\n\ + using variable order\n\ + --prop-row-length=N sets the maximum row length to be used in propagation\n\ + --disable-dio-solver turns off Linear Diophantine Equation solver \n\ + (Griggio, JSAT 2012)\n\ + --enable-arith-rewrite-equalities turns on the preprocessing rewrite\n\ + turning equalities into a conjunction of inequalities.\n \ + --disable-arith-rewrite-equalities turns off the preprocessing rewrite\n\ + turning equalities into a conjunction of inequalities.\n \ + UF:\n\ + --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\ + CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ - --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ - --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\ --threads=N sets the number of solver threads\n\ --threadN=string configures thread N (0..#threads-1)\n\ --filter-lemma-length=N don't share lemmas strictly longer than N\n\ @@ -315,6 +336,44 @@ pipe to perform on-line checking. The --dump-to option can be used to dump\n\ to a file.\n\ "; +static const string arithPresolveLemmasHelp = "\ +Presolve lemmas are generated before SAT search begins using the relationship\n\ +of constant terms and polynomials.\n\ +Modes currently supported by the --arith-presolve-lemmas option:\n\ ++ none \n\ ++ ineqs \n\ + Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\ ++ eqs \n\ + Outputs lemmas of the general forms\n\ + (= p c) implies (<= p d) for c < d, or\n\ + (= p c) implies (not (= p d)) for c != d.\n\ ++ all \n\ + A combination of inequalities and equalities.\n\ +"; + +static const string propagationModeHelp = "\ +This decides on kind of propagation arithmetic attempts to do during the search.\n\ ++ none\n\ ++ unate\n\ + use constraints to do unate propagation\n\ ++ bi (Bounds Inference)\n\ + infers bounds on basic variables using the upper and lower bounds of the\n\ + non-basic variables in the tableau.\n\ ++both\n\ +"; + +static const string pivotRulesHelp = "\ +This decides on the rule used by simplex during hueristic rounds\n\ +for deciding the next basic variable to select.\n\ +Pivot rules available:\n\ ++min\n\ + The minimum abs() value of the variable's violation of its bound. (default)\n\ ++min-break-ties\n\ + The minimum violation with ties broken by variable order (total)\n\ ++max\n\ + The maximum violation the bound\n\ +"; + string Options::getDescription() const { return optionsDescription; } @@ -341,7 +400,8 @@ void Options::printLanguageHelp(std::ostream& out) { * any collision. */ enum OptionValue { - SMTCOMP = 256, /* avoid clashing with char options */ + OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */ + SMTCOMP, STATS, SEGV_NOSPIN, OUTPUT_LANGUAGE, @@ -377,13 +437,14 @@ enum OptionValue { EAGER_TYPE_CHECKING, REPLAY, REPLAY_LOG, - PIVOT_RULE, PRINT_WINNER, RANDOM_FREQUENCY, RANDOM_SEED, SAT_RESTART_FIRST, SAT_RESTART_INC, - ARITHMETIC_PROPAGATION, + ARITHMETIC_UNATE_LEMMA_MODE, + ARITHMETIC_PROPAGATION_MODE, + ARITHMETIC_PIVOT_RULE, ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH, ARITHMETIC_DIO_SOLVER, @@ -401,7 +462,8 @@ enum OptionValue { BITVECTOR_EAGER_BITBLAST, BITVECTOR_SHARE_LEMMAS, BITVECTOR_EAGER_FULLCHECK, - SAT_REFINE_CONFLICTS + SAT_REFINE_CONFLICTS, + OPTION_VALUE_END };/* enum OptionValue */ /** @@ -475,15 +537,16 @@ static struct option cmdlineOptions[] = { { "incremental", no_argument , NULL, 'i' }, { "replay" , required_argument, NULL, REPLAY }, { "replay-log" , required_argument, NULL, REPLAY_LOG }, - { "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 }, { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST }, { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC }, { "print-winner", no_argument , NULL, PRINT_WINNER }, - { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, + { "unate-lemmas", required_argument, NULL, ARITHMETIC_UNATE_LEMMA_MODE }, + { "arith-prop", required_argument, NULL, ARITHMETIC_PROPAGATION_MODE }, + { "pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE }, + { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD }, + { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER }, { "enable-arith-rewrite-equalities", no_argument, NULL, ENABLE_ARITHMETIC_REWRITE_EQUALITIES }, { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES }, @@ -878,24 +941,6 @@ throw(OptionException) { #endif /* CVC4_REPLAY */ break; - case ARITHMETIC_PROPAGATION: - arithPropagation = false; - break; - - case ARITHMETIC_DIO_SOLVER: - dioSolver = false; - break; - - case ENABLE_ARITHMETIC_REWRITE_EQUALITIES: - arithRewriteEq = true; - arithRewriteEqSetByUser = true; - break; - - case DISABLE_ARITHMETIC_REWRITE_EQUALITIES: - arithRewriteEq = false; - arithRewriteEqSetByUser = true; - break; - case ENABLE_SYMMETRY_BREAKER: ufSymmetryBreaker = true; ufSymmetryBreakerSetByUser = true; @@ -993,21 +1038,62 @@ throw(OptionException) { } break; - case PIVOT_RULE: + case ARITHMETIC_UNATE_LEMMA_MODE: + if(!strcmp(optarg, "all")) { + arithUnateLemmaMode = ALL_PRESOLVE_LEMMAS; + break; + } else if(!strcmp(optarg, "none")) { + arithUnateLemmaMode = NO_PRESOLVE_LEMMAS; + break; + } else if(!strcmp(optarg, "ineqs")) { + arithUnateLemmaMode = INEQUALITY_PRESOLVE_LEMMAS; + break; + } else if(!strcmp(optarg, "eqs")) { + arithUnateLemmaMode = EQUALITY_PRESOLVE_LEMMAS; + break; + } else if(!strcmp(optarg, "help")) { + puts(arithPresolveLemmasHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --arith-presolve-lemmas: `") + + optarg + "'. Try --arith-presolve-lemmas=help."); + } + break; + + case ARITHMETIC_PROPAGATION_MODE: + if(!strcmp(optarg, "none")) { + arithPropagationMode = NO_PROP; + break; + } else if(!strcmp(optarg, "unate")) { + arithPropagationMode = UNATE_PROP; + break; + } else if(!strcmp(optarg, "bi")) { + arithPropagationMode = BOUND_INFERENCE_PROP; + break; + } else if(!strcmp(optarg, "both")) { + arithPropagationMode = BOTH_PROP; + break; + } else if(!strcmp(optarg, "help")) { + puts(propagationModeHelp.c_str()); + exit(1); + } else { + throw OptionException(string("unknown option for --arith-prop: `") + + optarg + "'. Try --arith-prop help."); + } + break; + + case ARITHMETIC_PIVOT_RULE: if(!strcmp(optarg, "min")) { - pivotRule = MINIMUM; + arithPivotRule = MINIMUM; break; } else if(!strcmp(optarg, "min-break-ties")) { - pivotRule = BREAK_TIES; + arithPivotRule = BREAK_TIES; break; } else if(!strcmp(optarg, "max")) { - pivotRule = MAXIMUM; + arithPivotRule = MAXIMUM; break; } else if(!strcmp(optarg, "help")) { - printf("Pivot rules available:\n"); - printf("min\n"); - printf("min-break-ties\n"); - printf("max\n"); + puts(pivotRulesHelp.c_str()); exit(1); } else { throw OptionException(string("unknown option for --pivot-rule: `") + @@ -1023,6 +1109,20 @@ throw(OptionException) { arithPropagateMaxLength = atoi(optarg); break; + case ARITHMETIC_DIO_SOLVER: + arithDioSolver = false; + break; + + case ENABLE_ARITHMETIC_REWRITE_EQUALITIES: + arithRewriteEq = true; + arithRewriteEqSetByUser = true; + break; + + case DISABLE_ARITHMETIC_REWRITE_EQUALITIES: + arithRewriteEq = false; + arithRewriteEqSetByUser = true; + break; + case SHOW_DEBUG_TAGS: if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { printf("available tags:"); @@ -1121,7 +1221,8 @@ throw(OptionException) { case ':': // This can be a long or short option, and the way to get at the name of it is different. - if(optopt == 0) { // was a long option + if(optopt == 0 || // was a long option + (optopt >= OPTION_VALUE_BEGIN && optopt <= OPTION_VALUE_END)) { // OptionValue option throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument"); } else { // was a short option throw OptionException(string("option `-") + char(optopt) + "' missing its required argument"); diff --git a/src/util/options.h b/src/util/options.h index 896f77297..9c36a471d 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -203,9 +203,6 @@ struct CVC4_PUBLIC Options { /** Log to write replay instructions to; NULL if not logging. */ std::ostream* replayLog; - /** Turn on and of arithmetic propagation. */ - bool arithPropagation; - /** * Frequency for the sat solver to make random decisions. * Should be between 0 and 1. @@ -230,9 +227,17 @@ struct CVC4_PUBLIC Options { /** Restart interval increase factor for Minisat */ double satRestartInc; + /** Determines the type of Arithmetic Presolve Lemmas are generated.*/ + typedef enum { NO_PRESOLVE_LEMMAS, INEQUALITY_PRESOLVE_LEMMAS, EQUALITY_PRESOLVE_LEMMAS, ALL_PRESOLVE_LEMMAS} ArithUnateLemmaMode; + ArithUnateLemmaMode arithUnateLemmaMode; + + /** Determines the mode of arithmetic propagation. */ + typedef enum { NO_PROP, UNATE_PROP, BOUND_INFERENCE_PROP, BOTH_PROP} ArithPropagationMode; + ArithPropagationMode arithPropagationMode; + /** The pivot rule for arithmetic */ typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; - ArithPivotRule pivotRule; + ArithPivotRule arithPivotRule; /** * The number of pivots before Bland's pivot rule is used on a basic @@ -245,23 +250,11 @@ struct CVC4_PUBLIC Options { */ uint16_t arithPropagateMaxLength; - /** - * Whether to do the symmetry-breaking preprocessing in UF as - * described by Deharbe et al. in CADE 2011 (on by default). - */ - bool ufSymmetryBreaker; - - /** - * Whether the user explicitly requested that the symmetry - * breaker be enabled or disabled. - */ - bool ufSymmetryBreakerSetByUser; - /** * Whether to do the linear diophantine equation solver * in Arith as described by Griggio JSAT 2012 (on by default). */ - bool dioSolver; + bool arithDioSolver; /** * Whether to split (= x y) into (and (<= x y) (>= x y)) in @@ -274,6 +267,19 @@ struct CVC4_PUBLIC Options { */ bool arithRewriteEqSetByUser; + /** + * Whether to do the symmetry-breaking preprocessing in UF as + * described by Deharbe et al. in CADE 2011 (on by default). + */ + bool ufSymmetryBreaker; + + /** + * Whether the user explicitly requested that the symmetry + * breaker be enabled or disabled. + */ + bool ufSymmetryBreakerSetByUser; + + /** The output channel to receive notfication events for new lemmas */ LemmaOutputChannel* lemmaOutputChannel; LemmaInputChannel* lemmaInputChannel; diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 161329c06..b4d5c0086 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -171,16 +171,20 @@ public: Node gt0Orlt1 = NodeBuilder<2>(OR) << gt0 << lt1; Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1; - cout << d_outputChannel.getIthNode(0) << endl; - cout << d_outputChannel.getIthNode(1) << endl; + cout << d_outputChannel.getIthNode(0) << endl << endl; + cout << d_outputChannel.getIthNode(1) << endl << endl; + cout << d_outputChannel.getIthNode(2) << endl << endl; - TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq1); } @@ -210,14 +214,22 @@ public: cout << d_outputChannel.getIthNode(0) << endl; cout << d_outputChannel.getIthNode(1) << endl; + cout << d_outputChannel.getIthNode(2) << endl; + cout << d_outputChannel.getIthNode(3) << endl; - TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1 ); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), PROPAGATE); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq1); } void testTPLeq1() { -- 2.30.2