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/linear_equality.cpp | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
-rw-r--r-- | src/theory/arith/linear_equality.cpp | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 7f729751b..8c7d22088 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -365,7 +365,6 @@ void LinearEqualityModule::debugCheckTracking(){ << "computed " << computed << " tracking " << d_btracking[ridx] << endl; Assert(computed == d_btracking[ridx]); - } } } @@ -574,12 +573,10 @@ void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bo Assert(sgn != 0); bool selectUb = rowUp ? (sgn > 0) : (sgn < 0); - Assert( nonbasic != v || - ( rowUp && a_ij.sgn() > 0 && c->isLowerBound()) || - ( rowUp && a_ij.sgn() < 0 && c->isUpperBound()) || - (!rowUp && a_ij.sgn() > 0 && c->isUpperBound()) || - (!rowUp && a_ij.sgn() < 0 && c->isLowerBound()) - ); + Assert(nonbasic != v || (rowUp && a_ij.sgn() > 0 && c->isLowerBound()) + || (rowUp && a_ij.sgn() < 0 && c->isUpperBound()) + || (!rowUp && a_ij.sgn() > 0 && c->isUpperBound()) + || (!rowUp && a_ij.sgn() < 0 && c->isLowerBound())); if(Debug.isOn("arith::propagateRow")){ if(nonbasic == v){ @@ -743,7 +740,7 @@ ConstraintCP LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithV fcs.addConstraint(c, coeff, adjustSgn); if(basicVar == v){ - Assert(! c->negationHasProof() ); + Assert(!c->negationHasProof()); fcs.makeLastConsequent(); } } @@ -1400,8 +1397,8 @@ void LinearEqualityModule::pop_block(BorderHeap& heap, int& brokenInBlock, int& heap.pop_heap(); }else{ // does not belong to the block - Assert((heap.direction() > 0) ? - (blockValue < top.d_diff) : (blockValue > top.d_diff)); + Assert((heap.direction() > 0) ? (blockValue < top.d_diff) + : (blockValue > top.d_diff)); break; } } |