From: Tim King <taking@cs.nyu.edu>
Date: Thu, 3 Mar 2011 18:00:35 +0000 (+0000)
Subject: - Creates a queue for lemmas discovered during the simplex procedure. Lemmas are... 
X-Git-Tag: cvc5-1.0.0~8673
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=43bf1fc1ba1770715fbe9fa15fa0be2cf6fb164a;p=cvc5.git

- 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(...).
---

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 2053379d9..59b4e9bef 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -224,6 +224,18 @@ struct RightHandRationalLT
   }
 };
 
+inline Node negateConjunctionAsClause(TNode conjunction){
+  Assert(conjunction.getKind() == kind::AND);
+  NodeBuilder<> orBuilder(kind::OR);
+
+  for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){
+    TNode child = *i;
+    Node negatedChild = NodeBuilder<1>(kind::NOT)<<(child);
+    orBuilder << negatedChild;
+  }
+  return orBuilder;
+}
+
 }; /* namesapce arith */
 }; /* namespace theory */
 }; /* namespace CVC4 */
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 0809e0788..68ab429ca 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -22,6 +22,7 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_successAfterDiffSearch("theory::arith::successAfterDiffSearch",0),
   d_attemptDuringVarOrderSearch("theory::arith::attemptDuringVarOrderSearch",0),
   d_successDuringVarOrderSearch("theory::arith::successDuringVarOrderSearch",0),
+  d_delayedConflicts("theory::arith::delayedConflicts",0),
   d_pivotTime("theory::arith::pivotTime"),
   d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"),
   d_avgNumRowsNotContainingOnPivot("theory::arith::avgNumRowsNotContainingOnPivot")
@@ -41,6 +42,8 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_attemptDuringVarOrderSearch);
   StatisticsRegistry::registerStat(&d_successDuringVarOrderSearch);
 
+  StatisticsRegistry::registerStat(&d_delayedConflicts);
+
   StatisticsRegistry::registerStat(&d_pivotTime);
 
   StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnUpdate);
@@ -63,6 +66,7 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_attemptDuringVarOrderSearch);
   StatisticsRegistry::unregisterStat(&d_successDuringVarOrderSearch);
 
+  StatisticsRegistry::unregisterStat(&d_delayedConflicts);
   StatisticsRegistry::unregisterStat(&d_pivotTime);
 
   StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnUpdate);
@@ -401,7 +405,7 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
   case DuringVarOrderSearch: ++(d_statistics.d_attemptDuringVarOrderSearch); break;
   }
 
-  Node bestConflict = Node::null();
+  Node firstConflict = Node::null();
   ArithPriorityQueue::const_iterator i = d_queue.begin();
   ArithPriorityQueue::const_iterator end = d_queue.end();
   for(; i != end; ++i){
@@ -410,19 +414,22 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
     if(d_tableau.isBasic(x_i)){
       Node possibleConflict = checkBasicForConflict(x_i);
       if(!possibleConflict.isNull()){
-
-        bestConflict = betterConflict(bestConflict, possibleConflict);
+        if(firstConflict.isNull()){
+          firstConflict = possibleConflict;
+        }else{
+          delayConflictAsLemma(possibleConflict);
+        }
       }
     }
   }
-  if(!bestConflict.isNull()){
+  if(!firstConflict.isNull()){
     switch(type){
     case BeforeDiffSearch:     ++(d_statistics.d_successBeforeDiffSearch); break;
     case AfterDiffSearch:      ++(d_statistics.d_successAfterDiffSearch); break;
     case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break;
     }
   }
-  return bestConflict;
+  return firstConflict;
 }
 
 Node SimplexDecisionProcedure::updateInconsistentVars(){
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;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 3899e5e80..60eed27d1 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -556,7 +556,12 @@ void TheoryArith::explain(TNode n) {
 }
 
 void TheoryArith::propagate(Effort e) {
-
+  if(quickCheckOrMore(e)){
+    while(d_simplex.hasMoreLemmas()){
+      Node lemma = d_simplex.popLemma();
+      d_out->lemma(lemma);
+    }
+  }
   // if(quickCheckOrMore(e)){
   //   std::vector<Node> implied = d_propagator.getImpliedLiterals();
   //   for(std::vector<Node>::iterator i = implied.begin();