diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-16 12:35:17 -0700 |
|---|---|---|
| committer | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-16 16:52:50 -0700 |
| commit | d6b04a419b5b8032ac715d4318a907ae871209f6 (patch) | |
| tree | a1c4b887078f343999c544e0cf2614ca5114eff6 | |
| parent | 3dc80e17818632e1dd4fd65e64c302d944b23db9 (diff) | |
clang-format
| -rw-r--r-- | src/theory/arith/constraint.cpp | 3 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 4 |
2 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index cdab772f8..11c6c15a7 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -503,8 +503,7 @@ bool Constraint::hasSimpleFarkasProof() const // For each antecdent ... AntecedentId i = getConstraintRule().d_antecedentEnd; - for (ConstraintCP a = d_database->getAntecedent(i); - a != NullConstraint; + for (ConstraintCP a = d_database->getAntecedent(i); a != NullConstraint; a = d_database->getAntecedent(--i)) { // ... that antecdent must be an assumption ... diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 54bac3e26..4e2a5bba1 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4954,7 +4954,9 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C Assert(coeffs != RationalVectorPSentinel); Assert(conflictInFarkasCoefficientOrder.getNumChildren() == coeffs->size()); - if (std::all_of(explain.begin(), explain.end(), [](ConstraintCP c) { return c->isAssumption() || c->hasIntTightenProof(); })) + if (std::all_of(explain.begin(), explain.end(), [](ConstraintCP c) { + return c->isAssumption() || c->hasIntTightenProof(); + })) { d_containing.d_proofRecorder->saveFarkasCoefficients( conflictInFarkasCoefficientOrder, coeffs); |