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/soi_simplex.cpp | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/arith/soi_simplex.cpp')
-rw-r--r-- | src/theory/arith/soi_simplex.cpp | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index e23273a09..e50d9d060 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -405,7 +405,8 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes 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)){ @@ -642,7 +643,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){ if(d_errorSize <= 2){ ArithVarVec inError; d_errorSet.pushFocusInto(inError); - + Assert(debugIsASet(inError)); subsets.push_back(inError); return subsets; @@ -712,7 +713,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){ if(hasParticipated.isMember(v)){ continue; } hasParticipated.add(v); - + Assert(d_soiVar == ARITHVAR_SENTINEL); //d_soiVar's row = \sumofinfeasibilites underConstruction ArithVarVec underConstruction; @@ -770,7 +771,6 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){ // } } - Assert(d_soiVar == ARITHVAR_SENTINEL); Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets done" << endl; return subsets; @@ -781,7 +781,7 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, subset); Assert(!subset.empty()); Assert(!d_conflictBuilder->underConstruction()); - + Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) start" << endl; bool success = false; @@ -791,7 +791,6 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ ConstraintP violated = d_errorSet.getViolated(e); Assert(violated != NullConstraint); - int sgn = d_errorSet.getSgn(e); const Rational& violatedCoeff = sgn > 0 ? d_negOne : d_posOne; Debug("arith::generateSOIConflict") << "basic error var: " @@ -815,7 +814,7 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ // pick a violated constraint arbitrarily. any of them may be selected for the conflict Assert(d_conflictBuilder->underConstruction()); Assert(d_conflictBuilder->consequentIsSet()); - + for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){ const Tableau::Entry& entry = *i; ArithVar v = entry.getColVar(); @@ -864,7 +863,7 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ generateSOIConflict(d_qeConflict); }else{ vector<ArithVarVec> subsets = greedyConflictSubsets(); - Assert( d_soiVar == ARITHVAR_SENTINEL); + Assert(d_soiVar == ARITHVAR_SENTINEL); bool anySuccess = false; Assert(!subsets.empty()); for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){ @@ -879,7 +878,7 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ } Assert(anySuccess); } - Assert( d_soiVar == ARITHVAR_SENTINEL); + Assert(d_soiVar == ARITHVAR_SENTINEL); d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization); //reportConflict(conf); do not do this. We need a custom explanations! @@ -965,7 +964,6 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ Assert(d_conflictVariables.empty()); Assert(d_soiVar == ARITHVAR_SENTINEL); - //d_scores.purge(); d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiFocusConstructionTimer); |