diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/theory/arith/fc_simplex.cpp | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/arith/fc_simplex.cpp')
-rw-r--r-- | src/theory/arith/fc_simplex.cpp | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 827323302..29177d3f4 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -118,8 +118,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ }else if(d_errorSet.errorEmpty()){ //if(verbose){ Message() << "fcFindModel("<< instance <<") fixed itself" << endl; } Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl; - if(verbose) - Assert(!d_errorSet.moreSignals()); + if (verbose) Assert(!d_errorSet.moreSignals()); Assert(d_conflictVariables.empty()); return Result::SAT; } @@ -264,7 +263,7 @@ WitnessImprovement FCSimplexDecisionProcedure::adjustFocusShrank(const ArithVarV WitnessImprovement FCSimplexDecisionProcedure::focusDownToJust(ArithVar v){ // uint32_t newErrorSize = d_errorSet.errorSize(); // uint32_t newFocusSize = d_errorSet.focusSize(); - Assert(d_focusSize == d_errorSet.focusSize()); + Assert(d_focusSize == d_errorSet.focusSize()); Assert(d_focusSize > 1); Assert(d_errorSet.inFocus(v)); @@ -558,7 +557,8 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit int prevFocusSgn = d_errorSet.popSignal(); if(d_tableau.isBasic(updated)){ - Assert(!d_variables.assignmentIsConsistent(updated) == d_errorSet.inError(updated)); + Assert(!d_variables.assignmentIsConsistent(updated) + == d_errorSet.inError(updated)); if(Debug.isOn("updateAndSignal")){debugPrintSignal(updated);} if(!d_variables.assignmentIsConsistent(updated)){ if(checkBasicForConflict(updated)){ @@ -582,7 +582,8 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit } if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } - Assert(debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize())); + Assert( + debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize())); adjustFocusAndError(selected, focusChanges); } @@ -729,7 +730,6 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ Assert(d_conflictVariables.empty()); Assert(d_focusErrorVar == ARITHVAR_SENTINEL); - d_scores.purge(); d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); @@ -752,8 +752,8 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ d_focusSize = d_errorSet.focusSize(); - Assert( d_errorSize == d_focusSize); - Assert( d_errorSize >= 1 ); + Assert(d_errorSize == d_focusSize); + Assert(d_errorSize >= 1); d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); @@ -795,7 +795,8 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ if(verbose){ debugDualLike(w, Message(), instance, prevFocusSize, prevErrorSize); } - Assert(debugDualLike(w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize)); + Assert(debugDualLike( + w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize)); } |