- Adds an additional round of checks for a conflict after the difference heuristic...

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 76db6b580ded7fc8c0bf70a7a0e822ba4c892827..417115ab9fbc7dcf4e3c87ba8938faeae2231a5d 100644 (file)
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -15,10 +15,10 @@ ArithPriorityQueue::ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tab
   d_partialModel(pm), d_tableau(tableau), d_modeInUse(Collection), d_ZERO_DELTA(0,0)
 {}
 
-ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){
+ArithVar ArithPriorityQueue::dequeueInconsistentBasicVariable(){
   AlwaysAssert(!inCollectionMode());
 
-  Debug("arith_update") << "popInconsistentBasicVariable()" << endl;
+  Debug("arith_update") << "dequeueInconsistentBasicVariable()" << endl;
 
   if(inDifferenceMode()){
     while(!d_diffQueue.empty()){

diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index 9cee8b29be0d40bd47b4f4f2384c7d2a80bd480b..2f150b73a8466341110d119c504ad5831a93445d 100644 (file)
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -116,7 +116,7 @@ public:
 
   ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau);
 
-  ArithVar popInconsistentBasicVariable();
+  ArithVar dequeueInconsistentBasicVariable();
 
   void enqueueIfInconsistent(ArithVar basic);
 

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index ced76c843378adfea4f1d4332321c0f5c9d359b5..25d154bae7ec73b49bacc809a2e34acd5cab3b79 100644 (file)
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -15,11 +15,13 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
   d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
   d_statUpdateConflicts("theory::arith::UpdateConflicts", 0),
-  d_statEarlyConflicts("theory::arith::EarlyConflicts", 0),
-  d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0),
-  d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"),
-  d_pivotsAfterConflict("theory::arith::pivotsAfterConflict", 0),
-  d_checksWithWastefulPivots("theory::arith::checksWithWastefulPivots", 0),
+  d_findConflictOnTheQueueTime("theory::arith::findConflictOnTheQueueTime"),
+  d_attemptBeforeDiffSearch("theory::arith::attemptBeforeDiffSearch",0),
+  d_successBeforeDiffSearch("theory::arith::successBeforeDiffSearch",0),
+  d_attemptAfterDiffSearch("theory::arith::attemptAfterDiffSearch",0),
+  d_successAfterDiffSearch("theory::arith::successAfterDiffSearch",0),
+  d_attemptDuringVarOrderSearch("theory::arith::attemptDuringVarOrderSearch",0),
+  d_successDuringVarOrderSearch("theory::arith::successDuringVarOrderSearch",0),
   d_pivotTime("theory::arith::pivotTime"),
   d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"),
   d_avgNumRowsNotContainingOnPivot("theory::arith::avgNumRowsNotContainingOnPivot")
@@ -29,12 +31,16 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
   StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
   StatisticsRegistry::registerStat(&d_statUpdateConflicts);
-  StatisticsRegistry::registerStat(&d_statEarlyConflicts);
-  StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements);
-  StatisticsRegistry::registerStat(&d_selectInitialConflictTime);
 
-  StatisticsRegistry::registerStat(&d_pivotsAfterConflict);
-  StatisticsRegistry::registerStat(&d_checksWithWastefulPivots);
+  StatisticsRegistry::registerStat(&d_findConflictOnTheQueueTime);
+
+  StatisticsRegistry::registerStat(&d_attemptBeforeDiffSearch);
+  StatisticsRegistry::registerStat(&d_successBeforeDiffSearch);
+  StatisticsRegistry::registerStat(&d_attemptAfterDiffSearch);
+  StatisticsRegistry::registerStat(&d_successAfterDiffSearch);
+  StatisticsRegistry::registerStat(&d_attemptDuringVarOrderSearch);
+  StatisticsRegistry::registerStat(&d_successDuringVarOrderSearch);
+
   StatisticsRegistry::registerStat(&d_pivotTime);
 
   StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnUpdate);
@@ -47,12 +53,16 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
   StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
   StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
-  StatisticsRegistry::unregisterStat(&d_statEarlyConflicts);
-  StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements);
-  StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime);
 
-  StatisticsRegistry::unregisterStat(&d_pivotsAfterConflict);
-  StatisticsRegistry::unregisterStat(&d_checksWithWastefulPivots);
+  StatisticsRegistry::unregisterStat(&d_findConflictOnTheQueueTime);
+
+  StatisticsRegistry::unregisterStat(&d_attemptBeforeDiffSearch);
+  StatisticsRegistry::unregisterStat(&d_successBeforeDiffSearch);
+  StatisticsRegistry::unregisterStat(&d_attemptAfterDiffSearch);
+  StatisticsRegistry::unregisterStat(&d_successAfterDiffSearch);
+  StatisticsRegistry::unregisterStat(&d_attemptDuringVarOrderSearch);
+  StatisticsRegistry::unregisterStat(&d_successDuringVarOrderSearch);
+
   StatisticsRegistry::unregisterStat(&d_pivotTime);
 
   StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnUpdate);
