From 33239a85e160bcbdfa23b44e316065166e361af8 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 22 Mar 2011 13:37:11 +0000 Subject: [PATCH] Merges the small changes on the queue-period branch into trunk. This branch importantly removes an unintentional line of code that had it pivoting more times than intended before rechecking the queue. Importantly, it does this without losing any examples with rewrite-equality enabled. This adds a parameter NUM_CHECKS which determines how many times the queue chould be checked during difference mode. A value of 10 for NUM_CHECKS has been empirically determined to be good in practice. See jobs 1815, 1824, 1825, 1821, 1814. --- src/theory/arith/simplex.cpp | 62 +++++++++++++++++++----------------- src/theory/arith/simplex.h | 3 +- 2 files changed, 34 insertions(+), 31 deletions(-) diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index bfa2d56d3..6e73ca999 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -9,10 +9,10 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::arith; -static const bool LATE_COMER = true; -static const bool s_CHECK_AFTER_PIVOT = true; -static const uint32_t DIFF_CHECK_PERIOD = 20; -static const uint32_t VARORDER_CHECK_PERIOD = 100; + +static const uint32_t NUM_CHECKS = 10; +static const bool CHECK_AFTER_PIVOT = true; +static const uint32_t VARORDER_CHECK_PERIOD = 200; SimplexDecisionProcedure::Statistics::Statistics(): d_statPivots("theory::arith::pivots",0), @@ -21,14 +21,16 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), d_statUpdateConflicts("theory::arith::UpdateConflicts", 0), d_findConflictOnTheQueueTime("theory::arith::findConflictOnTheQueueTime"), - d_attemptBeforeDiffSearch("theory::arith::attemptBeforeDiffSearch",0), - d_successBeforeDiffSearch("theory::arith::successBeforeDiffSearch",0), - d_attemptAfterDiffSearch("theory::arith::attemptAfterDiffSearch",0), - d_successAfterDiffSearch("theory::arith::successAfterDiffSearch",0), - d_attemptDuringDiffSearch("theory::arith::attemptDuringDiffSearch",0), - d_successDuringDiffSearch("theory::arith::successDuringDiffSearch",0), - d_attemptDuringVarOrderSearch("theory::arith::attemptDuringVarOrderSearch",0), - d_successDuringVarOrderSearch("theory::arith::successDuringVarOrderSearch",0), + d_attemptBeforeDiffSearch("theory::arith::qi::BeforeDiffSearch::attempt",0), + d_successBeforeDiffSearch("theory::arith::qi::BeforeDiffSearch::success",0), + d_attemptAfterDiffSearch("theory::arith::qi::AfterDiffSearch::attempt",0), + d_successAfterDiffSearch("theory::arith::qi::AfterDiffSearch::success",0), + d_attemptDuringDiffSearch("theory::arith::qi::DuringDiffSearch::attempt",0), + d_successDuringDiffSearch("theory::arith::qi::DuringDiffSearch::success",0), + d_attemptDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::attempt",0), + d_successDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::success",0), + d_attemptAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::attempt",0), + d_successAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::success",0), d_delayedConflicts("theory::arith::delayedConflicts",0), d_pivotTime("theory::arith::pivotTime"), d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"), @@ -50,6 +52,8 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_successDuringDiffSearch); StatisticsRegistry::registerStat(&d_attemptDuringVarOrderSearch); StatisticsRegistry::registerStat(&d_successDuringVarOrderSearch); + StatisticsRegistry::registerStat(&d_attemptAfterVarOrderSearch); + StatisticsRegistry::registerStat(&d_successAfterVarOrderSearch); StatisticsRegistry::registerStat(&d_delayedConflicts); @@ -76,6 +80,8 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_successDuringDiffSearch); StatisticsRegistry::unregisterStat(&d_attemptDuringVarOrderSearch); StatisticsRegistry::unregisterStat(&d_successDuringVarOrderSearch); + StatisticsRegistry::unregisterStat(&d_attemptAfterVarOrderSearch); + StatisticsRegistry::unregisterStat(&d_successAfterVarOrderSearch); StatisticsRegistry::unregisterStat(&d_delayedConflicts); StatisticsRegistry::unregisterStat(&d_pivotTime); @@ -429,6 +435,7 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re case DuringDiffSearch: ++(d_statistics.d_attemptDuringDiffSearch); break; case AfterDiffSearch: ++(d_statistics.d_attemptAfterDiffSearch); break; case DuringVarOrderSearch: ++(d_statistics.d_attemptDuringVarOrderSearch); break; + case AfterVarOrderSearch: ++(d_statistics.d_attemptAfterVarOrderSearch); break; } bool success = false; @@ -456,6 +463,7 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re case DuringDiffSearch: ++(d_statistics.d_successDuringDiffSearch); break; case AfterDiffSearch: ++(d_statistics.d_successAfterDiffSearch); break; case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break; + case AfterVarOrderSearch: ++(d_statistics.d_successAfterVarOrderSearch); break; } } return firstConflict; @@ -478,32 +486,24 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ possibleConflict = findConflictOnTheQueue(BeforeDiffSearch); } if(possibleConflict.isNull()){ - uint32_t pivotsSoFar = 0; - possibleConflict = searchForFeasibleSolution(d_numVariables + 1); + uint32_t numHueristicPivots = d_numVariables + 1; + uint32_t pivotsRemaining = numHueristicPivots; + uint32_t pivotsPerCheck = (numHueristicPivots/NUM_CHECKS) + (NUM_CHECKS-1); while(!d_queue.empty() && possibleConflict.isNull() && - pivotsSoFar <= d_numVariables + 1){ - possibleConflict = searchForFeasibleSolution(DIFF_CHECK_PERIOD); - pivotsSoFar += DIFF_CHECK_PERIOD; + pivotsRemaining > 0){ + uint32_t pivotsToDo = min(pivotsPerCheck, pivotsRemaining); + possibleConflict = searchForFeasibleSolution(pivotsToDo); + pivotsRemaining -= pivotsToDo; //Once every CHECK_PERIOD examine the entire queue for conflicts if(possibleConflict.isNull()){ possibleConflict = findConflictOnTheQueue(DuringDiffSearch); + }else{ + findConflictOnTheQueue(AfterDiffSearch, false); } } } - if(LATE_COMER){ - if(d_queue.size() > 1 && possibleConflict.isNull()){ - possibleConflict = findConflictOnTheQueue(AfterDiffSearch); - }else if (d_queue.size() > 1){ - findConflictOnTheQueue(AfterDiffSearch, false); - } - }else{ - if(d_queue.size() > 1 && possibleConflict.isNull()){ - possibleConflict = findConflictOnTheQueue(AfterDiffSearch); - } - } - if(!d_queue.empty() && possibleConflict.isNull()){ d_queue.transitionToVariableOrderMode(); @@ -513,6 +513,8 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ //Once every CHECK_PERIOD examine the entire queue for conflicts if(possibleConflict.isNull()){ possibleConflict = findConflictOnTheQueue(DuringVarOrderSearch); + }else{ + findConflictOnTheQueue(AfterVarOrderSearch, false); } } } @@ -595,7 +597,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera } Assert(x_j != ARITHVAR_SENTINEL); //Check to see if we already have a conflict with x_j to prevent wasteful work - if(s_CHECK_AFTER_PIVOT){ + if(CHECK_AFTER_PIVOT){ Node earlyConflict = checkBasicForConflict(x_j); if(!earlyConflict.isNull()){ return earlyConflict; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 66d0a97da..93574b3da 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -139,7 +139,7 @@ public: private: template Node searchForFeasibleSolution(uint32_t maxIterations); - enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch}; + enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch}; Node findConflictOnTheQueue(SearchPeriod period, bool returnFirst = true); @@ -261,6 +261,7 @@ private: IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch; IntStat d_attemptDuringDiffSearch, d_successDuringDiffSearch; IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch; + IntStat d_attemptAfterVarOrderSearch, d_successAfterVarOrderSearch; IntStat d_delayedConflicts; -- 2.30.2