This updates the internal data structure for strings inferences "InferInfo" such that it is amenable to proof reconstruction.
Currently, the explanation for a conclusion is in two parts:
(1) d_ant, the antecedents that can be explained by the current equality engine,
(2) d_antn, the antecedents that cannot.
For proof reconstruction, the order of some antecedents matters. This is difficult with the above data structure since elements in these two vectors are not given an ordering relative to each other. After this PR, we store:
(1) d_ant, all antecedants, which are ordered in a way that is amenable to proofs (to be introduced on following PRs),
(2) d_noExplain, the subset of d_ant that cannot be explained by the current equality engine.
This PR modifies calls to InferenceManager in preparation for extending it with a proof reconstructor InferProofCons which will convert strings::InferInfo into instructions for building ProofNode.
// 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).
- d_im.sendInference(exp, conc, infType);
+ d_im.sendInference(exp, conc, infType, isRev);
if (d_state.isInConflict())
{
return;
// can infer that this string must be empty
Node eq = nfkv[index_k].eqNode(emp);
Assert(!d_state.areEqual(emp, nfkv[index_k]));
- d_im.sendInference(curr_exp, eq, Inference::N_ENDPOINT_EMP);
+ d_im.sendInference(curr_exp, eq, Inference::N_ENDPOINT_EMP, isRev);
index_k++;
}
break;
if (x.isConst() && y.isConst())
{
// if both are constant, it's just a constant conflict
- d_im.sendInference(ant, d_false, Inference::N_CONST, true);
+ d_im.sendInference(ant, d_false, Inference::N_CONST, isRev, true);
return;
}
// `x` and `y` have the same length. We infer that the two components
// set the explanation for length
Node lant = utils::mkAnd(lenExp);
ant.push_back(lant);
- d_im.sendInference(ant, eq, Inference::N_UNIFY);
+ d_im.sendInference(ant, eq, Inference::N_UNIFY, isRev);
break;
}
else if ((!x.isConst() && index == nfiv.size() - rproc - 1)
{
std::vector<Node> antec;
NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, antec);
- d_im.sendInference(
- antec, eqn[0].eqNode(eqn[1]), Inference::N_ENDPOINT_EQ, true);
+ d_im.sendInference(antec,
+ eqn[0].eqNode(eqn[1]),
+ Inference::N_ENDPOINT_EQ,
+ isRev,
+ true);
}
else
{
// E.g. "abc" ++ ... = "bc" ++ ... ---> conflict
std::vector<Node> antec;
NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, antec);
- d_im.sendInference(antec, d_false, Inference::N_CONST, true);
+ d_im.sendInference(antec, d_false, Inference::N_CONST, isRev, true);
break;
}
}
if (detectLoop(nfi, nfj, index, lhsLoopIdx, rhsLoopIdx, rproc))
{
// We are dealing with a looping word equation.
+ // Note we could make this code also run in the reverse direction, but
+ // this is not implemented currently.
if (!isRev)
- { // FIXME
+ {
+ // add temporarily to the antecedant of iinfo.
NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, iinfo.d_ant);
ProcessLoopResult plr =
processLoop(lhsLoopIdx != -1 ? nfi : nfj,
break;
}
Assert(plr == ProcessLoopResult::SKIPPED);
+ // not processing an inference here, undo changes to ant
+ iinfo.d_ant.clear();
}
}
<< " explanation was : " << et.second << std::endl;
lentTestSuccess = e;
lenConstraint = entLit;
- // its not explained by the equality engine of this class
- iinfo.d_antn.push_back(lenConstraint);
+ // Its not explained by the equality engine of this class, so its
+ // marked as not being explained. The length constraint is
+ // additionally being saved and added to the length constraint
+ // vector lcVec below, which is added to iinfo.d_ant below. Length
+ // constraints are being added as the last antecedant for the sake
+ // of proof reconstruction, which expect length constraints to come
+ // last.
+ iinfo.d_noExplain.push_back(lenConstraint);
break;
}
}
}
}
+ // lcVec stores the length constraint portion of the antecedant.
std::vector<Node> lcVec;
if (lenConstraint.isNull())
{
lenConstraint = nm->mkNode(EQUAL, xLenTerm, yLenTerm).negate();
lcVec.push_back(lenConstraint);
}
+ else
+ {
+ utils::flattenOp(AND, lenConstraint, lcVec);
+ }
NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, iinfo.d_ant);
// Add premises for x != "" ^ y != ""
else
{
tnz = x.eqNode(emp).negate();
- // lcVec.push_back(tnz);
- iinfo.d_antn.push_back(tnz);
+ lcVec.push_back(tnz);
+ iinfo.d_noExplain.push_back(tnz);
}
}
SkolemCache* skc = d_termReg.getSkolemCache();
iinfo.d_conc =
getConclusion(y, x, PfRule::CONCAT_LPROP, isRev, skc, newSkolems);
}
+ // add the length constraint(s) as the last antecedant
Node lc = utils::mkAnd(lcVec);
iinfo.d_ant.push_back(lc);
iinfo.d_idRev = isRev;
{
Trace("strings-loop") << "Strings::Loop: tails are different."
<< std::endl;
- d_im.sendInference(iinfo.d_ant, conc, Inference::FLOOP_CONFLICT, true);
+ d_im.sendInference(
+ iinfo.d_ant, conc, Inference::FLOOP_CONFLICT, false, true);
return ProcessLoopResult::CONFLICT;
}
}
Node expNonEmpty = d_state.explainNonEmpty(t);
if (expNonEmpty.isNull())
{
+ // no antecedants necessary
+ iinfo.d_ant.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 = Inference::LEN_SPLIT_EMP;
}
std::vector<Node> antecLen;
antecLen.push_back(nm->mkNode(GEQ, nckLenTerm, d_one));
- d_im.sendInference({},
+ d_im.sendInference(antecLen,
antecLen,
conc,
Inference::DEQ_DISL_FIRST_CHAR_STRING_SPLIT,
+ false,
true);
return;
}
d_termReg.registerTermAtomic(newSkolems[1], LENGTH_GEQ_ONE);
std::vector<Node> antecLen;
antecLen.push_back(nm->mkNode(GT, uxLen, uyLen));
- d_im.sendInference(
- {}, antecLen, conc, Inference::DEQ_DISL_STRINGS_SPLIT, true);
+ d_im.sendInference(antecLen,
+ antecLen,
+ conc,
+ Inference::DEQ_DISL_STRINGS_SPLIT,
+ false,
+ true);
}
return;
Node conc = cc.size() == 1
? cc[0]
: NodeManager::currentNM()->mkNode(kind::AND, cc);
- d_im.sendInference(ant, conc, Inference::DEQ_NORM_EMP, true);
+ d_im.sendInference(ant, conc, Inference::DEQ_NORM_EMP, isRev, true);
return true;
}
{
Node eq = llt.eqNode(lc);
ei->d_normalizedLength.set(eq);
- d_im.sendInference(ant, eq, Inference::LEN_NORM, true);
+ d_im.sendInference(ant, eq, Inference::LEN_NORM, false, true);
}
}
}
namespace theory {
namespace strings {
-ExtfSolver::ExtfSolver(context::Context* c,
- context::UserContext* u,
- SolverState& s,
+ExtfSolver::ExtfSolver(SolverState& s,
InferenceManager& im,
TermRegistry& tr,
StringsRewriter& rewriter,
d_csolver(cs),
d_extt(et),
d_statistics(statistics),
- d_preproc(d_termReg.getSkolemCache(), u, statistics),
- d_hasExtf(c, false),
- d_extfInferCache(c),
- d_reduced(u)
+ d_preproc(d_termReg.getSkolemCache(), s.getUserContext(), statistics),
+ d_hasExtf(s.getSatContext(), false),
+ d_extfInferCache(s.getSatContext()),
+ d_reduced(s.getUserContext())
{
d_extt.addFunctionKind(kind::STRING_SUBSTR);
d_extt.addFunctionKind(kind::STRING_UPDATE);
lexp.push_back(lenx.eqNode(lens));
lexp.push_back(n.negate());
Node xneqs = x.eqNode(s).negate();
- d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true);
+ d_im.sendInference(
+ lexp, xneqs, Inference::CTN_NEG_EQUAL, false, true);
}
// this depends on the current assertions, so this
// inference is context-dependent
Node s = n[1];
// positive contains reduces to a equality
SkolemCache* skc = d_termReg.getSkolemCache();
- Node sk1 = skc->mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1");
- Node sk2 = skc->mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_POST, "sc2");
- Node eq = Rewriter::rewrite(x.eqNode(utils::mkNConcat(sk1, s, sk2)));
- std::vector<Node> exp_vec;
- exp_vec.push_back(n);
- d_im.sendInference(d_emptyVec, exp_vec, eq, Inference::CTN_POS, true);
+ Node eq = d_termReg.eagerReduce(n, skc);
+ Assert(!eq.isNull());
+ Assert(eq.getKind() == ITE && eq[0] == n);
+ eq = eq[1];
+ std::vector<Node> expn;
+ expn.push_back(n);
+ d_im.sendInference(expn, expn, eq, Inference::CTN_POS, false, true);
Trace("strings-extf-debug")
<< " resolve extf : " << n << " based on positive contain reduction."
<< std::endl;
std::vector<Node> new_nodes;
Node res = d_preproc.simplify(n, new_nodes);
Assert(res != n);
- new_nodes.push_back(res.eqNode(n));
+ new_nodes.push_back(n.eqNode(res));
Node nnlem =
new_nodes.size() == 1 ? new_nodes[0] : nm->mkNode(AND, new_nodes);
- nnlem = Rewriter::rewrite(nnlem);
Trace("strings-red-lemma")
<< "Reduction_" << effort << " lemma : " << nnlem << std::endl;
Trace("strings-red-lemma") << "...from " << n << std::endl;
- d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true);
+ d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, false, true);
Trace("strings-extf-debug")
<< " resolve extf : " << n << " based on reduction." << std::endl;
// add as reduction lemma
}
// If there is information involving the children, attempt to do an
// inference and/or mark n as reduced.
- Node to_reduce;
+ bool reduced = false;
+ Node to_reduce = n;
if (schanged)
{
Node sn = nm->mkNode(n.getKind(), schildren);
Trace("strings-extf")
<< " resolve extf : " << sn << " -> " << nrc << std::endl;
Inference inf = effort == 0 ? Inference::EXTF : Inference::EXTF_N;
- d_im.sendInference(einfo.d_exp, conc, inf, true);
+ d_im.sendInference(einfo.d_exp, conc, inf, false, true);
d_statistics.d_cdSimplifications << n.getKind();
if (d_state.isInConflict())
{
einfo.d_modelActive = false;
}
}
+ reduced = true;
}
else
{
effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N;
d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer);
}
- // We must use the original n here to avoid circular justifications for
- // why extended functions are reduced below. In particular, to_reduce
- // should never be a duplicate of another term considered in the block
- // of code for checkExtfInference below.
- to_reduce = n;
+ to_reduce = nrc;
}
}
- else
- {
- to_reduce = n;
- }
+ // We must use the original n here to avoid circular justifications for
+ // why extended functions are reduced. In particular, n should never be a
+ // duplicate of another term considered in the block of code for
+ // checkExtfInference below.
// if not reduced and not processed
- if (!to_reduce.isNull()
- && inferProcessed.find(to_reduce) == inferProcessed.end())
+ if (!reduced && !n.isNull()
+ && inferProcessed.find(n) == inferProcessed.end())
{
- inferProcessed.insert(to_reduce);
+ inferProcessed.insert(n);
Assert(effort < 3);
if (effort == 1)
{
Trace("strings-extf")
<< " cannot rewrite extf : " << to_reduce << std::endl;
}
+ // we take to_reduce to be the (partially) reduced version of n, which
+ // is justified by the explanation in einfo.
checkExtfInference(n, to_reduce, einfo, effort);
if (Trace.isOn("strings-extf-list"))
{
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
- ExtfSolver(context::Context* c,
- context::UserContext* u,
- SolverState& s,
+ ExtfSolver(SolverState& s,
InferenceManager& im,
TermRegistry& tr,
StringsRewriter& rewriter,
#include "theory/strings/infer_info.h"
+#include "theory/strings/theory_strings_utils.h"
+
namespace CVC4 {
namespace theory {
namespace strings {
case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL";
case Inference::CTN_POS: return "CTN_POS";
case Inference::REDUCTION: return "REDUCTION";
+ case Inference::PREFIX_CONFLICT: return "PREFIX_CONFLICT";
default: return "?";
}
}
bool InferInfo::isConflict() const
{
Assert(!d_conc.isNull());
- return d_conc.isConst() && !d_conc.getConst<bool>() && d_antn.empty();
+ return d_conc.isConst() && !d_conc.getConst<bool>() && d_noExplain.empty();
}
bool InferInfo::isFact() const
{
Assert(!d_conc.isNull());
TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc;
- return !atom.isConst() && atom.getKind() != kind::OR && d_antn.empty();
+ return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty();
+}
+
+Node InferInfo::getAntecedant() const
+{
+ // d_noExplain is a subset of d_ant
+ return utils::mkAnd(d_ant);
}
std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
{
out << " :ant (" << ii.d_ant << ")";
}
- if (!ii.d_antn.empty())
+ if (!ii.d_noExplain.empty())
{
- out << " :antn (" << ii.d_antn << ")";
+ out << " :no-explain (" << ii.d_noExplain << ")";
}
out << ")";
return out;
*/
enum class Inference : uint32_t
{
+ BEGIN,
//-------------------------------------- base solver
// initial normalize singular
// x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
// (see theory_strings_preprocess).
REDUCTION,
//-------------------------------------- end extended function solver
+ //-------------------------------------- prefix conflict
+ // prefix conflict (coarse-grained)
+ PREFIX_CONFLICT,
+ //-------------------------------------- end prefix conflict
NONE,
};
/**
* The "new literal" antecedant(s) of the inference, interpreted
* conjunctively. These are literals that were needed to show the conclusion
- * but do not currently hold in the equality engine.
+ * but do not currently hold in the equality engine. These should be a subset
+ * of d_ant. In other words, antecedants that are not explained are stored
+ * in *both* d_ant and d_noExplain.
*/
- std::vector<Node> d_antn;
+ std::vector<Node> d_noExplain;
/**
* A list of new skolems introduced as a result of this inference. They
* are mapped to by a length status, indicating the length constraint that
bool isTrivial() const;
/**
* Does this infer info correspond to a conflict? True if d_conc is false
- * and it has no new antecedants (d_antn).
+ * and it has no new antecedants (d_noExplain).
*/
bool isConflict() const;
/**
* Does this infer info correspond to a "fact". A fact is an inference whose
* conclusion should be added as an equality or predicate to the equality
- * engine with no new external antecedants (d_antn).
+ * engine with no new external antecedants (d_noExplain).
*/
bool isFact() const;
+ /** Get antecedant */
+ Node getAntecedant() const;
};
/**
}
void InferenceManager::sendInference(const std::vector<Node>& exp,
- const std::vector<Node>& expn,
+ const std::vector<Node>& noExplain,
Node eq,
Inference infer,
+ bool isRev,
bool asLemma)
{
eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
// wrap in infer info and send below
InferInfo ii;
ii.d_id = infer;
+ ii.d_idRev = isRev;
ii.d_conc = eq;
ii.d_ant = exp;
- ii.d_antn = expn;
+ ii.d_noExplain = noExplain;
sendInference(ii, asLemma);
}
void InferenceManager::sendInference(const std::vector<Node>& exp,
Node eq,
Inference infer,
+ bool isRev,
bool asLemma)
{
- std::vector<Node> expn;
- sendInference(exp, expn, eq, infer, asLemma);
+ std::vector<Node> noExplain;
+ sendInference(exp, noExplain, eq, infer, isRev, asLemma);
}
void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
InferInfo& ii = d_pending[i];
// At this point, ii should be a "fact", i.e. something whose conclusion
// should be added as a normal equality or predicate to the equality engine
- // with no new external assumptions (ii.d_antn).
+ // with no new external assumptions (ii.d_noExplain).
Assert(ii.isFact());
Node facts = ii.d_conc;
Node exp = utils::mkAnd(ii.d_ant);
Node eqExp;
if (options::stringRExplainLemmas())
{
- eqExp = mkExplain(ii.d_ant, ii.d_antn);
+ eqExp = mkExplain(ii.d_ant, ii.d_noExplain);
}
else
{
std::vector<Node> ev;
ev.insert(ev.end(), ii.d_ant.begin(), ii.d_ant.end());
- ev.insert(ev.end(), ii.d_antn.begin(), ii.d_antn.end());
eqExp = utils::mkAnd(ev);
}
// make the lemma node
Node InferenceManager::mkExplain(const std::vector<Node>& a) const
{
- std::vector<Node> an;
- return mkExplain(a, an);
+ std::vector<Node> noExplain;
+ return mkExplain(a, noExplain);
}
Node InferenceManager::mkExplain(const std::vector<Node>& a,
- const std::vector<Node>& an) const
+ const std::vector<Node>& noExplain) const
{
std::vector<TNode> antec_exp;
// copy to processing vector
eq::EqualityEngine* ee = d_state.getEqualityEngine();
for (const Node& apc : aconj)
{
+ if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end())
+ {
+ if (std::find(antec_exp.begin(), antec_exp.end(), apc) == antec_exp.end())
+ {
+ Debug("strings-explain")
+ << "Add to explanation (new literal) " << apc << std::endl;
+ antec_exp.push_back(apc);
+ }
+ continue;
+ }
Assert(apc.getKind() != AND);
Debug("strings-explain") << "Add to explanation " << apc << std::endl;
if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
// now, explain
explain(apc, antec_exp);
}
- for (const Node& anc : an)
- {
- if (std::find(antec_exp.begin(), antec_exp.end(), anc) == antec_exp.end())
- {
- Debug("strings-explain")
- << "Add to explanation (new literal) " << anc << std::endl;
- antec_exp.push_back(anc);
- }
- }
Node ant;
if (antec_exp.empty())
{
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
+ * This function should be called when exp => eq. The set exp
* contains literals that are explainable, i.e. those that hold in the
* equality engine of the theory of strings. On the other hand, the set
- * exp_n ("explanations new") contain nodes that are not explainable by the
- * theory of strings. This method may call sendLemma or otherwise add a
- * InferInfo to d_pending, indicating a fact should be asserted to the
- * equality engine. Overall, the result of this method is one of the
- * following:
+ * noExplain contains nodes that are not explainable by the theory of strings.
+ * This method may call sendLemma or otherwise add a InferInfo to d_pending,
+ * indicating a fact should be asserted to the equality engine. Overall, the
+ * result of this method is one of the following:
*
- * [1] (No-op) Do nothing if eq is true,
+ * [1] (No-op) Do nothing if eq is equivalent to true,
*
* [2] (Infer) Indicate that eq should be added to the equality engine of this
* class with explanation exp, where exp is a set of literals that currently
* hold in the equality engine. We add this to the pending vector d_pending.
*
- * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should
- * be sent on the output channel of the theory of strings, where EXPLAIN
- * returns the explanation of the node in exp in terms of the literals
+ * [3] (Lemma) Indicate that the lemma
+ * ( EXPLAIN(exp \ noExplain) ^ noExplain ) => eq
+ * should be sent on the output channel of the theory of strings, where
+ * EXPLAIN returns the explanation of the node in exp in terms of the literals
* asserted to the theory of strings, as computed by the equality engine.
* This is also added to a pending vector, d_pendingLem.
*
* channel of the theory of strings.
*
* Determining which case to apply depends on the form of eq and whether
- * 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.
+ * noExplain is empty. In particular, lemmas must be used whenever noExplain
+ * is non-empty, conflicts are used when noExplain is empty and eq is false.
*
- * The argument infer identifies the reason for inference, used for
+ * @param exp The explanation of eq.
+ * @param noExplain The subset of exp that cannot be explained by the
+ * equality engine. This may impact whether we are processing this call as a
+ * fact or as a lemma.
+ * @param eq The conclusion.
+ * @param 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
+ * @param isRev Whether this is the "reverse variant" of the inference, which
+ * is used as a hint for proof reconstruction.
+ * @param asLemma If true, then this method will send a lemma instead
* of a fact whenever applicable.
*/
void sendInference(const std::vector<Node>& exp,
- const std::vector<Node>& exp_n,
+ const std::vector<Node>& noExplain,
Node eq,
Inference infer,
+ bool isRev = false,
bool asLemma = false);
- /** same as above, but where exp_n is empty */
+ /** same as above, but where noExplain is empty */
void sendInference(const std::vector<Node>& exp,
Node eq,
Inference infer,
+ bool isRev = false,
bool asLemma = false);
/** Send inference
* that have been asserted to the equality engine.
*/
Node mkExplain(const std::vector<Node>& a) const;
- /** Same as above, but the new literals an are append to the result */
- Node mkExplain(const std::vector<Node>& a, const std::vector<Node>& an) const;
+ /** Same as above, but with a subset noExplain that should not be explained */
+ Node mkExplain(const std::vector<Node>& a,
+ const std::vector<Node>& noExplain) const;
/**
* Explain literal l, add conjuncts to assumptions vector instead of making
* the node corresponding to their conjunction.
else
{
// we have a conflict
- std::vector<Node> exp_n;
- exp_n.push_back(assertion);
+ std::vector<Node> iexp = nfexp;
+ std::vector<Node> noExplain;
+ iexp.push_back(assertion);
+ noExplain.push_back(assertion);
Node conc = Node::null();
- d_im.sendInference(nfexp, exp_n, conc, Inference::RE_NF_CONFLICT);
+ d_im.sendInference(
+ iexp, noExplain, conc, Inference::RE_NF_CONFLICT);
addedLemma = true;
break;
}
// if simplifying successfully generated a lemma
if (!conc.isNull())
{
- std::vector<Node> exp_n;
- exp_n.push_back(assertion);
+ std::vector<Node> iexp = rnfexp;
+ std::vector<Node> noExplain;
+ iexp.push_back(assertion);
+ noExplain.push_back(assertion);
Assert(atom.getKind() == STRING_IN_REGEXP);
if (polarity)
{
}
Inference inf =
polarity ? Inference::RE_UNFOLD_POS : Inference::RE_UNFOLD_NEG;
- d_im.sendInference(rnfexp, exp_n, conc, inf);
+ d_im.sendInference(iexp, noExplain, conc, inf);
addedLemma = true;
if (changed)
{
Node conc;
d_im.sendInference(
- vec_nodes, conc, Inference::RE_INTER_INCLUDE, true);
+ vec_nodes, conc, Inference::RE_INTER_INCLUDE, false, true);
return false;
}
}
vec_nodes.push_back(mi[0].eqNode(m[0]));
}
Node conc;
- d_im.sendInference(vec_nodes, conc, Inference::RE_INTER_CONF, true);
+ d_im.sendInference(
+ vec_nodes, conc, Inference::RE_INTER_CONF, false, true);
// conflict, return
return false;
}
// rewrite to ensure the equality checks below are precise
- Node mres = Rewriter::rewrite(nm->mkNode(STRING_IN_REGEXP, mi[0], resR));
- if (mres == mi)
+ Node mres = nm->mkNode(STRING_IN_REGEXP, mi[0], resR);
+ Node mresr = Rewriter::rewrite(mres);
+ if (mresr == mi)
{
// if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent
// to x in R1, hence x in R2 can be marked redundant.
d_im.markReduced(m);
}
- else if (mres == m)
+ else if (mresr == m)
{
// same as above, opposite direction
d_im.markReduced(mi);
{
vec_nodes.push_back(mi[0].eqNode(m[0]));
}
- d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true);
+ d_im.sendInference(
+ vec_nodes, mres, Inference::RE_INTER_INFER, false, true);
// both are reduced
d_im.markReduced(m);
d_im.markReduced(mi);
{
case 0:
{
- std::vector<Node> exp_n;
- exp_n.push_back(atom);
- exp_n.push_back(x.eqNode(d_emptyString));
- d_im.sendInference(nf_exp, exp_n, exp, Inference::RE_DELTA);
+ std::vector<Node> noExplain;
+ noExplain.push_back(atom);
+ noExplain.push_back(x.eqNode(d_emptyString));
+ std::vector<Node> iexp = nf_exp;
+ iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
+ d_im.sendInference(iexp, noExplain, exp, Inference::RE_DELTA);
addedLemma = true;
d_regexp_ccached.insert(atom);
return false;
}
case 2:
{
- std::vector<Node> exp_n;
- exp_n.push_back(atom);
- exp_n.push_back(x.eqNode(d_emptyString));
- Node conc;
- d_im.sendInference(nf_exp, exp_n, conc, Inference::RE_DELTA_CONF);
+ std::vector<Node> noExplain;
+ noExplain.push_back(atom);
+ noExplain.push_back(x.eqNode(d_emptyString));
+ std::vector<Node> iexp = nf_exp;
+ iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
+ d_im.sendInference(iexp, noExplain, d_false, Inference::RE_DELTA_CONF);
addedLemma = true;
d_regexp_ccached.insert(atom);
return false;
conc = NodeManager::currentNM()->mkNode(STRING_IN_REGEXP, left, dc);
}
}
- std::vector<Node> exp_n;
- exp_n.push_back(atom);
- d_im.sendInference(ant, exp_n, conc, Inference::RE_DERIVE);
+ std::vector<Node> iexp = ant;
+ std::vector<Node> noExplain;
+ noExplain.push_back(atom);
+ iexp.push_back(atom);
+ d_im.sendInference(iexp, noExplain, conc, Inference::RE_DERIVE);
return true;
}
return false;
d_rewriter(&d_statistics.d_rewrites),
d_bsolver(d_state, d_im),
d_csolver(d_state, d_im, d_termReg, d_bsolver),
- d_esolver(c,
- u,
- d_state,
+ d_esolver(d_state,
d_im,
d_termReg,
d_rewriter,
d_csolver,
d_extTheory,
d_statistics),
- d_rsolver(d_state, d_im, d_termReg.getSkolemCache(),
- d_csolver, d_esolver, d_statistics),
+ d_rsolver(d_state,
+ d_im,
+ d_termReg.getSkolemCache(),
+ d_csolver,
+ d_esolver,
+ d_statistics),
d_stringsFmf(c, u, valuation, d_termReg)
{
bool eagerEval = options::stringEagerEval();
projects / cvc5.git / commitdiff