diff options
25 files changed, 68 insertions, 183 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index a70339c01..a13b02900 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -97,16 +97,17 @@ ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongru : 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) { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index f3b5641b4..d46346fd8 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -61,8 +61,6 @@ private: public: ArithCongruenceNotify(ArithCongruenceManager& acm); - bool eqNotifyTriggerEquality(TNode equality, bool value) override; - bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; bool eqNotifyTriggerTermEquality(TheoryId tag, diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 51e1b367c..4cc51a87e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -697,7 +697,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) 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 diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 530f8e0e1..b69450ac4 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -296,26 +296,17 @@ class TheoryArrays : public Theory { 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, diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 48ec81a1e..7e2b8a8b0 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -105,7 +105,7 @@ void CoreSolver::enableSlicer() { 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); @@ -383,22 +383,12 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { 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) { diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 33f119e5f..19183c129 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -54,7 +54,6 @@ class CoreSolver : public SubtheorySolver { 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, diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index e625f57eb..ee750e646 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -542,10 +542,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { 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; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index bdc13b5e5..37848f10e 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -58,24 +58,13 @@ class TheoryDatatypes : public Theory { 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, diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index 8cac225be..ededa956e 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -107,10 +107,6 @@ class EqEngineManagerDistributed : public EqEngineManager */ void eqNotifyNewClass(TNode t) override; - bool eqNotifyTriggerEquality(TNode equality, bool value) override - { - return true; - } bool eqNotifyTriggerPredicate(TNode predicate, bool value) override { return true; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index f5cc16ea9..ff0855889 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -816,7 +816,7 @@ void TheoryFp::registerTerm(TNode node) { // Add to the equality engine if (k == kind::EQUAL) { - d_equalityEngine->addTriggerEquality(node); + d_equalityEngine->addTriggerPredicate(node); } else { @@ -1143,19 +1143,6 @@ bool TheoryFp::collectModelInfo(TheoryModel *m) 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") @@ -1164,9 +1151,8 @@ bool TheoryFp::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, 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, diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 02e7e4232..2584d574e 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -80,7 +80,6 @@ class TheoryFp : public Theory { 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, diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 1e8099054..9ecee8896 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -246,10 +246,6 @@ private: 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; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 84a7025f0..40182fc19 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -152,27 +152,19 @@ class TheorySep : public Theory { 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, 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, diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index cb8fdfbc3..36e6ac65d 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -78,7 +78,6 @@ class TheorySets : public Theory { 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, diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 879862d15..f7c7ae7f9 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1464,8 +1464,13 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) << 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; } diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 52ce34756..99584b167 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -46,7 +46,7 @@ SharedTermsDatabase::~SharedTermsDatabase() void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { d_registeredEqualities.insert(equality); - d_equalityEngine.addTriggerEquality(equality); + d_equalityEngine.addTriggerPredicate(equality); checkForConflict(); } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 55cd84e58..05ce88d99 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -78,15 +78,10 @@ private: 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; } diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 353e89668..3e6f66b73 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -155,7 +155,7 @@ void TermRegistry::preRegisterTerm(TNode n) 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) diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 500daac1f..da48ece90 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -126,28 +126,13 @@ class TheoryStrings : public Theory { 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, diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 643029b05..5ccda1dc2 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1704,11 +1704,11 @@ void EqualityEngine::addTriggerEquality(TNode eq) { // 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; } @@ -1726,8 +1726,12 @@ void EqualityEngine::addTriggerEquality(TNode eq) { } 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"; @@ -1997,8 +2001,8 @@ void EqualityEngine::propagate() { 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; } @@ -2007,8 +2011,8 @@ void EqualityEngine::propagate() { 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; } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 9d1fc6165..c3041dfe7 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -658,9 +658,15 @@ private: /** 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. */ @@ -787,16 +793,13 @@ public: 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); diff --git a/src/theory/uf/equality_engine_notify.h b/src/theory/uf/equality_engine_notify.h index f63a887ef..1467cacf3 100644 --- a/src/theory/uf/equality_engine_notify.h +++ b/src/theory/uf/equality_engine_notify.h @@ -33,15 +33,8 @@ class EqualityEngineNotify 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 @@ -103,10 +96,6 @@ class EqualityEngineNotify class EqualityEngineNotifyNone : public EqualityEngineNotify { public: - bool eqNotifyTriggerEquality(TNode equality, bool value) override - { - return true; - } bool eqNotifyTriggerPredicate(TNode predicate, bool value) override { return true; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4f9c3bed5..7bca9da74 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -246,7 +246,7 @@ void TheoryUF::preRegisterTerm(TNode node) { 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: diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 001c947e9..414a2dd6a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -45,17 +45,6 @@ public: 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; |