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.
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;
}
}
}
Node conc = d_false;
- d_im.sendInference(exp, conc, "F_NCTN");
+ d_im.sendInference(exp, conc, Inference::F_NCTN);
return;
}
}
}
}
-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 << "<None>"; 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 << "<Unknown>"; break;
- }
- return os;
-}
-
-} // namespace
-
void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
size_t start,
bool isRev)
{
std::vector<Node> 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)
}
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];
}
Assert(!conc_c.empty());
conc = utils::mkAnd(conc_c);
- infType = FlatFormInfer::ENDPOINT_EMP;
+ infType = Inference::F_ENDPOINT_EMP;
Assert(count > 0);
break;
}
d_bsolver.explainConstantEqc(ac,curr,exp);
d_bsolver.explainConstantEqc(bc,cc,exp);
conc = d_false;
- infType = FlatFormInfer::CONST;
+ infType = Inference::F_CONST;
break;
}
}
&& (d_flat_form[b].size() - 1) == count)
{
conc = ac.eqNode(bc);
- infType = FlatFormInfer::ENDPOINT_EQ;
+ infType = Inference::F_ENDPOINT_EQ;
break;
}
else
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;
}
}
{
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
// 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;
{
std::vector<Node> 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{
//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();
}
}
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;
// 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);
}
}
}
{
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;
}
}
}
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);
}
}
}
{
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);
}
}
}
// 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;
}
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);
}
}
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";
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";
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";
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";
// 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 = ""
// 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 != ""
// 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
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,
bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
Node conc,
- const char* c)
+ Inference infer)
{
if (conc.getKind() == AND
|| (conc.getKind() == NOT && conc[0].getKind() == OR))
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;
// already holds
return true;
}
- sendInference(exp, conc, c);
+ sendInference(exp, conc, infer);
return true;
}
void InferenceManager::sendInference(const std::vector<Node>& exp,
const std::vector<Node>& 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;
{
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()
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<Node>& exp,
- Node eq,
- const char* c,
- bool asLemma)
-{
- std::vector<Node> exp_n;
- sendInference(exp, exp_n, eq, c, asLemma);
-}
-
-void InferenceManager::sendInference(const std::vector<Node>& exp,
- const std::vector<Node>& 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<Node>& exp,
Node eq,
Inference infer,
bool asLemma)
{
- d_statistics.d_inferences << infer;
- sendInference(exp, eq, toString(infer), asLemma);
+ std::vector<Node> 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();
{
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())
{
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++)
<< " " << vars[i] << " -> " << subs[i] << std::endl;
}
}
- sendLemma(d_true, eqs, c);
+ sendLemma(d_true, eqs, infer);
return;
}
if (Trace.isOn("strings-lemma-debug"))
}
}
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);
{
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);
* 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<Node>& exp, Node conc, const char* c);
+ bool sendInternalInference(std::vector<Node>& exp,
+ Node conc,
+ Inference infer);
/** send inference
*
* This function should be called when ( exp ^ exp_n ) => eq. The set exp
* 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<Node>& exp,
- const std::vector<Node>& exp_n,
- Node eq,
- const char* c,
- bool asLemma = false);
- /** same as above, but where exp_n is empty */
- void sendInference(const std::vector<Node>& 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<Node>& exp,
const std::vector<Node>& 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<Node>& exp,
Node eq,
Inference infer,
* 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
* 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.
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);
}
// 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);
}
}
}
projects / cvc5.git / commitdiff