This PR adds comprehensive stats for reductions, lemmas and conflicts in TheoryStrings. Remaining stats will track all inferences (which are finer grained steps that may lead to lemmas/conflicts).
Additionally this PR refactors calls to OutputChannel::lemma in TheoryStrings / InferenceManager. There are now only 2 calls to lemma(...) during registerTerm(...), one for "atomic" string terms (corresponding to length splits typically) and one for non-atomic terms.
// right
Node sk_w = d_skCache.mkSkolem("w_loop");
Node sk_y = d_skCache.mkSkolem("y_loop");
- d_im.registerLength(sk_y, LENGTH_GEQ_ONE);
+ d_im.registerTermAtomic(sk_y, LENGTH_GEQ_ONE);
Node sk_z = d_skCache.mkSkolem("z_loop");
// t1 * ... * tn = y * z
Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z));
{
Node sk = d_skCache.mkSkolemCached(
nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt");
- d_im.registerLength(sk, LENGTH_ONE);
+ d_im.registerTermAtomic(sk, LENGTH_ONE);
Node skr =
d_skCache.mkSkolemCached(nconst_k,
SkolemCache::SK_ID_DC_SPT_REM,
i, j, SkolemCache::SK_ID_DEQ_Y, "y_dsplit");
Node sk3 = d_skCache.mkSkolemCached(
i, j, SkolemCache::SK_ID_DEQ_Z, "z_dsplit");
- d_im.registerLength(sk3, LENGTH_GEQ_ONE);
+ d_im.registerTermAtomic(sk3, LENGTH_GEQ_ONE);
Node lsk1 = utils::mkNLength(sk1);
conc.push_back( lsk1.eqNode( li ) );
Node lsk2 = utils::mkNLength(sk2);
{
for (const Node& n : sks.second)
{
- d_im.registerLength(n, sks.first);
+ d_im.registerTermAtomic(n, sks.first);
}
}
}
SkolemCache& skc,
BaseSolver& bs,
CoreSolver& cs,
- ExtTheory* et)
+ ExtTheory* et,
+ SequencesStatistics& stats)
: d_state(s),
d_im(im),
d_skCache(skc),
d_bsolver(bs),
d_csolver(cs),
d_extt(et),
- d_preproc(&skc, u),
+ d_preproc(&skc, u, stats),
d_hasExtf(c, false),
d_extfInferCache(c)
{
#include "theory/strings/base_solver.h"
#include "theory/strings/core_solver.h"
#include "theory/strings/inference_manager.h"
+#include "theory/strings/sequences_stats.h"
#include "theory/strings/skolem_cache.h"
#include "theory/strings/solver_state.h"
#include "theory/strings/theory_strings_preprocess.h"
SkolemCache& skc,
BaseSolver& bs,
CoreSolver& cs,
- ExtTheory* et);
+ ExtTheory* et,
+ SequencesStatistics& stats);
~ExtfSolver();
/** check extended functions evaluation
<< std::endl;
Trace("strings-assert")
<< "(assert (not " << ant << ")) ; conflict " << c << std::endl;
+ ++(d_statistics.d_conflictsInfer);
d_out.conflict(ant);
d_state.setConflict();
return;
return NodeManager::currentNM()->mkNode(n.getKind(), children);
}
-void InferenceManager::registerLength(Node n)
+Node InferenceManager::registerTerm(Node n)
{
Assert(n.getType().isStringLike());
NodeManager* nm = NodeManager::currentNM();
// can register length term if it does not rewrite
if (lsum == lsumb)
{
- registerLength(n, LENGTH_SPLIT);
- return;
+ registerTermAtomic(n, LENGTH_SPLIT);
+ return Node::null();
}
}
Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
StringsProxyVarAttribute spva;
sk.setAttribute(spva, true);
Node eq = Rewriter::rewrite(sk.eqNode(n));
- Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
d_proxyVar[n] = sk;
// If we are introducing a proxy for a constant or concat term, we do not
// need to send lemmas about its length, since its length is already
if (n.isConst() || n.getKind() == STRING_CONCAT)
{
// do not send length lemma for sk.
- registerLength(sk, LENGTH_IGNORE);
+ registerTermAtomic(sk, LENGTH_IGNORE);
}
- Trace("strings-assert") << "(assert " << eq << ")" << std::endl;
- d_out.lemma(eq);
Node skl = nm->mkNode(STRING_LENGTH, sk);
if (n.getKind() == STRING_CONCAT)
{
Assert(!lsum.isNull());
d_proxyVarToLength[sk] = lsum;
Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
- Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
- Trace("strings-lemma-debug")
- << " prerewrite : " << skl.eqNode(lsum) << std::endl;
- Trace("strings-assert") << "(assert " << ceq << ")" << std::endl;
- d_out.lemma(ceq);
+
+ return nm->mkNode(AND, eq, ceq);
}
-void InferenceManager::registerLength(Node n, LengthStatus s)
+void InferenceManager::registerTermAtomic(Node n, LengthStatus s)
{
if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
{
// ignore it
return;
}
+ std::map<Node, bool> reqPhase;
+ Node lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
+ if (!lenLem.isNull())
+ {
+ Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
+ << std::endl;
+ Trace("strings-assert") << "(assert " << lenLem << ")" << std::endl;
+ ++(d_statistics.d_lemmasRegisterTermAtomic);
+ d_out.lemma(lenLem);
+ }
+ for (const std::pair<const Node, bool>& rp : reqPhase)
+ {
+ d_out.requirePhase(rp.first, rp.second);
+ }
+}
+Node InferenceManager::getRegisterTermAtomicLemma(
+ Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
+{
NodeManager* nm = NodeManager::currentNM();
Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
<< std::endl;
Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
- d_out.lemma(len_geq_one);
- return;
+ return len_geq_one;
}
if (s == LENGTH_ONE)
Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
<< std::endl;
Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
- d_out.lemma(len_one);
- return;
+ return len_one;
}
Assert(s == LENGTH_SPLIT);
+ std::vector<Node> lems;
if (options::stringSplitEmp() || !options::stringLenGeqZ())
{
Node n_len_eq_z = n_len.eqNode(d_zero);
if (!case_empty.isConst())
{
Node lem = nm->mkNode(OR, case_empty, case_nempty);
- d_out.lemma(lem);
+ lems.push_back(lem);
Trace("strings-lemma")
<< "Strings::Lemma LENGTH >= 0 : " << lem << std::endl;
// prefer trying the empty case first
// occur in the CNF stream.
n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
Assert(!n_len_eq_z.isConst());
- d_out.requirePhase(n_len_eq_z, true);
+ reqPhase[n_len_eq_z] = true;
n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
Assert(!n_len_eq_z_2.isConst());
- d_out.requirePhase(n_len_eq_z_2, true);
+ reqPhase[n_len_eq_z_2] = true;
}
else if (!case_empty.getConst<bool>())
{
Trace("strings-lemma")
<< "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty
<< std::endl;
- d_out.lemma(case_nempty);
+ lems.push_back(case_nempty);
}
else
{
{
Node n_len_geq = nm->mkNode(kind::GEQ, n_len, d_zero);
n_len_geq = Rewriter::rewrite(n_len_geq);
- d_out.lemma(n_len_geq);
+ lems.push_back(n_len_geq);
+ }
+
+ if (lems.empty())
+ {
+ return Node::null();
}
+ return lems.size() == 1 ? lems[0] : nm->mkNode(AND, lems);
}
void InferenceManager::addToExplanation(Node a,
* exists, otherwise it returns null.
*/
Node getProxyVariableFor(Node n) const;
- /** register length
+ /** register term
+ *
+ * This method is called on non-constant string terms n. It returns a lemma
+ * that should be sent on the output channel of theory of strings upon
+ * registration of this term, or null if no lemma is necessary.
*
- * This method is called on non-constant string terms n. It sends a lemma
- * on the output channel that ensures that the length n satisfies its assigned
- * status (given by argument s).
+ * If n is an atomic term, the method registerTermAtomic is called for n
+ * and s = LENGTH_SPLIT and no lemma is returned.
*/
- void registerLength(Node n);
+ Node registerTerm(Node n);
/** register length
*
- * This method is called on non-constant string terms n. It sends a lemma
- * on the output channel that ensures that the length n satisfies its assigned
- * status (given by argument s).
+ * This method is called on non-constant string terms n that are "atomic"
+ * with respect to length. That is, the rewritten form of len(n) is itself.
+ *
+ * It sends a lemma on the output channel that ensures that the length n
+ * satisfies its assigned status (given by argument s).
*
* If the status is LENGTH_ONE, we send the lemma len( n ) = 1.
*
* In contrast to the above functions, it makes immediate calls to the output
* channel instead of adding them to pending lists.
*/
- void registerLength(Node n, LengthStatus s);
+ void registerTermAtomic(Node n, LengthStatus s);
//---------------------------- end proxy variables and length elaboration
//----------------------------constructing antecedants
* equality engine of this class.
*/
void sendInfer(Node eq_exp, Node eq, const char* c);
+ /**
+ * Get the lemma required for registering the length information for
+ * atomic term n given length status s. For details, see registerTermAtomic.
+ *
+ * Additionally, this method may map literals to a required polarity in the
+ * argument reqPhase, which should be processed by a call to requiredPhase by
+ * the caller of this method.
+ */
+ Node getRegisterTermAtomicLemma(Node n,
+ LengthStatus s,
+ std::map<Node, bool>& reqPhase);
/** the parent theory of strings object */
TheoryStrings& d_parent;
namespace strings {
SequencesStatistics::SequencesStatistics()
- : d_inferences("theory::strings::inferences")
+ : d_inferences("theory::strings::inferences"),
+ d_reductions("theory::strings::reductions"),
+ d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
+ d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0),
+ d_conflictsInfer("theory::strings::conflictsInfer", 0),
+ d_lemmasEagerPreproc("theory::strings::lemmasEagerPreproc", 0),
+ d_lemmasCmiSplit("theory::strings::lemmasCmiSplit", 0),
+ d_lemmasRegisterTerm("theory::strings::lemmasRegisterTerm", 0),
+ d_lemmasRegisterTermAtomic("theory::strings::lemmasRegisterTermAtomic",
+ 0),
+ d_lemmasInfer("theory::strings::lemmasInfer", 0)
{
smtStatisticsRegistry()->registerStat(&d_inferences);
+ smtStatisticsRegistry()->registerStat(&d_reductions);
+ smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
+ smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix);
+ smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
+ smtStatisticsRegistry()->registerStat(&d_lemmasEagerPreproc);
+ smtStatisticsRegistry()->registerStat(&d_lemmasCmiSplit);
+ smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTerm);
+ smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTermAtomic);
+ smtStatisticsRegistry()->registerStat(&d_lemmasInfer);
}
SequencesStatistics::~SequencesStatistics()
{
smtStatisticsRegistry()->unregisterStat(&d_inferences);
+ smtStatisticsRegistry()->unregisterStat(&d_reductions);
+ smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
+ smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix);
+ smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
+ smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc);
+ smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit);
+ smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTerm);
+ smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTermAtomic);
+ smtStatisticsRegistry()->unregisterStat(&d_lemmasInfer);
}
}
#ifndef CVC4__THEORY__STRINGS__SEQUENCES_STATS_H
#define CVC4__THEORY__STRINGS__SEQUENCES_STATS_H
+#include "expr/kind.h"
#include "theory/strings/infer_info.h"
#include "util/statistics_registry.h"
SequencesStatistics();
~SequencesStatistics();
- /** Counts the number of inferences made of each type of inference */
+ /** Counts the number of applications of each type of inference */
HistogramStat<Inference> d_inferences;
+ /** Counts the number of applications of each type of reduction */
+ HistogramStat<Kind> d_reductions;
+ //--------------- conflicts, partition of calls to OutputChannel::conflict
+ /** Number of equality engine conflicts */
+ IntStat d_conflictsEqEngine;
+ /** Number of eager prefix conflicts */
+ IntStat d_conflictsEagerPrefix;
+ /** Number of inference conflicts */
+ IntStat d_conflictsInfer;
+ //--------------- end of conflicts
+ //--------------- lemmas, partition of calls to OutputChannel::lemma
+ /** Number of lemmas added due to eager preprocessing */
+ IntStat d_lemmasEagerPreproc;
+ /** Number of collect model info splits */
+ IntStat d_lemmasCmiSplit;
+ /** Number of lemmas added due to registering terms */
+ IntStat d_lemmasRegisterTerm;
+ /** Number of lemmas added due to registering atomic terms */
+ IntStat d_lemmasRegisterTermAtomic;
+ /** Number of lemmas added due to inferences */
+ IntStat d_lemmasInfer;
+ //--------------- end of lemmas
};
-
}
}
}
const LogicInfo& logicInfo)
: Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
d_notify(*this),
- d_equalityEngine(d_notify, c, "theory::strings", true),
+ d_equalityEngine(d_notify, c, "theory::strings::ee", true),
d_state(c, d_equalityEngine, d_valuation),
d_im(*this, c, u, d_state, d_sk_cache, out, d_statistics),
d_pregistered_terms_cache(u),
{
setupExtTheory();
ExtTheory* extt = getExtTheory();
- d_esolver.reset(new ExtfSolver(
- c, u, d_state, d_im, d_sk_cache, d_bsolver, d_csolver, extt));
+ d_esolver.reset(new ExtfSolver(c,
+ u,
+ d_state,
+ d_im,
+ d_sk_cache,
+ d_bsolver,
+ d_csolver,
+ extt,
+ d_statistics));
d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u));
// The kinds we are treating as function application in congruence
for (const Node& sl : len_splits)
{
Node spl = nm->mkNode(OR, sl, sl.negate());
+ ++(d_statistics.d_lemmasCmiSplit);
d_out->lemma(spl);
}
return false;
Node conflictNode;
conflictNode = explain( a.eqNode(b) );
Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
+ ++(d_statistics.d_conflictsEqEngine);
d_out->conflict( conflictNode );
}
}
d_state.setConflict();
Trace("strings-conflict")
<< "CONFLICT: Eager prefix : " << conflictNode << std::endl;
+ ++(d_statistics.d_conflictsEagerPrefix);
d_out->conflict(conflictNode);
}
}
NodeManager* nm = NodeManager::currentNM();
Debug("strings-register") << "TheoryStrings::registerTerm() " << n
<< ", effort = " << effort << std::endl;
+ Node regTermLem;
if (tn.isStringLike())
{
// register length information:
// for variables, split on empty vs positive length
// for concat/const/replace, introduce proxy var and state length relation
- d_im.registerLength(n);
+ regTermLem = d_im.registerTerm(n);
}
else if (n.getKind() == STRING_TO_CODE)
{
AND,
nm->mkNode(GEQ, n, d_zero),
nm->mkNode(LT, n, nm->mkConst(Rational(CVC4::String::num_codes()))));
- Node lem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
- Trace("strings-lemma") << "Strings::Lemma CODE : " << lem << std::endl;
- Trace("strings-assert") << "(assert " << lem << ")" << std::endl;
- d_out->lemma(lem);
+ regTermLem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
}
else if (n.getKind() == STRING_STRIDOF)
{
Node len = utils::mkNLength(n[0]);
- Node lem = nm->mkNode(AND,
- nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
- nm->mkNode(LEQ, n, len));
- Trace("strings-lemma") << "Strings::Lemma IDOF range : " << lem
+ regTermLem = nm->mkNode(AND,
+ nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
+ nm->mkNode(LEQ, n, len));
+ }
+ if (!regTermLem.isNull())
+ {
+ Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
<< std::endl;
- d_out->lemma(lem);
+ Trace("strings-assert") << "(assert " << regTermLem << ")" << std::endl;
+ ++(d_statistics.d_lemmasRegisterTerm);
+ d_out->lemma(regTermLem);
}
}
Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl;
for( unsigned i=0; i<new_nodes.size(); i++ ){
Trace("strings-ppr") << " lemma : " << new_nodes[i] << std::endl;
+ ++(d_statistics.d_lemmasEagerPreproc);
d_out->lemma( new_nodes[i] );
}
return ret;
namespace theory {
namespace strings {
-StringsPreprocess::StringsPreprocess(SkolemCache *sc, context::UserContext *u)
- : d_sc(sc)
+StringsPreprocess::StringsPreprocess(SkolemCache* sc,
+ context::UserContext* u,
+ SequencesStatistics& stats)
+ : d_sc(sc), d_statistics(stats)
{
//Constants
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
Trace("strings-preprocess") << " " << new_nodes[i] << std::endl;
}
}
+ d_statistics.d_reductions << t.getKind();
}
else
{
#include <vector>
#include "context/cdhashmap.h"
#include "theory/rewriter.h"
+#include "theory/strings/sequences_stats.h"
#include "theory/strings/skolem_cache.h"
#include "theory/theory.h"
#include "util/hash.h"
* reductions" inference schema of TheoryStrings.
*/
class StringsPreprocess {
-public:
- StringsPreprocess(SkolemCache *sc, context::UserContext *u);
- ~StringsPreprocess();
- /**
- * Returns a node t' such that
- * (exists k) new_nodes => t = t'
- * is valid, where k are the free skolems introduced when constructing
- * new_nodes.
- */
- Node simplify(Node t, std::vector<Node> &new_nodes);
- /**
- * Applies simplifyRec on t until a fixed point is reached, and returns
- * the resulting term t', which is such that
- * (exists k) new_nodes => t = t'
- * is valid, where k are the free skolems introduced when constructing
- * new_nodes.
- */
- Node processAssertion(Node t, std::vector<Node> &new_nodes);
- /**
- * Replaces all formulas t in vec_node with an equivalent formula t' that
- * contains no free instances of extended functions (that is, extended
- * functions may only appear beneath quantifiers). This applies simplifyRec
- * on each assertion in vec_node until a fixed point is reached.
- */
- void processAssertions(std::vector<Node> &vec_node);
+ public:
+ StringsPreprocess(SkolemCache* sc,
+ context::UserContext* u,
+ SequencesStatistics& stats);
+ ~StringsPreprocess();
+ /**
+ * Returns a node t' such that
+ * (exists k) new_nodes => t = t'
+ * is valid, where k are the free skolems introduced when constructing
+ * new_nodes.
+ */
+ Node simplify(Node t, std::vector<Node>& new_nodes);
+ /**
+ * Applies simplifyRec on t until a fixed point is reached, and returns
+ * the resulting term t', which is such that
+ * (exists k) new_nodes => t = t'
+ * is valid, where k are the free skolems introduced when constructing
+ * new_nodes.
+ */
+ Node processAssertion(Node t, std::vector<Node>& new_nodes);
+ /**
+ * Replaces all formulas t in vec_node with an equivalent formula t' that
+ * contains no free instances of extended functions (that is, extended
+ * functions may only appear beneath quantifiers). This applies simplifyRec
+ * on each assertion in vec_node until a fixed point is reached.
+ */
+ void processAssertions(std::vector<Node>& vec_node);
-private:
- /** commonly used constants */
- Node d_zero;
- Node d_one;
- Node d_neg_one;
- Node d_empty_str;
- /** pointer to the skolem cache used by this class */
- SkolemCache *d_sc;
- /**
- * Applies simplify to all top-level extended function subterms of t. New
- * assertions created in this reduction are added to new_nodes. The argument
- * visited stores a cache of previous results.
- */
- Node simplifyRec(Node t,
- std::vector<Node> &new_nodes,
- std::map<Node, Node> &visited);
+ private:
+ /** commonly used constants */
+ Node d_zero;
+ Node d_one;
+ Node d_neg_one;
+ Node d_empty_str;
+ /** pointer to the skolem cache used by this class */
+ SkolemCache* d_sc;
+ /** Reference to the statistics for the theory of strings/sequences. */
+ SequencesStatistics& d_statistics;
+ /**
+ * Applies simplify to all top-level extended function subterms of t. New
+ * assertions created in this reduction are added to new_nodes. The argument
+ * visited stores a cache of previous results.
+ */
+ Node simplifyRec(Node t,
+ std::vector<Node>& new_nodes,
+ std::map<Node, Node>& visited);
};
}/* CVC4::theory::strings namespace */
projects / cvc5.git / commitdiff