<< 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;
}
/**
* @brief Returns whether this constraint is provable using a Farkas
- * proof that has input assertions as its antecedents.
+ * proof applied to (possibly tightened) input assertions.
*
* An example of a constraint that has a simple Farkas proof:
* x <= 0 proven from x + y <= 0 and x - y <= 0.
*
- * An example of a constraint that does not have a simple Farkas proof:
+ * An example of another constraint that has a simple Farkas proof:
* x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y
- * (since integer reasoning is also required!).
- * Another example of a constraint that might be proven without a simple
+ * (integer bound-tightening is applied first!).
+ *
+ * An example of a constraint that might be proven **without** a simple
* Farkas proof:
* x < 0 proven from not(x == 0) and not(x > 0).
*