theory/strings/regexp_solver.h
theory/strings/sequences_rewriter.cpp
theory/strings/sequences_rewriter.h
+ theory/strings/sequences_stats.cpp
+ theory/strings/sequences_stats.h
theory/strings/skolem_cache.cpp
theory/strings/skolem_cache.h
theory/strings/solver_state.cpp
bool set_use_index = false;
Trace("strings-solve") << "Possible inferences (" << pinfer.size()
<< ") : " << std::endl;
- unsigned min_id = 9;
+ Inference min_id = Inference::NONE;
unsigned max_index = 0;
for (unsigned i = 0, size = pinfer.size(); i < size; i++)
{
// can infer that this string must be empty
Node eq = nfkv[index_k].eqNode(d_emptyString);
Assert(!d_state.areEqual(d_emptyString, nfkv[index_k]));
- d_im.sendInference(curr_exp, eq, "N_EndpointEmp");
+ d_im.sendInference(curr_exp, eq, Inference::N_ENDPOINT_EMP);
index_k++;
}
break;
Node leneq = xLenTerm.eqNode(yLenTerm);
NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, lenExp);
lenExp.push_back(leneq);
- d_im.sendInference(lenExp, eq, "N_Unify");
+ d_im.sendInference(lenExp, eq, Inference::N_UNIFY);
break;
}
else if ((x.getKind() != CONST_STRING && 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]), "N_EndpointEq", true);
+ d_im.sendInference(
+ antec, eqn[0].eqNode(eqn[1]), Inference::N_ENDPOINT_EQ, true);
}
else
{
// E.g. "abc" ++ ... = "bc" ++ ... ---> conflict
std::vector<Node> antec;
NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, antec);
- d_im.sendInference(antec, d_false, "N_Const", true);
+ d_im.sendInference(antec, d_false, Inference::N_CONST, true);
break;
}
}
lenEq = Rewriter::rewrite(lenEq);
info.d_conc = nm->mkNode(OR, lenEq, lenEq.negate());
info.d_pending_phase[lenEq] = true;
- info.d_id = INFER_LEN_SPLIT;
+ info.d_id = Inference::LEN_SPLIT;
pinfer.push_back(info);
break;
}
// inferred
info.d_conc = nm->mkNode(
AND, p.eqNode(nc), !eq.getConst<bool>() ? pEq.negate() : pEq);
- info.d_id = INFER_INFER_EMP;
+ info.d_id = Inference::INFER_EMP;
}
else
{
info.d_conc = nm->mkNode(OR, eq, eq.negate());
- info.d_id = INFER_LEN_SPLIT_EMP;
+ info.d_id = Inference::LEN_SPLIT_EMP;
}
pinfer.push_back(info);
break;
info.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, prea)
: utils::mkNConcat(prea, sk));
info.d_new_skolem[LENGTH_SPLIT].push_back(sk);
- info.d_id = INFER_SSPLIT_CST_PROP;
+ info.d_id = Inference::SSPLIT_CST_PROP;
pinfer.push_back(info);
break;
}
info.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
: utils::mkNConcat(firstChar, sk));
info.d_new_skolem[LENGTH_SPLIT].push_back(sk);
- info.d_id = INFER_SSPLIT_CST;
+ info.d_id = Inference::SSPLIT_CST;
pinfer.push_back(info);
break;
}
{
info.d_antn.push_back(lentTestExp);
info.d_conc = lentTestSuccess == 0 ? eq1 : eq2;
- info.d_id = INFER_SSPLIT_VAR_PROP;
+ info.d_id = Inference::SSPLIT_VAR_PROP;
}
else
{
Node ldeq = nm->mkNode(EQUAL, xLenTerm, yLenTerm).negate();
info.d_ant.push_back(ldeq);
info.d_conc = nm->mkNode(OR, eq1, eq2);
- info.d_id = INFER_SSPLIT_VAR;
+ info.d_id = Inference::SSPLIT_VAR;
}
pinfer.push_back(info);
break;
{
// try to make t equal to empty to avoid loop
info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
- info.d_id = INFER_LEN_SPLIT_EMP;
+ info.d_id = Inference::LEN_SPLIT_EMP;
return ProcessLoopResult::INFERENCE;
}
else
// we will be done
info.d_conc = conc;
- info.d_id = INFER_FLOOP;
+ info.d_id = Inference::FLOOP;
info.d_nf_pair[0] = nfi.d_base;
info.d_nf_pair[1] = nfj.d_base;
return ProcessLoopResult::INFERENCE;
{
switch (i)
{
- case INFER_INFER_EMP: out << "Infer-Emp"; break;
- case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
- case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
- case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;
- case INFER_LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
- case INFER_SSPLIT_CST: out << "S-Split(CST-P)"; break;
- case INFER_SSPLIT_VAR: out << "S-Split(VAR)"; break;
- case INFER_FLOOP: out << "F-Loop"; break;
+ case Inference::N_ENDPOINT_EMP: out << "N_EndpointEmp"; break;
+ case Inference::N_UNIFY: out << "N_Unify"; break;
+ case Inference::N_ENDPOINT_EQ: out << "N_EndpointEq"; break;
+ case Inference::N_CONST: out << "N_Const"; break;
+ case Inference::INFER_EMP: out << "Infer-Emp"; break;
+ case Inference::SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
+ case Inference::SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
+ case Inference::LEN_SPLIT: out << "Len-Split(Len)"; break;
+ case Inference::LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
+ case Inference::SSPLIT_CST: out << "S-Split(CST-P)"; break;
+ case Inference::SSPLIT_VAR: out << "S-Split(VAR)"; break;
+ case Inference::FLOOP: out << "F-Loop"; break;
default: out << "?"; break;
}
return out;
}
-InferInfo::InferInfo() : d_id(INFER_NONE), d_index(0), d_rev(false) {}
+InferInfo::InferInfo() : d_id(Inference::NONE), d_index(0), d_rev(false) {}
} // namespace strings
} // namespace theory
*
* These are variants of the inference rules in Figures 3-5 of Liang et al.
* "A DPLL(T) Solver for a Theory of Strings and Regular Expressions", CAV 2014.
+ *
+ * Note: The order in this enum matters in certain cases (e.g. inferences
+ * related to normal forms), inferences that come first are generally
+ * preferred.
*/
-enum Inference
+enum class Inference : uint32_t
{
- INFER_NONE = 0,
+ // 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 = ""
+ N_ENDPOINT_EMP,
+ // Given two normal forms, infers that two components have to be the same if
+ // they have the same length. For example:
+ // If x1 ++ x2 = x3 ++ x4 and len(x1) = len(x3) then x1 = x3
+ N_UNIFY,
+ // Given two normal forms, infers that the endpoints have to be the same. For
+ // example:
+ // If x1 ++ x2 = x3 ++ x4 ++ x5 and x1 = x3 then x2 = x4 ++ x5
+ N_ENDPOINT_EQ,
+ // Given two normal forms with constant endpoints, infers a conflict if the
+ // endpoints do not agree. For example:
+ // If "abc" ++ ... = "bc" ++ ... then conflict
+ N_CONST,
// infer empty, for example:
// (~) x = ""
// This is inferred when we encounter an x such that x = "" rewrites to a
// constant. This inference is used for instance when we otherwise would have
// split on the emptiness of x but the rewriter tells us the emptiness of x
// can be inferred.
- INFER_INFER_EMP = 1,
+ INFER_EMP,
// string split constant propagation, for example:
// x = y, x = "abc", y = y1 ++ "b" ++ y2
// implies y1 = "a" ++ y1'
- INFER_SSPLIT_CST_PROP,
+ SSPLIT_CST_PROP,
// string split variable propagation, for example:
// x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
// implies x1 = y1 ++ x1'
// This is inspired by Zheng et al CAV 2015.
- INFER_SSPLIT_VAR_PROP,
+ SSPLIT_VAR_PROP,
// length split, for example:
// len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
// This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
- INFER_LEN_SPLIT,
+ LEN_SPLIT,
// length split empty, for example:
// z = "" V z != ""
// This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
- INFER_LEN_SPLIT_EMP,
+ LEN_SPLIT_EMP,
// string split constant
// x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
// implies y1 = "c" ++ y1'
// This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
- INFER_SSPLIT_CST,
+ SSPLIT_CST,
// string split variable, for example:
// x = y, x = x1 ++ x2, y = y1 ++ y2
// implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
// This is rule F-Split in Figure 5 of Liang et al CAV 2014.
- INFER_SSPLIT_VAR,
+ SSPLIT_VAR,
// flat form loop, for example:
// x = y, x = x1 ++ z, y = z ++ y2
// implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
// for fresh u, u1, u2.
// This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
- INFER_FLOOP,
+ FLOOP,
+ NONE,
};
std::ostream& operator<<(std::ostream& out, Inference i);
context::UserContext* u,
SolverState& s,
SkolemCache& skc,
- OutputChannel& out)
+ OutputChannel& out,
+ SequencesStatistics& statistics)
: d_parent(p),
d_state(s),
d_skCache(skc),
d_out(out),
+ d_statistics(statistics),
d_keep(c),
d_proxyVar(u),
d_proxyVarToLength(u),
sendInference(exp, exp_n, eq, c, asLemma);
}
-void InferenceManager::sendInference(const InferInfo& i)
+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)
{
- std::stringstream ssi;
- ssi << i.d_id;
- sendInference(i.d_ant, i.d_antn, i.d_conc, ssi.str().c_str(), true);
+ d_statistics.d_inferences << infer;
+ std::stringstream ss;
+ ss << infer;
+ sendInference(exp, eq, ss.str().c_str(), 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)
{
if (conc.isNull() || conc == d_false)
#include "expr/node.h"
#include "theory/output_channel.h"
#include "theory/strings/infer_info.h"
+#include "theory/strings/sequences_stats.h"
#include "theory/strings/skolem_cache.h"
#include "theory/strings/solver_state.h"
#include "theory/uf/equality_engine.h"
context::UserContext* u,
SolverState& s,
SkolemCache& skc,
- OutputChannel& out);
+ OutputChannel& out,
+ SequencesStatistics& statistics);
~InferenceManager() {}
/** send internal inferences
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.
+ */
+ void sendInference(const std::vector<Node>& exp,
+ Node eq,
+ Inference infer,
+ bool asLemma = false);
+
/** Send inference
*
* Makes the appropriate call to send inference based on the infer info
* This is a reference to the output channel of the theory of strings.
*/
OutputChannel& d_out;
+
+ /** Reference to the statistics for the theory of strings/sequences. */
+ SequencesStatistics& d_statistics;
+
/** Common constants */
Node d_emptyString;
Node d_true;
NodeNodeMap d_proxyVarToLength;
/** List of terms that we have register length for */
NodeSet d_lengthLemmaTermsCache;
+
/** infer substitution proxy vars
*
* This method attempts to (partially) convert the formula n into a
--- /dev/null
+/********************* */
+/*! \file sequences_stats.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Statistics for the theory of strings/sequences
+ **/
+
+
+#include "theory/strings/sequences_stats.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+SequencesStatistics::SequencesStatistics()
+ : d_inferences("theory::strings::inferences")
+{
+ smtStatisticsRegistry()->registerStat(&d_inferences);
+}
+
+SequencesStatistics::~SequencesStatistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_inferences);
+}
+
+}
+}
+}
--- /dev/null
+/********************* */
+/*! \file sequences_stats.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Statistics for the theory of strings/sequences
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__SEQUENCES_STATS_H
+#define CVC4__THEORY__STRINGS__SEQUENCES_STATS_H
+
+#include "theory/strings/infer_info.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+class SequencesStatistics
+{
+ public:
+ SequencesStatistics();
+ ~SequencesStatistics();
+
+ /** Counts the number of inferences made of each type of inference */
+ HistogramStat<Inference> d_inferences;
+};
+
+
+}
+}
+}
+
+#endif /* CVC4__THEORY__STRINGS__SEQUENCES_STATS_H */
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::strings", true),
d_state(c, d_equalityEngine, d_valuation),
- d_im(*this, c, u, d_state, d_sk_cache, out),
+ d_im(*this, c, u, d_state, d_sk_cache, out, d_statistics),
d_pregistered_terms_cache(u),
d_registered_terms_cache(u),
d_functionsTerms(c),
return atom;
}
-// Stats
-TheoryStrings::Statistics::Statistics()
- : d_splits("theory::strings::NumOfSplitOnDemands", 0),
- d_eq_splits("theory::strings::NumOfEqSplits", 0),
- d_deq_splits("theory::strings::NumOfDiseqSplits", 0),
- d_loop_lemmas("theory::strings::NumOfLoops", 0)
-{
- smtStatisticsRegistry()->registerStat(&d_splits);
- smtStatisticsRegistry()->registerStat(&d_eq_splits);
- smtStatisticsRegistry()->registerStat(&d_deq_splits);
- smtStatisticsRegistry()->registerStat(&d_loop_lemmas);
-}
-
-TheoryStrings::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_splits);
- smtStatisticsRegistry()->unregisterStat(&d_eq_splits);
- smtStatisticsRegistry()->unregisterStat(&d_deq_splits);
- smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas);
-}
-
/** run the given inference step */
void TheoryStrings::runInferStep(InferStep s, int effort)
{
#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_H
#define CVC4__THEORY__STRINGS__THEORY_STRINGS_H
+#include <climits>
+#include <deque>
+
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "expr/attribute.h"
#include "theory/strings/regexp_elim.h"
#include "theory/strings/regexp_operation.h"
#include "theory/strings/regexp_solver.h"
+#include "theory/strings/sequences_stats.h"
#include "theory/strings/skolem_cache.h"
#include "theory/strings/solver_state.h"
#include "theory/strings/strings_fmf.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
-#include <climits>
-#include <deque>
-
namespace CVC4 {
namespace theory {
namespace strings {
uint32_t d_cardSize;
/** The notify class */
NotifyClass d_notify;
+
+ /**
+ * Statistics for the theory of strings/sequences. All statistics for these
+ * theories is collected in this object.
+ */
+ SequencesStatistics d_statistics;
+
/** Equaltity engine */
eq::EqualityEngine d_equalityEngine;
/** The solver state object */
// ppRewrite
Node ppRewrite(TNode atom) override;
- public:
- /** statistics class */
- class Statistics {
- public:
- IntStat d_splits;
- IntStat d_eq_splits;
- IntStat d_deq_splits;
- IntStat d_loop_lemmas;
- Statistics();
- ~Statistics();
- };/* class TheoryStrings::Statistics */
- Statistics d_statistics;
-
private:
//-----------------------inference steps
/** check register terms pre-normal forms
*/
void runStrategy(unsigned sbegin, unsigned send);
//-----------------------end representation of the strategy
-
};/* class TheoryStrings */
}/* CVC4::theory::strings namespace */
projects / cvc5.git / commitdiff