1 files changed, 81 insertions, 35 deletions

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index b1ebe2972..f0dc5d62e 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -10,6 +10,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
 #include "theory/arith/partial_model.h"
+#include "theory/arith/arith_prop_manager.h"
 
 #include "util/options.h"
 
@@ -33,36 +34,23 @@ private:
   Tableau& d_tableau;
   ArithPriorityQueue d_queue;
 
+  ArithPropManager& d_propManager;
+
   ArithVar d_numVariables;
 
   std::queue<Node> d_delayedLemmas;
 
+  PermissiveBackArithVarSet d_updatedBounds;
+  PermissiveBackArithVarSet d_candidateBasics;
+
   Rational d_ZERO;
+  DeltaRational d_DELTA_ZERO;
 
 public:
-  SimplexDecisionProcedure(ArithPartialModel& pm,
-                           Tableau& tableau) :
-    d_partialModel(pm),
-    d_tableau(tableau),
-    d_queue(pm, tableau),
-    d_numVariables(0),
-    d_delayedLemmas(),
-    d_ZERO(0)
-  {
-    switch(Options::ArithPivotRule rule = Options::current()->pivotRule) {
-    case Options::MINIMUM:
-      d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
-      break;
-    case Options::BREAK_TIES:
-      d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
-      break;
-    case Options::MAXIMUM:
-      d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
-      break;
-    default:
-      Unhandled(rule);
-    }
-  }
+  SimplexDecisionProcedure(ArithPropManager& propManager,
+                           ArithPartialModel& pm,
+                           Tableau& tableau);
+
 
   /**
    * Assert*(n, orig) takes an bound n that is implied by orig.
@@ -165,32 +153,49 @@ private:
    * This returns ARITHVAR_SENTINEL if none exists.
    *
    * More formally one of the following conditions must be satisfied:
-   * -  above && a_ij < 0 && assignment(x_j) < upperbound(x_j)
-   * -  above && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
-   * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j)
-   * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
+   * -  lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j)
+   * -  lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
+   * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j)
+   * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
    *
    */
-  template <bool above, PreferenceFunction>  ArithVar selectSlack(ArithVar x_i);
-  template <PreferenceFunction pf> ArithVar selectSlackBelow(ArithVar x_i) {
-    return selectSlack<false, pf>(x_i);
-  }
-  template <PreferenceFunction pf> ArithVar selectSlackAbove(ArithVar x_i) {
+  template <bool lowerBound, PreferenceFunction>  ArithVar selectSlack(ArithVar x_i);
+  template <PreferenceFunction pf> ArithVar selectSlackLowerBound(ArithVar x_i) {
     return selectSlack<true, pf>(x_i);
   }
+  template <PreferenceFunction pf> ArithVar selectSlackUpperBound(ArithVar x_i) {
+    return selectSlack<false, pf>(x_i);
+  }
   /**
    * Returns the smallest basic variable whose assignment is not consistent
    * with its upper and lower bounds.
    */
   ArithVar selectSmallestInconsistentVar();
 
+
+  /**
+   * Exports either the explanation of an upperbound or a lower bound
+   * of the basic variable basic, using the non-basic variables in the row.
+   */
+  template <bool upperBound>
+  void explainNonbasics(ArithVar basic, NodeBuilder<>& output);
+  void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){
+    explainNonbasics<false>(basic, output);
+  }
+  void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){
+    explainNonbasics<true>(basic, output);
+  }
+
+  Node deduceUpperBound(ArithVar basicVar);
+  Node deduceLowerBound(ArithVar basicVar);
+
   /**
    * Given a non-basic variable that is know to not be updatable
    * to a consistent value, construct and return a conflict.
    * Follows section 4.2 in the CAV06 paper.
    */
-  Node generateConflictAbove(ArithVar conflictVar);
-  Node generateConflictBelow(ArithVar conflictVar);
+  Node generateConflictAboveUpperBound(ArithVar conflictVar);
+  Node generateConflictBelowLowerBound(ArithVar conflictVar);
 
 public:
   /**
@@ -210,6 +215,11 @@ public:
    */
   DeltaRational computeRowValue(ArithVar x, bool useSafe);
 
+  bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
+  void clearUpdates(){
+    d_updatedBounds.purge();
+  }
+  void propagateCandidates();
 
   void increaseMax() {d_numVariables++;}
 
@@ -234,7 +244,7 @@ private:
 
   /** Adds a conflict as a lemma to the queue. */
   void delayConflictAsLemma(Node conflict){
-    Node negatedConflict = negateConjunctionAsClause(conflict);
+   Node negatedConflict = negateConjunctionAsClause(conflict);
     pushLemma(negatedConflict);
   }
 
@@ -254,6 +264,36 @@ private:
    */
   Node checkBasicForConflict(ArithVar b);
 
+  Node weakenConflict(bool aboveUpper, ArithVar basicVar);
+  TNode weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic);
+
+  void propagateCandidate(ArithVar basic);
+  bool propagateCandidateBound(ArithVar basic, bool upperBound);
+
+  inline bool propagateCandidateLowerBound(ArithVar basic){
+    return propagateCandidateBound(basic, false);
+  }
+  inline bool propagateCandidateUpperBound(ArithVar basic){
+    return propagateCandidateBound(basic, true);
+  }
+
+  bool hasBounds(ArithVar basic, bool upperBound);
+  bool hasLowerBounds(ArithVar basic){
+    return hasBounds(basic, false);
+  }
+  bool hasUpperBounds(ArithVar basic){
+    return hasBounds(basic, true);
+  }
+  DeltaRational computeBound(ArithVar basic, bool upperBound);
+
+  inline DeltaRational computeLowerBound(ArithVar basic){
+    return computeBound(basic, false);
+  }
+  inline DeltaRational computeUpperBound(ArithVar basic){
+    return computeBound(basic, true);
+  }
+
+
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
   public:
@@ -270,6 +310,12 @@ private:
     IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch;
     IntStat d_attemptAfterVarOrderSearch, d_successAfterVarOrderSearch;
 
+    IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
+    TimerStat d_weakenTime;
+
+    TimerStat d_boundComputationTime;
+    IntStat d_boundComputations, d_boundPropagations;
+
     IntStat d_delayedConflicts;
 
     TimerStat d_pivotTime;