7 files changed, 267 insertions, 53 deletions

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index bd2939df9..04ca62571 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -240,10 +240,41 @@ void ArithPriorityQueue::transitionToVariableOrderMode() {
 
 void ArithPriorityQueue::transitionToCollectionMode() {
   Assert(inDifferenceMode() || inVariableOrderMode());
-  Assert(d_diffQueue.empty());
   Assert(d_candidates.empty());
+
+  if(inDifferenceMode()){
+    Assert(d_varSet.empty());
+    Assert(d_varOrderQueue.empty());
+    Assert(inDifferenceMode());
+
+    DifferenceArray::const_iterator i = d_diffQueue.begin(), end = d_diffQueue.end();
+    for(; i != end; ++i){
+      ArithVar var = (*i).variable();
+      if(basicAndInconsistent(var) && !d_varSet.isMember(var)){
+        d_candidates.push_back(var);
+        d_varSet.add(var);
+      }
+    }
+    d_diffQueue.clear();
+  }else{
+    Assert(d_diffQueue.empty());
+    Assert(inVariableOrderMode());
+
+    d_varSet.purge();
+
+    ArithVarArray::const_iterator i = d_varOrderQueue.begin(), end = d_varOrderQueue.end();
+    for(; i != end; ++i){
+      ArithVar var = *i;
+      if(basicAndInconsistent(var)){
+        d_candidates.push_back(var);
+        d_varSet.add(var); // cannot have duplicates.
+      }
+    }
+    d_varOrderQueue.clear();
+  }
+
+  Assert(d_diffQueue.empty());
   Assert(d_varOrderQueue.empty());
-  Assert(d_varSet.empty());
 
   Debug("arith::priorityqueue") << "transitionToCollectionMode()" << endl;
 
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index e11a8ba53..a4f30e18b 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -136,6 +136,11 @@ private:
    */
   ArithVarArray d_varOrderQueue;
 
+  /**
+   * A superset of the basic variables that may be inconsistent.
+   * This is empty during DiffOrderMode, and otherwise it is the same set as candidates
+   * or varOrderQueue.
+   */
   DenseSet d_varSet;
 
   /**
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index d67cd46a9..f42b6d398 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -854,6 +854,15 @@ public:
     return getHead().isConstant();
   }
 
+  uint32_t size() const{
+    if(singleton()){
+      return 1;
+    }else{
+      Assert(getNode().getKind() == kind::PLUS);
+      return getNode().getNumChildren();
+    }
+  }
+
   Monomial getHead() const {
     return *(begin());
   }
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 8fb99a9ae..73087d4e8 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -28,10 +28,7 @@ using namespace CVC4::kind;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
-
-static const uint32_t NUM_CHECKS = 10;
 static const bool CHECK_AFTER_PIVOT = true;
-static const uint32_t VARORDER_CHECK_PERIOD = 200;
 
 SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel) :
   d_conflictVariable(ARITHVAR_SENTINEL),
@@ -44,7 +41,7 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq,
   d_pivotsInRound(),
   d_DELTA_ZERO(0,0)
 {
-  switch(Options::ArithPivotRule rule = Options::current()->arithPivotRule) {
+  switch(Options::ArithHeuristicPivotRule rule = Options::current()->arithHeuristicPivotRule) {
   case Options::MINIMUM:
     d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
     break;
@@ -242,74 +239,144 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
   }
 }
 
-bool SimplexDecisionProcedure::findModel(){
+Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
   Assert(d_conflictVariable == ARITHVAR_SENTINEL);
 
   if(d_queue.empty()){
-    return false;
+    return Result::SAT;
   }
-  bool foundConflict = false;
-
   static CVC4_THREADLOCAL(unsigned int) instance = 0;
   instance = instance + 1;
   Debug("arith::findModel") << "begin findModel()" << instance << endl;
 
   d_queue.transitionToDifferenceMode();
 
-  if(d_queue.size() > 1){
-    foundConflict = findConflictOnTheQueue(BeforeDiffSearch);
+  Result::Sat result = Result::SAT_UNKNOWN;
+
+  if(d_queue.empty()){
+    result = Result::SAT;
+  }else if(d_queue.size() > 1){
+    if(findConflictOnTheQueue(BeforeDiffSearch)){
+      result = Result::UNSAT;
+    }
   }
-  if(!foundConflict){
-    uint32_t numHeuristicPivots = d_numVariables + 1;
-    uint32_t pivotsRemaining = numHeuristicPivots;
-    uint32_t pivotsPerCheck = (numHeuristicPivots/NUM_CHECKS) + (NUM_CHECKS-1);
+  static const bool verbose = false;
+  exactResult |= Options::current()->arithStandardCheckVarOrderPivots < 0;
+  const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : Options::current()->arithStandardCheckVarOrderPivots;
+
+  uint32_t checkPeriod = Options::current()->arithSimplexCheckPeriod;
+  if(result == Result::SAT_UNKNOWN){
+    uint32_t numDifferencePivots = Options::current()->arithHeuristicPivots < 0 ?
+      d_numVariables + 1 : Options::current()->arithHeuristicPivots;
+    // The signed to unsigned conversion is safe.
+    uint32_t pivotsRemaining = numDifferencePivots;
     while(!d_queue.empty() &&
-          !foundConflict &&
+          result != Result::UNSAT &&
           pivotsRemaining > 0){
-      uint32_t pivotsToDo = min(pivotsPerCheck, pivotsRemaining);
-      foundConflict = searchForFeasibleSolution(pivotsToDo);
+      uint32_t pivotsToDo = min(checkPeriod, pivotsRemaining);
       pivotsRemaining -= pivotsToDo;
-      //Once every CHECK_PERIOD examine the entire queue for conflicts
-      if(!foundConflict){
-        foundConflict = findConflictOnTheQueue(DuringDiffSearch);
+      if(searchForFeasibleSolution(pivotsToDo)){
+        result = Result::UNSAT;
+      }//Once every CHECK_PERIOD examine the entire queue for conflicts
+      if(result != Result::UNSAT){
+        if(findConflictOnTheQueue(DuringDiffSearch)) { result = Result::UNSAT; }
       }else{
-        findConflictOnTheQueue(AfterDiffSearch);
+        findConflictOnTheQueue(AfterDiffSearch); // already unsat
+      }
+    }
+
+    if(verbose && numDifferencePivots > 0){
+      if(result ==  Result::UNSAT){
+        cout << "diff order found unsat" << endl;
+      }else if(d_queue.empty()){
+        cout << "diff order found model" << endl;
+      }else{
+        cout << "diff order missed" << endl;
       }
     }
   }
 
-  if(!d_queue.empty() && !foundConflict){
-    d_queue.transitionToVariableOrderMode();
+  if(!d_queue.empty() && result != Result::UNSAT){
+    if(exactResult){
+      d_queue.transitionToVariableOrderMode();
 
-    while(!d_queue.empty() && !foundConflict){
-      foundConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD);
+      while(!d_queue.empty() && result != Result::UNSAT){
+        if(searchForFeasibleSolution(checkPeriod)){
+          result = Result::UNSAT;
+        }
 
-      //Once every CHECK_PERIOD examine the entire queue for conflicts
-      if(!foundConflict){
-        foundConflict = findConflictOnTheQueue(DuringVarOrderSearch);
-      } else{
-        findConflictOnTheQueue(AfterVarOrderSearch);
+        //Once every CHECK_PERIOD examine the entire queue for conflicts
+        if(result != Result::UNSAT){
+          if(findConflictOnTheQueue(DuringVarOrderSearch)){
+            result = Result::UNSAT;
+          }
+        } else{
+          findConflictOnTheQueue(AfterVarOrderSearch);
+        }
+      }
+      if(verbose){
+        if(result ==  Result::UNSAT){
+          cout << "bland found unsat" << endl;
+        }else if(d_queue.empty()){
+          cout << "bland found model" << endl;
+        }else{
+          cout << "bland order missed" << endl;
+        }
+      }
+    }else{
+      d_queue.transitionToVariableOrderMode();
+
+      if(searchForFeasibleSolution(inexactResultsVarOrderPivots)){
+        result = Result::UNSAT;
+        findConflictOnTheQueue(AfterVarOrderSearch); // already unsat
+      }else{
+        if(findConflictOnTheQueue(AfterVarOrderSearch)) { result = Result::UNSAT; }
+      }
+
+      if(verbose){
+        if(result ==  Result::UNSAT){
+          cout << "restricted var order found unsat" << endl;
+        }else if(d_queue.empty()){
+          cout << "restricted var order found model" << endl;
+        }else{
+          cout << "restricted var order missed" << endl;
+        }
       }
     }
   }
 
-  Assert(foundConflict || d_queue.empty());
+  if(result == Result::SAT_UNKNOWN && d_queue.empty()){
+    result = Result::SAT;
+  }
+
+
 
-  // Curiously the invariant that we always do a full check
-  // means that the assignment we can always empty these queues.
-  d_queue.clear();
   d_pivotsInRound.purge();
   d_conflictVariable = ARITHVAR_SENTINEL;
 
-  Assert(!d_queue.inCollectionMode());
   d_queue.transitionToCollectionMode();
+  Assert(d_queue.inCollectionMode());
+  Debug("arith::findModel") << "end findModel() " << instance << " " << result <<  endl;
+  return result;
 
 
-  Assert(d_queue.inCollectionMode());
+  // Assert(foundConflict || d_queue.empty());
+
+  // // Curiously the invariant that we always do a full check
+  // // means that the assignment we can always empty these queues.
+  // d_queue.clear();
+  // d_pivotsInRound.purge();
+  // d_conflictVariable = ARITHVAR_SENTINEL;
+
+  // Assert(!d_queue.inCollectionMode());
+  // d_queue.transitionToCollectionMode();
+
+
+  // Assert(d_queue.inCollectionMode());
 
-  Debug("arith::findModel") << "end findModel() " << instance << endl;
+  // Debug("arith::findModel") << "end findModel() " << instance << endl;
 
-  return foundConflict;
+  // return foundConflict;
 }
 
 Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 8450afb06..d260ff9b4 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -62,6 +62,7 @@
 #include "util/dense_map.h"
 #include "util/options.h"
 #include "util/stats.h"
+#include "util/result.h"
 
 #include <queue>
 
@@ -130,7 +131,7 @@ public:
    *
    * Corresponds to the "check()" procedure in [Cav06].
    */
-  bool findModel();
+  Result::Sat findModel(bool exactResult);
 
 private:
 
@@ -218,6 +219,11 @@ private:
 public:
   void increaseMax() {d_numVariables++;}
 
+
+  void clearQueue() {
+    d_queue.clear();
+  }
+
 private:
 
   /** Reports a conflict to on the output channel. */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 3ba987124..62a258fe2 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -55,6 +55,8 @@ const uint32_t RESET_START = 2;
 
 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
+  d_qflraStatus(Result::SAT_UNKNOWN),
+  d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
   d_learner(d_pbSubstitutions),
   d_setupLiteralCallback(this),
@@ -102,7 +104,13 @@ TheoryArith::Statistics::Statistics():
   d_restartTimer("theory::arith::restartTimer"),
   d_boundComputationTime("theory::arith::bound::time"),
   d_boundComputations("theory::arith::bound::boundComputations",0),
-  d_boundPropagations("theory::arith::bound::boundPropagations",0)
+  d_boundPropagations("theory::arith::bound::boundPropagations",0),
+  d_unknownChecks("theory::arith::status::unknowns", 0),
+  d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0),
+  d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow"),
+  d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0),
+  d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0),
+  d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0)
 {
   StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
   StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
@@ -127,6 +135,13 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_boundComputationTime);
   StatisticsRegistry::registerStat(&d_boundComputations);
   StatisticsRegistry::registerStat(&d_boundPropagations);
