diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-18 22:33:10 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-18 22:33:10 +0100 |
commit | 94fdbe4bb325b1ff1874a2e699cad6ea76f44185 (patch) | |
tree | 1927e234fb4a59899ceac0aa3920f52e62bbb6ab /src/theory/sets | |
parent | ba30b690b29e7e52dd8ea1ea953525c401abf3d9 (diff) |
Add InferenceIds for sets theory. (#5900)
This PR introduces new InferenceId for the theory of sets and uses them instead of InferenceId::UNKNOWN.
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/cardinality_extension.cpp | 37 | ||||
-rw-r--r-- | src/theory/sets/inference_manager.cpp | 38 | ||||
-rw-r--r-- | src/theory/sets/inference_manager.h | 17 | ||||
-rw-r--r-- | src/theory/sets/term_registry.cpp | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 27 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 65 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.h | 9 |
7 files changed, 100 insertions, 99 deletions
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 5997d1217..a3120ffcb 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -132,8 +132,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) // (=> true (<= (card (as univset t)) cardUniv) if (!d_state.isEntailed(leq, true)) { - d_im.assertInference( - leq, d_true, "univset cardinality <= type cardinality", 1); + d_im.assertInference(leq, InferenceId::SETS_CARD_UNIV_TYPE, d_true, 1); } } @@ -158,7 +157,8 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) subset = Rewriter::rewrite(subset); if (!d_state.isEntailed(subset, true)) { - d_im.assertInference(subset, d_true, "univset is a super set", 1); + d_im.assertInference( + subset, InferenceId::SETS_CARD_UNIV_SUPERSET, d_true, 1); } // negative members are members in the universe set @@ -176,7 +176,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) // (not (member negativeMember representative))) // (member negativeMember (as univset t))) d_im.assertInference( - member, notMember, "negative members are in the universe", 1); + member, InferenceId::SETS_CARD_NEGATIVE_MEMBER, notMember, 1); } } } @@ -268,7 +268,8 @@ void CardinalityExtension::registerCardinalityTerm(Node n) cterms.push_back(s); } Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, n), d_zero); - d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1); + d_im.assertInference( + pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1); } else { @@ -279,13 +280,14 @@ void CardinalityExtension::registerCardinalityTerm(Node n) Node nn = cterms[k]; Node nk = d_treg.getProxy(nn); Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, nk), d_zero); - d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1); + d_im.assertInference( + pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1); if (nn != nk) { Node lem = nm->mkNode(EQUAL, nm->mkNode(CARD, nk), nm->mkNode(CARD, nn)); lem = Rewriter::rewrite(lem); Trace("sets-card") << " " << k << " : " << lem << std::endl; - d_im.assertInference(lem, d_emp_exp, "card", 1); + d_im.assertInference(lem, InferenceId::SETS_CARD_EQUAL, d_emp_exp, 1); } } d_im.doPendingLemmas(); @@ -342,7 +344,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(AND, conc); Trace("sets-cycle-debug") << "CYCLE: " << fact << " from " << exp << std::endl; - d_im.assertInference(fact, exp, "card_cycle"); + d_im.assertInference(fact, InferenceId::SETS_CARD_CYCLE, exp); d_im.doPendingLemmas(); } else @@ -418,7 +420,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, conc.push_back(n[e].eqNode(sib[e])); } } - d_im.assertInference(conc, n.eqNode(emp_set), "cg_emp"); + d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EMP, n.eqNode(emp_set)); d_im.doPendingLemmas(); if (d_im.hasSent()) { @@ -450,7 +452,8 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, { Trace("sets-debug") << " it is empty..." << std::endl; Assert(!d_state.areEqual(n, emp_set)); - d_im.assertInference(n.eqNode(emp_set), p.eqNode(emp_set), "cg_emppar"); + d_im.assertInference( + n.eqNode(emp_set), InferenceId::SETS_CARD_GRAPH_EMP_PARENT, p.eqNode(emp_set)); d_im.doPendingLemmas(); if (d_im.hasSent()) { @@ -497,7 +500,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, } Trace("sets-debug") << "...derived " << conc.size() << " conclusions" << std::endl; - d_im.assertInference(conc, n.eqNode(p), "cg_eqpar"); + d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT, n.eqNode(p)); d_im.doPendingLemmas(); if (d_im.hasSent()) { @@ -549,14 +552,14 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, if (eq_parent) { Node conc = n.eqNode(cpk); - d_im.assertInference(conc, exps, "cg_par_sing"); + d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON, exps); d_im.doPendingLemmas(); } else { // split on empty Trace("sets-nf") << "Split empty : " << n << std::endl; - d_im.split(n.eqNode(emp_set), 1); + d_im.split(n.eqNode(emp_set), InferenceId::UNKNOWN, 1); } Assert(d_im.hasSent()); return; @@ -604,7 +607,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, conc.push_back(cpk.eqNode(n)); } } - d_im.assertInference(conc, cpk.eqNode(cpnl), "cg_pareq"); + d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2, cpk.eqNode(cpnl)); d_im.doPendingLemmas(); if (d_im.hasSent()) { @@ -788,7 +791,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, Trace("sets-nf") << "Actual Split : "; d_treg.debugPrintSet(r, "sets-nf"); Trace("sets-nf") << std::endl; - d_im.split(r.eqNode(emp_set), 1); + d_im.split(r.eqNode(emp_set), InferenceId::UNKNOWN, 1); Assert(d_im.hasSent()); return; } @@ -860,7 +863,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, && !d_state.hasMembers(eqc)) { Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl; - d_im.split(eqc.eqNode(emp_set)); + d_im.split(eqc.eqNode(emp_set), InferenceId::UNKNOWN); success = false; } else @@ -972,7 +975,7 @@ void CardinalityExtension::checkMinCard() Node conc = nm->mkNode(GEQ, cardTerm, nm->mkConst(Rational(members.size()))); Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); - d_im.assertInference(conc, expn, "mincard", 1); + d_im.assertInference(conc, InferenceId::SETS_CARD_MINIMAL, expn, 1); } } // flush the lemmas diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 2629e2cbd..161a66bfe 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -32,7 +32,7 @@ InferenceManager::InferenceManager(Theory& t, d_false = NodeManager::currentNM()->mkConst(false); } -bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) +bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType) { // should we send this fact out as a lemma? if ((options::setsInferAsLemmas() && inferType != -1) || inferType == 1) @@ -46,7 +46,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) { lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact); } - addPendingLemma(lem, InferenceId::UNKNOWN); + addPendingLemma(lem, id); return true; } Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp @@ -57,7 +57,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) if (fact == d_false) { Trace("sets-lemma") << "Conflict : " << exp << std::endl; - conflict(exp, InferenceId::UNKNOWN); + conflict(exp, id); return true; } return false; @@ -70,7 +70,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) for (unsigned i = 0; i < f.getNumChildren(); i++) { Node factc = fact.getKind() == NOT ? f[i].negate() : f[i]; - bool tret = assertFactRec(factc, exp, inferType); + bool tret = assertFactRec(factc, id, exp, inferType); ret = ret || tret; if (d_state.isInConflict()) { @@ -90,7 +90,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) || (atom.getKind() == EQUAL && atom[0].getType().isSet())) { // send to equality engine - if (assertInternalFact(atom, polarity, InferenceId::UNKNOWN, exp)) + if (assertInternalFact(atom, polarity, id, exp)) { // return true if this wasn't redundant return true; @@ -104,67 +104,67 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) { lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact); } - addPendingLemma(lem, InferenceId::UNKNOWN); + addPendingLemma(lem, id); return true; } return false; } void InferenceManager::assertInference(Node fact, + InferenceId id, Node exp, - const char* c, int inferType) { - if (assertFactRec(fact, exp, inferType)) + if (assertFactRec(fact, id, exp, inferType)) { Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by " - << c << std::endl; - Trace("sets-assertion") - << "(assert (=> " << exp << " " << fact << ")) ; by " << c << std::endl; + << id << std::endl; + Trace("sets-assertion") << "(assert (=> " << exp << " " << fact + << ")) ; by " << id << std::endl; } } void InferenceManager::assertInference(Node fact, + InferenceId id, std::vector<Node>& exp, - const char* c, int inferType) { Node exp_n = exp.empty() ? d_true : (exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp)); - assertInference(fact, exp_n, c, inferType); + assertInference(fact, id, exp_n, inferType); } void InferenceManager::assertInference(std::vector<Node>& conc, + InferenceId id, Node exp, - const char* c, int inferType) { if (!conc.empty()) { Node fact = conc.size() == 1 ? conc[0] : NodeManager::currentNM()->mkNode(AND, conc); - assertInference(fact, exp, c, inferType); + assertInference(fact, id, exp, inferType); } } void InferenceManager::assertInference(std::vector<Node>& conc, + InferenceId id, std::vector<Node>& exp, - const char* c, int inferType) { Node exp_n = exp.empty() ? d_true : (exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp)); - assertInference(conc, exp_n, c, inferType); + assertInference(conc, id, exp_n, inferType); } -void InferenceManager::split(Node n, int reqPol) +void InferenceManager::split(Node n, InferenceId id, int reqPol) { n = Rewriter::rewrite(n); Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate()); // send the lemma - lemma(lem, InferenceId::UNKNOWN); + lemma(lem, id); Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl; if (reqPol != 0) { diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index c52fcf3d4..a4eeb1f1c 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -50,24 +50,25 @@ class InferenceManager : public InferenceManagerBuffered * fact is processed as a lemma, where inferType=1 forces fact to be * set as a lemma, and inferType=-1 forces fact to be processed as a fact * (if possible). - * - * The argument c is the name of the inference, which is used for debugging. */ - void assertInference(Node fact, Node exp, const char* c, int inferType = 0); + void assertInference(Node fact, + InferenceId id, + Node exp, + int inferType = 0); /** same as above, where exp is interpreted as a conjunction */ void assertInference(Node fact, + InferenceId id, std::vector<Node>& exp, - const char* c, int inferType = 0); /** same as above, where conc is interpreted as a conjunction */ void assertInference(std::vector<Node>& conc, + InferenceId id, Node exp, - const char* c, int inferType = 0); /** same as above, where both exp and conc are interpreted as conjunctions */ void assertInference(std::vector<Node>& conc, + InferenceId id, std::vector<Node>& exp, - const char* c, int inferType = 0); /** flush the splitting lemma ( n OR (NOT n) ) @@ -75,7 +76,7 @@ class InferenceManager : public InferenceManagerBuffered * If reqPol is not 0, then a phase requirement for n is requested with * polarity ( reqPol>0 ). */ - void split(Node n, int reqPol = 0); + void split(Node n, InferenceId id, int reqPol = 0); private: /** constants */ @@ -94,7 +95,7 @@ class InferenceManager : public InferenceManagerBuffered * The argument inferType determines the policy on whether fact is processed * as a fact or as a lemma (see assertInference above). */ - bool assertFactRec(Node fact, Node exp, int inferType = 0); + bool assertFactRec(Node fact, InferenceId id, Node exp, int inferType = 0); }; } // namespace sets diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index 975581dfa..464846b1a 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -53,13 +53,13 @@ Node TermRegistry::getProxy(Node n) d_proxy_to_term[k] = n; Node eq = k.eqNode(n); Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl; - d_im.lemma(eq, InferenceId::UNKNOWN, LemmaProperty::NONE, false); + d_im.lemma(eq, InferenceId::SETS_PROXY, LemmaProperty::NONE, false); if (nk == SINGLETON) { Node slem = nm->mkNode(MEMBER, n[0], k); Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" << std::endl; - d_im.lemma(slem, InferenceId::UNKNOWN, LemmaProperty::NONE, false); + d_im.lemma(slem, InferenceId::SETS_PROXY_SINGLETON, LemmaProperty::NONE, false); } return k; } @@ -104,7 +104,7 @@ Node TermRegistry::getUnivSet(TypeNode tn) Node ulem = nm->mkNode(SUBSET, n1, n2); Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" << std::endl; - d_im.lemma(ulem, InferenceId::UNKNOWN, LemmaProperty::NONE, false); + d_im.lemma(ulem, InferenceId::SETS_UNIV_TYPE, LemmaProperty::NONE, false); } } d_univset[tn] = n; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 867c87c59..e69113c97 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -104,7 +104,7 @@ 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::UNKNOWN, exp); + d_im.assertInternalFact(eq, true, InferenceId::SETS_SINGLETON_EQ, exp); } else { @@ -137,7 +137,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2) Assert(facts.size() == 1); Trace("sets-prop") << "Propagate eq-mem conflict : " << facts[0] << std::endl; - d_im.conflict(facts[0], InferenceId::UNKNOWN); + d_im.conflict(facts[0], InferenceId::SETS_EQ_MEM_CONFLICT); return; } for (const Node& f : facts) @@ -145,7 +145,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::UNKNOWN, f[0]); + d_im.assertInternalFact(f[1], true, InferenceId::SETS_EQ_MEM, f[0]); } } } @@ -449,7 +449,7 @@ void TheorySetsPrivate::checkDownwardsClosure() std::vector<Node> exp; exp.push_back(mem); exp.push_back(mem[1].eqNode(eq_set)); - d_im.assertInference(nmem, exp, "downc"); + d_im.assertInference(nmem, InferenceId::SETS_DOWN_CLOSURE, exp); if (d_state.isInConflict()) { return; @@ -474,7 +474,7 @@ void TheorySetsPrivate::checkDownwardsClosure() nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem); } - d_im.assertInference(nmem, exp, "downc"); + d_im.assertInference(nmem, InferenceId::SETS_DOWN_CLOSURE, exp); } } } @@ -578,7 +578,8 @@ void TheorySetsPrivate::checkUpwardsClosure() { Node kk = d_treg.getProxy(term); Node fact = nm->mkNode(kind::MEMBER, x, kk); - d_im.assertInference(fact, exp, "upc", inferType); + d_im.assertInference( + fact, InferenceId::SETS_UP_CLOSURE, exp, inferType); if (d_state.isInConflict()) { return; @@ -605,7 +606,7 @@ void TheorySetsPrivate::checkUpwardsClosure() d_state.addEqualityToExp(term[1], itm2m.second[1], exp); Node r = d_treg.getProxy(term); Node fact = nm->mkNode(kind::MEMBER, x, r); - d_im.assertInference(fact, exp, "upc2"); + d_im.assertInference(fact, InferenceId::SETS_UP_CLOSURE_2, exp); if (d_state.isInConflict()) { return; @@ -667,7 +668,7 @@ void TheorySetsPrivate::checkUpwardsClosure() exp.push_back(v.eqNode(it2.second[1])); } Node fact = nm->mkNode(kind::MEMBER, it2.second[0], u); - d_im.assertInference(fact, exp, "upuniv"); + d_im.assertInference(fact, InferenceId::SETS_UP_UNIV, exp); if (d_state.isInConflict()) { return; @@ -724,7 +725,7 @@ void TheorySetsPrivate::checkDisequalities() Node mem2 = nm->mkNode(MEMBER, x, deq[1]); Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate()); lem = Rewriter::rewrite(lem); - d_im.assertInference(lem, d_true, "diseq", 1); + d_im.assertInference(lem, InferenceId::SETS_DEQ, d_true, 1); d_im.doPendingLemmas(); if (d_im.hasSent()) { @@ -764,7 +765,7 @@ void TheorySetsPrivate::checkReduceComprehensions() nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem)); Trace("sets-comprehension") << "Comprehension reduction: " << lem << std::endl; - d_im.lemma(lem, InferenceId::UNKNOWN); + d_im.lemma(lem, InferenceId::SETS_COMPREHENSION); } } @@ -818,14 +819,14 @@ 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::UNKNOWN, pexp); + d_im.assertInternalFact(eq, true, InferenceId::SETS_MEM_EQ, pexp); } } else { Trace("sets-prop") << "Propagate mem-eq conflict : " << pexp << std::endl; - d_im.conflict(pexp, InferenceId::UNKNOWN); + d_im.conflict(pexp, InferenceId::SETS_MEM_EQ_CONFLICT); } } } @@ -896,7 +897,7 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, { Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl; - d_im.split(x.eqNode(y)); + d_im.split(x.eqNode(y), InferenceId::UNKNOWN); } } } diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index ebb7f845d..62f1776a3 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -346,8 +346,8 @@ void TheorySetsRels::check(Theory::Effort level) Assert(reasons.size() >= 1); sendInfer( new_membership, - reasons.size() > 1 ? nm->mkNode(AND, reasons) : reasons[0], - "JOIN-IMAGE UP"); + InferenceId::UNKNOWN, + reasons.size() > 1 ? nm->mkNode(AND, reasons) : reasons[0]); break; } } @@ -404,7 +404,7 @@ void TheorySetsRels::check(Theory::Effort level) if( distinct_skolems.size() >= 2 ) { conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) ); } - sendInfer(conclusion, reason, "JOIN-IMAGE DOWN"); + sendInfer(conclusion, InferenceId::SETS_RELS_JOIN_IMAGE_DOWN, reason); Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl; } @@ -437,8 +437,8 @@ void TheorySetsRels::check(Theory::Effort level) reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) ); } sendInfer(nm->mkNode(AND, fact, nm->mkNode(EQUAL, fst_mem, snd_mem)), - reason, - "IDENTITY-DOWN"); + InferenceId::SETS_RELS_IDENTITY_DOWN, + reason); Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyIdenRule on " << iden_term << std::endl; } @@ -469,7 +469,8 @@ void TheorySetsRels::check(Theory::Effort level) if( (*mem_rep_exp_it)[1] != iden_term_rel ) { reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it)[1], iden_term_rel ) ); } - sendInfer(nm->mkNode(MEMBER, new_mem, iden_term), reason, "IDENTITY-UP"); + sendInfer( + nm->mkNode(MEMBER, new_mem, iden_term), InferenceId::SETS_RELS_IDENTITY_UP, reason); ++mem_rep_exp_it; } Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for Iden Term = " << iden_term << std::endl; @@ -712,12 +713,12 @@ void TheorySetsRels::check(Theory::Effort level) } if( all_reasons.size() > 1) { sendInfer(nm->mkNode(MEMBER, tc_mem, tc_rel), - nm->mkNode(AND, all_reasons), - "TCLOSURE-Forward"); + InferenceId::SETS_RELS_TCLOSURE_FWD, + nm->mkNode(AND, all_reasons)); } else { sendInfer(nm->mkNode(MEMBER, tc_mem, tc_rel), - all_reasons.front(), - "TCLOSURE-Forward"); + InferenceId::SETS_RELS_TCLOSURE_FWD, + all_reasons.front()); } // check if cur_node has been traversed or not @@ -790,8 +791,8 @@ void TheorySetsRels::check(Theory::Effort level) if( pt_rel != exp[1] ) { reason = NodeManager::currentNM()->mkNode(kind::AND, exp, NodeManager::currentNM()->mkNode(kind::EQUAL, pt_rel, exp[1])); } - sendInfer(fact_1, reason, "product-split"); - sendInfer(fact_2, reason, "product-split"); + sendInfer(fact_1, InferenceId::SETS_RELS_PRODUCT_SPLIT, reason); + sendInfer(fact_2, InferenceId::SETS_RELS_PRODUCT_SPLIT, reason); } /* join-split rule: (a, b) IS_IN (X JOIN Y) @@ -861,9 +862,9 @@ void TheorySetsRels::check(Theory::Effort level) reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, join_rel, exp[1])); } Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, join_rel[0]); - sendInfer(fact, reason, "JOIN-Split-1"); + sendInfer(fact, InferenceId::SETS_RELS_JOIN_SPLIT_1, reason); fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]); - sendInfer(fact, reason, "JOIN-Split-2"); + sendInfer(fact, InferenceId::SETS_RELS_JOIN_SPLIT_2, reason); makeSharedTerm(shared_x, shared_type); } @@ -885,8 +886,8 @@ void TheorySetsRels::check(Theory::Effort level) for( unsigned int i = 1; i < tp_terms.size(); i++ ) { Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE-Equal rule on transposed term = " << tp_terms[0] << " and " << tp_terms[i] << std::endl; sendInfer(nm->mkNode(EQUAL, tp_terms[0][0], tp_terms[i][0]), - nm->mkNode(EQUAL, tp_terms[0], tp_terms[i]), - "TRANSPOSE-Equal"); + InferenceId::SETS_RELS_TRANSPOSE_EQ, + nm->mkNode(EQUAL, tp_terms[0], tp_terms[i])); } } @@ -911,8 +912,8 @@ void TheorySetsRels::check(Theory::Effort level) reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tp_rel, exp[1])); } sendInfer(nm->mkNode(MEMBER, reversed_mem, tp_rel[0]), - reason, - "TRANSPOSE-Reverse"); + InferenceId::SETS_RELS_TRANSPOSE_REV, + reason); } void TheorySetsRels::doTCInference() { @@ -1003,8 +1004,8 @@ void TheorySetsRels::check(Theory::Effort level) reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, rel[0], exps[i][1])); } sendInfer(nm->mkNode(MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel), - reason, - "TRANSPOSE-reverse"); + InferenceId::SETS_RELS_TRANSPOSE_REV, + reason); } } } @@ -1076,14 +1077,14 @@ void TheorySetsRels::check(Theory::Effort level) reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1]) ); } if( isProduct ) { - sendInfer(fact, - nm->mkNode(kind::AND, reasons), - "PRODUCT-Compose"); + sendInfer( + fact, InferenceId::SETS_RELS_PRODUCE_COMPOSE, nm->mkNode(kind::AND, reasons)); } else { if( r1_rmost != r2_lmost ) { reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1_rmost, r2_lmost) ); } - sendInfer(fact, nm->mkNode(kind::AND, reasons), "JOIN-Compose"); + sendInfer( + fact, InferenceId::SETS_RELS_JOIN_COMPOSE, nm->mkNode(kind::AND, reasons)); } } } @@ -1100,11 +1101,11 @@ void TheorySetsRels::check(Theory::Effort level) { if (p.getKind() == IMPLIES) { - processInference(p[1], p[0], "rels"); + processInference(p[1], InferenceId::UNKNOWN, p[0]); } else { - processInference(p, d_trueNode, "rels"); + processInference(p, InferenceId::UNKNOWN, d_trueNode); } if (d_state.isInConflict()) { @@ -1120,7 +1121,7 @@ void TheorySetsRels::check(Theory::Effort level) d_pending.clear(); } - void TheorySetsRels::processInference(Node conc, Node exp, const char* c) + void TheorySetsRels::processInference(Node conc, InferenceId id, Node exp) { Trace("sets-pinfer") << "Process inference: " << exp << " => " << conc << std::endl; @@ -1129,11 +1130,11 @@ void TheorySetsRels::check(Theory::Effort level) Trace("sets-pinfer") << " must assert as lemma" << std::endl; // we wrap the spurious explanation into a splitting lemma Node lem = NodeManager::currentNM()->mkNode(OR, exp.negate(), conc); - d_im.assertInference(lem, d_trueNode, c, 1); + d_im.assertInference(lem, id, d_trueNode, 1); return; } // try to assert it as a fact - d_im.assertInference(conc, exp, c); + d_im.assertInference(conc, id, exp); } bool TheorySetsRels::isRelationKind( Kind k ) { @@ -1235,7 +1236,7 @@ void TheorySetsRels::check(Theory::Effort level) Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); tuple_reduct = NodeManager::currentNM()->mkNode(kind::MEMBER,tuple_reduct, n[1]); Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::EQUAL, n, tuple_reduct); - sendInfer(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); + sendInfer(tuple_reduction_lemma, InferenceId::SETS_RELS_TUPLE_REDUCTION, d_trueNode); d_symbolic_tuples.insert(n); } } @@ -1323,10 +1324,10 @@ void TheorySetsRels::check(Theory::Effort level) } } - void TheorySetsRels::sendInfer(Node fact, Node reason, const char* c) + void TheorySetsRels::sendInfer(Node fact, InferenceId id, Node reason) { Trace("rels-lemma") << "Rels::lemma " << fact << " from " << reason - << " by " << c << std::endl; + << " by " << id << std::endl; Node lemma = NodeManager::currentNM()->mkNode(IMPLIES, reason, fact); d_pending.push_back(lemma); } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 95a13f4d5..312e55b0d 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -127,12 +127,9 @@ private: * Called when we have inferred fact from explanation reason, where the * latter should be a conjunction of facts that hold in the current context. * - * The argument c is used for debugging, to give the name of the inference - * rule being used. - * * This method adds the node (=> reason exp) to the pending vector d_pending. */ - void sendInfer(Node fact, Node reason, const char* c); + void sendInfer(Node fact, InferenceId id, Node reason); /** * This method flushes the inferences in the pending vector d_pending to * theory of sets, which may process them as lemmas or as facts to assert to @@ -143,10 +140,8 @@ private: * * A wrapper around d_im.assertInference that ensures that we do not send * inferences with explanations that are not entailed. - * - * Argument c is used for debugging, typically the name of the inference. */ - void processInference(Node conc, Node exp, const char* c); + void processInference(Node conc, InferenceId id, Node exp); /** Methods used in full effort */ void check(); |