Also eliminates use of raw output channel in strings.
case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS";
case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION";
case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT";
+ case InferenceId::STRINGS_REGISTER_TERM_ATOMIC:
+ return "STRINGS_REGISTER_TERM_ATOMIC";
+ case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM";
+ case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT";
case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
STRINGS_CARD_SP,
// The cardinality inference for strings, see Liang et al CAV 2014.
STRINGS_CARDINALITY,
- //-------------------- end base solver
//-------------------- core solver
// A cycle in the empty string equivalence class, e.g.:
// x ++ y = "" => x = ""
// is unknown, we apply the inference:
// len(s) != len(t) V len(s) = len(t)
STRINGS_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.
STRINGS_CODE_PROXY,
// str.code(x) = -1 V str.code(x) != str.code(y) V x = y
STRINGS_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
STRINGS_RE_DELTA_CONF,
// regular expression derive ???
STRINGS_RE_DERIVE,
- //-------------------- end regexp solver
//-------------------- extended function solver
// Standard extended function inferences from context-dependent rewriting
// produced by constant substitutions. See Reynolds et al CAV 2017. These are
// f(x1, .., xn) and P is the reduction predicate for f
// (see theory_strings_preprocess).
STRINGS_REDUCTION,
- //-------------------- end extended function solver
//-------------------- prefix conflict
// prefix conflict (coarse-grained)
STRINGS_PREFIX_CONFLICT,
- //-------------------- end prefix conflict
+ //-------------------- other
+ // a lemma added during term registration for an atomic term
+ STRINGS_REGISTER_TERM_ATOMIC,
+ // a lemma added during term registration
+ STRINGS_REGISTER_TERM,
+ // a split during collect model info
+ STRINGS_CMI_SPLIT,
//-------------------------------------- end strings theory
//-------------------------------------- uf theory
SkolemCache* skc = d_termReg.getSkolemCache();
Node sk_w = skc->mkSkolem("w_loop");
Node sk_y = skc->mkSkolem("y_loop");
- d_termReg.registerTermAtomic(sk_y, LENGTH_GEQ_ONE);
+ iinfo.d_skolems[LENGTH_GEQ_ONE].push_back(sk_y);
Node sk_z = skc->mkSkolem("z_loop");
// t1 * ... * tn = y * z
Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z));
<< ii.getId() << std::endl;
Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
<< ii.getId() << std::endl;
- ++(d_statistics.d_lemmasInfer);
-
return tlem;
}
d_rewrites("theory::strings::rewrites"),
d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
d_conflictsEager("theory::strings::conflictsEager", 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)
+ d_conflictsInfer("theory::strings::conflictsInfer", 0)
{
smtStatisticsRegistry()->registerStat(&d_checkRuns);
smtStatisticsRegistry()->registerStat(&d_strategyRuns);
smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
smtStatisticsRegistry()->registerStat(&d_conflictsEager);
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_conflictsEqEngine);
smtStatisticsRegistry()->unregisterStat(&d_conflictsEager);
smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
- smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc);
- smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit);
- smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTerm);
- smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTermAtomic);
- smtStatisticsRegistry()->unregisterStat(&d_lemmasInfer);
}
}
*
* "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
{
/** 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
};
}
#include "options/strings_options.h"
#include "smt/logic_exception.h"
#include "theory/rewriter.h"
+#include "theory/strings/inference_manager.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
StringsProxyVarAttribute;
TermRegistry::TermRegistry(SolverState& s,
- OutputChannel& out,
SequencesStatistics& statistics,
ProofNodeManager* pnm)
: d_state(s),
- d_out(out),
+ d_im(nullptr),
d_statistics(statistics),
d_hasStrCode(false),
d_functionsTerms(s.getSatContext()),
TermRegistry::~TermRegistry() {}
+void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
+
Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
{
NodeManager* nm = NodeManager::currentNM();
}
else if (k == STRING_IN_REGEXP)
{
- d_out.requirePhase(n, true);
+ d_im->requirePhase(n, true);
ee->addTriggerPredicate(n);
ee->addTerm(n[0]);
ee->addTerm(n[1]);
<< std::endl;
Trace("strings-assert")
<< "(assert " << regTermLem.getNode() << ")" << std::endl;
- ++(d_statistics.d_lemmasRegisterTerm);
- d_out.trustedLemma(regTermLem);
+ d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
}
}
<< std::endl;
Trace("strings-assert")
<< "(assert " << lenLem.getNode() << ")" << std::endl;
- ++(d_statistics.d_lemmasRegisterTermAtomic);
- d_out.trustedLemma(lenLem);
+ d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
}
for (const std::pair<const Node, bool>& rp : reqPhase)
{
- d_out.requirePhase(rp.first, rp.second);
+ d_im->requirePhase(rp.first, rp.second);
}
}
namespace theory {
namespace strings {
+class InferenceManager;
/**
* This class manages all the (pre)registration tasks for terms. These tasks
* include:
public:
TermRegistry(SolverState& s,
- OutputChannel& out,
SequencesStatistics& statistics,
ProofNodeManager* pnm);
~TermRegistry();
+ /** Finish initialize, which sets the inference manager */
+ void finishInit(InferenceManager* im);
/** The eager reduce routine
*
* Constructs a lemma for t that is incomplete, but communicates pertinent
uint32_t d_cardSize;
/** Reference to the solver state of the theory of strings. */
SolverState& d_state;
- /** Reference to the output channel of the theory of strings. */
- OutputChannel& d_out;
+ /** Pointer to the inference manager of the theory of strings. */
+ InferenceManager* d_im;
/** Reference to the statistics for the theory of strings/sequences. */
SequencesStatistics& d_statistics;
/** have we asserted any str.code terms? */
d_statistics(),
d_state(c, u, d_valuation),
d_eagerSolver(d_state),
- d_termReg(d_state, out, d_statistics, pnm),
+ d_termReg(d_state, d_statistics, pnm),
d_extTheoryCb(),
d_extTheory(d_extTheoryCb, c, u, out),
d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm),
d_regexp_elim(options::regExpElimAgg(), pnm, u),
d_stringsFmf(c, u, valuation, d_termReg)
{
+ d_termReg.finishInit(&d_im);
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
bool TheoryStrings::propagateLit(TNode literal)
{
- Debug("strings-propagate")
- << "TheoryStrings::propagateLit(" << literal << ")" << std::endl;
- // If already in conflict, no more propagation
- if (d_state.isInConflict())
- {
- Debug("strings-propagate") << "TheoryStrings::propagateLit(" << literal
- << "): already in conflict" << std::endl;
- return false;
- }
- // Propagate out
- bool ok = d_out->propagate(literal);
- if (!ok) {
- d_state.notifyInConflict();
- }
- return ok;
+ return d_im.propagateLit(literal);
}
TrustNode TheoryStrings::explain(TNode literal)
for (const Node& sl : len_splits)
{
Node spl = nm->mkNode(OR, sl, sl.negate());
- ++(d_statistics.d_lemmasCmiSplit);
- d_out->lemma(spl);
+ d_im.lemma(spl, InferenceId::STRINGS_CMI_SPLIT);
Trace("strings-lemma")
<< "Strings::CollectModelInfoSplit: " << spl << std::endl;
}
projects / cvc5.git / commitdiff