@@ -299,13 +309,6 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
 
   // Pivots
   ++(d_statistics.d_statPivots);
-  if( d_foundAConflict ){
-    ++d_pivotsSinceConflict;
-    if(d_pivotsSinceConflict == 1){
-      ++(d_statistics.d_checksWithWastefulPivots);
-    }
-    ++(d_statistics.d_pivotsAfterConflict);
-  }
 
   Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_j));
   double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_j));
@@ -315,34 +318,19 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
 
   d_queue.enqueueIfInconsistent(x_j);
 
-  // Debug found conflict
-  if( !d_foundAConflict ){
-    DeltaRational beta_j = d_partialModel.getAssignment(x_j);
-
-    if(d_partialModel.belowLowerBound(x_j, beta_j, true)){
-      if(selectSlackBelow(x_j) == ARITHVAR_SENTINEL ){
-        d_foundAConflict = true;
-      }
-    }else if(d_partialModel.aboveUpperBound(x_j, beta_j, true)){
-      if(selectSlackAbove(x_j) == ARITHVAR_SENTINEL ){
-        d_foundAConflict = true;
-      }
-    }
-  }
-
   if(Debug.isOn("tableau")){
     d_tableau.printTableau();
   }
 }
 
 template <bool above>
-ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
+ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, bool first){
   ReducedRowVector& row_i = d_tableau.lookup(x_i);
 
   ArithVar slack = ARITHVAR_SENTINEL;
   uint32_t numRows = std::numeric_limits<uint32_t>::max();
 
-  bool pivotStage = d_queue.inDifferenceMode();
+  bool pivotStage = !first;
 
   for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
       nbi != end; ++nbi){
@@ -404,12 +392,16 @@ Node betterConflict(TNode x, TNode y){
   else return y;
 }
 
-Node SimplexDecisionProcedure::selectInitialConflict() {
-  Node bestConflict = Node::null();
+Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
+  TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime);
 
-  TimerStat::CodeTimer codeTimer(d_statistics.d_selectInitialConflictTime);
+  switch(type){
+  case BeforeDiffSearch:     ++(d_statistics.d_attemptBeforeDiffSearch); break;
+  case AfterDiffSearch:      ++(d_statistics.d_attemptAfterDiffSearch); break;
+  case DuringVarOrderSearch: ++(d_statistics.d_attemptDuringVarOrderSearch); break;
+  }
 
-  int conflictChanges = 0;
+  Node bestConflict = Node::null();
   ArithPriorityQueue::const_iterator i = d_queue.begin();
   ArithPriorityQueue::const_iterator end = d_queue.end();
   for(; i != end; ++i){
@@ -418,18 +410,18 @@ Node SimplexDecisionProcedure::selectInitialConflict() {
     if(d_tableau.isBasic(x_i)){
       Node possibleConflict = checkBasicForConflict(x_i);
       if(!possibleConflict.isNull()){
-        Node better = betterConflict(bestConflict, possibleConflict);
 
-        if(better != bestConflict){
-          ++conflictChanges;
-        }
-        bestConflict = better;
-        ++(d_statistics.d_statEarlyConflicts);
+        bestConflict = betterConflict(bestConflict, possibleConflict);
       }
     }
   }
-
-  if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements);
+  if(!bestConflict.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;
 }
 
@@ -438,19 +430,18 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
     return Node::null();
   }
 
-  d_foundAConflict = false;
-  d_pivotsSinceConflict = 0;
-
   d_queue.transitionToDifferenceMode();
 
   Node possibleConflict = Node::null();
   if(d_queue.size() > 1){
-    possibleConflict = selectInitialConflict();
+    possibleConflict = findConflictOnTheQueue(BeforeDiffSearch);
   }
   if(possibleConflict.isNull()){
     possibleConflict = searchForFeasibleSolution<true>(d_numVariables + 1);
   }
