From eee14382af077bd043d53b75c038050b325dd04a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Aug 2020 20:34:39 -0500 Subject: Simplify trigger notifications in equality engine (#4921) 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. --- src/theory/sets/theory_sets.cpp | 21 +-------------------- 1 file changed, 1 insertion(+), 20 deletions(-) (limited to 'src/theory/sets/theory_sets.cpp') diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index fc544f46f..2627f72e3 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -206,22 +206,6 @@ bool TheorySets::isEntailed( Node n, bool pol ) { /**************************** 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) { @@ -231,10 +215,7 @@ bool TheorySets::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, { return d_theory.propagate(predicate); } - else - { - return d_theory.propagate(predicate.notNode()); - } + return d_theory.propagate(predicate.notNode()); } bool TheorySets::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, -- cgit v1.2.3