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.cpp | |
| parent | 36abd7a3687cb20d059a8c930177277995b562e8 (diff) | |
Combining d_conflictHasBeenRaised and d_conflictIndex into a CDMaybe. (#1332)
Diffstat (limited to 'src/theory/arith/dio_solver.cpp')
| -rw-r--r-- | src/theory/arith/dio_solver.cpp | 31 |
1 files changed, 15 insertions, 16 deletions
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), |