-
+  if(d_queue.size() > 1 && possibleConflict.isNull()){
+    possibleConflict = findConflictOnTheQueue(AfterDiffSearch);
+  }
   if(!d_queue.empty() && possibleConflict.isNull()){
     d_queue.transitionToVariableOrderMode();
     possibleConflict = searchForFeasibleSolution<false>(0);
@@ -477,12 +468,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
   const DeltaRational& beta = d_partialModel.getAssignment(basic);
 
   if(d_partialModel.belowLowerBound(basic, beta, true)){
-    ArithVar x_j = selectSlackBelow(basic);
+    ArithVar x_j = selectSlackBelow(basic, true);
     if(x_j == ARITHVAR_SENTINEL ){
       return generateConflictBelow(basic);
     }
   }else if(d_partialModel.aboveUpperBound(basic, beta, true)){
-    ArithVar x_j = selectSlackAbove(basic);
+    ArithVar x_j = selectSlackAbove(basic, true);
     if(x_j == ARITHVAR_SENTINEL ){
       return generateConflictAbove(basic);
     }
@@ -495,10 +486,12 @@ template <bool limitIterations>
 Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
   Debug("arith") << "updateInconsistentVars" << endl;
 
+  static const uint32_t CHECK_PERIOD = 1000;
+
   while(!limitIterations || remainingIterations > 0){
     if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
 
-    ArithVar x_i = d_queue.popInconsistentBasicVariable();
+    ArithVar x_i = d_queue.dequeueInconsistentBasicVariable();
     Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
     if(x_i == ARITHVAR_SENTINEL){
       Debug("arith_update") << "No inconsistent variables" << endl;
@@ -511,7 +504,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
     ArithVar x_j = ARITHVAR_SENTINEL;
 
     if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
-      x_j = selectSlackBelow(x_i);
+      x_j = selectSlackBelow(x_i, !limitIterations);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictBelow(x_i); //unsat
@@ -520,7 +513,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
       pivotAndUpdate(x_i, x_j, l_i);
 
     }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
-      x_j = selectSlackAbove(x_i);
+      x_j = selectSlackAbove(x_i, !limitIterations);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictAbove(x_i); //unsat
@@ -534,6 +527,13 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
     if(!earlyConflict.isNull()){
       return earlyConflict;
     }
+    //Once every CHECK_PERIOD examine the entire queue for conflicts
+    // if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){
+    //   Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch);
+    //   if(!earlyConflict.isNull()){
+    //     return earlyConflict;
+    //   }
+    // }
   }
   AlwaysAssert(limitIterations && remainingIterations == 0);
 
@@ -646,23 +646,6 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe
   return sum;
 }
 
-/*
-void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){
-  Assert(d_tableau.isBasic(basic));
-  if(!d_partialModel.assignmentIsConsistent(basic)){
-    if(d_pivotStage){
-      const DeltaRational& beta = d_partialModel.getAssignment(basic);
-      DeltaRational diff = d_partialModel.belowLowerBound(basic,beta,true) ?
-        d_partialModel.getLowerBound(basic) - beta:
-        beta - d_partialModel.getUpperBound(basic);
-      d_griggioRuleQueue.push(make_pair(basic,diff));
-    }else{
-      d_possiblyInconsistent.push(basic);
-    }
-  }
-}
-*/
-
 /**
  * This check is quite expensive.
  * It should be wrapped in a Debug.isOn() guard.

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 9fed7dc0bec719eabec59ebf8e9a4c21fc2bb3c7..3b86935bd078685325e3170797566b297e4eae9b 100644 (file)
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -108,7 +108,9 @@ public:
 private:
   template <bool limitIterations> Node searchForFeasibleSolution(uint32_t maxIterations);
 
-  Node selectInitialConflict();
+  enum SearchPeriod {BeforeDiffSearch, AfterDiffSearch, DuringVarOrderSearch};
+
+  Node findConflictOnTheQueue(SearchPeriod period);
 
 private:
   /**
@@ -117,16 +119,22 @@ private:
    * in the tableau that can "take up the slack" to let x_i satisfy its bounds.
    * This returns TNode::null() if none exists.
    *
+   * If first is true, return the first ArithVar in the row to satisfy these conditions.
+   * If first is false, return the ArithVar with the smallest row count.
+   *
    * 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)
    */
-  template <bool above>  ArithVar selectSlack(ArithVar x_i);
-
-  ArithVar selectSlackBelow(ArithVar x_i) { return selectSlack<false>(x_i); }
-  ArithVar selectSlackAbove(ArithVar x_i) { return selectSlack<true>(x_i);  }
+  template <bool above>  ArithVar selectSlack(ArithVar x_i, bool first);
+  ArithVar selectSlackBelow(ArithVar x_i, bool first) {
+    return selectSlack<false>(x_i, first);
+  }
+  ArithVar selectSlackAbove(ArithVar x_i, bool first) {
+    return selectSlack<true>(x_i, first);
+  }
   /**
    * Returns the smallest basic variable whose assignment is not consistent
    * with its upper and lower bounds.
@@ -166,9 +174,6 @@ private:
    */
   Node checkBasicForConflict(ArithVar b);
 
-  bool d_foundAConflict; // This field is used for statistics keeping ONLY!
-  unsigned d_pivotsSinceConflict; // This field is used for statistics keeping ONLY!
-
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
   public:
@@ -176,11 +181,13 @@ private:
 
     IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
     IntStat d_statUpdateConflicts;
-    IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements;
 
-    TimerStat d_selectInitialConflictTime;
+    TimerStat d_findConflictOnTheQueueTime;
+
+    IntStat d_attemptBeforeDiffSearch, d_successBeforeDiffSearch;
+    IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch;
+    IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch;
 
-    IntStat d_pivotsAfterConflict, d_checksWithWastefulPivots;
     TimerStat d_pivotTime;
 
     AverageStat d_avgNumRowsNotContainingOnUpdate;