This is further work towards a centralized approach for equality engines.
This PR merges the eqNotifyTriggerEquality callback with the eqNotifyTriggerPredicate callback, and adds assertions that capture the current behavior. It furthermore makes addTriggerEquality private in equality engine and invoked as a special case of addTriggerPredicate. Note this PR does not impact the internal implementation of these methods in equality engine, which indeed is different.
There are two reasons to merge these callbacks:
(1) all theories implement exactly the same method for the two callbacks, whenever they implement both. It would be trivial to do something different (by case splitting on the kind of predicate that is being notified), and moreover it is not recommended they do anything other than immediately propagate the predicate (regardless of whether it is an equality).
(2) It leads to some confusion with eqNotifyTriggerTermEquality, which is invoked when two trigger terms are merged.
: d_acm(acm)
{}
-bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerEquality(TNode equality, bool value) {
- Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
+bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerPredicate(
+ TNode predicate, bool value)
+{
+ Assert(predicate.getKind() == kind::EQUAL);
+ Debug("arith::congruences")
+ << "ArithCongruenceNotify::eqNotifyTriggerPredicate(" << predicate << ", "
+ << (value ? "true" : "false") << ")" << std::endl;
if (value) {
- return d_acm.propagate(equality);
- } else {
- return d_acm.propagate(equality.notNode());
+ return d_acm.propagate(predicate);
}
-}
-bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerPredicate(TNode predicate, bool value) {
- Unreachable();
+ return d_acm.propagate(predicate.notNode());
}
bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
public:
ArithCongruenceNotify(ArithCongruenceManager& acm);
- bool eqNotifyTriggerEquality(TNode equality, bool value) override;
-
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
bool eqNotifyTriggerTermEquality(TheoryId tag,
case kind::EQUAL:
// Add the trigger for equality
// NOTE: note that if the equality is true or false already, it might not be added
- d_equalityEngine->addTriggerEquality(node);
+ d_equalityEngine->addTriggerPredicate(node);
break;
case kind::SELECT: {
// Invariant: array terms should be preregistered before being added to the equality engine
public:
NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
- // Just forward to arrays
- if (value) {
- return d_arrays.propagate(equality);
- } else {
- return d_arrays.propagate(equality.notNode());
- }
- }
-
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
- Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
+ Debug("arrays::propagate")
+ << spaces(d_arrays.getSatContext()->getLevel())
+ << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", "
+ << (value ? "true" : "false") << ")" << std::endl;
// Just forward to arrays
if (value) {
return d_arrays.propagate(predicate);
- } else {
- return d_arrays.propagate(predicate.notNode());
}
+ return d_arrays.propagate(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
void CoreSolver::preRegister(TNode node) {
d_preregisterCalled = true;
if (node.getKind() == kind::EQUAL) {
- d_equalityEngine->addTriggerEquality(node);
+ d_equalityEngine->addTriggerPredicate(node);
if (d_useSlicer)
{
d_slicer->processEquality(node);
return true;
}
-bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
- Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
- if (value) {
- return d_solver.storePropagation(equality);
- } else {
- return d_solver.storePropagation(equality.notNode());
- }
-}
-
bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
if (value) {
return d_solver.storePropagation(predicate);
- } else {
- return d_solver.storePropagation(predicate.notNode());
}
+ return d_solver.storePropagation(predicate.notNode());
}
bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
public:
NotifyClass(CoreSolver& solver): d_solver(solver) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override;
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
collectTerms( n );
switch (n.getKind()) {
case kind::EQUAL:
- // Add the trigger for equality
- d_equalityEngine->addTriggerEquality(n);
- break;
case kind::APPLY_TESTER:
+ // add predicate trigger for testers and equalities
// Get triggered for both equal and dis-equal
d_equalityEngine->addTriggerPredicate(n);
break;
TheoryDatatypes& d_dt;
public:
NotifyClass(TheoryDatatypes& dt): d_dt(dt) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- Debug("dt") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
- if (value) {
- return d_dt.propagate(equality);
- } else {
- // We use only literal triggers so taking not is safe
- return d_dt.propagate(equality.notNode());
- }
- }
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
return d_dt.propagate(predicate);
- } else {
- return d_dt.propagate(predicate.notNode());
}
+ return d_dt.propagate(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
*/
void eqNotifyNewClass(TNode t) override;
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- return true;
- }
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
return true;
// Add to the equality engine
if (k == kind::EQUAL)
{
- d_equalityEngine->addTriggerEquality(node);
+ d_equalityEngine->addTriggerPredicate(node);
}
else
{
return true;
}
-bool TheoryFp::NotifyClass::eqNotifyTriggerEquality(TNode equality,
- bool value) {
- Debug("fp-eq")
- << "TheoryFp::eqNotifyTriggerEquality(): call back as equality "
- << equality << " is " << value << std::endl;
-
- if (value) {
- return d_theorySolver.handlePropagation(equality);
- } else {
- return d_theorySolver.handlePropagation(equality.notNode());
- }
-}
-
bool TheoryFp::NotifyClass::eqNotifyTriggerPredicate(TNode predicate,
bool value) {
Debug("fp-eq")
if (value) {
return d_theorySolver.handlePropagation(predicate);
- } else {
- return d_theorySolver.handlePropagation(predicate.notNode());
}
+ return d_theorySolver.handlePropagation(predicate.notNode());
}
bool TheoryFp::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1,
public:
NotifyClass(TheoryFp& solver) : d_theorySolver(solver) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override;
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
ConjectureGenerator& d_sg;
public:
NotifyClass(ConjectureGenerator& sg): d_sg(sg) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- return true;
- }
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
return true;
public:
NotifyClass(TheorySep& sep) : d_sep(sep) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
Debug("sep::propagate")
- << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", "
+ << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", "
<< (value ? "true" : "false") << ")" << std::endl;
+ Assert(predicate.getKind() == kind::EQUAL);
// Just forward to sep
if (value)
{
- return d_sep.propagate(equality);
- }
- else
- {
- return d_sep.propagate(equality.notNode());
+ return d_sep.propagate(predicate);
}
+ return d_sep.propagate(predicate.notNode());
}
-
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
- {
- Unreachable();
- }
-
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
/**************************** eq::NotifyClass *****************************/
-bool TheorySets::NotifyClass::eqNotifyTriggerEquality(TNode equality,
- bool value)
-{
- Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = "
- << equality << " value = " << value << std::endl;
- if (value)
- {
- return d_theory.propagate(equality);
- }
- else
- {
- // We use only literal triggers so taking not is safe
- return d_theory.propagate(equality.notNode());
- }
-}
-
bool TheorySets::NotifyClass::eqNotifyTriggerPredicate(TNode predicate,
bool value)
{
{
return d_theory.propagate(predicate);
}
- else
- {
- return d_theory.propagate(predicate.notNode());
- }
+ return d_theory.propagate(predicate.notNode());
}
bool TheorySets::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag,
{
public:
NotifyClass(TheorySetsPrivate& theory) : d_theory(theory) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override;
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
<< std::endl;
switch (node.getKind())
{
- case kind::EQUAL: d_equalityEngine->addTriggerEquality(node); break;
- case kind::MEMBER: d_equalityEngine->addTriggerPredicate(node); break;
+ case kind::EQUAL:
+ case kind::MEMBER:
+ {
+ // add trigger predicate for equality and membership
+ d_equalityEngine->addTriggerPredicate(node);
+ }
+ break;
case kind::CARD: d_equalityEngine->addTriggerTerm(node, THEORY_SETS); break;
default: d_equalityEngine->addTerm(node); break;
}
void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
d_registeredEqualities.insert(equality);
- d_equalityEngine.addTriggerEquality(equality);
+ d_equalityEngine.addTriggerPredicate(equality);
checkForConflict();
}
SharedTermsDatabase& d_sharedTerms;
public:
EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- d_sharedTerms.propagateEquality(equality, value);
- return true;
- }
-
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
- Unreachable();
+ Assert(predicate.getKind() == kind::EQUAL);
+ d_sharedTerms.propagateEquality(predicate, value);
return true;
}
ss << "Equality between regular expressions is not supported";
throw LogicException(ss.str());
}
- ee->addTriggerEquality(n);
+ ee->addTriggerPredicate(n);
return;
}
else if (k == STRING_IN_REGEXP)
class NotifyClass : public eq::EqualityEngineNotify {
public:
NotifyClass(TheoryStrings& ts) : d_str(ts), d_state(ts.d_state) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality
- << ", " << (value ? "true" : "false") << ")" << std::endl;
- if (value)
- {
- return d_str.propagate(equality);
- }
- else
- {
- // We use only literal triggers so taking not is safe
- return d_str.propagate(equality.notNode());
- }
- }
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
return d_str.propagate(predicate);
- } else {
- return d_str.propagate(predicate.notNode());
}
+ return d_str.propagate(predicate.notNode());
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
// If they are equal or disequal already, no need for the trigger
if (areEqual(eq[0], eq[1])) {
- d_notify.eqNotifyTriggerEquality(eq, true);
+ d_notify.eqNotifyTriggerPredicate(eq, true);
skipTrigger = true;
}
if (areDisequal(eq[0], eq[1], true)) {
- d_notify.eqNotifyTriggerEquality(eq, false);
+ d_notify.eqNotifyTriggerPredicate(eq, false);
skipTrigger = true;
}
}
void EqualityEngine::addTriggerPredicate(TNode predicate) {
- Assert(predicate.getKind() != kind::NOT
- && predicate.getKind() != kind::EQUAL);
+ Assert(predicate.getKind() != kind::NOT);
+ if (predicate.getKind() == kind::EQUAL)
+ {
+ // equality is handled separately
+ return addTriggerEquality(predicate);
+ }
Assert(d_congruenceKinds.tst(predicate.getKind()))
<< "No point in adding non-congruence predicates";
d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId));
}
storePropagatedDisequality(THEORY_LAST, lhsId, rhsId);
- if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger,
- triggerInfo.d_polarity))
+ if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger,
+ triggerInfo.d_polarity))
{
d_done = true;
}
else
{
// Equalities are simple
- if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger,
- triggerInfo.d_polarity))
+ if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger,
+ triggerInfo.d_polarity))
{
d_done = true;
}
/** The internal addTerm */
void addTermInternal(TNode t, bool isOperator = false);
+ /**
+ * Adds a notify trigger for equality. When equality becomes true
+ * eqNotifyTriggerPredicate will be called with value = true, and when
+ * equality becomes false eqNotifyTriggerPredicate will be called with value =
+ * false.
+ */
+ void addTriggerEquality(TNode equality);
-public:
-
+ public:
/**
* Adds a term to the term database.
*/
TNode getTriggerTermRepresentative(TNode t, TheoryId theoryTag) const;
/**
- * Adds a notify trigger for equality. When equality becomes true eqNotifyTriggerEquality
- * will be called with value = true, and when equality becomes false eqNotifyTriggerEquality
- * will be called with value = false.
- */
- void addTriggerEquality(TNode equality);
-
- /**
- * Adds a notify trigger for the predicate p. When the predicate becomes true
- * eqNotifyTriggerPredicate will be called with value = true, and when equality becomes false
+ * Adds a notify trigger for the predicate p, where notice that p can be
+ * an equality. When the predicate becomes true, eqNotifyTriggerPredicate will
+ * be called with value = true, and when predicate becomes false
* eqNotifyTriggerPredicate will be called with value = false.
+ *
+ * Notice that if p is an equality, then we use a separate method for
+ * determining when to call eqNotifyTriggerPredicate.
*/
void addTriggerPredicate(TNode predicate);
virtual ~EqualityEngineNotify(){};
/**
- * Notifies about a trigger equality that became true or false.
- *
- * @param equality the equality that became true or false
- * @param value the value of the equality
- */
- virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0;
-
- /**
- * Notifies about a trigger predicate that became true or false.
+ * Notifies about a trigger predicate that became true or false. Notice that
+ * predicate can be an equality.
*
* @param predicate the trigger predicate that became true or false
* @param value the value of the predicate
class EqualityEngineNotifyNone : public EqualityEngineNotify
{
public:
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- return true;
- }
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
return true;
switch (node.getKind()) {
case kind::EQUAL:
// Add the trigger for equality
- d_equalityEngine->addTriggerEquality(node);
+ d_equalityEngine->addTriggerPredicate(node);
break;
case kind::APPLY_UF:
case kind::HO_APPLY:
public:
NotifyClass(TheoryUF& uf): d_uf(uf) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) override
- {
- Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
- if (value) {
- return d_uf.propagate(equality);
- } else {
- // We use only literal triggers so taking not is safe
- return d_uf.propagate(equality.notNode());
- }
- }
-
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
projects / cvc5.git / commitdiff