- Creates a queue for lemmas discovered during the simplex procedure. Lemmas are sent to the sat solver during theory propagation. The lemmas currently come from additional conflicts that are discovered by findConflictOnTheQueue(...).

1 files changed, 37 insertions, 3 deletions

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index a32a188b4..b847259a0 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -16,7 +16,7 @@
 
 #include "util/stats.h"
 
-#include <queue>
+#include <vector>
 
 namespace CVC4 {
 namespace theory {
@@ -42,6 +42,9 @@ private:
 
   ArithVar d_numVariables;
 
+  std::vector<Node> d_delayedLemmas;
+  uint32_t d_delayedLemmasPos;
+
 public:
   SimplexDecisionProcedure(const ArithConstants& constants,
                            ArithPartialModel& pm,
@@ -52,10 +55,13 @@ public:
     d_out(out),
     d_tableau(tableau),
     d_queue(pm, tableau),
-    d_numVariables(0)
+    d_numVariables(0),
+    d_delayedLemmas(),
+    d_delayedLemmasPos(0)
   {}
 
-  void increaseMax() {d_numVariables++;}
+
+public:
 
   /**
    * Assert*(n, orig) takes an bound n that is implied by orig.
@@ -183,7 +189,33 @@ public:
    */
   DeltaRational computeRowValue(ArithVar x, bool useSafe);
 
+
+  void increaseMax() {d_numVariables++;}
+
+  /** Returns true if the simplex procedure has more delayed lemmas in its queue.*/
+  bool hasMoreLemmas() const {
+    return d_delayedLemmasPos < d_delayedLemmas.size();
+  }
+  /** Returns the next delayed lemmas on the queue.*/
+  Node popLemma(){
+    Assert(hasMoreLemmas());
+    Node lemma = d_delayedLemmas[d_delayedLemmasPos];
+    ++d_delayedLemmasPos;
+    return lemma;
+  }
+
 private:
+  /** Adds a lemma to the queue. */
+  void pushLemma(Node lemma){
+    d_delayedLemmas.push_back(lemma);
+    ++(d_statistics.d_delayedConflicts);
+  }
+
+  /** Adds a conflict as a lemma to the queue. */
+  void delayConflictAsLemma(Node conflict){
+    Node negatedConflict = negateConjunctionAsClause(conflict);
+    pushLemma(negatedConflict);
+  }
 
   /**
    * Checks a basic variable, b, to see if it is in conflict.
@@ -206,6 +238,8 @@ private:
     IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch;
     IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch;
 
+    IntStat d_delayedConflicts;
+
     TimerStat d_pivotTime;
 
     AverageStat d_avgNumRowsNotContainingOnUpdate;