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, 3 insertions, 0 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index c95ca6cc4..5d39f626c 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -125,6 +125,8 @@ public:
     check(FULL_EFFORT);
   }
 
+  void staticLearning(TNode in, NodeBuilder<>& learned);
+
   std::string identify() const { return std::string("TheoryArith"); }
 
 private:
@@ -167,6 +169,7 @@ private:
     IntStat d_statUserVariables, d_statSlackVariables;
     IntStat d_statDisequalitySplits;
     IntStat d_statDisequalityConflicts;
+    TimerStat d_staticLearningTimer;
 
     Statistics();
     ~Statistics();