From 5aeb8b78c4a26b274dbfecc882c0e0bb836cb398 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Aug 2020 18:33:49 -0500 Subject: [PATCH] Add a few basic extensions for equality engine (#4937) This includes a standard method for safe explanations and the option to disable all trigger terms. --- src/theory/uf/equality_engine.cpp | 159 +++++++++++++++++++++--------- src/theory/uf/equality_engine.h | 45 +++++++-- 2 files changed, 153 insertions(+), 51 deletions(-) diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 5ccda1dc2..7bb857425 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -109,53 +109,61 @@ EqualityEngine::~EqualityEngine() { free(d_triggerDatabase); } - -EqualityEngine::EqualityEngine(context::Context* context, std::string name, bool constantsAreTriggers) -: ContextNotifyObj(context) -, d_masterEqualityEngine(0) -, d_context(context) -, d_done(context, false) -, d_performNotify(true) -, d_notify(s_notifyNone) -, d_applicationLookupsCount(context, 0) -, d_nodesCount(context, 0) -, d_assertedEqualitiesCount(context, 0) -, d_equalityTriggersCount(context, 0) -, d_subtermEvaluatesSize(context, 0) -, d_stats(name) -, d_inPropagate(false) -, d_constantsAreTriggers(constantsAreTriggers) -, d_triggerDatabaseSize(context, 0) -, d_triggerTermSetUpdatesSize(context, 0) -, d_deducedDisequalitiesSize(context, 0) -, d_deducedDisequalityReasonsSize(context, 0) -, d_propagatedDisequalities(context) -, d_name(name) +EqualityEngine::EqualityEngine(context::Context* context, + std::string name, + bool constantsAreTriggers, + bool anyTermTriggers) + : ContextNotifyObj(context), + d_masterEqualityEngine(0), + d_context(context), + d_done(context, false), + d_performNotify(true), + d_notify(s_notifyNone), + d_applicationLookupsCount(context, 0), + d_nodesCount(context, 0), + d_assertedEqualitiesCount(context, 0), + d_equalityTriggersCount(context, 0), + d_subtermEvaluatesSize(context, 0), + d_stats(name), + d_inPropagate(false), + d_constantsAreTriggers(constantsAreTriggers), + d_anyTermsAreTriggers(anyTermTriggers), + d_triggerDatabaseSize(context, 0), + d_triggerTermSetUpdatesSize(context, 0), + d_deducedDisequalitiesSize(context, 0), + d_deducedDisequalityReasonsSize(context, 0), + d_propagatedDisequalities(context), + d_name(name) { init(); } -EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name, bool constantsAreTriggers) -: ContextNotifyObj(context) -, d_masterEqualityEngine(0) -, d_context(context) -, d_done(context, false) -, d_performNotify(true) -, d_notify(notify) -, d_applicationLookupsCount(context, 0) -, d_nodesCount(context, 0) -, d_assertedEqualitiesCount(context, 0) -, d_equalityTriggersCount(context, 0) -, d_subtermEvaluatesSize(context, 0) -, d_stats(name) -, d_inPropagate(false) -, d_constantsAreTriggers(constantsAreTriggers) -, d_triggerDatabaseSize(context, 0) -, d_triggerTermSetUpdatesSize(context, 0) -, d_deducedDisequalitiesSize(context, 0) -, d_deducedDisequalityReasonsSize(context, 0) -, d_propagatedDisequalities(context) -, d_name(name) +EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, + context::Context* context, + std::string name, + bool constantsAreTriggers, + bool anyTermTriggers) + : ContextNotifyObj(context), + d_masterEqualityEngine(0), + d_context(context), + d_done(context, false), + d_performNotify(true), + d_notify(notify), + d_applicationLookupsCount(context, 0), + d_nodesCount(context, 0), + d_assertedEqualitiesCount(context, 0), + d_equalityTriggersCount(context, 0), + d_subtermEvaluatesSize(context, 0), + d_stats(name), + d_inPropagate(false), + d_constantsAreTriggers(constantsAreTriggers), + d_anyTermsAreTriggers(anyTermTriggers), + d_triggerDatabaseSize(context, 0), + d_triggerTermSetUpdatesSize(context, 0), + d_deducedDisequalitiesSize(context, 0), + d_deducedDisequalityReasonsSize(context, 0), + d_propagatedDisequalities(context), + d_name(name) { init(); } @@ -1073,7 +1081,7 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, // The terms must be there already Assert(hasTerm(t1) && hasTerm(t2)); - ; + if (Debug.isOn("equality::internal")) { debugPrintGraph(); @@ -1242,6 +1250,63 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity, getNodeId(p), polarity ? d_trueId : d_falseId, assertions, cache, eqp); } +void EqualityEngine::explainLit(TNode lit, std::vector& assumptions) +{ + bool polarity = lit.getKind() != kind::NOT; + TNode atom = polarity ? lit : lit[0]; + std::vector tassumptions; + if (atom.getKind() == kind::EQUAL) + { + Assert(hasTerm(atom[0])); + Assert(hasTerm(atom[1])); + if (!polarity) + { + // ensure that we are ready to explain the disequality + AlwaysAssert(areDisequal(atom[0], atom[1], true)); + } + else if (atom[0] == atom[1]) + { + // no need to explain reflexivity + return; + } + explainEquality(atom[0], atom[1], polarity, tassumptions); + } + else + { + explainPredicate(atom, polarity, tassumptions); + } + // ensure that duplicates are removed + for (const TNode a : tassumptions) + { + if (std::find(assumptions.begin(), assumptions.end(), a) + == assumptions.end()) + { + assumptions.push_back(a); + } + } +} + +Node EqualityEngine::mkExplainLit(TNode lit) +{ + std::vector assumptions; + explainLit(lit, assumptions); + Node ret; + NodeManager* nm = NodeManager::currentNM(); + if (assumptions.empty()) + { + ret = nm->mkConst(true); + } + else if (assumptions.size() == 1) + { + ret = assumptions[0]; + } + else + { + ret = nm->mkNode(kind::AND, assumptions); + } + return ret; +} + void EqualityEngine::getExplanation( EqualityNodeId t1Id, EqualityNodeId t2Id, @@ -2174,6 +2239,12 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Add the term if it's not already there addTermInternal(t); + if (!d_anyTermsAreTriggers) + { + // if we are not using triggers, we only add the term, but not as a trigger + return; + } + // Get the node id EqualityNodeId eqNodeId = getNodeId(t); EqualityNode& eqNode = getEqualityNode(eqNodeId); diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index c3041dfe7..91dae2509 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -80,17 +80,26 @@ class EqualityEngine : public context::ContextNotifyObj { */ EqualityEngine* d_masterEqualityEngine; -public: - + public: /** * Initialize the equality engine, given the notification class. + * + * @param constantTriggers Whether we treat constants as trigger terms + * @param anyTermTriggers Whether we use any terms as triggers */ - EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name, bool constantsAreTriggers); + EqualityEngine(EqualityEngineNotify& notify, + context::Context* context, + std::string name, + bool constantTriggers, + bool anyTermTriggers = true); /** * Initialize the equality engine with no notification class. */ - EqualityEngine(context::Context* context, std::string name, bool constantsAreTriggers); + EqualityEngine(context::Context* context, + std::string name, + bool constantsAreTriggers, + bool anyTermTriggers = true); /** * Just a destructor. @@ -98,13 +107,14 @@ public: virtual ~EqualityEngine(); /** - * Set the master equality engine for this one. Master engine will get copies of all - * the terms and equalities from this engine. + * Set the master equality engine for this one. Master engine will get copies + * of all the terms and equalities from this engine. */ void setMasterEqualityEngine(EqualityEngine* master); /** Statistics about the equality engine instance */ - struct Statistics { + struct Statistics + { /** Total number of merges */ IntStat d_mergesCount; /** Number of terms managed by the system */ @@ -506,6 +516,11 @@ private: /** Are the constants triggers */ bool d_constantsAreTriggers; + /** + * Are any terms triggers? If this is false, then all trigger terms are + * ignored (e.g. this means that addTriggerTerm is equivalent to addTerm). + */ + bool d_anyTermsAreTriggers; /** The information about trigger terms is stored in this easily maintained memory. */ char* d_triggerDatabase; @@ -767,6 +782,22 @@ private: void explainPredicate(TNode p, bool polarity, std::vector& assertions, EqProof* eqp = nullptr) const; + //--------------------------- standard safe explanation methods + /** + * Explain literal, add its explanation to assumptions. This method does not + * add duplicates to assumptions. It requires that the literal + * holds in this class. If lit is a disequality, it + * moreover ensures this class is ready to explain it via areDisequal with + * ensureProof = true. + */ + void explainLit(TNode lit, std::vector& assumptions); + /** + * Explain literal, return the conjunction. This method relies on the above + * method. + */ + Node mkExplainLit(TNode lit); + //--------------------------- end standard safe explanation methods + /** * Add term to the set of trigger terms with a corresponding tag. The notify class will get * notified when two trigger terms with the same tag become equal or dis-equal. The notification -- 2.30.2