Enable default equality proofs for sets (#6931)

This enables default support for equality proofs in the theory of sets.

This is in preparation for proofs in the central equality engine, which requires that all active theories that use the central equality engine at least support the default interaction with the equality engine.

4 files changed, 23 insertions, 7 deletions

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 73c6db35f..d0dc21839 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -92,7 +92,7 @@ bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int in
       || (atom.getKind() == EQUAL && atom[0].getType().isSet()))
   {
     // send to equality engine
-    if (assertInternalFact(atom, polarity, id, exp))
+    if (assertSetsFact(atom, polarity, id, exp))
     {
       // return true if this wasn't redundant
       return true;
@@ -111,6 +111,17 @@ bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int in
   }
   return false;
 }
+
+bool InferenceManager::assertSetsFact(Node atom,
+                                      bool polarity,
+                                      InferenceId id,
+                                      Node exp)
+{
+  Node conc = polarity ? atom : atom.notNode();
+  return assertInternalFact(
+      atom, polarity, id, PfRule::THEORY_INFERENCE, {exp}, {conc});
+}
+
 void InferenceManager::assertInference(Node fact,
                                        InferenceId id,
                                        Node exp,
diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h
index 7a64b10c7..0a7c42e11 100644
--- a/src/theory/sets/inference_manager.h
+++ b/src/theory/sets/inference_manager.h
@@ -71,6 +71,10 @@ class InferenceManager : public InferenceManagerBuffered
                        InferenceId id,
                        std::vector<Node>& exp,
                        int inferType = 0);
+  /**
+   * Immediately assert an internal fact with the default handling of proofs.
+   */
+  bool assertSetsFact(Node atom, bool polarity, InferenceId id, Node exp);
 
   /** flush the splitting lemma ( n OR (NOT n) )
    *
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 439e9443d..718077888 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -36,7 +36,7 @@ TheorySets::TheorySets(context::Context* c,
     : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
       d_skCache(),
       d_state(c, u, valuation, d_skCache),
-      d_im(*this, d_state, nullptr),
+      d_im(*this, d_state, pnm),
       d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)),
       d_notify(*d_internal.get(), d_im)
 {
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 4ac74d76c..3817079a3 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -108,14 +108,15 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
             // infer equality between elements of singleton
             Node exp = s1.eqNode(s2);
             Node eq = s1[0].eqNode(s2[0]);
-            d_im.assertInternalFact(eq, true, InferenceId::SETS_SINGLETON_EQ, exp);
+            d_im.assertSetsFact(eq, true, InferenceId::SETS_SINGLETON_EQ, exp);
           }
           else
           {
             // singleton equal to emptyset, conflict
             Trace("sets-prop")
                 << "Propagate conflict : " << s1 << " == " << s2 << std::endl;
-            d_im.conflictEqConstantMerge(s1, s2);
+            Node eqs = s1.eqNode(s2);
+            d_im.conflict(eqs, InferenceId::SETS_EQ_CONFLICT);
             return;
           }
         }
@@ -149,7 +150,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
       Assert(f.getKind() == kind::IMPLIES);
       Trace("sets-prop") << "Propagate eq-mem eq inference : " << f[0] << " => "
                          << f[1] << std::endl;
-      d_im.assertInternalFact(f[1], true, InferenceId::SETS_EQ_MEM, f[0]);
+      d_im.assertSetsFact(f[1], true, InferenceId::SETS_EQ_MEM, f[0]);
     }
   }
 }
@@ -829,7 +830,7 @@ void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
             Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl;
             Node eq = s[0].eqNode(atom[0]);
             // triggers an internal inference
-            d_im.assertInternalFact(eq, true, InferenceId::SETS_MEM_EQ, pexp);
+            d_im.assertSetsFact(eq, true, InferenceId::SETS_MEM_EQ, pexp);
           }
         }
         else
@@ -907,7 +908,7 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
                 {
                   Trace("sets-cg-lemma")
                       << "Should split on : " << x << "==" << y << std::endl;
-                  d_im.split(x.eqNode(y), InferenceId::UNKNOWN);
+                  d_im.split(x.eqNode(y), InferenceId::SETS_CG_SPLIT);
                 }
               }
             }