This PR makes it so that the module dependencies in the theory of strings are acyclic. This is important for further organization towards proofs for strings.
The main change in this PR is to ensure that InferenceManager has a pointer to ExtTheory, which is needed for several of its methods. This required changing several solvers into unique_ptr to properly initialize.
StringsRewriter& rewriter,
BaseSolver& bs,
CoreSolver& cs,
- ExtTheory* et,
+ ExtTheory& et,
SequencesStatistics& statistics)
: d_state(s),
d_im(im),
d_extfInferCache(c),
d_reduced(u)
{
- d_extt->addFunctionKind(kind::STRING_SUBSTR);
- d_extt->addFunctionKind(kind::STRING_STRIDOF);
- d_extt->addFunctionKind(kind::STRING_ITOS);
- d_extt->addFunctionKind(kind::STRING_STOI);
- d_extt->addFunctionKind(kind::STRING_STRREPL);
- d_extt->addFunctionKind(kind::STRING_STRREPLALL);
- d_extt->addFunctionKind(kind::STRING_STRCTN);
- d_extt->addFunctionKind(kind::STRING_IN_REGEXP);
- d_extt->addFunctionKind(kind::STRING_LEQ);
- d_extt->addFunctionKind(kind::STRING_TO_CODE);
- d_extt->addFunctionKind(kind::STRING_TOLOWER);
- d_extt->addFunctionKind(kind::STRING_TOUPPER);
- d_extt->addFunctionKind(kind::STRING_REV);
+ d_extt.addFunctionKind(kind::STRING_SUBSTR);
+ d_extt.addFunctionKind(kind::STRING_STRIDOF);
+ d_extt.addFunctionKind(kind::STRING_ITOS);
+ d_extt.addFunctionKind(kind::STRING_STOI);
+ d_extt.addFunctionKind(kind::STRING_STRREPL);
+ d_extt.addFunctionKind(kind::STRING_STRREPLALL);
+ d_extt.addFunctionKind(kind::STRING_STRCTN);
+ d_extt.addFunctionKind(kind::STRING_IN_REGEXP);
+ d_extt.addFunctionKind(kind::STRING_LEQ);
+ d_extt.addFunctionKind(kind::STRING_TO_CODE);
+ d_extt.addFunctionKind(kind::STRING_TOLOWER);
+ d_extt.addFunctionKind(kind::STRING_TOUPPER);
+ d_extt.addFunctionKind(kind::STRING_REV);
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
// this depends on the current assertions, so this
// inference is context-dependent
- d_extt->markReduced(n, true);
+ d_extt.markReduced(n, true);
return true;
}
else
Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
<< " => " << eq << std::endl;
// context-dependent because it depends on the polarity of n itself
- d_extt->markReduced(n, true);
+ d_extt.markReduced(n, true);
}
else if (k != kind::STRING_TO_CODE)
{
// Notice we don't make a standard call to ExtTheory::doReductions here,
// since certain optimizations like context-dependent reductions and
// stratifying effort levels are done in doReduction below.
- std::vector<Node> extf = d_extt->getActive();
+ std::vector<Node> extf = d_extt.getActive();
Trace("strings-process") << " checking " << extf.size() << " active extf"
<< std::endl;
for (const Node& n : extf)
d_extfInfoTmp.clear();
NodeManager* nm = NodeManager::currentNM();
bool has_nreduce = false;
- std::vector<Node> terms = d_extt->getActive();
+ std::vector<Node> terms = d_extt.getActive();
for (const Node& n : terms)
{
// Setup information about n, including if it is equal to a constant.
{
if (effort < 3)
{
- d_extt->markReduced(n);
+ d_extt.markReduced(n);
Trace("strings-extf-debug")
<< " resolvable by evaluation..." << std::endl;
std::vector<Node> exps;
}
Trace("strings-extf-list") << std::endl;
}
- if (d_extt->isActive(n) && einfo.d_modelActive)
+ if (d_extt.isActive(n) && einfo.d_modelActive)
{
has_nreduce = true;
}
// we are in conflict
d_im.sendInference(in.d_exp, conc, Inference::CTN_DECOMPOSE);
}
- else if (d_extt->hasFunctionKind(conc.getKind()))
+ else if (d_extt.hasFunctionKind(conc.getKind()))
{
// can mark as reduced, since model for n implies model for conc
- d_extt->markReduced(conc);
+ d_extt.markReduced(conc);
}
}
}
// satisfied by all models of str.contains( x, y ) ^ x=z and thus can
// be ignored.
Trace("strings-extf-debug") << " redundant." << std::endl;
- d_extt->markReduced(n);
+ d_extt.markReduced(n);
}
}
return;
std::vector<Node> ExtfSolver::getActive(Kind k) const
{
- return d_extt->getActive(k);
+ return d_extt.getActive(k);
}
} // namespace strings
StringsRewriter& rewriter,
BaseSolver& bs,
CoreSolver& cs,
- ExtTheory* et,
+ ExtTheory& et,
SequencesStatistics& statistics);
~ExtfSolver();
* checkExtfEval.
*/
const std::map<Node, ExtfInfoTmp>& getInfo() const;
+ //---------------------------------- information about ExtTheory
/** Are there any active extended functions? */
bool hasExtendedFunctions() const;
/**
* context (see ExtTheory::getActive).
*/
std::vector<Node> getActive(Kind k) const;
-
+ //---------------------------------- end information about ExtTheory
private:
/** do reduction
*
/** reference to the core solver, used for certain queries */
CoreSolver& d_csolver;
/** the extended theory object for the theory of strings */
- ExtTheory* d_extt;
+ ExtTheory& d_extt;
/** Reference to the statistics for the theory of strings/sequences. */
SequencesStatistics& d_statistics;
/** preprocessing utility, for performing strings reductions */
#include "theory/strings/inference_manager.h"
-#include "expr/kind.h"
#include "options/strings_options.h"
#include "theory/ext_theory.h"
#include "theory/rewriter.h"
-#include "theory/strings/theory_strings.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
namespace theory {
namespace strings {
-InferenceManager::InferenceManager(TheoryStrings& p,
- context::Context* c,
+InferenceManager::InferenceManager(context::Context* c,
context::UserContext* u,
SolverState& s,
TermRegistry& tr,
+ ExtTheory& e,
OutputChannel& out,
SequencesStatistics& statistics)
- : d_parent(p),
- d_state(s),
+ : d_state(s),
d_termReg(tr),
+ d_extt(e),
d_out(out),
d_statistics(statistics),
d_keep(c)
d_false = nm->mkConst(false);
}
+void InferenceManager::sendAssumption(TNode lit)
+{
+ bool polarity = lit.getKind() != kind::NOT;
+ TNode atom = polarity ? lit : lit[0];
+ // assert pending fact
+ assertPendingFact(atom, polarity, lit);
+}
+
bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
Node conc,
Inference infer)
d_pendingReqPhase[lit] = pol;
}
+void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
+
void InferenceManager::addToExplanation(Node a,
Node b,
std::vector<Node>& exp) const
{
bool polarity = lit.getKind() != NOT;
TNode atom = polarity ? lit : lit[0];
- d_parent.assertPendingFact(atom, polarity, exp);
+ assertPendingFact(atom, polarity, exp);
}
}
else
{
bool polarity = fact.getKind() != NOT;
TNode atom = polarity ? fact : fact[0];
- d_parent.assertPendingFact(atom, polarity, exp);
+ assertPendingFact(atom, polarity, exp);
}
i++;
}
d_pendingReqPhase.clear();
}
+void InferenceManager::assertPendingFact(Node atom, bool polarity, Node exp)
+{
+ eq::EqualityEngine* ee = d_state.getEqualityEngine();
+ Trace("strings-pending") << "Assert pending fact : " << atom << " "
+ << polarity << " from " << exp << std::endl;
+ Assert(atom.getKind() != OR) << "Infer error: a split.";
+ if (atom.getKind() == EQUAL)
+ {
+ // we must ensure these terms are registered
+ Trace("strings-pending-debug") << " Register term" << std::endl;
+ for (const Node& t : atom)
+ {
+ // terms in the equality engine are already registered, hence skip
+ // currently done for only string-like terms, but this could potentially
+ // be avoided.
+ if (!ee->hasTerm(t) && t.getType().isStringLike())
+ {
+ d_termReg.registerTerm(t, 0);
+ }
+ }
+ Trace("strings-pending-debug") << " Now assert equality" << std::endl;
+ ee->assertEquality(atom, polarity, exp);
+ Trace("strings-pending-debug") << " Finished assert equality" << std::endl;
+ }
+ else
+ {
+ ee->assertPredicate(atom, polarity, exp);
+ if (atom.getKind() == STRING_IN_REGEXP)
+ {
+ if (polarity && atom[1].getKind() == REGEXP_CONCAT)
+ {
+ Node eqc = ee->getRepresentative(atom[0]);
+ d_state.addEndpointsToEqcInfo(atom, atom[1], eqc);
+ }
+ }
+ }
+ // process the conflict
+ if (!d_state.isInConflict())
+ {
+ Node pc = d_state.getPendingConflict();
+ if (!pc.isNull())
+ {
+ std::vector<Node> a;
+ a.push_back(pc);
+ Trace("strings-pending")
+ << "Process pending conflict " << pc << std::endl;
+ Node conflictNode = mkExplain(a);
+ d_state.setConflict();
+ Trace("strings-conflict")
+ << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
+ ++(d_statistics.d_conflictsEagerPrefix);
+ d_out.conflict(conflictNode);
+ }
+ }
+ Trace("strings-pending-debug") << " Now collect terms" << std::endl;
+ // Collect extended function terms in the atom. Notice that we must register
+ // all extended functions occurring in assertions and shared terms. We
+ // make a similar call to registerTermRec in TheoryStrings::addSharedTerm.
+ d_extt.registerTermRec(atom);
+ Trace("strings-pending-debug") << " Finished collect terms" << std::endl;
+}
+
bool InferenceManager::hasProcessed() const
{
return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty();
}
else
{
- ant = NodeManager::currentNM()->mkNode(kind::AND, antec_exp);
+ ant = NodeManager::currentNM()->mkNode(AND, antec_exp);
}
return ant;
}
}
}
}
-void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
void InferenceManager::markCongruent(Node a, Node b)
{
Assert(a.getKind() == b.getKind());
- ExtTheory* eth = d_parent.getExtTheory();
- if (eth->hasFunctionKind(a.getKind()))
+ if (d_extt.hasFunctionKind(a.getKind()))
{
- eth->markCongruent(a, b);
+ d_extt.markCongruent(a, b);
}
}
+void InferenceManager::markReduced(Node n, bool contextDepend)
+{
+ d_extt.markReduced(n, contextDepend);
+}
+
} // namespace strings
} // namespace theory
} // namespace CVC4
#include "context/cdhashset.h"
#include "context/context.h"
#include "expr/node.h"
+#include "theory/ext_theory.h"
#include "theory/output_channel.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/sequences_stats.h"
namespace theory {
namespace strings {
-class TheoryStrings;
-
/** Inference Manager
*
* The purpose of this class is to process inference steps for strategies
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
public:
- InferenceManager(TheoryStrings& p,
- context::Context* c,
+ InferenceManager(context::Context* c,
context::UserContext* u,
SolverState& s,
TermRegistry& tr,
+ ExtTheory& e,
OutputChannel& out,
SequencesStatistics& statistics);
~InferenceManager() {}
+ /** send assumption
+ *
+ * This is called when a fact is asserted to TheoryStrings. It adds lit
+ * to the equality engine maintained by this class immediately.
+ */
+ void sendAssumption(TNode lit);
+
/** send internal inferences
*
* This is called when we have inferred exp => conc, where exp is a set
* decided with polarity pol.
*/
void sendPhaseRequirement(Node lit, bool pol);
+ /**
+ * Set that we are incomplete for the current set of assertions (in other
+ * words, we must answer "unknown" instead of "sat"); this calls the output
+ * channel's setIncomplete method.
+ */
+ void setIncomplete();
//----------------------------constructing antecedants
/**
*
* This method asserts pending facts (d_pending) with explanations
* (d_pendingExp) to the equality engine of the theory of strings via calls
- * to assertPendingFact in the theory of strings.
+ * to assertPendingFact.
*
* It terminates early if a conflict is encountered, for instance, by
* equality reasoning within the equality engine.
* the node corresponding to their conjunction.
*/
void explain(TNode literal, std::vector<TNode>& assumptions) const;
- /**
- * Set that we are incomplete for the current set of assertions (in other
- * words, we must answer "unknown" instead of "sat"); this calls the output
- * channel's setIncomplete method.
- */
- void setIncomplete();
+ // ------------------------------------------------- extended theory
/**
* Mark that terms a and b are congruent in the current context.
* This makes a call to markCongruent in the extended theory object of
* theory.
*/
void markCongruent(Node a, Node b);
+ /**
+ * Mark that extended function is reduced. If contextDepend is true,
+ * then this mark is SAT-context dependent, otherwise it is user-context
+ * dependent (see ExtTheory::markReduced).
+ */
+ void markReduced(Node n, bool contextDepend = true);
+ // ------------------------------------------------- end extended theory
private:
+ /** assert pending fact
+ *
+ * This asserts atom with polarity to the equality engine of this class,
+ * where exp is the explanation of why (~) atom holds.
+ *
+ * This call may trigger further initialization steps involving the terms
+ * of atom, including calls to registerTerm.
+ */
+ void assertPendingFact(Node atom, bool polarity, Node exp);
/**
* Indicates that ant => conc should be sent on the output channel of this
* class. This will either trigger an immediate call to the conflict
* equality engine of this class.
*/
void sendInfer(Node eq_exp, Node eq, Inference infer);
-
- /** the parent theory of strings object */
- TheoryStrings& d_parent;
/** Reference to the solver state of the theory of strings. */
SolverState& d_state;
/** Reference to the term registry of theory of strings */
TermRegistry& d_termReg;
- /** Reference to the output channel of the theory of strings. */
+ /** the extended theory object for the theory of strings */
+ ExtTheory& d_extt;
+ /** 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;
#include "options/strings_options.h"
#include "theory/ext_theory.h"
-#include "theory/strings/theory_strings.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/theory_model.h"
namespace theory {
namespace strings {
-RegExpSolver::RegExpSolver(TheoryStrings& p,
- SolverState& s,
+RegExpSolver::RegExpSolver(SolverState& s,
InferenceManager& im,
+ CoreSolver& cs,
ExtfSolver& es,
SequencesStatistics& stats,
context::Context* c,
context::UserContext* u)
- : d_parent(p),
- d_state(s),
+ : d_state(s),
d_im(im),
+ d_csolver(cs),
d_esolver(es),
d_statistics(stats),
d_regexp_ucached(u),
Node nx = x;
if (!x.isConst())
{
- nx = d_parent.getNormalString(x, nfexp);
+ nx = d_csolver.getNormalString(x, nfexp);
}
// If r is not a constant regular expression, we update it based on
// normal forms, which may concretize its variables.
else
{
// otherwise we are incomplete
- d_parent.getOutputChannel().setIncomplete();
+ d_im.setIncomplete();
}
}
if (d_state.isInConflict())
{
// ~str.in.re(x, R1) includes ~str.in.re(x, R2) --->
// mark ~str.in.re(x, R2) as reduced
- d_parent.getExtTheory()->markReduced(m2Lit);
+ d_im.markReduced(m2Lit);
remove.insert(m2);
}
else
{
// str.in.re(x, R1) includes str.in.re(x, R2) --->
// mark str.in.re(x, R1) as reduced
- d_parent.getExtTheory()->markReduced(m1Lit);
+ d_im.markReduced(m1Lit);
remove.insert(m1);
// We don't need to process m1 anymore
{
// 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_parent.getExtTheory()->markReduced(m);
+ d_im.markReduced(m);
}
else if (mres == m)
{
// same as above, opposite direction
- d_parent.getExtTheory()->markReduced(mi);
+ d_im.markReduced(mi);
}
else
{
}
d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true);
// both are reduced
- d_parent.getExtTheory()->markReduced(m);
- d_parent.getExtTheory()->markReduced(mi);
+ d_im.markReduced(m);
+ d_im.markReduced(mi);
// do not send more than one lemma for this class
return true;
}
{
if (!r[0].isConst())
{
- Node tmp = d_parent.getNormalString(r[0], nf_exp);
+ Node tmp = d_csolver.getNormalString(r[0], nf_exp);
if (tmp != r[0])
{
ret = NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, tmp);
namespace theory {
namespace strings {
-class TheoryStrings;
-
class RegExpSolver
{
typedef context::CDList<Node> NodeList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
- RegExpSolver(TheoryStrings& p,
- SolverState& s,
+ RegExpSolver(SolverState& s,
InferenceManager& im,
+ CoreSolver& cs,
ExtfSolver& es,
SequencesStatistics& stats,
context::Context* c,
Node d_emptyRegexp;
Node d_true;
Node d_false;
- /** the parent of this object */
- TheoryStrings& d_parent;
/** The solver state of the parent of this object */
SolverState& d_state;
/** the output channel of the parent of this object */
InferenceManager& d_im;
+ /** reference to the core solver, used for certain queries */
+ CoreSolver& d_csolver;
/** reference to the extended function solver of the parent */
ExtfSolver& d_esolver;
/** Reference to the statistics for the theory of strings/sequences. */
d_equalityEngine(d_notify, c, "theory::strings::ee", true),
d_state(c, d_equalityEngine, d_valuation),
d_termReg(c, u, d_equalityEngine, out, d_statistics),
- d_im(*this, c, u, d_state, d_termReg, out, d_statistics),
+ d_im(nullptr),
d_rewriter(&d_statistics.d_rewrites),
- d_bsolver(c, u, d_state, d_im),
- d_csolver(c, u, d_state, d_im, d_termReg, d_bsolver),
+ d_bsolver(nullptr),
+ d_csolver(nullptr),
d_esolver(nullptr),
d_rsolver(nullptr),
d_stringsFmf(c, u, valuation, d_termReg),
{
setupExtTheory();
ExtTheory* extt = getExtTheory();
+ // initialize the inference manager, which requires the extended theory
+ d_im.reset(
+ new InferenceManager(c, u, d_state, d_termReg, *extt, out, d_statistics));
+ // initialize the solvers
+ d_bsolver.reset(new BaseSolver(c, u, d_state, *d_im));
+ d_csolver.reset(new CoreSolver(c, u, d_state, *d_im, d_termReg, *d_bsolver));
d_esolver.reset(new ExtfSolver(c,
u,
d_state,
- d_im,
+ *d_im,
d_termReg,
d_rewriter,
- d_bsolver,
- d_csolver,
- extt,
+ *d_bsolver,
+ *d_csolver,
+ *extt,
d_statistics));
- d_rsolver.reset(
- new RegExpSolver(*this, d_state, d_im, *d_esolver, d_statistics, c, u));
+ d_rsolver.reset(new RegExpSolver(
+ d_state, *d_im, *d_csolver, *d_esolver, d_statistics, c, u));
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
return false;
}
-Node TheoryStrings::getNormalString(Node x, std::vector<Node>& nf_exp)
-{
- return d_csolver.getNormalString(x, nf_exp);
-}
-
void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_equalityEngine.setMasterEqualityEngine(eq);
}
Node TheoryStrings::explain( TNode literal ){
Debug("strings-explain") << "explain called on " << literal << std::endl;
std::vector< TNode > assumptions;
- d_im.explain(literal, assumptions);
+ d_im->explain(literal, assumptions);
if( assumptions.empty() ){
return d_true;
}else if( assumptions.size()==1 ){
//check if col[i][j] has only variables
if (!eqc.isConst())
{
- NormalForm& nfe = d_csolver.getNormalForm(eqc);
+ NormalForm& nfe = d_csolver->getNormalForm(eqc);
if (nfe.d_nf.size() == 1)
{
// does it have a code and the length of these equivalence classes are
//step 4 : assign constants to all other equivalence classes
for( unsigned i=0; i<nodes.size(); i++ ){
if( processed.find( nodes[i] )==processed.end() ){
- NormalForm& nf = d_csolver.getNormalForm(nodes[i]);
+ NormalForm& nf = d_csolver->getNormalForm(nodes[i]);
if (Trace.isOn("strings-model"))
{
Trace("strings-model")
TimerStat::CodeTimer checkTimer(d_checkTime);
- bool polarity;
- TNode atom;
// Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
Trace("strings-check-debug")
<< "Theory of strings, check : " << e << std::endl;
TNode fact = assertion.d_assertion;
Trace("strings-assertion") << "get assertion: " << fact << endl;
- polarity = fact.getKind() != kind::NOT;
- atom = polarity ? fact : fact[0];
-
- //assert pending fact
- assertPendingFact( atom, polarity, fact );
+ d_im->sendAssumption(fact);
}
- d_im.doPendingFacts();
+ d_im->doPendingFacts();
Assert(d_strategy_init);
std::map<Effort, std::pair<unsigned, unsigned> >::iterator itsr =
Trace("strings-check") << " * Run strategy..." << std::endl;
runStrategy(sbegin, send);
// flush the facts
- addedFact = d_im.hasPendingFact();
- addedLemma = d_im.hasPendingLemma();
- d_im.doPendingFacts();
- d_im.doPendingLemmas();
+ addedFact = d_im->hasPendingFact();
+ addedLemma = d_im->hasPendingLemma();
+ d_im->doPendingFacts();
+ d_im->doPendingLemmas();
if (Trace.isOn("strings-check"))
{
Trace("strings-check") << " ...finish run strategy: ";
} while (!d_state.isInConflict() && !addedLemma && addedFact);
}
Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
- Assert(!d_im.hasPendingFact());
- Assert(!d_im.hasPendingLemma());
+ Assert(!d_im->hasPendingFact());
+ Assert(!d_im->hasPendingLemma());
}
bool TheoryStrings::needsCheckLastEffort() {
}
}
-void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
- Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl;
- Assert(atom.getKind() != kind::OR) << "Infer error: a split.";
- if( atom.getKind()==kind::EQUAL ){
- Trace("strings-pending-debug") << " Register term" << std::endl;
- for( unsigned j=0; j<2; j++ ) {
- if (!d_equalityEngine.hasTerm(atom[j])
- && atom[j].getType().isStringLike())
- {
- d_termReg.registerTerm(atom[j], 0);
- }
- }
- Trace("strings-pending-debug") << " Now assert equality" << std::endl;
- d_equalityEngine.assertEquality( atom, polarity, exp );
- Trace("strings-pending-debug") << " Finished assert equality" << std::endl;
- } else {
- d_equalityEngine.assertPredicate( atom, polarity, exp );
- if (atom.getKind() == STRING_IN_REGEXP)
- {
- if (polarity && atom[1].getKind() == REGEXP_CONCAT)
- {
- Node eqc = d_equalityEngine.getRepresentative(atom[0]);
- d_state.addEndpointsToEqcInfo(atom, atom[1], eqc);
- }
- }
- }
- // process the conflict
- if (!d_state.isInConflict())
- {
- Node pc = d_state.getPendingConflict();
- if (!pc.isNull())
- {
- std::vector<Node> a;
- a.push_back(pc);
- Trace("strings-pending")
- << "Process pending conflict " << pc << std::endl;
- Node conflictNode = d_im.mkExplain(a);
- d_state.setConflict();
- Trace("strings-conflict")
- << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
- ++(d_statistics.d_conflictsEagerPrefix);
- d_out->conflict(conflictNode);
- }
- }
- Trace("strings-pending-debug") << " Now collect terms" << std::endl;
- // Collect extended function terms in the atom. Notice that we must register
- // all extended functions occurring in assertions and shared terms. We
- // make a similar call to registerTermRec in addSharedTerm.
- getExtTheory()->registerTermRec( atom );
- Trace("strings-pending-debug") << " Finished collect terms" << std::endl;
-}
-
void TheoryStrings::checkRegisterTermsPreNormalForm()
{
- const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+ const std::vector<Node>& seqc = d_bsolver->getStringEqc();
for (const Node& eqc : seqc)
{
eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
while (!eqc_i.isFinished())
{
Node n = (*eqc_i);
- if (!d_bsolver.isCongruent(n))
+ if (!d_bsolver->isCongruent(n))
{
d_termReg.registerTerm(n, 2);
}
// str.code applied to the proxy variables for each equivalence classes that
// are constants of size one
std::vector<Node> const_codes;
- const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+ const std::vector<Node>& seqc = d_bsolver->getStringEqc();
for (const Node& eqc : seqc)
{
- NormalForm& nfe = d_csolver.getNormalForm(eqc);
+ NormalForm& nfe = d_csolver->getNormalForm(eqc);
if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst())
{
Node c = nfe.d_nf[0];
Node vc = nm->mkNode(STRING_TO_CODE, cp);
if (!d_state.areEqual(cc, vc))
{
- d_im.sendInference(d_empty_vec, cc.eqNode(vc), Inference::CODE_PROXY);
+ std::vector<Node> emptyVec;
+ d_im->sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
}
const_codes.push_back(vc);
}
}
}
}
- if (d_im.hasProcessed())
+ if (d_im->hasProcessed())
{
return;
}
Node eqn = c1[0].eqNode(c2[0]);
// str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
- d_im.sendPhaseRequirement(deq, false);
- d_im.sendInference(d_empty_vec, inj_lem, Inference::CODE_INJ);
+ d_im->sendPhaseRequirement(deq, false);
+ std::vector<Node> emptyVec;
+ d_im->sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
}
}
}
void TheoryStrings::checkRegisterTermsNormalForms()
{
- const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+ const std::vector<Node>& seqc = d_bsolver->getStringEqc();
for (const Node& eqc : seqc)
{
- NormalForm& nfi = d_csolver.getNormalForm(eqc);
+ NormalForm& nfi = d_csolver->getNormalForm(eqc);
// check if there is a length term for this equivalence class
EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
Node lt = ei ? ei->d_lengthTerm : Node::null();
Trace("strings-process") << "..." << std::endl;
switch (s)
{
- case CHECK_INIT: d_bsolver.checkInit(); break;
- case CHECK_CONST_EQC: d_bsolver.checkConstantEquivalenceClasses(); break;
+ case CHECK_INIT: d_bsolver->checkInit(); break;
+ case CHECK_CONST_EQC: d_bsolver->checkConstantEquivalenceClasses(); break;
case CHECK_EXTF_EVAL: d_esolver->checkExtfEval(effort); break;
- case CHECK_CYCLES: d_csolver.checkCycles(); break;
- case CHECK_FLAT_FORMS: d_csolver.checkFlatForms(); break;
+ case CHECK_CYCLES: d_csolver->checkCycles(); break;
+ case CHECK_FLAT_FORMS: d_csolver->checkFlatForms(); break;
case CHECK_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break;
- case CHECK_NORMAL_FORMS_EQ: d_csolver.checkNormalFormsEq(); break;
- case CHECK_NORMAL_FORMS_DEQ: d_csolver.checkNormalFormsDeq(); break;
+ case CHECK_NORMAL_FORMS_EQ: d_csolver->checkNormalFormsEq(); break;
+ case CHECK_NORMAL_FORMS_DEQ: d_csolver->checkNormalFormsDeq(); break;
case CHECK_CODES: checkCodes(); break;
- case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break;
+ case CHECK_LENGTH_EQC: d_csolver->checkLengthsEqc(); break;
case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break;
case CHECK_EXTF_REDUCTION: d_esolver->checkExtfReductions(effort); break;
case CHECK_MEMBERSHIP: d_rsolver->checkMemberships(); break;
- case CHECK_CARDINALITY: d_bsolver.checkCardinality(); break;
+ case CHECK_CARDINALITY: d_bsolver->checkCardinality(); break;
default: Unreachable(); break;
}
Trace("strings-process") << "Done " << s
- << ", addedFact = " << d_im.hasPendingFact()
- << ", addedLemma = " << d_im.hasPendingLemma()
+ << ", addedFact = " << d_im->hasPendingFact()
+ << ", addedLemma = " << d_im->hasPendingLemma()
<< ", conflict = " << d_state.isInConflict()
<< std::endl;
}
InferStep curr = d_infer_steps[i];
if (curr == BREAK)
{
- if (d_im.hasProcessed())
+ if (d_im->hasProcessed())
{
break;
}
SolverState& d_state;
};/* class TheoryStrings::NotifyClass */
- //--------------------------- helper functions
- /** get normal string
- *
- * This method returns the node that is equivalent to the normal form of x,
- * and adds the corresponding explanation to nf_exp.
- *
- * For example, if x = y ++ z is an assertion in the current context, then
- * this method returns the term y ++ z and adds x = y ++ z to nf_exp.
- */
- Node getNormalString(Node x, std::vector<Node>& nf_exp);
- //-------------------------- end helper functions
-
private:
// Constants
Node d_emptyString;
/** The term registry for this theory */
TermRegistry d_termReg;
/** The (custom) output channel of the theory of strings */
- InferenceManager d_im;
- std::vector< Node > d_empty_vec;
-private:
+ std::unique_ptr<InferenceManager> d_im;
+ private:
std::map< Node, Node > d_eqc_to_len_term;
* The base solver, responsible for reasoning about congruent terms and
* inferring constants for equivalence classes.
*/
- BaseSolver d_bsolver;
+ std::unique_ptr<BaseSolver> d_bsolver;
/**
* The core solver, responsible for reasoning about string concatenation
* with length constraints.
*/
- CoreSolver d_csolver;
+ std::unique_ptr<CoreSolver> d_csolver;
/**
* Extended function solver, responsible for reductions and simplifications
* involving extended string functions.
projects / cvc5.git / commitdiff