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.

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<TNode>& assumptions)
+{
+  bool polarity = lit.getKind() != kind::NOT;
+  TNode atom = polarity ? lit : lit[0];
+  std::vector<TNode> 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<TNode> 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<TNode>& 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<TNode>& 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