From f5486884229348516ac26300273e4f5458a74208 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 11 Feb 2021 20:00:18 +0100 Subject: [PATCH] Add InferenceId member to TheoryInference, adapt all derived classes. (#5894) This PR adds a new InferenceId member to the TheoryInference class. All classes derived from TheoryInference are adapted accordingly. --- src/theory/arith/arith_lemma.h | 5 +-- src/theory/arith/inference_manager.cpp | 4 +- src/theory/arith/nl/nonlinear_extension.cpp | 4 +- src/theory/bags/infer_info.cpp | 4 +- src/theory/bags/infer_info.h | 4 +- src/theory/bags/inference_generator.cpp | 41 +++++++++------------ src/theory/datatypes/infer_proof_cons.cpp | 2 +- src/theory/datatypes/inference.cpp | 8 ++-- src/theory/datatypes/inference.h | 4 -- src/theory/inference_manager_buffered.cpp | 4 +- src/theory/strings/core_solver.cpp | 32 ++++++++-------- src/theory/strings/core_solver.h | 2 +- src/theory/strings/infer_info.cpp | 4 +- src/theory/strings/infer_info.h | 4 +- src/theory/strings/infer_proof_cons.cpp | 2 +- src/theory/strings/inference_manager.cpp | 33 ++++++++--------- src/theory/strings/solver_state.cpp | 5 +-- src/theory/strings/theory_strings.cpp | 2 +- src/theory/theory_inference.cpp | 10 +++-- src/theory/theory_inference.h | 14 ++++++- src/theory/theory_inference_manager.h | 1 + 21 files changed, 89 insertions(+), 100 deletions(-) diff --git a/src/theory/arith/arith_lemma.h b/src/theory/arith/arith_lemma.h index 85e55b1e3..e50df15c0 100644 --- a/src/theory/arith/arith_lemma.h +++ b/src/theory/arith/arith_lemma.h @@ -41,13 +41,10 @@ class ArithLemma : public SimpleTheoryLemma LemmaProperty p, ProofGenerator* pg, InferenceId inf = InferenceId::UNKNOWN) - : SimpleTheoryLemma(n, p, pg), d_inference(inf) + : SimpleTheoryLemma(inf, n, p, pg) { } virtual ~ArithLemma() {} - - /** The inference id for the lemma */ - InferenceId d_inference; }; /** * Writes an arithmetic lemma to a stream. diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 6a1f898d3..aa0aa4f2a 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -32,7 +32,7 @@ InferenceManager::InferenceManager(TheoryArith& ta, void InferenceManager::addPendingArithLemma(std::unique_ptr lemma, bool isWaiting) { - Trace("arith::infman") << "Add " << lemma->d_inference << " " << lemma->d_node + Trace("arith::infman") << "Add " << lemma->getId() << " " << lemma->d_node << (isWaiting ? " as waiting" : "") << std::endl; if (hasCachedLemma(lemma->d_node, lemma->d_property)) { @@ -81,7 +81,7 @@ void InferenceManager::flushWaitingLemmas() for (auto& lem : d_waitingLem) { Trace("arith::infman") << "Flush waiting lemma to pending: " - << lem->d_inference << " " << lem->d_node + << lem->getId() << " " << lem->d_node << std::endl; d_pendingLem.emplace_back(std::move(lem)); } diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index d6a1e94a1..709b1e777 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -89,10 +89,10 @@ void NonlinearExtension::sendLemmas(const std::vector& out) { for (const NlLemma& nlem : out) { - Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_inference + Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.getId() << " : " << nlem.d_node << std::endl; d_im.addPendingArithLemma(nlem); - d_stats.d_inferences << nlem.d_inference; + d_stats.d_inferences << nlem.getId(); } } diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp index 9b5187689..c4e957087 100644 --- a/src/theory/bags/infer_info.cpp +++ b/src/theory/bags/infer_info.cpp @@ -20,7 +20,7 @@ namespace CVC4 { namespace theory { namespace bags { -InferInfo::InferInfo() : d_id(InferenceId::UNKNOWN) {} +InferInfo::InferInfo(InferenceId id) : TheoryInference(id) {} bool InferInfo::process(TheoryInferenceManager* im, bool asLemma) { @@ -77,7 +77,7 @@ bool InferInfo::isFact() const std::ostream& operator<<(std::ostream& out, const InferInfo& ii) { - out << "(infer :id " << ii.d_id << std::endl; + out << "(infer :id " << ii.getId() << std::endl; out << ":conclusion " << ii.d_conclusion << std::endl; if (!ii.d_premises.empty()) { diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h index 8628d19f6..66d75b5dc 100644 --- a/src/theory/bags/infer_info.h +++ b/src/theory/bags/infer_info.h @@ -38,12 +38,10 @@ class InferenceManager; class InferInfo : public TheoryInference { public: - InferInfo(); + InferInfo(InferenceId id); ~InferInfo() {} /** Process this inference */ bool process(TheoryInferenceManager* im, bool asLemma) override; - /** The inference identifier */ - InferenceId d_id; /** The conclusion */ Node d_conclusion; /** diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 6d8b6a33b..2d4a5afed 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -37,8 +37,7 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e) Assert(n.getType().isBag()); Assert(e.getType() == n.getType().getBagElementType()); - InferInfo inferInfo; - inferInfo.d_id = InferenceId::BAG_NON_NEGATIVE_COUNT; + InferInfo inferInfo(InferenceId::BAG_NON_NEGATIVE_COUNT); Node count = d_nm->mkNode(kind::BAG_COUNT, e, n); Node gte = d_nm->mkNode(kind::GEQ, count, d_zero); @@ -51,28 +50,30 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e) Assert(n.getKind() == kind::MK_BAG); Assert(e.getType() == n.getType().getBagElementType()); - InferInfo inferInfo; - Node skolem = getSkolem(n, inferInfo); - Node count = getMultiplicityTerm(e, skolem); if (n[0] == e) { // TODO issue #78: refactor this with BagRewriter // (=> true (= (bag.count e (bag e c)) c)) - inferInfo.d_id = InferenceId::BAG_MK_BAG_SAME_ELEMENT; + InferInfo inferInfo(InferenceId::BAG_MK_BAG_SAME_ELEMENT); + Node skolem = getSkolem(n, inferInfo); + Node count = getMultiplicityTerm(e, skolem); inferInfo.d_conclusion = count.eqNode(n[1]); + return inferInfo; } else { // (=> // true // (= (bag.count e (bag x c)) (ite (= e x) c 0))) - inferInfo.d_id = InferenceId::BAG_MK_BAG; + InferInfo inferInfo(InferenceId::BAG_MK_BAG); + Node skolem = getSkolem(n, inferInfo); + Node count = getMultiplicityTerm(e, skolem); Node same = d_nm->mkNode(kind::EQUAL, n[0], e); Node ite = d_nm->mkNode(kind::ITE, same, n[1], d_zero); Node equal = count.eqNode(ite); inferInfo.d_conclusion = equal; + return inferInfo; } - return inferInfo; } struct BagsDeqAttributeId @@ -87,8 +88,7 @@ InferInfo InferenceGenerator::bagDisequality(Node n) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo; - inferInfo.d_id = InferenceId::BAG_DISEQUALITY; + InferInfo inferInfo(InferenceId::BAG_DISEQUALITY); TypeNode elementType = A.getType().getBagElementType(); BoundVarManager* bvm = d_nm->getBoundVarManager(); @@ -121,9 +121,8 @@ InferInfo InferenceGenerator::empty(Node n, Node e) Assert(n.getKind() == kind::EMPTYBAG); Assert(e.getType() == n.getType().getBagElementType()); - InferInfo inferInfo; + InferInfo inferInfo(InferenceId::BAG_EMPTY); Node skolem = getSkolem(n, inferInfo); - inferInfo.d_id = InferenceId::BAG_EMPTY; Node count = getMultiplicityTerm(e, skolem); Node equal = count.eqNode(d_zero); @@ -138,8 +137,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo; - inferInfo.d_id = InferenceId::BAG_UNION_DISJOINT; + InferInfo inferInfo(InferenceId::BAG_UNION_DISJOINT); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -161,8 +159,7 @@ InferInfo InferenceGenerator::unionMax(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo; - inferInfo.d_id = InferenceId::BAG_UNION_MAX; + InferInfo inferInfo(InferenceId::BAG_UNION_MAX); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -185,8 +182,7 @@ InferInfo InferenceGenerator::intersection(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo; - inferInfo.d_id = InferenceId::BAG_INTERSECTION_MIN; + InferInfo inferInfo(InferenceId::BAG_INTERSECTION_MIN); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -207,8 +203,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo; - inferInfo.d_id = InferenceId::BAG_DIFFERENCE_SUBTRACT; + InferInfo inferInfo(InferenceId::BAG_DIFFERENCE_SUBTRACT); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -230,8 +225,7 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e) Node A = n[0]; Node B = n[1]; - InferInfo inferInfo; - inferInfo.d_id = InferenceId::BAG_DIFFERENCE_REMOVE; + InferInfo inferInfo(InferenceId::BAG_DIFFERENCE_REMOVE); Node countA = getMultiplicityTerm(e, A); Node countB = getMultiplicityTerm(e, B); @@ -252,8 +246,7 @@ InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e) Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; - InferInfo inferInfo; - inferInfo.d_id = InferenceId::BAG_DUPLICATE_REMOVAL; + InferInfo inferInfo(InferenceId::BAG_DUPLICATE_REMOVAL); Node countA = getMultiplicityTerm(e, A); Node skolem = getSkolem(n, inferInfo); diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index fcf16b127..14dc9fbf1 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -261,7 +261,7 @@ std::shared_ptr InferProofCons::getProofFor(Node fact) // now go back and convert it to proof steps and add to proof std::shared_ptr di = (*it).second; // run the conversion - convert(di->getInferId(), di->d_conc, di->d_exp, &pf); + convert(di->getId(), di->d_conc, di->d_exp, &pf); return pf.getProofFor(fact); } diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp index 0f5a5e869..5d68159f7 100644 --- a/src/theory/datatypes/inference.cpp +++ b/src/theory/datatypes/inference.cpp @@ -29,7 +29,7 @@ DatatypesInference::DatatypesInference(InferenceManager* im, Node conc, Node exp, InferenceId i) - : SimpleTheoryInternalFact(conc, exp, nullptr), d_im(im), d_id(i) + : SimpleTheoryInternalFact(i, conc, exp, nullptr), d_im(im) { // false is not a valid explanation Assert(d_exp.isNull() || !d_exp.isConst() || d_exp.getConst()); @@ -68,13 +68,11 @@ bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma) // sent as a lemma in addPendingInference below. if (asLemma || mustCommunicateFact(d_conc, d_exp)) { - return d_im->processDtLemma(d_conc, d_exp, d_id); + return d_im->processDtLemma(d_conc, d_exp, getId()); } - return d_im->processDtFact(d_conc, d_exp, d_id); + return d_im->processDtFact(d_conc, d_exp, getId()); } -InferenceId DatatypesInference::getInferId() const { return d_id; } - } // namespace datatypes } // namespace theory } // namespace CVC4 diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h index ca7e08f43..d31f7b839 100644 --- a/src/theory/datatypes/inference.h +++ b/src/theory/datatypes/inference.h @@ -62,14 +62,10 @@ class DatatypesInference : public SimpleTheoryInternalFact * above method. */ bool process(TheoryInferenceManager* im, bool asLemma) override; - /** Get the inference identifier */ - InferenceId getInferId() const; private: /** Pointer to the inference manager */ InferenceManager* d_im; - /** The inference */ - InferenceId d_id; }; } // namespace datatypes diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index bc038a149..e5f6ae4e4 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -59,7 +59,7 @@ bool InferenceManagerBuffered::addPendingLemma(Node lem, } } // make the simple theory lemma - d_pendingLem.emplace_back(new SimpleTheoryLemma(lem, p, pg)); + d_pendingLem.emplace_back(new SimpleTheoryLemma(InferenceId::UNKNOWN, lem, p, pg)); return true; } @@ -75,7 +75,7 @@ void InferenceManagerBuffered::addPendingFact(Node conc, { // make a simple theory internal fact Assert(conc.getKind() != AND && conc.getKind() != OR); - d_pendingFact.emplace_back(new SimpleTheoryInternalFact(conc, exp, pg)); + d_pendingFact.emplace_back(new SimpleTheoryInternalFact(InferenceId::UNKNOWN, conc, exp, pg)); } void InferenceManagerBuffered::addPendingFact( diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 343332da5..7268a35e2 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -30,7 +30,7 @@ namespace CVC4 { namespace theory { namespace strings { -CoreInferInfo::CoreInferInfo() : d_index(0), d_rev(false) {} +CoreInferInfo::CoreInferInfo(InferenceId id) : d_infer(id), d_index(0), d_rev(false) {} CoreSolver::CoreSolver(SolverState& s, InferenceManager& im, @@ -1223,11 +1223,11 @@ void CoreSolver::processNEqc(Node eqc, InferInfo& ii = ipii.d_infer; Trace("strings-solve") << "#" << i << ": From " << ipii.d_i << " / " << ipii.d_j << " (rev=" << ipii.d_rev << ") : "; - Trace("strings-solve") << ii.d_conc << " by " << ii.d_id << std::endl; - if (!set_use_index || ii.d_id < min_id - || (ii.d_id == min_id && ipii.d_index > max_index)) + Trace("strings-solve") << ii.d_conc << " by " << ii.getId() << std::endl; + if (!set_use_index || ii.getId() < min_id + || (ii.getId() == min_id && ipii.d_index > max_index)) { - min_id = ii.d_id; + min_id = ii.getId(); max_index = ipii.d_index; use_index = i; set_use_index = true; @@ -1443,7 +1443,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, } // The candidate inference "info" - CoreInferInfo info; + CoreInferInfo info(InferenceId::UNKNOWN); InferInfo& iinfo = info.d_infer; info.d_index = index; // for debugging @@ -1466,7 +1466,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, Node lenEq = nm->mkNode(EQUAL, xLenTerm, yLenTerm); lenEq = Rewriter::rewrite(lenEq); iinfo.d_conc = nm->mkNode(OR, lenEq, lenEq.negate()); - iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT; + iinfo.setId(InferenceId::STRINGS_LEN_SPLIT); info.d_pendingPhase[lenEq] = true; pinfer.push_back(info); break; @@ -1546,12 +1546,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // inferred iinfo.d_conc = nm->mkNode( AND, p.eqNode(nc), !eq.getConst() ? pEq.negate() : pEq); - iinfo.d_id = InferenceId::STRINGS_INFER_EMP; + iinfo.setId(InferenceId::STRINGS_INFER_EMP); } else { iinfo.d_conc = nm->mkNode(OR, eq, eq.negate()); - iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT_EMP; + iinfo.setId(InferenceId::STRINGS_LEN_SPLIT_EMP); } pinfer.push_back(info); break; @@ -1594,7 +1594,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, xcv, stra, PfRule::CONCAT_CPROP, isRev, skc, newSkolems); Assert(newSkolems.size() == 1); iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]); - iinfo.d_id = InferenceId::STRINGS_SSPLIT_CST_PROP; + iinfo.setId(InferenceId::STRINGS_SSPLIT_CST_PROP); iinfo.d_idRev = isRev; pinfer.push_back(info); break; @@ -1614,7 +1614,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, iinfo.d_premises.push_back(expNonEmpty); Assert(newSkolems.size() == 1); iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]); - iinfo.d_id = InferenceId::STRINGS_SSPLIT_CST; + iinfo.setId(InferenceId::STRINGS_SSPLIT_CST); iinfo.d_idRev = isRev; pinfer.push_back(info); break; @@ -1703,7 +1703,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // make the conclusion if (lentTestSuccess == -1) { - iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR; + iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR); iinfo.d_conc = getConclusion(x, y, PfRule::CONCAT_SPLIT, isRev, skc, newSkolems); if (options::stringUnifiedVSpt() && !options::stringLenConc()) @@ -1714,14 +1714,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, } else if (lentTestSuccess == 0) { - iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR_PROP; + iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR_PROP); iinfo.d_conc = getConclusion(x, y, PfRule::CONCAT_LPROP, isRev, skc, newSkolems); } else { Assert(lentTestSuccess == 1); - iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR_PROP; + iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR_PROP); iinfo.d_conc = getConclusion(y, x, PfRule::CONCAT_LPROP, isRev, skc, newSkolems); } @@ -1856,7 +1856,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, iinfo.d_premises.clear(); // try to make t equal to empty to avoid loop iinfo.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate()); - iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT_EMP; + iinfo.setId(InferenceId::STRINGS_LEN_SPLIT_EMP); return ProcessLoopResult::INFERENCE; } else @@ -1973,7 +1973,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, // we will be done iinfo.d_conc = conc; - iinfo.d_id = InferenceId::STRINGS_FLOOP; + iinfo.setId(InferenceId::STRINGS_FLOOP); info.d_nfPair[0] = nfi.d_base; info.d_nfPair[1] = nfj.d_base; return ProcessLoopResult::INFERENCE; diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index 6e536cbfa..8c4c28a96 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -40,7 +40,7 @@ namespace strings { class CoreInferInfo { public: - CoreInferInfo(); + CoreInferInfo(InferenceId id); ~CoreInferInfo() {} /** The infer info of this class */ InferInfo d_infer; diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index c543de0e0..7242c58bc 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -21,7 +21,7 @@ namespace CVC4 { namespace theory { namespace strings { -InferInfo::InferInfo() : d_sim(nullptr), d_id(InferenceId::UNKNOWN), d_idRev(false) +InferInfo::InferInfo(InferenceId id): TheoryInference(id), d_sim(nullptr), d_idRev(false) { } @@ -61,7 +61,7 @@ Node InferInfo::getPremises() const std::ostream& operator<<(std::ostream& out, const InferInfo& ii) { - out << "(infer " << ii.d_id << " " << ii.d_conc; + out << "(infer " << ii.getId() << " " << ii.d_conc; if (ii.d_idRev) { out << " :rev"; diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index c0667e53c..d697f42ae 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -72,14 +72,12 @@ class InferenceManager; class InferInfo : public TheoryInference { public: - InferInfo(); + InferInfo(InferenceId id); ~InferInfo() {} /** Process this inference */ bool process(TheoryInferenceManager* im, bool asLemma) override; /** Pointer to the class used for processing this info */ InferenceManager* d_sim; - /** The inference identifier */ - InferenceId d_id; /** Whether it is the reverse form of the above id */ bool d_idRev; /** The conclusion */ diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 4817df39d..c3e1ce294 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -987,7 +987,7 @@ std::shared_ptr InferProofCons::getProofFor(Node fact) TheoryProofStepBuffer psb(d_pnm->getChecker()); std::shared_ptr ii = (*it).second; // run the conversion - convert(ii->d_id, ii->d_idRev, ii->d_conc, ii->d_premises, ps, psb, useBuffer); + convert(ii->getId(), ii->d_idRev, ii->d_conc, ii->d_premises, ps, psb, useBuffer); // make the proof based on the step or the buffer if (useBuffer) { diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 6a4fd55df..a348585e7 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -139,8 +139,7 @@ bool InferenceManager::sendInference(const std::vector& exp, return false; } // wrap in infer info and send below - InferInfo ii; - ii.d_id = infer; + InferInfo ii(infer); ii.d_idRev = isRev; ii.d_conc = eq; ii.d_premises = exp; @@ -171,8 +170,8 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma) { Trace("strings-infer-debug") << "...as conflict" << std::endl; Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by " - << ii.d_id << std::endl; - Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.d_id << std::endl; + << ii.getId() << std::endl; + Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.getId() << std::endl; ++(d_statistics.d_conflictsInfer); // process the conflict immediately processConflict(ii); @@ -194,11 +193,10 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma) if (unproc.empty()) { Node eqs = ii.d_conc; - InferInfo iiSubsLem; - iiSubsLem.d_sim = this; // keep the same id for now, since we are transforming the form of the // inference, not the root reason. - iiSubsLem.d_id = ii.d_id; + InferInfo iiSubsLem(ii.getId()); + iiSubsLem.d_sim = this; iiSubsLem.d_conc = eqs; if (Trace.isOn("strings-lemma-debug")) { @@ -234,9 +232,8 @@ bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq) return false; } NodeManager* nm = NodeManager::currentNM(); - InferInfo iiSplit; + InferInfo iiSplit(infer); iiSplit.d_sim = this; - iiSplit.d_id = infer; iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq)); eq = Rewriter::rewrite(eq); addPendingPhaseRequirement(eq, preq); @@ -291,7 +288,7 @@ void InferenceManager::processConflict(const InferInfo& ii) { Assert(!d_state.isInConflict()); // setup the fact to reproduce the proof in the call below - d_statistics.d_inferences << ii.d_id; + d_statistics.d_inferences << ii.getId(); if (d_ipc != nullptr) { d_ipc->notifyFact(ii); @@ -300,7 +297,7 @@ void InferenceManager::processConflict(const InferInfo& ii) TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get()); Assert(tconf.getKind() == TrustNodeKind::CONFLICT); Trace("strings-assert") << "(assert (not " << tconf.getNode() - << ")) ; conflict " << ii.d_id << std::endl; + << ")) ; conflict " << ii.getId() << std::endl; // send the trusted conflict trustedConflict(tconf); } @@ -321,9 +318,9 @@ bool InferenceManager::processFact(InferInfo& ii) facts.push_back(ii.d_conc); } Trace("strings-assert") << "(assert (=> " << ii.getPremises() << " " - << ii.d_conc << ")) ; fact " << ii.d_id << std::endl; + << ii.d_conc << ")) ; fact " << ii.getId() << std::endl; Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from " - << ii.getPremises() << " by " << ii.d_id + << ii.getPremises() << " by " << ii.getId() << std::endl; std::vector exp; for (const Node& ec : ii.d_premises) @@ -335,7 +332,7 @@ bool InferenceManager::processFact(InferInfo& ii) for (const Node& fact : facts) { ii.d_conc = fact; - d_statistics.d_inferences << ii.d_id; + d_statistics.d_inferences << ii.getId(); bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; bool curRet = false; @@ -390,7 +387,7 @@ bool InferenceManager::processLemma(InferInfo& ii) } // ensure that the proof generator is ready to explain the final conclusion // of the lemma (ii.d_conc). - d_statistics.d_inferences << ii.d_id; + d_statistics.d_inferences << ii.getId(); if (d_ipc != nullptr) { d_ipc->notifyFact(ii); @@ -412,14 +409,14 @@ bool InferenceManager::processLemma(InferInfo& ii) } } LemmaProperty p = LemmaProperty::NONE; - if (ii.d_id == InferenceId::STRINGS_REDUCTION) + if (ii.getId() == InferenceId::STRINGS_REDUCTION) { p |= LemmaProperty::NEEDS_JUSTIFY; } Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma " - << ii.d_id << std::endl; + << ii.getId() << std::endl; Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by " - << ii.d_id << std::endl; + << ii.getId() << std::endl; ++(d_statistics.d_lemmasInfer); // call the trusted lemma, without caching diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index b6e9c68f4..e42952175 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -28,7 +28,7 @@ namespace strings { SolverState::SolverState(context::Context* c, context::UserContext* u, Valuation& v) - : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false) + : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false), d_pendingConflict(InferenceId::UNKNOWN) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_false = NodeManager::currentNM()->mkConst(false); @@ -137,8 +137,7 @@ void SolverState::setPendingPrefixConflictWhen(Node conf) { return; } - InferInfo iiPrefixConf; - iiPrefixConf.d_id = InferenceId::STRINGS_PREFIX_CONFLICT; + InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT); iiPrefixConf.d_conc = d_false; utils::flattenOp(AND, conf, iiPrefixConf.d_premises); setPendingConflict(iiPrefixConf); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 48d461f7a..0157a47f0 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -615,7 +615,7 @@ void TheoryStrings::notifyFact(TNode atom, // process pending conflicts due to reasoning about endpoints if (!d_state.isInConflict() && d_state.hasPendingConflict()) { - InferInfo iiPendingConf; + InferInfo iiPendingConf(InferenceId::UNKNOWN); d_state.getPendingConflict(iiPendingConf); Trace("strings-pending") << "Process pending conflict " << iiPendingConf.d_premises << std::endl; diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp index 8e52c8cd1..f64b88daa 100644 --- a/src/theory/theory_inference.cpp +++ b/src/theory/theory_inference.cpp @@ -21,10 +21,11 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -SimpleTheoryLemma::SimpleTheoryLemma(Node n, +SimpleTheoryLemma::SimpleTheoryLemma(InferenceId id, + Node n, LemmaProperty p, ProofGenerator* pg) - : d_node(n), d_property(p), d_pg(pg) + : TheoryInference(id), d_node(n), d_property(p), d_pg(pg) { } @@ -36,10 +37,11 @@ bool SimpleTheoryLemma::process(TheoryInferenceManager* im, bool asLemma) return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), d_property); } -SimpleTheoryInternalFact::SimpleTheoryInternalFact(Node conc, +SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id, + Node conc, Node exp, ProofGenerator* pg) - : d_conc(conc), d_exp(exp), d_pg(pg) + : TheoryInference(id), d_conc(conc), d_exp(exp), d_pg(pg) { } diff --git a/src/theory/theory_inference.h b/src/theory/theory_inference.h index 4fea944d6..9cf787886 100644 --- a/src/theory/theory_inference.h +++ b/src/theory/theory_inference.h @@ -18,6 +18,7 @@ #define CVC4__THEORY__THEORY_INFERENCE_H #include "expr/node.h" +#include "theory/inference_id.h" #include "theory/output_channel.h" namespace CVC4 { @@ -34,6 +35,7 @@ class TheoryInferenceManager; class TheoryInference { public: + TheoryInference(InferenceId id) : d_id(id) {} virtual ~TheoryInference() {} /** * Called by the provided inference manager to process this inference. This @@ -60,6 +62,14 @@ class TheoryInference * lemma that was already cached by im and hence was discarded. */ virtual bool process(TheoryInferenceManager* im, bool asLemma) = 0; + + /** Get the InferenceId of this theory inference. */ + InferenceId getId() const { return d_id; } + /** Set the InferenceId of this theory inference. */ + void setId(InferenceId id) { d_id = id; } + + private: + InferenceId d_id; }; /** @@ -69,7 +79,7 @@ class TheoryInference class SimpleTheoryLemma : public TheoryInference { public: - SimpleTheoryLemma(Node n, LemmaProperty p, ProofGenerator* pg); + SimpleTheoryLemma(InferenceId id, Node n, LemmaProperty p, ProofGenerator* pg); virtual ~SimpleTheoryLemma() {} /** * Send the lemma using inference manager im, return true if the lemma was @@ -97,7 +107,7 @@ class SimpleTheoryLemma : public TheoryInference class SimpleTheoryInternalFact : public TheoryInference { public: - SimpleTheoryInternalFact(Node conc, Node exp, ProofGenerator* pg); + SimpleTheoryInternalFact(InferenceId id, Node conc, Node exp, ProofGenerator* pg); virtual ~SimpleTheoryInternalFact() {} /** * Send the lemma using inference manager im, return true if the lemma was diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 124b88e3e..324ceb5e1 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -21,6 +21,7 @@ #include "context/cdhashset.h" #include "expr/node.h" +#include "theory/inference_id.h" #include "theory/output_channel.h" #include "theory/theory_state.h" #include "theory/trust_node.h" -- 2.30.2