Introduce enum values for all calls to sendInference outside of the core solver.
This included some minor refactoring.
}
}
// infer the equality
- d_im.sendInference(exp, n.eqNode(nc), "I_Norm");
+ d_im.sendInference(exp, n.eqNode(nc), Inference::I_NORM);
}
else
{
}
AlwaysAssert(foundNEmpty);
// infer the equality
- d_im.sendInference(exp, n.eqNode(ns), "I_Norm_S");
+ d_im.sendInference(exp, n.eqNode(ns), Inference::I_NORM_S);
}
d_congruent.insert(n);
congruent[k]++;
Assert(countc == vecc.size());
if (d_state.hasTerm(c))
{
- d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE");
+ d_im.sendInference(exp, n.eqNode(c), Inference::I_CONST_MERGE);
return;
}
else if (!d_im.hasProcessed())
exp.push_back(d_eqcToConstExp[nr]);
d_im.addToExplanation(n, d_eqcToConstBase[nr], exp);
}
- d_im.sendInference(exp, d_false, "I_CONST_CONFLICT");
+ d_im.sendInference(exp, d_false, Inference::I_CONST_CONFLICT);
return;
}
else
if (!cons.isConst() || !cons.getConst<bool>())
{
std::vector<Node> emptyVec;
- d_im.sendInference(emptyVec, vec_node, cons, "CARDINALITY", true);
+ d_im.sendInference(
+ emptyVec, vec_node, cons, Inference::CARDINALITY, true);
return;
}
}
d_bsolver(bs),
d_csolver(cs),
d_extt(et),
+ d_statistics(stats),
d_preproc(&skc, u, stats),
d_hasExtf(c, false),
d_extfInferCache(c)
lexp.push_back(lenx.eqNode(lens));
lexp.push_back(n.negate());
Node xneqs = x.eqNode(s).negate();
- d_im.sendInference(lexp, xneqs, "NEG-CTN-EQL", true);
+ d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true);
}
// this depends on the current assertions, so we set that this
// inference is context-dependent.
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, "POS-CTN", true);
+ d_im.sendInference(d_emptyVec, exp_vec, eq, Inference::CTN_POS, true);
Trace("strings-extf-debug")
<< " resolve extf : " << n << " based on positive contain reduction."
<< std::endl;
Trace("strings-red-lemma")
<< "Reduction_" << effort << " lemma : " << nnlem << std::endl;
Trace("strings-red-lemma") << "...from " << n << std::endl;
- d_im.sendInference(d_emptyVec, nnlem, "Reduction", true);
+ d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true);
Trace("strings-extf-debug")
<< " resolve extf : " << n << " based on reduction." << std::endl;
isCd = false;
{
Trace("strings-extf")
<< " resolve extf : " << sn << " -> " << nrc << std::endl;
- d_im.sendInference(
- einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true);
+ Inference inf = effort == 0 ? Inference::EXTF : Inference::EXTF_N;
+ d_im.sendInference(einfo.d_exp, conc, inf, true);
+ d_statistics.d_cdSimplifications << n.getKind();
if (d_state.isInConflict())
{
Trace("strings-extf-debug") << " conflict, return." << std::endl;
if (d_state.areEqual(conc, d_false))
{
// we are in conflict
- d_im.sendInference(in.d_exp, conc, "CTN_Decompose");
+ d_im.sendInference(in.d_exp, conc, Inference::CTN_DECOMPOSE);
}
else if (d_extt->hasFunctionKind(conc.getKind()))
{
exp_c.insert(exp_c.end(),
d_extfInfoTmp[ofrom].d_exp.begin(),
d_extfInfoTmp[ofrom].d_exp.end());
- d_im.sendInference(exp_c, conc, "CTN_Trans");
+ d_im.sendInference(exp_c, conc, Inference::CTN_TRANS);
}
}
}
CoreSolver& d_csolver;
/** the extended theory object for the theory of strings */
ExtTheory* d_extt;
+ /** Reference to the statistics for the theory of strings/sequences. */
+ SequencesStatistics& d_statistics;
/** preprocessing utility, for performing strings reductions */
StringsPreprocess d_preproc;
/** Common constants */
{
switch (i)
{
+ case Inference::I_NORM_S: return "I_NORM_S";
+ 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::CARDINALITY: return "CARDINALITY";
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::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_INTER_INCLUDE: return "RE_INTER_INCLUDE";
+ case Inference::RE_INTER_CONF: return "RE_INTER_CONF";
+ case Inference::RE_INTER_INFER: return "RE_INTER_INFER";
+ case Inference::RE_DELTA: return "RE_DELTA";
+ case Inference::RE_DELTA_CONF: return "RE_DELTA_CONF";
+ case Inference::RE_DERIVE: return "RE_DERIVE";
+ case Inference::EXTF: return "EXTF";
+ case Inference::EXTF_N: return "EXTF_N";
+ case Inference::CTN_TRANS: return "CTN_TRANS";
+ case Inference::CTN_DECOMPOSE: return "CTN_DECOMPOSE";
+ case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL";
+ case Inference::CTN_POS: return "CTN_POS";
+ case Inference::REDUCTION: return "REDUCTION";
default: return "?";
}
}
*/
enum class Inference : uint32_t
{
+ //-------------------------------------- base solver
+ // initial normalize singular
+ // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
+ // x1 ++ ... ++ xn = xi
+ I_NORM_S,
+ // initial constant merge
+ // explain_constant(x, c) => x = c
+ // Above, explain_constant(x,c) is a basic explanation of why x must be equal
+ // to string constant c, which is computed by taking arguments of
+ // concatentation terms that are entailed to be constants. For example:
+ // ( y = "AB" ^ z = "C" ) => y ++ z = "ABC"
+ I_CONST_MERGE,
+ // initial constant conflict
+ // ( explain_constant(x, c1) ^ explain_constant(x, c2) ^ x = y) => false
+ // where c1 != c2.
+ I_CONST_CONFLICT,
+ // initial normalize
+ // Given two concatenation terms, this is applied when we find that they are
+ // equal after e.g. removing strings that are currently empty. For example:
+ // y = "" ^ z = "" => x ++ y = z ++ x
+ I_NORM,
+ // The cardinality inference for strings, see Liang et al CAV 2014.
+ CARDINALITY,
+ //-------------------------------------- end base solver
+ //-------------------------------------- core solver
// 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,
+ //-------------------------------------- end core solver
+ //-------------------------------------- regexp solver
+ // regular expression normal form conflict
+ // ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
+ // where y is the normal form computed for x.
+ RE_NF_CONFLICT,
+ // regular expression unfolding
+ // This is a general class of inferences of the form:
+ // (x in R) => F
+ // where F is formula expressing the next step of checking whether x is in
+ // R. For example:
+ // (x in (R)*) =>
+ // x = "" V x in R V ( x = x1 ++ x2 ++ x3 ^ x1 in R ^ x2 in (R)* ^ x3 in R)
+ RE_UNFOLD_POS,
+ // Same as above, for negative memberships
+ RE_UNFOLD_NEG,
+ // intersection inclusion conflict
+ // (x in R1 ^ ~ x in R2) => false where [[includes(R2,R1)]]
+ // Where includes(R2,R1) is a heuristic check for whether R2 includes R1.
+ RE_INTER_INCLUDE,
+ // intersection conflict, using regexp intersection computation
+ // (x in R1 ^ x in R2) => false where [[intersect(R1, R2) = empty]]
+ RE_INTER_CONF,
+ // intersection inference
+ // (x in R1 ^ y in R2 ^ x = y) => (x in re.inter(R1,R2))
+ RE_INTER_INFER,
+ // regular expression delta
+ // (x = "" ^ x in R) => C
+ // where "" in R holds if and only if C holds.
+ RE_DELTA,
+ // regular expression delta conflict
+ // (x = "" ^ x in R) => false
+ // where R does not accept the empty string.
+ RE_DELTA_CONF,
+ // regular expression derive ???
+ 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
+ // 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,
+ // contain transitive
+ // ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ).
+ CTN_TRANS,
+ // contain decompose
+ // str.contains( x, str.++( y1, ..., yn ) ) => str.contains( x, yi ) or
+ // ~str.contains( str.++( x1, ..., xn ), y ) => ~str.contains( xi, y )
+ CTN_DECOMPOSE,
+ // contain neg equal
+ // ( len( x ) = len( s ) ^ ~contains( x, s ) ) => x != s
+ CTN_NEG_EQUAL,
+ // contain positive
+ // str.contains( x, y ) => x = w1 ++ y ++ w2
+ // where w1 and w2 are skolem variables.
+ CTN_POS,
+ // All reduction inferences of the form:
+ // f(x1, .., xn) = y ^ P(x1, ..., xn, y)
+ // where f is an extended function, y is the purification variable for
+ // f(x1, .., xn) and P is the reduction predicate for f
+ // (see theory_strings_preprocess).
+ REDUCTION,
+ //-------------------------------------- end extended function solver
NONE,
};
void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes, bool polarity) {
Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t << ", polarity=" << polarity << std::endl;
Assert(t.getKind() == kind::STRING_IN_REGEXP);
- Node str = Rewriter::rewrite(t[0]);
- Node re = Rewriter::rewrite(t[1]);
+ Node str = t[0];
+ Node re = t[1];
if(polarity) {
simplifyPRegExp( str, re, new_nodes );
} else {
SolverState& s,
InferenceManager& im,
ExtfSolver& es,
+ SequencesStatistics& stats,
context::Context* c,
context::UserContext* u)
: d_parent(p),
d_state(s),
d_im(im),
d_esolver(es),
+ d_statistics(stats),
d_regexp_ucached(u),
d_regexp_ccached(c),
d_processed_memberships(c)
<< "We have regular expression assertion : " << assertion
<< std::endl;
Node atom = assertion.getKind() == NOT ? assertion[0] : assertion;
+ Assert(atom == Rewriter::rewrite(atom));
bool polarity = assertion.getKind() != NOT;
if (polarity != (e == 0))
{
std::vector<Node> exp_n;
exp_n.push_back(assertion);
Node conc = Node::null();
- d_im.sendInference(nfexp, exp_n, conc, "REGEXP NF Conflict");
+ d_im.sendInference(nfexp, exp_n, conc, Inference::RE_NF_CONFLICT);
addedLemma = true;
break;
}
std::vector<Node> exp_n;
exp_n.push_back(assertion);
Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec);
- d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
+ Assert(atom.getKind() == STRING_IN_REGEXP);
+ if (polarity)
+ {
+ d_statistics.d_regexpUnfoldingsPos << atom[1].getKind();
+ }
+ else
+ {
+ d_statistics.d_regexpUnfoldingsNeg << atom[1].getKind();
+ }
+ Inference inf =
+ polarity ? Inference::RE_UNFOLD_POS : Inference::RE_UNFOLD_NEG;
+ d_im.sendInference(rnfexp, exp_n, conc, inf);
addedLemma = true;
if (changed)
{
}
Node conc;
- d_im.sendInference(vec_nodes, conc, "Intersect inclusion", true);
+ d_im.sendInference(
+ vec_nodes, conc, Inference::RE_INTER_INCLUDE, true);
return false;
}
}
vec_nodes.push_back(mi[0].eqNode(m[0]));
}
Node conc;
- d_im.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
+ d_im.sendInference(vec_nodes, conc, Inference::RE_INTER_CONF, true);
// conflict, return
return false;
}
else
{
// new conclusion
- // (x in R ^ y in R2 ^ x = y) => (x in intersect(R1,R2))
+ // (x in R1 ^ y in R2 ^ x = y) => (x in intersect(R1,R2))
std::vector<Node> vec_nodes;
vec_nodes.push_back(mi);
vec_nodes.push_back(m);
{
vec_nodes.push_back(mi[0].eqNode(m[0]));
}
- d_im.sendInference(vec_nodes, mres, "INTERSECT INFER", true);
+ d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true);
// both are reduced
d_parent.getExtTheory()->markReduced(m);
d_parent.getExtTheory()->markReduced(mi);
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, "RegExp Delta");
+ d_im.sendInference(nf_exp, exp_n, exp, Inference::RE_DELTA);
addedLemma = true;
d_regexp_ccached.insert(atom);
return false;
exp_n.push_back(atom);
exp_n.push_back(x.eqNode(d_emptyString));
Node conc;
- d_im.sendInference(nf_exp, exp_n, conc, "RegExp Delta CONFLICT");
+ d_im.sendInference(nf_exp, exp_n, conc, Inference::RE_DELTA_CONF);
addedLemma = true;
d_regexp_ccached.insert(atom);
return false;
}
std::vector<Node> exp_n;
exp_n.push_back(atom);
- d_im.sendInference(ant, exp_n, conc, "RegExp-Derive");
+ d_im.sendInference(ant, exp_n, conc, Inference::RE_DERIVE);
return true;
}
return false;
#include "theory/strings/extf_solver.h"
#include "theory/strings/inference_manager.h"
#include "theory/strings/regexp_operation.h"
+#include "theory/strings/sequences_stats.h"
#include "theory/strings/solver_state.h"
#include "util/string.h"
SolverState& s,
InferenceManager& im,
ExtfSolver& es,
+ SequencesStatistics& stats,
context::Context* c,
context::UserContext* u);
~RegExpSolver() {}
InferenceManager& d_im;
/** reference to the extended function solver of the parent */
ExtfSolver& d_esolver;
+ /** Reference to the statistics for the theory of strings/sequences. */
+ SequencesStatistics& d_statistics;
// check membership constraints
Node mkAnd(Node c1, Node c2);
/**
SequencesStatistics::SequencesStatistics()
: d_inferences("theory::strings::inferences"),
+ d_cdSimplifications("theory::strings::cdSimplifications"),
d_reductions("theory::strings::reductions"),
+ d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"),
+ d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"),
d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0),
d_conflictsInfer("theory::strings::conflictsInfer", 0),
d_lemmasInfer("theory::strings::lemmasInfer", 0)
{
smtStatisticsRegistry()->registerStat(&d_inferences);
+ smtStatisticsRegistry()->registerStat(&d_cdSimplifications);
smtStatisticsRegistry()->registerStat(&d_reductions);
+ smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsPos);
+ smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg);
smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix);
smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
SequencesStatistics::~SequencesStatistics()
{
smtStatisticsRegistry()->unregisterStat(&d_inferences);
+ smtStatisticsRegistry()->unregisterStat(&d_cdSimplifications);
smtStatisticsRegistry()->unregisterStat(&d_reductions);
+ smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsPos);
+ smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg);
smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix);
smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
namespace theory {
namespace strings {
+/**
+ * Statistics for the theory of strings.
+ *
+ * This is roughly broken up into the following parts:
+ * (1) Inferences,
+ * (2) Conflicts,
+ * (3) Lemmas.
+ *
+ * "Inferences" (1) are steps invoked during solving, which either trigger:
+ * (a) An internal update to the state of the solver (e.g. adding an inferred
+ * equality to the equality engine),
+ * (b) A call to OutputChannel::conflict,
+ * (c) A call to OutputChannel::lemma.
+ * For details, see InferenceManager. We track stats on each kind of
+ * inference that have been indicated by the solvers in TheoryStrings.
+ * Some kinds of inferences are further distinguished by the Kind of the node
+ * they operate on (see d_cdSimplifications, d_reductions, d_regexpUnfoldings).
+ *
+ * "Conflicts" (2) arise from various kinds of reasoning, listed below,
+ * where inferences are one of the possible methods for deriving conflicts.
+ *
+ * "Lemmas" (3) also arise from various kinds of reasoning, listed below,
+ * where inferences are one of the possible methods for deriving lemmas.
+ */
class SequencesStatistics
{
public:
SequencesStatistics();
~SequencesStatistics();
-
+ //--------------- inferences
/** Counts the number of applications of each type of inference */
HistogramStat<Inference> d_inferences;
- /** Counts the number of applications of each type of reduction */
+ /**
+ * Counts the number of applications of each type of context-dependent
+ * simplification. The sum of this map is equal to the number of EXTF or
+ * EXTF_N inferences.
+ */
+ HistogramStat<Kind> d_cdSimplifications;
+ /**
+ * Counts the number of applications of each type of reduction. The sum of
+ * this map is equal to the number of REDUCTION inferences (when
+ * options::stringLazyPreproc is true).
+ */
HistogramStat<Kind> d_reductions;
+ /**
+ * Counts the number of applications of each type of regular expression
+ * positive (resp. negative) unfoldings. The sum of this map is equal to the
+ * number of RE_UNFOLD_POS (resp. RE_UNFOLD_NEG) inferences.
+ */
+ HistogramStat<Kind> d_regexpUnfoldingsPos;
+ HistogramStat<Kind> d_regexpUnfoldingsNeg;
+ //--------------- end of inferences
//--------------- conflicts, partition of calls to OutputChannel::conflict
/** Number of equality engine conflicts */
IntStat d_conflictsEqEngine;
d_csolver,
extt,
d_statistics));
- d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u));
+ d_rsolver.reset(
+ new RegExpSolver(*this, d_state, d_im, *d_esolver, d_statistics, c, u));
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
projects / cvc5.git / commitdiff