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.

1 files changed, 2 insertions, 1 deletions

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 <PreferenceFunction> 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;