- This commit adds some debugging information to ArithPriorityQueue.

- There was a missing break statement in ArithPriorityQueue. This addresses the bug discovered in the debug regression (http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1566&reference_id=1548&category=1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29&p=10).

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 417115ab9fbc7dcf4e3c87ba8938faeae2231a5d..14a228e62deef3ddadec65fc713230c882007c25 100644 (file)
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -70,6 +70,7 @@ void ArithPriorityQueue::enqueueIfInconsistent(ArithVar basic){
     case VariableOrder:
       d_varOrderQueue.push_back(basic);
       push_heap(d_varOrderQueue.begin(), d_varOrderQueue.end(), std::greater<ArithVar>());
+      break;
     case Difference:
       d_diffQueue.push_back(computeDiff(basic));
       push_heap(d_diffQueue.begin(), d_diffQueue.end());
@@ -85,6 +86,8 @@ void ArithPriorityQueue::transitionToDifferenceMode() {
   Assert(d_varOrderQueue.empty());
   Assert(d_diffQueue.empty());
 
+  Debug("arith::priorityqueue") << "transitionToDifferenceMode()" << endl;
+
   ArithVarArray::const_iterator i = d_candidates.begin(), end = d_candidates.end();
   for(; i != end; ++i){
     ArithVar var = *i;
@@ -106,6 +109,8 @@ void ArithPriorityQueue::transitionToVariableOrderMode() {
   Assert(d_varOrderQueue.empty());
   Assert(d_candidates.empty());
 
+  Debug("arith::priorityqueue") << "transitionToVariableOrderMode()" << endl;
+
   DifferenceArray::const_iterator i = d_diffQueue.begin(), end = d_diffQueue.end();
   for(; i != end; ++i){
     ArithVar var = (*i).variable();
@@ -128,6 +133,8 @@ void ArithPriorityQueue::transitionToCollectionMode() {
   Assert(d_candidates.empty());
   Assert(d_varOrderQueue.empty());
 
+  Debug("arith::priorityqueue") << "transitionToCollectionMode()" << endl;
+
   d_modeInUse = Collection;
 }
 

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 25d154bae7ec73b49bacc809a2e34acd5cab3b79..c8f1ce3e8c870252e370da1d67ff3ab77b49e8f0 100644 (file)
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -429,6 +429,11 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   if(d_queue.empty()){
     return Node::null();
   }
+  static unsigned int instance = 0;
+
+  ++instance;
+  Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() "
+                                         << instance << endl;
 
   d_queue.transitionToDifferenceMode();
 
@@ -459,6 +464,9 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
 
   Assert(d_queue.inCollectionMode());
 
+  Debug("arith::updateInconsistentVars") << "end updateInconsistentVars() "
+                                         << instance << endl;
+
   return possibleConflict;
 }