From fab7010523fd2e635c2c9dfd382acdefdb96d6b4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 6 Apr 2020 19:00:13 -0500 Subject: [PATCH] Enum for all remaining string inferences (#4220) Merges the Flat Form inferences enum into Inferences. Adds documentation for (most of) these inferences. Removes the old infrastructure for inferences based on a debug string in InferenceManager. --- src/theory/strings/base_solver.cpp | 2 +- src/theory/strings/core_solver.cpp | 65 ++++++------------- src/theory/strings/extf_solver.cpp | 7 ++- src/theory/strings/infer_info.cpp | 18 ++++++ src/theory/strings/infer_info.h | 72 ++++++++++++++++++++- src/theory/strings/inference_manager.cpp | 79 +++++++++--------------- src/theory/strings/inference_manager.h | 54 +++++----------- src/theory/strings/theory_strings.cpp | 4 +- 8 files changed, 158 insertions(+), 143 deletions(-) diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 076fc1cc5..1f8d2f49c 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -445,7 +445,7 @@ void BaseSolver::checkCardinality() if (!d_state.areDisequal(*itr1, *itr2)) { // add split lemma - if (d_im.sendSplit(*itr1, *itr2, "CARD-SP")) + if (d_im.sendSplit(*itr1, *itr2, Inference::CARD_SP)) { return; } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index cc92b0379..89d4a6f0c 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -179,7 +179,7 @@ void CoreSolver::checkFlatForms() } } Node conc = d_false; - d_im.sendInference(exp, conc, "F_NCTN"); + d_im.sendInference(exp, conc, Inference::F_NCTN); return; } } @@ -218,33 +218,6 @@ void CoreSolver::checkFlatForms() } } -namespace { - -enum class FlatFormInfer -{ - NONE, - CONST, - UNIFY, - ENDPOINT_EMP, - ENDPOINT_EQ, -}; - -std::ostream& operator<<(std::ostream& os, FlatFormInfer inf) -{ - switch (inf) - { - case FlatFormInfer::NONE: os << ""; break; - case FlatFormInfer::CONST: os << "F_Const"; break; - case FlatFormInfer::UNIFY: os << "F_Unify"; break; - case FlatFormInfer::ENDPOINT_EMP: os << "F_EndpointEmp"; break; - case FlatFormInfer::ENDPOINT_EQ: os << "F_EndpointEq"; break; - default: os << ""; break; - } - return os; -} - -} // namespace - void CoreSolver::checkFlatForm(std::vector& eqc, size_t start, bool isRev) @@ -265,7 +238,7 @@ void CoreSolver::checkFlatForm(std::vector& eqc, { std::vector exp; Node conc; - FlatFormInfer infType = FlatFormInfer::NONE; + Inference infType = Inference::NONE; size_t eqc_size = eqc.size(); size_t asize = d_flat_form[a].size(); if (count == asize) @@ -293,7 +266,7 @@ void CoreSolver::checkFlatForm(std::vector& eqc, } Assert(!conc_c.empty()); conc = utils::mkAnd(conc_c); - infType = FlatFormInfer::ENDPOINT_EMP; + infType = Inference::F_ENDPOINT_EMP; Assert(count > 0); // swap, will enforce is empty past current a = eqc[i]; @@ -333,7 +306,7 @@ void CoreSolver::checkFlatForm(std::vector& eqc, } Assert(!conc_c.empty()); conc = utils::mkAnd(conc_c); - infType = FlatFormInfer::ENDPOINT_EMP; + infType = Inference::F_ENDPOINT_EMP; Assert(count > 0); break; } @@ -356,7 +329,7 @@ void CoreSolver::checkFlatForm(std::vector& eqc, d_bsolver.explainConstantEqc(ac,curr,exp); d_bsolver.explainConstantEqc(bc,cc,exp); conc = d_false; - infType = FlatFormInfer::CONST; + infType = Inference::F_CONST; break; } } @@ -364,7 +337,7 @@ void CoreSolver::checkFlatForm(std::vector& eqc, && (d_flat_form[b].size() - 1) == count) { conc = ac.eqNode(bc); - infType = FlatFormInfer::ENDPOINT_EQ; + infType = Inference::F_ENDPOINT_EQ; break; } else @@ -397,7 +370,7 @@ void CoreSolver::checkFlatForm(std::vector& eqc, exp.insert(exp.end(), lexp2.begin(), lexp2.end()); d_im.addToExplanation(lcurr, lcc, exp); conc = ac.eqNode(bc); - infType = FlatFormInfer::UNIFY; + infType = Inference::F_UNIFY; break; } } @@ -424,8 +397,8 @@ void CoreSolver::checkFlatForm(std::vector& eqc, { Node c = t == 0 ? a : b; ssize_t jj; - if (infType == FlatFormInfer::ENDPOINT_EQ - || (t == 1 && infType == FlatFormInfer::ENDPOINT_EMP)) + if (infType == Inference::F_ENDPOINT_EQ + || (t == 1 && infType == Inference::F_ENDPOINT_EMP)) { // explain all the empty components for F_EndpointEq, all for // the short end for F_EndpointEmp @@ -452,9 +425,7 @@ void CoreSolver::checkFlatForm(std::vector& eqc, // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a) // when len(b)!=0. Although if we do not infer this conflict eagerly, // it may be applied (see #3272). - std::stringstream ss; - ss << infType; - d_im.sendInference(exp, conc, ss.str().c_str()); + d_im.sendInference(exp, conc, infType); if (d_state.isInConflict()) { return; @@ -493,7 +464,8 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< { std::vector exps; exps.push_back(n.eqNode(emp)); - d_im.sendInference(exps, n[i].eqNode(emp), "I_CYCLE_E"); + d_im.sendInference( + exps, n[i].eqNode(emp), Inference::I_CYCLE_E); return Node::null(); } }else{ @@ -514,7 +486,8 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< //take first non-empty if (j != i && !d_state.areEqual(n[j], emp)) { - d_im.sendInference(exp, n[j].eqNode(emp), "I_CYCLE"); + d_im.sendInference( + exp, n[j].eqNode(emp), Inference::I_CYCLE); return Node::null(); } } @@ -575,7 +548,7 @@ void CoreSolver::checkNormalFormsEq() nf_exp.push_back(utils::mkAnd(nfe.d_exp)); nf_exp.push_back(eqc_to_exp[itn->second]); Node eq = nfe.d_base.eqNode(nfe_eq.d_base); - d_im.sendInference(nf_exp, eq, "Normal_Form"); + d_im.sendInference(nf_exp, eq, Inference::NORMAL_FORM); if (d_im.hasProcessed()) { return; @@ -927,7 +900,7 @@ void CoreSolver::getNormalForms(Node eqc, // firstc/lastc, normal_forms_exp_depend. exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end()); Node conc = d_false; - d_im.sendInference(exp, conc, "N_NCTN"); + d_im.sendInference(exp, conc, Inference::N_NCTN); } } } @@ -1579,7 +1552,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, { Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl; - d_im.sendInference(info.d_ant, conc, "Loop Conflict", true); + d_im.sendInference(info.d_ant, conc, Inference::FLOOP_CONFLICT, true); return ProcessLoopResult::CONFLICT; } } @@ -2195,7 +2168,7 @@ void CoreSolver::checkNormalFormsDeq() } if (!d_state.areEqual(lt[0], lt[1]) && !d_state.areDisequal(lt[0], lt[1])) { - d_im.sendSplit(lt[0], lt[1], "DEQ-LENGTH-SP"); + d_im.sendSplit(lt[0], lt[1], Inference::DEQ_LENGTH_SP); } } } @@ -2295,7 +2268,7 @@ void CoreSolver::checkLengthsEqc() { { Node eq = llt.eqNode(lcr); ei->d_normalizedLength.set(eq); - d_im.sendInference(ant, eq, "LEN-NORM", true); + d_im.sendInference(ant, eq, Inference::LEN_NORM, true); } } } diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 0c46881e7..8ce2a3e81 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -407,8 +407,9 @@ void ExtfSolver::checkExtfEval(int effort) // reduced since this argument may be circular: we may infer than n // can be reduced to something else, but that thing may argue that it // can be reduced to n, in theory. - d_im.sendInternalInference( - einfo.d_exp, nrcAssert, effort == 0 ? "EXTF_d" : "EXTF_d-N"); + Inference infer = + effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N; + d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer); } to_reduce = nrc; } @@ -629,7 +630,7 @@ void ExtfSolver::checkExtfInference(Node n, inferEqrr = Rewriter::rewrite(inferEqrr); Trace("strings-extf-infer") << "checkExtfInference: " << inferEq << " ...reduces to " << inferEqrr << std::endl; - d_im.sendInternalInference(in.d_exp, inferEqrr, "EXTF_equality_rew"); + d_im.sendInternalInference(in.d_exp, inferEqrr, Inference::EXTF_EQ_REW); } } diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 07c67e167..6881970ef 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -26,7 +26,15 @@ const char* toString(Inference i) case Inference::I_CONST_MERGE: return "I_CONST_MERGE"; case Inference::I_CONST_CONFLICT: return "I_CONST_CONFLICT"; case Inference::I_NORM: return "I_NORM"; + case Inference::CARD_SP: return "CARD_SP"; case Inference::CARDINALITY: return "CARDINALITY"; + case Inference::I_CYCLE_E: return "I_CYCLE_E"; + case Inference::I_CYCLE: return "I_CYCLE"; + case Inference::F_CONST: return "F_CONST"; + case Inference::F_UNIFY: return "F_UNIFY"; + case Inference::F_ENDPOINT_EMP: return "F_ENDPOINT_EMP"; + case Inference::F_ENDPOINT_EQ: return "F_ENDPOINT_EQ"; + case Inference::F_NCTN: return "F_NCTN"; case Inference::N_ENDPOINT_EMP: return "N_ENDPOINT_EMP"; case Inference::N_UNIFY: return "N_UNIFY"; case Inference::N_ENDPOINT_EQ: return "N_ENDPOINT_EQ"; @@ -39,6 +47,10 @@ const char* toString(Inference i) case Inference::SSPLIT_CST: return "SSPLIT_CST"; case Inference::SSPLIT_VAR: return "SSPLIT_VAR"; case Inference::FLOOP: return "FLOOP"; + case Inference::FLOOP_CONFLICT: return "FLOOP_CONFLICT"; + case Inference::NORMAL_FORM: return "NORMAL_FORM"; + case Inference::N_NCTN: return "N_NCTN"; + case Inference::LEN_NORM: return "LEN_NORM"; case Inference::DEQ_DISL_EMP_SPLIT: return "DEQ_DISL_EMP_SPLIT"; case Inference::DEQ_DISL_FIRST_CHAR_EQ_SPLIT: return "DEQ_DISL_FIRST_CHAR_EQ_SPLIT"; @@ -48,6 +60,9 @@ const char* toString(Inference i) case Inference::DEQ_DISL_STRINGS_SPLIT: return "DEQ_DISL_STRINGS_SPLIT"; case Inference::DEQ_LENS_EQ: return "DEQ_LENS_EQ"; case Inference::DEQ_NORM_EMP: return "DEQ_NORM_EMP"; + case Inference::DEQ_LENGTH_SP: return "DEQ_LENGTH_SP"; + case Inference::CODE_PROXY: return "CODE_PROXY"; + case Inference::CODE_INJ: return "CODE_INJ"; case Inference::RE_NF_CONFLICT: return "RE_NF_CONFLICT"; case Inference::RE_UNFOLD_POS: return "RE_UNFOLD_POS"; case Inference::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG"; @@ -59,6 +74,9 @@ const char* toString(Inference i) case Inference::RE_DERIVE: return "RE_DERIVE"; case Inference::EXTF: return "EXTF"; case Inference::EXTF_N: return "EXTF_N"; + case Inference::EXTF_D: return "EXTF_D"; + case Inference::EXTF_D_N: return "EXTF_D_N"; + case Inference::EXTF_EQ_REW: return "EXTF_EQ_REW"; case Inference::CTN_TRANS: return "CTN_TRANS"; case Inference::CTN_DECOMPOSE: return "CTN_DECOMPOSE"; case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL"; diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 3ce673967..7fce2eaf2 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -59,10 +59,39 @@ enum class Inference : uint32_t // equal after e.g. removing strings that are currently empty. For example: // y = "" ^ z = "" => x ++ y = z ++ x I_NORM, + // A split due to cardinality + CARD_SP, // The cardinality inference for strings, see Liang et al CAV 2014. CARDINALITY, //-------------------------------------- end base solver //-------------------------------------- core solver + // A cycle in the empty string equivalence class, e.g.: + // x ++ y = "" => x = "" + // This is typically not applied due to length constraints implying emptiness. + I_CYCLE_E, + // A cycle in the containment ordering. + // x = y ++ x => y = "" or + // x = y ++ z ^ y = x ++ w => z = "" ^ w = "" + // This is typically not applied due to length constraints implying emptiness. + I_CYCLE, + // Flat form constant + // x = y ^ x = z ++ c ... ^ y = z ++ d => false + // where c and d are distinct constants. + F_CONST, + // Flat form unify + // x = y ^ x = z ++ x' ... ^ y = z ++ y' ^ len(x') = len(y') => x' = y' + // Notice flat form instances are similar to normal form inferences but do + // not involve recursive explanations. + F_UNIFY, + // Flat form endpoint empty + // x = y ^ x = z ^ y = z ++ y' => y' = "" + F_ENDPOINT_EMP, + // Flat form endpoint equal + // x = y ^ x = z ++ x' ^ y = z ++ y' => x' = y' + F_ENDPOINT_EQ, + // Flat form not contained + // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false + F_NCTN, // Given two normal forms, infers that the remainder one of them has to be // empty. For example: // If x1 ++ x2 = y1 and x1 = y1, then x2 = "" @@ -119,6 +148,18 @@ enum class Inference : uint32_t // for fresh u, u1, u2. // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014. FLOOP, + // loop conflict ??? + FLOOP_CONFLICT, + // Normal form inference + // x = y ^ z = y => x = z + // This is applied when y is the normal form of both x and z. + NORMAL_FORM, + // Normal form not contained, same as FFROM_NCTN but for normal forms + N_NCTN, + // Length normalization + // x = y => len( x ) = len( y ) + // Typically applied when y is the normal form of x. + LEN_NORM, // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y), we apply the // inference: // x = "" v x != "" @@ -152,7 +193,18 @@ enum class Inference : uint32_t // ni = px ++ x ++ ... ^ nj = py ^ len(ni) = len(nj) ---> // x = "" ^ ... DEQ_NORM_EMP, + // When two strings are disequal s != t and the comparison of their lengths + // is unknown, we apply the inference: + // len(s) != len(t) V len(s) = len(t) + DEQ_LENGTH_SP, //-------------------------------------- end core solver + //-------------------------------------- codes solver + // str.to_code( v ) = rewrite( str.to_code(c) ) + // where v is the proxy variable for c. + CODE_PROXY, + // str.code(x) = -1 V str.code(x) != str.code(y) V x = y + CODE_INJ, + //-------------------------------------- end codes solver //-------------------------------------- regexp solver // regular expression normal form conflict // ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false @@ -190,14 +242,30 @@ enum class Inference : uint32_t RE_DERIVE, //-------------------------------------- end regexp solver //-------------------------------------- extended function solver - // All extended function inferences from context-dependent rewriting produced - // by constant substitutions. See Reynolds et al CAV 2017. These are + // Standard extended function inferences from context-dependent rewriting + // produced by constant substitutions. See Reynolds et al CAV 2017. These are // inferences of the form: // X = Y => f(X) = t when rewrite( f(Y) ) = t // where X = Y is a vector of equalities, where some of Y may be constants. EXTF, // Same as above, for normal form substitutions. EXTF_N, + // Decompositions based on extended function inferences from context-dependent + // rewriting produced by constant substitutions. This is like the above, but + // handles cases where the inferred predicate is not necessarily an equality + // involving f(X). For example: + // x = "A" ^ contains( y ++ x, "B" ) => contains( y, "B" ) + // This is generally only inferred if contains( y, "B" ) is a known term in + // the current context. + EXTF_D, + // Same as above, for normal form substitutions. + EXTF_D_N, + // Extended function equality rewrite. This is an inference of the form: + // t = s => P + // where P is a predicate implied by rewrite( t = s ). + // Typically, t is an application of an extended function and s is a constant. + // It is generally only inferred if P is a predicate over known terms. + EXTF_EQ_REW, // contain transitive // ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ). CTN_TRANS, diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 94051a2bb..f262a2c7d 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -57,7 +57,7 @@ InferenceManager::InferenceManager(TheoryStrings& p, bool InferenceManager::sendInternalInference(std::vector& exp, Node conc, - const char* c) + Inference infer) { if (conc.getKind() == AND || (conc.getKind() == NOT && conc[0].getKind() == OR)) @@ -67,7 +67,7 @@ bool InferenceManager::sendInternalInference(std::vector& exp, bool ret = true; for (const Node& cc : conj) { - bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), c); + bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), infer); ret = ret && retc; } return ret; @@ -110,21 +110,21 @@ bool InferenceManager::sendInternalInference(std::vector& exp, // already holds return true; } - sendInference(exp, conc, c); + sendInference(exp, conc, infer); return true; } void InferenceManager::sendInference(const std::vector& exp, const std::vector& exp_n, Node eq, - const char* c, + Inference infer, bool asLemma) { eq = eq.isNull() ? d_false : Rewriter::rewrite(eq); if (Trace.isOn("strings-infer-debug")) { Trace("strings-infer-debug") - << "By " << c << ", infer : " << eq << " from: " << std::endl; + << "By " << infer << ", infer : " << eq << " from: " << std::endl; for (unsigned i = 0; i < exp.size(); i++) { Trace("strings-infer-debug") << " " << exp[i] << std::endl; @@ -138,6 +138,8 @@ void InferenceManager::sendInference(const std::vector& exp, { return; } + // only keep stats if not trivial conclusion + d_statistics.d_inferences << infer; Node atom = eq.getKind() == NOT ? eq[0] : eq; // check if we should send a lemma or an inference if (asLemma || atom == d_false || atom.getKind() == OR || !exp_n.empty() @@ -172,58 +174,38 @@ void InferenceManager::sendInference(const std::vector& exp, eq = eq_exp.negate(); eq_exp = d_true; } - sendLemma(eq_exp, eq, c); + sendLemma(eq_exp, eq, infer); } else { - sendInfer(utils::mkAnd(exp), eq, c); + sendInfer(utils::mkAnd(exp), eq, infer); } } -void InferenceManager::sendInference(const std::vector& exp, - Node eq, - const char* c, - bool asLemma) -{ - std::vector exp_n; - sendInference(exp, exp_n, eq, c, asLemma); -} - -void InferenceManager::sendInference(const std::vector& exp, - const std::vector& exp_n, - Node eq, - Inference infer, - bool asLemma) -{ - d_statistics.d_inferences << infer; - std::stringstream ss; - ss << infer; - sendInference(exp, exp_n, eq, ss.str().c_str(), asLemma); -} - void InferenceManager::sendInference(const std::vector& exp, Node eq, Inference infer, bool asLemma) { - d_statistics.d_inferences << infer; - sendInference(exp, eq, toString(infer), asLemma); + std::vector exp_n; + sendInference(exp, exp_n, eq, infer, asLemma); } void InferenceManager::sendInference(const InferInfo& i) { sendInference(i.d_ant, i.d_antn, i.d_conc, i.d_id, true); } -void InferenceManager::sendLemma(Node ant, Node conc, const char* c) + +void InferenceManager::sendLemma(Node ant, Node conc, Inference infer) { if (conc.isNull() || conc == d_false) { Trace("strings-conflict") - << "Strings::Conflict : " << c << " : " << ant << std::endl; - Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant + << "Strings::Conflict : " << infer << " : " << ant << std::endl; + Trace("strings-lemma") << "Strings::Conflict : " << infer << " : " << ant << std::endl; Trace("strings-assert") - << "(assert (not " << ant << ")) ; conflict " << c << std::endl; + << "(assert (not " << ant << ")) ; conflict " << infer << std::endl; ++(d_statistics.d_conflictsInfer); d_out.conflict(ant); d_state.setConflict(); @@ -238,13 +220,14 @@ void InferenceManager::sendLemma(Node ant, Node conc, const char* c) { lem = NodeManager::currentNM()->mkNode(IMPLIES, ant, conc); } - Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl; - Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c + Trace("strings-lemma") << "Strings::Lemma " << infer << " : " << lem + << std::endl; + Trace("strings-assert") << "(assert " << lem << ") ; lemma " << infer << std::endl; d_pendingLem.push_back(lem); } -void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c) +void InferenceManager::sendInfer(Node eq_exp, Node eq, Inference infer) { if (options::stringInferSym()) { @@ -259,7 +242,7 @@ void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c) if (Trace.isOn("strings-lemma-debug")) { Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " - << eq_exp << " by " << c << std::endl; + << eq_exp << " by " << infer << std::endl; Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl; for (unsigned i = 0, nvars = vars.size(); i < nvars; i++) @@ -268,7 +251,7 @@ void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c) << " " << vars[i] << " -> " << subs[i] << std::endl; } } - sendLemma(d_true, eqs, c); + sendLemma(d_true, eqs, infer); return; } if (Trace.isOn("strings-lemma-debug")) @@ -281,16 +264,16 @@ void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c) } } Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp - << " by " << c << std::endl; + << " by " << infer << std::endl; Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq - << ")) ; infer " << c << std::endl; + << ")) ; infer " << infer << std::endl; d_pending.push_back(eq); d_pendingExp[eq] = eq_exp; d_keep.insert(eq); d_keep.insert(eq_exp); } -bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq) +bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq) { Node eq = a.eqNode(b); eq = Rewriter::rewrite(eq); @@ -298,21 +281,17 @@ bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq) { return false; } + // update statistics + d_statistics.d_inferences << infer; NodeManager* nm = NodeManager::currentNM(); Node lemma_or = nm->mkNode(OR, eq, nm->mkNode(NOT, eq)); - Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or - << std::endl; + Trace("strings-lemma") << "Strings::Lemma " << infer + << " SPLIT : " << lemma_or << std::endl; d_pendingLem.push_back(lemma_or); sendPhaseRequirement(eq, preq); return true; } -bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq) -{ - d_statistics.d_inferences << infer; - return sendSplit(a, b, toString(infer), preq); -} - void InferenceManager::sendPhaseRequirement(Node lit, bool pol) { lit = Rewriter::rewrite(lit); diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 2a361aa44..af1f28a23 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -92,15 +92,17 @@ class InferenceManager * sendInference below in that it does not introduce any new non-constant * terms to the state. * - * The argument c is a string identifying the reason for the inference. - * This string is used for debugging purposes. + * The argument infer identifies the reason for the inference. + * This is used for debugging and statistics purposes. * * Return true if the inference is complete, in the sense that we infer * inferences that are equivalent to conc. This returns false e.g. if conc * (or one of its conjuncts if it is a conjunction) was not inferred due * to the criteria mentioned above. */ - bool sendInternalInference(std::vector& exp, Node conc, const char* c); + bool sendInternalInference(std::vector& exp, + Node conc, + Inference infer); /** send inference * * This function should be called when ( exp ^ exp_n ) => eq. The set exp @@ -127,39 +129,19 @@ class InferenceManager * exp_n is empty. In particular, lemmas must be used whenever exp_n is * non-empty, conflicts are used when exp_n is empty and eq is false. * - * The argument c is a string identifying the reason for inference, used for - * debugging. + * The argument infer identifies the reason for inference, used for + * debugging. This updates the statistics about the number of inferences made + * of each type. * * If the flag asLemma is true, then this method will send a lemma instead * of an inference whenever applicable. */ - void sendInference(const std::vector& exp, - const std::vector& exp_n, - Node eq, - const char* c, - bool asLemma = false); - /** same as above, but where exp_n is empty */ - void sendInference(const std::vector& exp, - Node eq, - const char* c, - bool asLemma = false); - - /** - * The same as `sendInference()` above but with an `Inference` instead of a - * string. This variant updates the statistics about the number of inferences - * made of each type. - */ void sendInference(const std::vector& exp, const std::vector& exp_n, Node eq, Inference infer, bool asLemma = false); - - /** - * The same as `sendInference()` above but with an `Inference` instead of a - * string. This variant updates the statistics about the number of inferences - * made of each type. - */ + /** same as above, but where exp_n is empty */ void sendInference(const std::vector& exp, Node eq, Inference infer, @@ -177,19 +159,13 @@ class InferenceManager * lemma. We additionally request a phase requirement for the equality a=b * with polarity preq. * - * The argument c is a string identifying the reason for inference, used for - * debugging. + * The argument infer identifies the reason for inference, used for + * debugging. This updates the statistics about the number of + * inferences made of each type. * * This method returns true if the split was non-trivial, and false * otherwise. A split is trivial if a=b rewrites to a constant. */ - bool sendSplit(Node a, Node b, const char* c, bool preq = true); - - /** - * The same as `sendSplit()` above but with an `Inference` instead of a - * string. This variant updates the statistics about the number of - * inferences made of each type. - */ bool sendSplit(Node a, Node b, Inference infer, bool preq = true); /** Send phase requirement @@ -339,17 +315,17 @@ class InferenceManager * above lemma to the lemma cache d_pending_lem, which may be flushed * later within the current call to TheoryStrings::check. * - * The argument c is a string identifying the reason for inference, used for + * The argument infer identifies the reason for inference, used for * debugging. */ - void sendLemma(Node ant, Node conc, const char* c); + void sendLemma(Node ant, Node conc, Inference infer); /** * Indicates that conc should be added to the equality engine of this class * with explanation eq_exp. It must be the case that eq_exp is a (conjunction * of) literals that each are explainable, i.e. they already hold in the * equality engine of this class. */ - void sendInfer(Node eq_exp, Node eq, const char* c); + void sendInfer(Node eq_exp, Node eq, Inference infer); /** * Get the lemma required for registering the length information for * atomic term n given length status s. For details, see registerTermAtomic. diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 92116582f..da8c3583d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1014,7 +1014,7 @@ void TheoryStrings::checkCodes() Node vc = nm->mkNode(STRING_TO_CODE, cp); if (!d_state.areEqual(cc, vc)) { - d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy"); + d_im.sendInference(d_empty_vec, cc.eqNode(vc), Inference::CODE_PROXY); } const_codes.push_back(vc); } @@ -1052,7 +1052,7 @@ void TheoryStrings::checkCodes() // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); d_im.sendPhaseRequirement(deq, false); - d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj"); + d_im.sendInference(d_empty_vec, inj_lem, Inference::CODE_INJ); } } } -- 2.30.2