diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-04 00:20:10 -0800 |
---|---|---|
committer | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-16 16:52:50 -0700 |
commit | 53a07d0331d71656904a7333b5ed0c835d7d4c38 (patch) | |
tree | acaa2afea8422ee55ced55526d0cd6b43fd14720 /src/theory/arith/constraint.cpp | |
parent | f4cd63a00f1c8cc9e4d9e42fd171f7cb1a64aaab (diff) |
Expand the definition of a "simple" farkas proof.
Before, a "simple farkas proof" was one that just applied the farkas
lemma.
Now it allows for the antecedents to (optionally) be tightened.
Note that hasSimpleFarkasProof was (and is) dead code.
We will use it to decide whether to print a proof or a hole.
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 36 |
1 files changed, 27 insertions, 9 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 56703c12a..98ce07fbc 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -500,21 +500,39 @@ bool Constraint::hasSimpleFarkasProof() const << std::endl; return false; } - const ConstraintRule& rule = getConstraintRule(); - AntecedentId antId = rule.d_antecedentEnd; - ConstraintCP antecdent = d_database->getAntecedent(antId); - while (antecdent != NullConstraint) + + // For each antecdent ... + for (AntecedentId i = getConstraintRule().d_antecedentEnd; + i != AntecedentIdSentinel; + --i) { - if (antecdent->getProofType() != AssumeAP) + ConstraintCP a = d_database->getAntecedent(i); + // ... that antecdent must be an assumption ... + if (a->isAssumption()) + { + continue; + } + + // ... OR a tightened assumption ... + if (a->hasIntTightenProof() + && a->getConstraintRule().d_antecedentEnd != AntecedentIdSentinel + && d_database->getAntecedent(a->getConstraintRule().d_antecedentEnd) + ->isAssumption()) + + { + continue; + } + + // ... otherwise, we do not have a simple Farkas proof. + if (Debug.isOn("constraints::hsfp")) { Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there " "is an antecdent w/ rule "; - antecdent->getConstraintRule().print(Debug("constraints::hsfp")); + a->getConstraintRule().print(Debug("constraints::hsfp")); Debug("constraints::hsfp") << std::endl; - return false; } - --antId; - antecdent = d_database->getAntecedent(antId); + + return false; } return true; } |