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/callbacks.cpp | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/arith/callbacks.cpp')
-rw-r--r-- | src/theory/arith/callbacks.cpp | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index a11dd729b..158a81e8d 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -93,13 +93,13 @@ void FarkasConflictBuilder::reset(){ /* Adds a constraint to the constraint under construction. */ void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){ - Assert(!PROOF_ON() || - (!underConstruction() && d_constraints.empty() && d_farkas.empty()) || - (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); + Assert( + !PROOF_ON() + || (!underConstruction() && d_constraints.empty() && d_farkas.empty()) + || (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); Assert(PROOF_ON() || d_farkas.empty()); Assert(c->isTrue()); - if(d_consequent == NullConstraint){ d_consequent = c; } else { @@ -136,7 +136,7 @@ void FarkasConflictBuilder::makeLastConsequent(){ d_consequentSet = true; } - Assert(! d_consequent->negationHasProof() ); + Assert(!d_consequent->negationHasProof()); Assert(d_consequentSet); } @@ -144,9 +144,10 @@ void FarkasConflictBuilder::makeLastConsequent(){ ConstraintCP FarkasConflictBuilder::commitConflict(){ Assert(underConstruction()); Assert(!d_constraints.empty()); - Assert(!PROOF_ON() || - (!underConstruction() && d_constraints.empty() && d_farkas.empty()) || - (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); + Assert( + !PROOF_ON() + || (!underConstruction() && d_constraints.empty() && d_farkas.empty()) + || (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); Assert(PROOF_ON() || d_farkas.empty()); Assert(d_consequentSet); @@ -156,7 +157,7 @@ ConstraintCP FarkasConflictBuilder::commitConflict(){ reset(); Assert(!underConstruction()); - Assert( not_c->inConflict() ); + Assert(not_c->inConflict()); Assert(!d_consequentSet); return not_c; } |