From a8f1f0e2cef69acd278f859fe32a2df7852256e0 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 14 Jun 2012 04:39:43 +0000 Subject: [PATCH] Brings the tuning branch into trunk. This includes the changes from restricted-simplex. --- src/smt/smt_engine.cpp | 30 +++++ src/theory/arith/arith_priority_queue.cpp | 35 +++++- src/theory/arith/arith_priority_queue.h | 5 + src/theory/arith/normal_form.h | 9 ++ src/theory/arith/simplex.cpp | 143 ++++++++++++++++------ src/theory/arith/simplex.h | 8 +- src/theory/arith/theory_arith.cpp | 100 +++++++++++++-- src/theory/arith/theory_arith.h | 20 +++ src/util/options.cpp | 56 +++++++-- src/util/options.h | 38 +++++- 10 files changed, 373 insertions(+), 71 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4887ef540..b91272d64 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -490,6 +490,36 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl; NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq; } + if(! Options::current()->arithHeuristicPivotsSetByUser){ + int16_t heuristicPivots = 5; + if(d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified()){ + if(d_logic.isDifferenceLogic()){ + heuristicPivots = -1; + }else if(!d_logic.areIntegersUsed()){ + heuristicPivots = 0; + } + } + Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots << std::endl; + NodeManager::currentNM()->getOptions()->arithHeuristicPivots = heuristicPivots; + } + if(! Options::current()->arithPivotThresholdSetByUser){ + uint16_t pivotThreshold = 2; + if(d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified()){ + if(d_logic.isDifferenceLogic()){ + pivotThreshold = 16; + } + } + Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold << std::endl; + NodeManager::currentNM()->getOptions()->arithPivotThreshold = pivotThreshold; + } + if(! Options::current()->arithStandardCheckVarOrderPivotsSetByUser){ + int16_t varOrderPivots = -1; + if(d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified()){ + varOrderPivots = 200; + } + Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots << std::endl; + NodeManager::currentNM()->getOptions()->arithStandardCheckVarOrderPivots = varOrderPivots; + } // Turn off early theory preprocessing if arithRewriteEq is on if (NodeManager::currentNM()->getOptions()->arithRewriteEq) { d_earlyTheoryPP = false; diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index bd2939df9..04ca62571 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -240,10 +240,41 @@ void ArithPriorityQueue::transitionToVariableOrderMode() { void ArithPriorityQueue::transitionToCollectionMode() { Assert(inDifferenceMode() || inVariableOrderMode()); - Assert(d_diffQueue.empty()); Assert(d_candidates.empty()); + + if(inDifferenceMode()){ + Assert(d_varSet.empty()); + Assert(d_varOrderQueue.empty()); + Assert(inDifferenceMode()); + + DifferenceArray::const_iterator i = d_diffQueue.begin(), end = d_diffQueue.end(); + for(; i != end; ++i){ + ArithVar var = (*i).variable(); + if(basicAndInconsistent(var) && !d_varSet.isMember(var)){ + d_candidates.push_back(var); + d_varSet.add(var); + } + } + d_diffQueue.clear(); + }else{ + Assert(d_diffQueue.empty()); + Assert(inVariableOrderMode()); + + d_varSet.purge(); + + ArithVarArray::const_iterator i = d_varOrderQueue.begin(), end = d_varOrderQueue.end(); + for(; i != end; ++i){ + ArithVar var = *i; + if(basicAndInconsistent(var)){ + d_candidates.push_back(var); + d_varSet.add(var); // cannot have duplicates. + } + } + d_varOrderQueue.clear(); + } + + Assert(d_diffQueue.empty()); Assert(d_varOrderQueue.empty()); - Assert(d_varSet.empty()); Debug("arith::priorityqueue") << "transitionToCollectionMode()" << endl; diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index e11a8ba53..a4f30e18b 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -136,6 +136,11 @@ private: */ ArithVarArray d_varOrderQueue; + /** + * A superset of the basic variables that may be inconsistent. + * This is empty during DiffOrderMode, and otherwise it is the same set as candidates + * or varOrderQueue. + */ DenseSet d_varSet; /** diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index d67cd46a9..f42b6d398 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -854,6 +854,15 @@ public: return getHead().isConstant(); } + uint32_t size() const{ + if(singleton()){ + return 1; + }else{ + Assert(getNode().getKind() == kind::PLUS); + return getNode().getNumChildren(); + } + } + Monomial getHead() const { return *(begin()); } diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 8fb99a9ae..73087d4e8 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -28,10 +28,7 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::arith; - -static const uint32_t NUM_CHECKS = 10; static const bool CHECK_AFTER_PIVOT = true; -static const uint32_t VARORDER_CHECK_PERIOD = 200; SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel) : d_conflictVariable(ARITHVAR_SENTINEL), @@ -44,7 +41,7 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, d_pivotsInRound(), d_DELTA_ZERO(0,0) { - switch(Options::ArithPivotRule rule = Options::current()->arithPivotRule) { + switch(Options::ArithHeuristicPivotRule rule = Options::current()->arithHeuristicPivotRule) { case Options::MINIMUM: d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); break; @@ -242,74 +239,144 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { } } -bool SimplexDecisionProcedure::findModel(){ +Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){ Assert(d_conflictVariable == ARITHVAR_SENTINEL); if(d_queue.empty()){ - return false; + return Result::SAT; } - bool foundConflict = false; - static CVC4_THREADLOCAL(unsigned int) instance = 0; instance = instance + 1; Debug("arith::findModel") << "begin findModel()" << instance << endl; d_queue.transitionToDifferenceMode(); - if(d_queue.size() > 1){ - foundConflict = findConflictOnTheQueue(BeforeDiffSearch); + Result::Sat result = Result::SAT_UNKNOWN; + + if(d_queue.empty()){ + result = Result::SAT; + }else if(d_queue.size() > 1){ + if(findConflictOnTheQueue(BeforeDiffSearch)){ + result = Result::UNSAT; + } } - if(!foundConflict){ - uint32_t numHeuristicPivots = d_numVariables + 1; - uint32_t pivotsRemaining = numHeuristicPivots; - uint32_t pivotsPerCheck = (numHeuristicPivots/NUM_CHECKS) + (NUM_CHECKS-1); + static const bool verbose = false; + exactResult |= Options::current()->arithStandardCheckVarOrderPivots < 0; + const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : Options::current()->arithStandardCheckVarOrderPivots; + + uint32_t checkPeriod = Options::current()->arithSimplexCheckPeriod; + if(result == Result::SAT_UNKNOWN){ + uint32_t numDifferencePivots = Options::current()->arithHeuristicPivots < 0 ? + d_numVariables + 1 : Options::current()->arithHeuristicPivots; + // The signed to unsigned conversion is safe. + uint32_t pivotsRemaining = numDifferencePivots; while(!d_queue.empty() && - !foundConflict && + result != Result::UNSAT && pivotsRemaining > 0){ - uint32_t pivotsToDo = min(pivotsPerCheck, pivotsRemaining); - foundConflict = searchForFeasibleSolution(pivotsToDo); + uint32_t pivotsToDo = min(checkPeriod, pivotsRemaining); pivotsRemaining -= pivotsToDo; - //Once every CHECK_PERIOD examine the entire queue for conflicts - if(!foundConflict){ - foundConflict = findConflictOnTheQueue(DuringDiffSearch); + if(searchForFeasibleSolution(pivotsToDo)){ + result = Result::UNSAT; + }//Once every CHECK_PERIOD examine the entire queue for conflicts + if(result != Result::UNSAT){ + if(findConflictOnTheQueue(DuringDiffSearch)) { result = Result::UNSAT; } }else{ - findConflictOnTheQueue(AfterDiffSearch); + findConflictOnTheQueue(AfterDiffSearch); // already unsat + } + } + + if(verbose && numDifferencePivots > 0){ + if(result == Result::UNSAT){ + cout << "diff order found unsat" << endl; + }else if(d_queue.empty()){ + cout << "diff order found model" << endl; + }else{ + cout << "diff order missed" << endl; } } } - if(!d_queue.empty() && !foundConflict){ - d_queue.transitionToVariableOrderMode(); + if(!d_queue.empty() && result != Result::UNSAT){ + if(exactResult){ + d_queue.transitionToVariableOrderMode(); - while(!d_queue.empty() && !foundConflict){ - foundConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD); + while(!d_queue.empty() && result != Result::UNSAT){ + if(searchForFeasibleSolution(checkPeriod)){ + result = Result::UNSAT; + } - //Once every CHECK_PERIOD examine the entire queue for conflicts - if(!foundConflict){ - foundConflict = findConflictOnTheQueue(DuringVarOrderSearch); - } else{ - findConflictOnTheQueue(AfterVarOrderSearch); + //Once every CHECK_PERIOD examine the entire queue for conflicts + if(result != Result::UNSAT){ + if(findConflictOnTheQueue(DuringVarOrderSearch)){ + result = Result::UNSAT; + } + } else{ + findConflictOnTheQueue(AfterVarOrderSearch); + } + } + if(verbose){ + if(result == Result::UNSAT){ + cout << "bland found unsat" << endl; + }else if(d_queue.empty()){ + cout << "bland found model" << endl; + }else{ + cout << "bland order missed" << endl; + } + } + }else{ + d_queue.transitionToVariableOrderMode(); + + if(searchForFeasibleSolution(inexactResultsVarOrderPivots)){ + result = Result::UNSAT; + findConflictOnTheQueue(AfterVarOrderSearch); // already unsat + }else{ + if(findConflictOnTheQueue(AfterVarOrderSearch)) { result = Result::UNSAT; } + } + + if(verbose){ + if(result == Result::UNSAT){ + cout << "restricted var order found unsat" << endl; + }else if(d_queue.empty()){ + cout << "restricted var order found model" << endl; + }else{ + cout << "restricted var order missed" << endl; + } } } } - Assert(foundConflict || d_queue.empty()); + if(result == Result::SAT_UNKNOWN && d_queue.empty()){ + result = Result::SAT; + } + + - // 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(); d_conflictVariable = ARITHVAR_SENTINEL; - Assert(!d_queue.inCollectionMode()); d_queue.transitionToCollectionMode(); + Assert(d_queue.inCollectionMode()); + Debug("arith::findModel") << "end findModel() " << instance << " " << result << endl; + return result; - Assert(d_queue.inCollectionMode()); + // Assert(foundConflict || d_queue.empty()); + + // // 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(); + // d_conflictVariable = ARITHVAR_SENTINEL; + + // Assert(!d_queue.inCollectionMode()); + // d_queue.transitionToCollectionMode(); + + + // Assert(d_queue.inCollectionMode()); - Debug("arith::findModel") << "end findModel() " << instance << endl; + // Debug("arith::findModel") << "end findModel() " << instance << endl; - return foundConflict; + // return foundConflict; } Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 8450afb06..d260ff9b4 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -62,6 +62,7 @@ #include "util/dense_map.h" #include "util/options.h" #include "util/stats.h" +#include "util/result.h" #include @@ -130,7 +131,7 @@ public: * * Corresponds to the "check()" procedure in [Cav06]. */ - bool findModel(); + Result::Sat findModel(bool exactResult); private: @@ -218,6 +219,11 @@ private: public: void increaseMax() {d_numVariables++;} + + void clearQueue() { + d_queue.clear(); + } + private: /** Reports a conflict to on the output channel. */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3ba987124..62a258fe2 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -55,6 +55,8 @@ const uint32_t RESET_START = 2; TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe), + d_qflraStatus(Result::SAT_UNKNOWN), + d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), d_learner(d_pbSubstitutions), d_setupLiteralCallback(this), @@ -102,7 +104,13 @@ TheoryArith::Statistics::Statistics(): d_restartTimer("theory::arith::restartTimer"), d_boundComputationTime("theory::arith::bound::time"), d_boundComputations("theory::arith::bound::boundComputations",0), - d_boundPropagations("theory::arith::bound::boundPropagations",0) + d_boundPropagations("theory::arith::bound::boundPropagations",0), + d_unknownChecks("theory::arith::status::unknowns", 0), + d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0), + d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow"), + d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0), + d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0), + d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0) { StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); @@ -127,6 +135,13 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_boundComputationTime); StatisticsRegistry::registerStat(&d_boundComputations); StatisticsRegistry::registerStat(&d_boundPropagations); + + StatisticsRegistry::registerStat(&d_unknownChecks); + StatisticsRegistry::registerStat(&d_maxUnknownsInARow); + StatisticsRegistry::registerStat(&d_avgUnknownsInARow); + StatisticsRegistry::registerStat(&d_revertsOnConflicts); + StatisticsRegistry::registerStat(&d_commitsOnConflicts); + StatisticsRegistry::registerStat(&d_nontrivialSatChecks); } TheoryArith::Statistics::~Statistics(){ @@ -153,6 +168,13 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_boundComputationTime); StatisticsRegistry::unregisterStat(&d_boundComputations); StatisticsRegistry::unregisterStat(&d_boundPropagations); + + StatisticsRegistry::unregisterStat(&d_unknownChecks); + StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow); + StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow); + StatisticsRegistry::unregisterStat(&d_revertsOnConflicts); + StatisticsRegistry::unregisterStat(&d_commitsOnConflicts); + StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks); } void TheoryArith::revertOutOfConflict(){ @@ -655,7 +677,12 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst // Add the substitution if not recursive Assert(elim == Rewriter::rewrite(elim)); - if(elim.hasSubterm(minVar)){ + + static const int MAX_SUB_SIZE = 20; + if(false && right.size() > MAX_SUB_SIZE){ + Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl; + Debug("simplify") << right.size() << endl; + }else if(elim.hasSubterm(minVar)){ Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl; }else if (!minVar.getType().isInteger() || right.isIntegral()) { Assert(!elim.hasSubterm(minVar)); @@ -1354,9 +1381,16 @@ void TheoryArith::outputConflicts(){ void TheoryArith::check(Effort effortLevel){ Assert(d_currentPropagationList.empty()); - Debug("arith") << "TheoryArith::check begun" << std::endl; + Debug("effortlevel") << "TheoryArith::check " << effortLevel << std::endl; + Debug("arith") << "TheoryArith::check begun " << effortLevel << std::endl; + + bool newFacts = !done(); + Result::Sat previous = d_qflraStatus; + if(newFacts){ + d_qflraStatus = Result::SAT_UNKNOWN; + d_hasDoneWorkSinceCut = true; + } - d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done(); while(!done()){ Constraint curr = constraintFromFactQueue(); if(curr != NullConstraint){ @@ -1366,6 +1400,7 @@ void TheoryArith::check(Effort effortLevel){ if(inConflict()){ revertOutOfConflict(); outputConflicts(); + d_qflraStatus = Result::UNSAT; return; } } @@ -1379,6 +1414,7 @@ void TheoryArith::check(Effort effortLevel){ Assert(!res || inConflict()); if(inConflict()){ + d_qflraStatus = Result::UNSAT; revertOutOfConflict(); outputConflicts(); return; @@ -1391,20 +1427,53 @@ void TheoryArith::check(Effort effortLevel){ } bool emmittedConflictOrSplit = false; + + Assert(d_conflicts.empty()); - bool foundConflict = d_simplex.findModel(); - if(foundConflict){ - revertOutOfConflict(); + + d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel)); + switch(d_qflraStatus){ + case Result::SAT: + if(newFacts){ + ++d_statistics.d_nontrivialSatChecks; + } + d_partialModel.commitAssignmentChanges(); + d_unknownsInARow = 0; + break; + case Result::SAT_UNKNOWN: + ++d_unknownsInARow; + ++(d_statistics.d_unknownChecks); + Assert(!fullEffort(effortLevel)); + d_partialModel.commitAssignmentChanges(); + d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow); + break; + case Result::UNSAT: + d_unknownsInARow = 0; + if(previous == Result::SAT){ + ++d_statistics.d_revertsOnConflicts; + + revertOutOfConflict(); + d_simplex.clearQueue(); + }else{ + ++d_statistics.d_commitsOnConflicts; + + d_partialModel.commitAssignmentChanges(); + revertOutOfConflict(); + } outputConflicts(); emmittedConflictOrSplit = true; - }else{ - d_partialModel.commitAssignmentChanges(); + break; + default: + Unimplemented(); } + d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow); + // This should be fine if sat or unknown if(!emmittedConflictOrSplit && (Options::current()->arithPropagationMode == Options::UNATE_PROP || Options::current()->arithPropagationMode == Options::BOTH_PROP)){ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); + Assert(d_qflraStatus != Result::UNSAT); while(!d_currentPropagationList.empty() && !inConflict()){ Constraint curr = d_currentPropagationList.front(); @@ -1618,6 +1687,8 @@ void TheoryArith::debugPrintModel(){ } } + + Node TheoryArith::explain(TNode n) { Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl; @@ -1637,7 +1708,9 @@ Node TheoryArith::explain(TNode n) { void TheoryArith::propagate(Effort e) { - if((Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP || + // This uses model values for safety. Disable for now. + if(d_qflraStatus == Result::SAT && + (Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP || Options::current()->arithPropagationMode == Options::BOTH_PROP) && hasAnyUpdates()){ propagateCandidates(); @@ -1693,6 +1766,7 @@ void TheoryArith::propagate(Effort e) { } bool TheoryArith::getDeltaAtomValue(TNode n) { + Assert(d_qflraStatus != Result::SAT_UNKNOWN); switch (n.getKind()) { case kind::EQUAL: // 2 args @@ -1712,7 +1786,7 @@ bool TheoryArith::getDeltaAtomValue(TNode n) { DeltaRational TheoryArith::getDeltaValue(TNode n) { - + Assert(d_qflraStatus != Result::SAT_UNKNOWN); Debug("arith::value") << n << std::endl; switch(n.getKind()) { @@ -1936,7 +2010,9 @@ void TheoryArith::presolve(){ } EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) { - if (getDeltaValue(a) == getDeltaValue(b)) { + if(d_qflraStatus == Result::SAT_UNKNOWN){ + return EQUALITY_UNKNOWN; + }else if (getDeltaValue(a) == getDeltaValue(b)) { return EQUALITY_TRUE_IN_MODEL; } else { return EQUALITY_FALSE_IN_MODEL; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e23a9a943..556495c97 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -44,6 +44,7 @@ #include "theory/arith/constraint.h" #include "util/stats.h" +#include "util/result.h" #include #include @@ -63,6 +64,15 @@ class InstantiatorTheoryArith; class TheoryArith : public Theory { friend class InstantiatorTheoryArith; private: + enum Result::Sat d_qflraStatus; + // check() + // !done() -> d_qflraStatus = Unknown + // fullEffort(e) -> simplex returns either sat or unsat + // !fullEffort(e) -> simplex returns either sat, unsat or unknown + // if unknown, save the assignment + // if unknown, the simplex priority queue cannot be emptied + int d_unknownsInARow; + bool rowImplication(ArithVar v, bool upperBound, const DeltaRational& r); /** @@ -113,6 +123,8 @@ private: } } d_setupLiteralCallback; + + /** * (For the moment) the type hierarchy goes as: * Integer <: Real @@ -489,6 +501,14 @@ private: TimerStat d_boundComputationTime; IntStat d_boundComputations, d_boundPropagations; + IntStat d_unknownChecks; + IntStat d_maxUnknownsInARow; + AverageStat d_avgUnknownsInARow; + + IntStat d_revertsOnConflicts; + IntStat d_commitsOnConflicts; + IntStat d_nontrivialSatChecks; + Statistics(); ~Statistics(); }; diff --git a/src/util/options.cpp b/src/util/options.cpp index 06dc6769b..8961d5b57 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -122,8 +122,14 @@ Options::Options() : satRestartInc(3.0), arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS), arithPropagationMode(BOTH_PROP), - arithPivotRule(MINIMUM), - arithPivotThreshold(16), + arithHeuristicPivots(0), + arithHeuristicPivotsSetByUser(false), + arithStandardCheckVarOrderPivots(-1), + arithStandardCheckVarOrderPivotsSetByUser(false), + arithHeuristicPivotRule(MINIMUM), + arithSimplexCheckPeriod(200), + arithPivotThreshold(2), + arithPivotThresholdSetByUser(false), arithPropagateMaxLength(16), arithDioSolver(true), arithRewriteEq(false), @@ -239,12 +245,17 @@ Additional CVC4 options:\n\ --restart-int-inc=F restart interval increase factor for the sat solver\n\ (F=3.0 by default)\n\ ARITHMETIC:\n\ - ---unate-lemmas=MODE determines which lemmas to add before solving\n\ + --unate-lemmas=MODE determines which lemmas to add before solving\n\ (default is 'all', see --unate-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\ + --heuristic-pivot-rule=RULE change the pivot rule for the basic variable\n\ + (default is 'min', see --heuristic-pivot-rule help)\n\ + --heuristic-pivots=N the number of times to apply the heuristic pivot rule.\n\ + If N < 0, this defaults to the number of variables\n\ + If this is unset, this is tuned by the logic selection.\n\ + --simplex-check-period=N The number of pivots to do in simplex before rechecking for\n\ + a conflict on all variables.\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\ @@ -528,7 +539,10 @@ enum OptionValue { SAT_RESTART_INC, ARITHMETIC_UNATE_LEMMA_MODE, ARITHMETIC_PROPAGATION_MODE, + ARITHMETIC_HEURISTIC_PIVOTS, + ARITHMETIC_VAR_ORDER_PIVOTS, ARITHMETIC_PIVOT_RULE, + ARITHMETIC_CHECK_PERIOD, ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH, ARITHMETIC_DIO_SOLVER, @@ -653,7 +667,10 @@ static struct option cmdlineOptions[] = { { "print-winner", no_argument , NULL, PRINT_WINNER }, { "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 }, + { "heuristic-pivots", required_argument, NULL, ARITHMETIC_HEURISTIC_PIVOTS }, + { "heuristic-pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE }, + { "standard-effort-variable-order-pivots", required_argument, NULL, ARITHMETIC_VAR_ORDER_PIVOTS }, + { "simplex-check-period" , required_argument, NULL, ARITHMETIC_CHECK_PERIOD }, { "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 }, @@ -1370,27 +1387,42 @@ throw(OptionException) { } break; + case ARITHMETIC_HEURISTIC_PIVOTS: + arithHeuristicPivots = atoi(optarg); + arithHeuristicPivotsSetByUser = true; + break; + + case ARITHMETIC_VAR_ORDER_PIVOTS: + arithStandardCheckVarOrderPivots = atoi(optarg); + arithStandardCheckVarOrderPivotsSetByUser = true; + break; + case ARITHMETIC_PIVOT_RULE: if(!strcmp(optarg, "min")) { - arithPivotRule = MINIMUM; + arithHeuristicPivotRule = MINIMUM; break; } else if(!strcmp(optarg, "min-break-ties")) { - arithPivotRule = BREAK_TIES; + arithHeuristicPivotRule = BREAK_TIES; break; } else if(!strcmp(optarg, "max")) { - arithPivotRule = MAXIMUM; + arithHeuristicPivotRule = MAXIMUM; break; } else if(!strcmp(optarg, "help")) { puts(pivotRulesHelp.c_str()); exit(1); } else { - throw OptionException(string("unknown option for --pivot-rule: `") + - optarg + "'. Try --pivot-rule help."); + throw OptionException(string("unknown option for --heuristic-pivot-rule: `") + + optarg + "'. Try --heuristic-pivot-rule help."); } break; + case ARITHMETIC_CHECK_PERIOD: + arithSimplexCheckPeriod = atoi(optarg); + break; + case ARITHMETIC_PIVOT_THRESHOLD: arithPivotThreshold = atoi(optarg); + arithPivotThresholdSetByUser = true; break; case ARITHMETIC_PROP_MAX_LENGTH: @@ -1601,7 +1633,7 @@ void Options::setInputLanguage(const char* str) throw(OptionException) { languageHelp = true; } -std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) { +std::ostream& operator<<(std::ostream& out, Options::ArithHeuristicPivotRule rule) { switch(rule) { case Options::MINIMUM: out << "MINIMUM"; diff --git a/src/util/options.h b/src/util/options.h index fb5f71060..7dbba2439 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -266,15 +266,41 @@ struct CVC4_PUBLIC Options { 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 arithPivotRule; + /** + * The maximum number of difference pivots to do per invokation of simplex. + * If this is negative, the number of pivots done is the number of variables. + * If this is not set by the user, different logics are free to chose different + * defaults. + */ + int16_t arithHeuristicPivots; + bool arithHeuristicPivotsSetByUser; + + /** + * The maximum number of variable order pivots to do per invokation of simplex. + * If this is negative, the number of pivots done is unlimited. + * If this is not set by the user, different logics are free to chose different + * defaults. + */ + int16_t arithStandardCheckVarOrderPivots; + bool arithStandardCheckVarOrderPivotsSetByUser; + + /** The heuristic pivot rule for arithmetic. */ + typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithHeuristicPivotRule; + ArithHeuristicPivotRule arithHeuristicPivotRule; + + /** + * The number of pivots before simplex rechecks every basic variable for a conflict. + */ + uint16_t arithSimplexCheckPeriod; /** - * The number of pivots before Bland's pivot rule is used on a basic - * variable in arithmetic. + * This is the pivots per basic variable that can be done using heuristic choices + * before variable order must be used. + * If this is not set by the user, different logics are free to chose different + * defaults. */ uint16_t arithPivotThreshold; + bool arithPivotThresholdSetByUser; /** * The maximum row length that arithmetic will use for propagation. @@ -529,7 +555,7 @@ inline std::ostream& operator<<(std::ostream& out, return out; } -std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, Options::ArithHeuristicPivotRule rule) CVC4_PUBLIC; }/* CVC4 namespace */ -- 2.30.2