From: Tim King <taking@cs.nyu.edu>
Date: Wed, 8 Nov 2017 02:25:22 +0000 (-0800)
Subject: Combining d_conflictHasBeenRaised and d_conflictIndex into a CDMaybe. (#1332)
X-Git-Tag: cvc5-1.0.0~5496
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b9f849471b752a4188230153d1b8b7b8a0a930b;p=cvc5.git

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 5b61385f3..744bc769e 100644
--- 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 292f2b856..367ea8faa 100644
--- 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();
   }
 
   /**