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.

diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index 7be07f7f5306dccf8df167c3c622833049733f17..27772ce516c08416c082fde946c5d457aa8b5499 100644 (file)
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -47,6 +47,7 @@ const char* toString(PfRule id)
     case PfRule::TRUST_SUBS: return "TRUST_SUBS";
     case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP";
     case PfRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ";
+    case PfRule::THEORY_INFERENCE: return "THEORY_INFERENCE";
     //================================================= Boolean rules
     case PfRule::RESOLUTION: return "RESOLUTION";
     case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 9625e1d28b78a0ca96d2bcd0b34813ec8217fab1..6625a1ad8c63c13eb1936f63c20db7738b19c98b 100644 (file)
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -257,6 +257,8 @@ enum class PfRule : uint32_t
   // where F is a solved equality of the form (= x t) derived as the solved
   // form of F', where F' is given as a child.
   TRUST_SUBS_EQ,
+  // where F is a fact derived by a theory-specific inference
+  THEORY_INFERENCE,
   // ========= SAT Refutation for assumption-based unsat cores
   // Children: (P1, ..., Pn)
   // Arguments: none

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index dae3922e682acc40391e7a0e56f778e66ee40f43..54d1779ec660563f7635759f38638d9d1f2265a3 100644 (file)
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -53,6 +53,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
   pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
   pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3);
+  pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
@@ -400,7 +401,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
            || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM
            || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE
            || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS
-           || id == PfRule::TRUST_SUBS_MAP || id == PfRule::TRUST_SUBS_EQ)
+           || id == PfRule::TRUST_SUBS_MAP || id == PfRule::TRUST_SUBS_EQ
+           || id == PfRule::THEORY_INFERENCE)
   {
     // "trusted" rules
     Assert(!args.empty());

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index a26147f0959e6c3d7d051eb6c424853b2f53e092..9fbe37254b4a2e1c400bcd8e7c06795242f33fe8 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -243,9 +243,11 @@ const char* toString(InferenceId i)
     case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF";
     case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND";
 
+    case InferenceId::SETS_CG_SPLIT: return "SETS_CG_SPLIT";
     case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION";
     case InferenceId::SETS_DEQ: return "SETS_DEQ";
     case InferenceId::SETS_DOWN_CLOSURE: return "SETS_DOWN_CLOSURE";
+    case InferenceId::SETS_EQ_CONFLICT: return "SETS_EQ_CONFLICT";
     case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM";
     case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT";
     case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ";

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index f32c80b68b5b529f819b023793e5c4e8471511f5..9ba324675998bb9eed3a16bcc0f98ab669a5523b 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -378,9 +378,13 @@ enum class InferenceId
 
   // ---------------------------------- sets theory
   //-------------------- sets core solver
+  // split when computing care graph
+  SETS_CG_SPLIT,
   SETS_COMPREHENSION,
   SETS_DEQ,
   SETS_DOWN_CLOSURE,
+  // conflict when two singleton/emptyset terms merge
+  SETS_EQ_CONFLICT,
   SETS_EQ_MEM,
   SETS_EQ_MEM_CONFLICT,
   SETS_MEM_EQ,

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 73c6db35fbccc886ce49a7ab15e4c63166767797..d0dc2183969ff387b7c0d0ef2f96f3593ab5f195 100644 (file)
--- 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 7a64b10c7d20d3a0bd1aa1aa45594700d1490e06..0a7c42e11bab4e8f730786dbf10d1f4410f8d133 100644 (file)
--- 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 439e9443d4e2c5650a99a427bb2e55a3791151a7..718077888f086b0d3cd5ce81d108ec296c9268ac 100644 (file)
--- 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 4ac74d76c9201629c6172fe9fe118017b02d6270..3817079a31bc47d73c98ea56f37429edde34f70c 100644 (file)
--- 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);
                 }
               }
             }

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index bfd23fb2304154501edeaff8c412e6bcb47ef767..bad90f06122958d476f5a9542f9a9f1f3d7fd75f 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -393,7 +393,7 @@ bool TheoryInferenceManager::processInternalFact(TNode atom,
   Assert(d_ee != nullptr);
   Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
                          << (pol ? Node(atom) : atom.notNode()) << " from "
-                         << expn << std::endl;
+                         << expn << " / " << iid << " " << id << std::endl;
   if (Configuration::isAssertionBuild())
   {
     // check that all facts hold in the equality engine, to ensure that we
@@ -431,10 +431,10 @@ bool TheoryInferenceManager::processInternalFact(TNode atom,
   }
   d_numCurrentFacts++;
   // Now, assert the fact. How to do so depends on whether proofs are enabled.
-  // If no proof production, or no proof rule was given
   bool ret = false;
-  if (d_pfee == nullptr || id == PfRule::UNKNOWN)
+  if (d_pfee == nullptr)
   {
+    Trace("infer-manager") << "...assert without proofs..." << std::endl;
     if (atom.getKind() == kind::EQUAL)
     {
       ret = d_ee->assertEquality(atom, pol, expn);
@@ -453,6 +453,8 @@ bool TheoryInferenceManager::processInternalFact(TNode atom,
   }
   else
   {
+    Assert(id != PfRule::UNKNOWN);
+    Trace("infer-manager") << "...assert with proofs..." << std::endl;
     // Note that we reconstruct the original literal lit here, since both the
     // original literal is needed for bookkeeping proofs. It is possible to
     // optimize this so that a few less nodes are created, but at the cost
@@ -472,7 +474,8 @@ bool TheoryInferenceManager::processInternalFact(TNode atom,
   // call the notify fact method with isInternal = true
   d_theory.notifyFact(atom, pol, expn, true);
   Trace("infer-manager")
-      << "TheoryInferenceManager::finished assertInternalFact" << std::endl;
+      << "TheoryInferenceManager::finished assertInternalFact, ret=" << ret
+      << std::endl;
   return ret;
 }
 

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index b11f21f1e08a3d335d3d0afc1f12eff359dc52d8..cea0e698bdb7c0f473085c32eb1a31d4744b48db 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -300,6 +300,8 @@ class TheoryInferenceManager
    * Theory's preNotifyFact and notifyFact method have been called with
    * isInternal = true.
    *
+   * Note this method should never be used when proofs are enabled.
+   *
    * @param atom The atom of the fact to assert
    * @param pol Its polarity
    * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid.