From 9a098337f9f25e7e2df07e493e6a120f6b8ce520 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Jul 2021 16:03:48 -0500 Subject: [PATCH] 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. --- src/proof/proof_rule.cpp | 1 + src/proof/proof_rule.h | 2 ++ src/theory/builtin/proof_checker.cpp | 4 +++- src/theory/inference_id.cpp | 2 ++ src/theory/inference_id.h | 4 ++++ src/theory/sets/inference_manager.cpp | 13 ++++++++++++- src/theory/sets/inference_manager.h | 4 ++++ src/theory/sets/theory_sets.cpp | 2 +- src/theory/sets/theory_sets_private.cpp | 11 ++++++----- src/theory/theory_inference_manager.cpp | 11 +++++++---- src/theory/theory_inference_manager.h | 2 ++ 11 files changed, 44 insertions(+), 12 deletions(-) diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 7be07f7f5..27772ce51 100644 --- 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 9625e1d28..6625a1ad8 100644 --- 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 dae3922e6..54d1779ec 100644 --- 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 a26147f09..9fbe37254 100644 --- 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 f32c80b68..9ba324675 100644 --- 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 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& 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); } } } diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index bfd23fb23..bad90f061 100644 --- 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 b11f21f1e..cea0e698b 100644 --- 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. -- 2.30.2