diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-07 18:25:22 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-07 20:25:22 -0600 |
commit | 9b9f849471b752a4188230153d1b8b7b8a0a930b (patch) | |
tree | 660225889cd0489a40d5925bb81533f81100699c /src/theory/arith/dio_solver.h | |
parent | 36abd7a3687cb20d059a8c930177277995b562e8 (diff) |
Combining d_conflictHasBeenRaised and d_conflictIndex into a CDMaybe. (#1332)
Diffstat (limited to 'src/theory/arith/dio_solver.h')
-rw-r--r-- | src/theory/arith/dio_solver.h | 14 |
1 files changed, 5 insertions, 9 deletions
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(); } /** |