+
+  StatisticsRegistry::registerStat(&d_unknownChecks);
+  StatisticsRegistry::registerStat(&d_maxUnknownsInARow);
+  StatisticsRegistry::registerStat(&d_avgUnknownsInARow);
+  StatisticsRegistry::registerStat(&d_revertsOnConflicts);
+  StatisticsRegistry::registerStat(&d_commitsOnConflicts);
+  StatisticsRegistry::registerStat(&d_nontrivialSatChecks);
 }
 
 TheoryArith::Statistics::~Statistics(){
@@ -153,6 +168,13 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_boundComputationTime);
   StatisticsRegistry::unregisterStat(&d_boundComputations);
   StatisticsRegistry::unregisterStat(&d_boundPropagations);
+
+  StatisticsRegistry::unregisterStat(&d_unknownChecks);
+  StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow);
+  StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow);
+  StatisticsRegistry::unregisterStat(&d_revertsOnConflicts);
+  StatisticsRegistry::unregisterStat(&d_commitsOnConflicts);
+  StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks);
 }
 
 void TheoryArith::revertOutOfConflict(){
@@ -655,7 +677,12 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst
       // Add the substitution if not recursive
       Assert(elim == Rewriter::rewrite(elim));
 
-      if(elim.hasSubterm(minVar)){
+
+      static const int MAX_SUB_SIZE = 20;
+      if(false && right.size() > MAX_SUB_SIZE){
+        Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
+        Debug("simplify") << right.size() << endl;
+      }else if(elim.hasSubterm(minVar)){
         Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
       }else if (!minVar.getType().isInteger() || right.isIntegral()) {
         Assert(!elim.hasSubterm(minVar));
@@ -1354,9 +1381,16 @@ void TheoryArith::outputConflicts(){
 
 void TheoryArith::check(Effort effortLevel){
   Assert(d_currentPropagationList.empty());
-  Debug("arith") << "TheoryArith::check begun" << std::endl;
+  Debug("effortlevel") << "TheoryArith::check " << effortLevel << std::endl;
+  Debug("arith") << "TheoryArith::check begun " << effortLevel << std::endl;
+
+  bool newFacts = !done();
+  Result::Sat previous = d_qflraStatus;
+  if(newFacts){
+    d_qflraStatus = Result::SAT_UNKNOWN;
+    d_hasDoneWorkSinceCut = true;
+  }
 
-  d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done();
   while(!done()){
     Constraint curr = constraintFromFactQueue();
     if(curr != NullConstraint){
@@ -1366,6 +1400,7 @@ void TheoryArith::check(Effort effortLevel){
     if(inConflict()){
       revertOutOfConflict();
       outputConflicts();
+      d_qflraStatus = Result::UNSAT;
       return;
     }
   }
@@ -1379,6 +1414,7 @@ void TheoryArith::check(Effort effortLevel){
     Assert(!res || inConflict());
 
     if(inConflict()){
+      d_qflraStatus = Result::UNSAT;
       revertOutOfConflict();
       outputConflicts();
       return;
@@ -1391,20 +1427,53 @@ void TheoryArith::check(Effort effortLevel){
   }
 
   bool emmittedConflictOrSplit = false;
+
+
   Assert(d_conflicts.empty());
-  bool foundConflict = d_simplex.findModel();
-  if(foundConflict){
-    revertOutOfConflict();
+
+  d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel));
+  switch(d_qflraStatus){
+  case Result::SAT:
+    if(newFacts){
+      ++d_statistics.d_nontrivialSatChecks;
+    }
+    d_partialModel.commitAssignmentChanges();
+    d_unknownsInARow = 0;
+    break;
+  case Result::SAT_UNKNOWN:
+    ++d_unknownsInARow;
+    ++(d_statistics.d_unknownChecks);
+    Assert(!fullEffort(effortLevel));
+    d_partialModel.commitAssignmentChanges();
+    d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
+    break;
+  case Result::UNSAT:
+    d_unknownsInARow = 0;
+    if(previous == Result::SAT){
+      ++d_statistics.d_revertsOnConflicts;
+
+      revertOutOfConflict();
+      d_simplex.clearQueue();
+    }else{
+      ++d_statistics.d_commitsOnConflicts;
+
+      d_partialModel.commitAssignmentChanges();
+      revertOutOfConflict();
+    }
     outputConflicts();
     emmittedConflictOrSplit = true;
-  }else{
-    d_partialModel.commitAssignmentChanges();
+    break;
+  default:
+    Unimplemented();
   }
+  d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
 
+  // This should be fine if sat or unknown
   if(!emmittedConflictOrSplit &&
      (Options::current()->arithPropagationMode == Options::UNATE_PROP ||
       Options::current()->arithPropagationMode == Options::BOTH_PROP)){
     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
+    Assert(d_qflraStatus != Result::UNSAT);
 
     while(!d_currentPropagationList.empty()  && !inConflict()){
       Constraint curr = d_currentPropagationList.front();
@@ -1618,6 +1687,8 @@ void TheoryArith::debugPrintModel(){
   }
 }
 
+
+
 Node TheoryArith::explain(TNode n) {
 
   Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
@@ -1637,7 +1708,9 @@ Node TheoryArith::explain(TNode n) {
 
 
 void TheoryArith::propagate(Effort e) {
-  if((Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
+  // This uses model values for safety. Disable for now.
+  if(d_qflraStatus == Result::SAT &&
+     (Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
       Options::current()->arithPropagationMode == Options::BOTH_PROP)
      && hasAnyUpdates()){
     propagateCandidates();
@@ -1693,6 +1766,7 @@ void TheoryArith::propagate(Effort e) {
 }
 
 bool TheoryArith::getDeltaAtomValue(TNode n) {
+  Assert(d_qflraStatus != Result::SAT_UNKNOWN);
 
   switch (n.getKind()) {
     case kind::EQUAL: // 2 args
@@ -1712,7 +1786,7 @@ bool TheoryArith::getDeltaAtomValue(TNode n) {
 
 
 DeltaRational TheoryArith::getDeltaValue(TNode n) {
-
+  Assert(d_qflraStatus != Result::SAT_UNKNOWN);
   Debug("arith::value") << n << std::endl;
 
   switch(n.getKind()) {
@@ -1936,7 +2010,9 @@ void TheoryArith::presolve(){
 }
 
 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
-  if (getDeltaValue(a) == getDeltaValue(b)) {
+  if(d_qflraStatus == Result::SAT_UNKNOWN){
+    return EQUALITY_UNKNOWN;
+  }else if (getDeltaValue(a) == getDeltaValue(b)) {
     return EQUALITY_TRUE_IN_MODEL;
   } else {
     return EQUALITY_FALSE_IN_MODEL;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e23a9a943..556495c97 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -44,6 +44,7 @@
 #include "theory/arith/constraint.h"
 
 #include "util/stats.h"
+#include "util/result.h"
 
 #include <vector>
 #include <map>
@@ -63,6 +64,15 @@ class InstantiatorTheoryArith;
 class TheoryArith : public Theory {
   friend class InstantiatorTheoryArith;
 private:
+  enum Result::Sat d_qflraStatus;
+  // check()
+  //   !done() -> d_qflraStatus = Unknown
+  //   fullEffort(e) -> simplex returns either sat or unsat
+  //   !fullEffort(e) -> simplex returns either sat, unsat or unknown
+  //                     if unknown, save the assignment
+  //                     if unknown, the simplex priority queue cannot be emptied
+  int d_unknownsInARow;
+
   bool rowImplication(ArithVar v, bool upperBound, const DeltaRational& r);
 
   /**
@@ -113,6 +123,8 @@ private:
     }
   } d_setupLiteralCallback;
 
+
+
   /**
    * (For the moment) the type hierarchy goes as:
    * Integer <: Real
@@ -489,6 +501,14 @@ private:
     TimerStat d_boundComputationTime;
     IntStat d_boundComputations, d_boundPropagations;
 
+    IntStat d_unknownChecks;
+    IntStat d_maxUnknownsInARow;
+    AverageStat d_avgUnknownsInARow;
+
+    IntStat d_revertsOnConflicts;
+    IntStat d_commitsOnConflicts;
+    IntStat d_nontrivialSatChecks;
+
     Statistics();
     ~Statistics();
   };