3 heuristics were added to arithmetic. A heuristic for detecting an encoding of min added to static learning in LRA. A heuristic added for when the true branch and false branch are both constants (also in static learning). A heuristic for checking whether any variables begin in conflict before pivoting.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 7514b6284..d8997af93 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -134,6 +134,8 @@ public:
 private:
   Node privateUpdateInconsistentVars();
 
+  Node selectInitialConflict();
+
 private:
   /**
    * Given the basic variable x_i,
@@ -197,6 +199,9 @@ private:
     IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
 
     IntStat d_statEjections, d_statUnEjections;
+
+    IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements;
+    TimerStat d_selectInitialConflictTime;
     Statistics();
     ~Statistics();
   };