From 5f04a78336d648b02bc5cfdaaf734b6b350ee805 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 19 Sep 2020 10:57:51 -0500 Subject: [PATCH] Standardize equality engine notifications in sets (#5098) --- src/theory/sets/theory_sets.cpp | 33 +------------------- src/theory/sets/theory_sets.h | 14 ++++----- src/theory/sets/theory_sets_private.cpp | 40 ++----------------------- src/theory/sets/theory_sets_private.h | 9 ------ 4 files changed, 9 insertions(+), 87 deletions(-) diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 66f35f24f..971a12dc2 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -38,7 +38,7 @@ TheorySets::TheorySets(context::Context* c, d_state(c, u, valuation, d_skCache), d_im(*this, d_state, pnm), d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)), - d_notify(*d_internal.get()) + d_notify(*d_internal.get(), d_im) { // use the official theory state and inference manager objects d_theoryState = &d_state; @@ -201,37 +201,6 @@ bool TheorySets::isEntailed( Node n, bool pol ) { /**************************** eq::NotifyClass *****************************/ -bool TheorySets::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, - bool value) -{ - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " - << predicate << " value = " << value << std::endl; - if (value) - { - return d_theory.propagate(predicate); - } - return d_theory.propagate(predicate.notNode()); -} - -bool TheorySets::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, - TNode t1, - TNode t2, - bool value) -{ - Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag - << " t1 = " << t1 << " t2 = " << t2 << " value = " << value - << std::endl; - d_theory.propagate(value ? t1.eqNode(t2) : t1.eqNode(t2).negate()); - return true; -} - -void TheorySets::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) -{ - Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " - << " t1 = " << t1 << " t2 = " << t2 << std::endl; - d_theory.conflict(t1, t2); -} - void TheorySets::NotifyClass::eqNotifyNewClass(TNode t) { Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index fce57ca6c..4d0c74516 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -25,6 +25,7 @@ #include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" #include "theory/theory.h" +#include "theory/theory_eq_notify.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -82,16 +83,13 @@ class TheorySets : public Theory private: /** Functions to handle callbacks from equality engine */ - class NotifyClass : public eq::EqualityEngineNotify + class NotifyClass : public TheoryEqNotifyClass { public: - NotifyClass(TheorySetsPrivate& theory) : d_theory(theory) {} - bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; - bool eqNotifyTriggerTermEquality(TheoryId tag, - TNode t1, - TNode t2, - bool value) override; - void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; + NotifyClass(TheorySetsPrivate& theory, TheoryInferenceManager& im) + : TheoryEqNotifyClass(im), d_theory(theory) + { + } void eqNotifyNewClass(TNode t) override; void eqNotifyMerge(TNode t1, TNode t2) override; void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index c92871898..8779ac489 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -111,7 +111,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2) // singleton equal to emptyset, conflict Trace("sets-prop") << "Propagate conflict : " << s1 << " == " << s2 << std::endl; - conflict(s1, s2); + d_im.conflictEqConstantMerge(s1, s2); return; } } @@ -829,7 +829,7 @@ void TheorySetsPrivate::postCheck(Theory::Effort level) if (!d_state.isInConflict() && !d_im.hasSentLemma() && d_full_check_incomplete) { - d_external.d_out->setIncomplete(); + d_im.setIncomplete(); } } } @@ -1234,44 +1234,8 @@ Node mkAnd(const std::vector& conjunctions) return conjunction; } /* mkAnd() */ -bool TheorySetsPrivate::propagate(TNode literal) -{ - Debug("sets-prop") << " propagate(" << literal << ")" << std::endl; - - // If already in conflict, no more propagation - if (d_state.isInConflict()) - { - Debug("sets-prop") << "TheoryUF::propagate(" << literal - << "): already in conflict" << std::endl; - return false; - } - - // Propagate out - bool ok = d_external.d_out->propagate(literal); - if (!ok) - { - d_state.notifyInConflict(); - } - - return ok; -} /* TheorySetsPrivate::propagate(TNode) */ - -OutputChannel* TheorySetsPrivate::getOutputChannel() -{ - return d_external.d_out; -} - Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; } -void TheorySetsPrivate::conflict(TNode a, TNode b) -{ - Node conf = explain(a.eqNode(b)); - d_im.conflict(conf); - Debug("sets") << "[sets] conflict: " << a << " iff " << b << ", explanation " - << conf << std::endl; - Trace("sets-lemma") << "Equality Conflict : " << conf << std::endl; -} - Node TheorySetsPrivate::explain(TNode literal) { Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index d58967c5f..b2d3723cd 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -213,17 +213,8 @@ class TheorySetsPrivate { void presolve(); - /** get default output channel */ - OutputChannel* getOutputChannel(); /** get the valuation */ Valuation& getValuation(); - - /** Proagate out to output channel */ - bool propagate(TNode); - - /** generate and send out conflict node */ - void conflict(TNode, TNode); - private: TheorySets& d_external; /** The state of the sets solver at full effort */ -- 2.30.2