Combining d_conflictHasBeenRaised and d_conflictIndex into a CDMaybe. (#1332)

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 5b61385f33c56b046b890f502a41fcfac10833b1..744bc769ec5279da34d92769f67a7125e7d6f834 100644 (file)
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -32,22 +32,21 @@ inline Node makeIntegerVariable(){
   return curr->mkSkolem("intvar", curr->integerType(), "is an integer variable created by the dio solver");
 }
 
-DioSolver::DioSolver(context::Context* ctxt) :
-  d_lastUsedProofVariable(ctxt,0),
-  d_inputConstraints(ctxt),
-  d_nextInputConstraintToEnqueue(ctxt, 0),
-  d_trail(ctxt),
-  d_subs(ctxt),
-  d_currentF(),
-  d_savedQueue(ctxt),
-  d_savedQueueIndex(ctxt, 0),
-  d_conflictHasBeenRaised(ctxt, false),
-  d_maxInputCoefficientLength(ctxt, 0),
-  d_usedDecomposeIndex(ctxt, false),
-  d_lastPureSubstitution(ctxt, 0),
-  d_pureSubstitionIter(ctxt, 0),
-  d_decompositionLemmaQueue(ctxt)
-{}
+DioSolver::DioSolver(context::Context* ctxt)
+    : d_lastUsedProofVariable(ctxt, 0),
+      d_inputConstraints(ctxt),
+      d_nextInputConstraintToEnqueue(ctxt, 0),
+      d_trail(ctxt),
+      d_subs(ctxt),
+      d_currentF(),
+      d_savedQueue(ctxt),
+      d_savedQueueIndex(ctxt, 0),
+      d_conflictIndex(ctxt),
+      d_maxInputCoefficientLength(ctxt, 0),
+      d_usedDecomposeIndex(ctxt, false),
+      d_lastPureSubstitution(ctxt, 0),
+      d_pureSubstitionIter(ctxt, 0),
+      d_decompositionLemmaQueue(ctxt) {}
 
 DioSolver::Statistics::Statistics() :
   d_conflictCalls("theory::arith::dio::conflictCalls",0),

diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 292f2b8563a76b25551940056b98218c71c40dc1..367ea8faab670cbaee778a643ee14bce8240cd5e 100644 (file)
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -26,6 +26,7 @@
 
 #include "base/output.h"
 #include "context/cdlist.h"
+#include "context/cdmaybe.h"
 #include "context/cdo.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
@@ -147,9 +148,7 @@ private:
   std::deque<TrailIndex> d_currentF;
   context::CDList<TrailIndex> d_savedQueue;
   context::CDO<size_t> d_savedQueueIndex;
-
-  context::CDO<bool> d_conflictHasBeenRaised;
-  TrailIndex d_conflictIndex;
+  context::CDMaybe<TrailIndex> d_conflictIndex;
 
   /**
    * Drop derived constraints with a coefficient length larger than
@@ -225,21 +224,18 @@ private:
    * Returns true if the context dependent flag for conflicts
    * has been raised.
    */
-  bool inConflict() const{
-    return d_conflictHasBeenRaised;
-  }
+  bool inConflict() const { return d_conflictIndex.isSet(); }
 
   /** Raises a conflict at the index ti. */
   void raiseConflict(TrailIndex ti){
     Assert(!inConflict());
-    d_conflictHasBeenRaised = true;
-    d_conflictIndex = ti;
+    d_conflictIndex.set(ti);
   }
 
   /** Returns the conflict index. */
   TrailIndex getConflictIndex() const{
     Assert(inConflict());
-    return d_conflictIndex;
+    return d_conflictIndex.get();
   }
 
   /**