This updates theory of strings to the new standard.
This makes strings use the standard template for check and collectModelInfo. It also updates its inference manager to the standard and makes use of assertFactInternal for processing internal facts. This now enables preNotifyFact and notifyFact to be defined in TheoryStrings instead of inside inference manager, which is clearer and eliminates some dependencies within inference manager.
Note that the inference manager of strings for now inherits from TheoryInferenceManager. Further standardization will make it inherit from the new InferenceManagerBuffered class.
This design will be merged into proof-new, which also has significant changes to strings inference manager.
namespace theory {
namespace strings {
-InferenceManager::InferenceManager(context::Context* c,
- context::UserContext* u,
+InferenceManager::InferenceManager(Theory& t,
SolverState& s,
TermRegistry& tr,
ExtTheory& e,
- OutputChannel& out,
- SequencesStatistics& statistics)
- : d_state(s),
+ SequencesStatistics& statistics,
+ ProofNodeManager* pnm)
+ : TheoryInferenceManager(t, s, pnm),
+ d_state(s),
d_termReg(tr),
d_extt(e),
- d_out(out),
- d_statistics(statistics),
- d_keep(c)
+ d_statistics(statistics)
{
NodeManager* nm = NodeManager::currentNM();
d_zero = nm->mkConst(Rational(0));
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)
TNode atom = polarity ? fact : fact[0];
// no double negation or double (conjunctive) conclusions
Assert(atom.getKind() != NOT && atom.getKind() != AND);
- assertPendingFact(atom, polarity, exp);
+ assertInternalFact(atom, polarity, exp);
}
}
else
TNode atom = polarity ? facts : facts[0];
// no double negation or double (conjunctive) conclusions
Assert(atom.getKind() != NOT && atom.getKind() != AND);
- assertPendingFact(atom, polarity, exp);
+ assertInternalFact(atom, polarity, exp);
}
- // Must reference count the equality and its explanation, which is not done
- // by the equality engine. Notice that we do not need to do this for
- // external assertions, which enter as facts through sendAssumption.
- d_keep.insert(facts);
- d_keep.insert(exp);
i++;
}
d_pending.clear();
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.notifyInConflict();
- 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();
{
utils::flattenOp(AND, ac, aconj);
}
- eq::EqualityEngine* ee = d_state.getEqualityEngine();
for (const Node& apc : aconj)
{
if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end())
Debug("strings-explain") << "Add to explanation " << apc << std::endl;
if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
{
- Assert(ee->hasTerm(apc[0][0]));
- Assert(ee->hasTerm(apc[0][1]));
+ Assert(d_ee->hasTerm(apc[0][0]));
+ Assert(d_ee->hasTerm(apc[0][1]));
// ensure that we are ready to explain the disequality
- AlwaysAssert(ee->areDisequal(apc[0][0], apc[0][1], true));
+ AlwaysAssert(d_ee->areDisequal(apc[0][0], apc[0][1], true));
}
- Assert(apc.getKind() != EQUAL || ee->areEqual(apc[0], apc[1]));
+ Assert(apc.getKind() != EQUAL || d_ee->areEqual(apc[0], apc[1]));
// now, explain
explain(apc, antec_exp);
}
{
Debug("strings-explain") << "Explain " << literal << " "
<< d_state.isInConflict() << std::endl;
- eq::EqualityEngine* ee = d_state.getEqualityEngine();
bool polarity = literal.getKind() != NOT;
TNode atom = polarity ? literal : literal[0];
std::vector<TNode> tassumptions;
{
if (atom[0] != atom[1])
{
- Assert(ee->hasTerm(atom[0]));
- Assert(ee->hasTerm(atom[1]));
- ee->explainEquality(atom[0], atom[1], polarity, tassumptions);
+ Assert(d_ee->hasTerm(atom[0]));
+ Assert(d_ee->hasTerm(atom[1]));
+ d_ee->explainEquality(atom[0], atom[1], polarity, tassumptions);
}
}
else
{
- ee->explainPredicate(atom, polarity, tassumptions);
+ d_ee->explainPredicate(atom, polarity, tassumptions);
}
for (const TNode a : tassumptions)
{
#include "theory/strings/sequences_stats.h"
#include "theory/strings/solver_state.h"
#include "theory/strings/term_registry.h"
+#include "theory/theory_inference_manager.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
* theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
* with the extended theory object e.g. markCongruent.
*/
-class InferenceManager
+class InferenceManager : public TheoryInferenceManager
{
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
public:
- InferenceManager(context::Context* c,
- context::UserContext* u,
+ InferenceManager(Theory& t,
SolverState& s,
TermRegistry& tr,
ExtTheory& e,
- OutputChannel& out,
- SequencesStatistics& statistics);
+ SequencesStatistics& statistics,
+ ProofNodeManager* pnm);
~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
// ------------------------------------------------- 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);
/** 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;
/** 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;
std::map<Node, bool> d_pendingReqPhase;
/** A list of pending lemmas to be sent on the output channel. */
std::vector<InferInfo> d_pendingLem;
- /**
- * The keep set of this class. This set is maintained to ensure that
- * facts and their explanations are ref-counted. Since facts and their
- * explanations are SAT-context-dependent, this set is also
- * SAT-context-dependent.
- */
- NodeSet d_keep;
};
} // namespace strings
d_state(c, u, d_valuation),
d_termReg(d_state, out, d_statistics, nullptr),
d_extTheory(this),
- d_im(c, u, d_state, d_termReg, d_extTheory, out, d_statistics),
+ d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm),
d_rewriter(&d_statistics.d_rewrites),
d_bsolver(d_state, d_im),
d_csolver(d_state, d_im, d_termReg, d_bsolver),
}
// use the state object as the official theory state
d_theoryState = &d_state;
+ // use the inference manager as the official inference manager
+ d_inferManager = &d_im;
}
TheoryStrings::~TheoryStrings() {
Debug("strings") << "TheoryStrings::notifySharedTerm() finished" << std::endl;
}
-EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
- if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
- {
- if (d_equalityEngine->areEqual(a, b))
- {
- // The terms are implied to be equal
- return EQUALITY_TRUE;
- }
- if (d_equalityEngine->areDisequal(a, b, false))
- {
- // The terms are implied to be dis-equal
- return EQUALITY_FALSE;
- }
- }
- return EQUALITY_UNKNOWN;
-}
-
bool TheoryStrings::propagateLit(TNode literal)
{
Debug("strings-propagate")
// MODEL GENERATION
/////////////////////////////////////////////////////////////////////////////
-bool TheoryStrings::collectModelInfo(TheoryModel* m)
+bool TheoryStrings::collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet)
{
- Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl;
- Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
-
- std::set<Node> termSet;
-
- // Compute terms appearing in assertions and shared terms
- const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
- computeAssertedTerms(termSet, irrKinds);
- // assert the (relevant) portion of the equality engine to the model
- if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
- {
- Unreachable()
- << "TheoryStrings::collectModelInfo: failed to assert equality engine"
- << std::endl;
- return false;
- }
+ Trace("strings-model") << "TheoryStrings : Collect model values" << std::endl;
std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet;
// Generate model
return TrustNode::null();
}
-void TheoryStrings::check(Effort e) {
- if (done() && e<EFFORT_FULL) {
- return;
+bool TheoryStrings::preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+ // this is only required for internal facts, others are already registered
+ if (isInternal && atom.getKind() == EQUAL)
+ {
+ // we must ensure these terms are registered
+ 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 (!d_equalityEngine->hasTerm(t) && t.getType().isStringLike())
+ {
+ d_termReg.registerTerm(t, 0);
+ }
+ }
}
+ return false;
+}
- TimerStat::CodeTimer checkTimer(d_checkTime);
-
- // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
- Trace("strings-check-debug")
- << "Theory of strings, check : " << e << std::endl;
- while (!done() && !d_state.isInConflict())
+void TheoryStrings::notifyFact(TNode atom,
+ bool polarity,
+ TNode fact,
+ bool isInternal)
+{
+ if (atom.getKind() == STRING_IN_REGEXP)
{
- // Get all the assertions
- Assertion assertion = get();
- TNode fact = assertion.d_assertion;
-
- Trace("strings-assertion") << "get assertion: " << fact << endl;
- d_im.sendAssumption(fact);
+ if (polarity && atom[1].getKind() == REGEXP_CONCAT)
+ {
+ Node eqc = d_equalityEngine->getRepresentative(atom[0]);
+ d_state.addEndpointsToEqcInfo(atom, atom[1], eqc);
+ }
}
+ // process pending conflicts due to reasoning about endpoints
+ 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);
+ Trace("strings-conflict")
+ << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
+ ++(d_statistics.d_conflictsEagerPrefix);
+ d_im.conflict(conflictNode);
+ return;
+ }
+ }
+ 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_extTheory.registerTermRec(atom);
+ Trace("strings-pending-debug") << " Finished collect terms" << std::endl;
+}
+
+void TheoryStrings::postCheck(Effort e)
+{
d_im.doPendingFacts();
Assert(d_strat.isStrategyInit());
{
Trace("strings-check-debug")
<< "Theory of strings " << e << " effort check " << std::endl;
- if(Trace.isOn("strings-eqc")) {
- for( unsigned t=0; t<2; t++ ) {
+ if (Trace.isOn("strings-eqc"))
+ {
+ for (unsigned t = 0; t < 2; t++)
+ {
eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
while( !eqcs2_i.isFinished() ){
++(d_statistics.d_strategyRuns);
Trace("strings-check") << " * Run strategy..." << std::endl;
runStrategy(e);
- // flush the facts
+ // Send the facts *and* the lemmas. We send lemmas regardless of whether
+ // we send facts since some lemmas cannot be dropped. Other lemmas are
+ // otherwise avoided by aborting the strategy when a fact is ready.
addedFact = d_im.hasPendingFact();
addedLemma = d_im.hasPendingLemma();
d_im.doPendingFacts();
void shutdown() override {}
/** add shared term */
void notifySharedTerm(TNode n) override;
- /** get equality status */
- EqualityStatus getEqualityStatus(TNode a, TNode b) override;
/** preregister term */
void preRegisterTerm(TNode n) override;
/** Expand definition */
TrustNode expandDefinition(Node n) override;
- /** Check at effort e */
- void check(Effort e) override;
- /** needs check last effort */
+ //--------------------------------- standard check
+ /** Do we need a check call at last call effort? */
bool needsCheckLastEffort() override;
+ bool preNotifyFact(TNode atom,
+ bool pol,
+ TNode fact,
+ bool isPrereg,
+ bool isInternal) override;
+ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+ /** Post-check, called after the fact queue of the theory is processed. */
+ void postCheck(Effort level) override;
+ //--------------------------------- end standard check
+ /** propagate method */
+ bool propagateLit(TNode literal);
/** Conflict when merging two constants */
void conflict(TNode a, TNode b);
/** called when a new equivalence class is created */
void eqNotifyNewClass(TNode t);
/** preprocess rewrite */
TrustNode ppRewrite(TNode atom) override;
- /**
- * Get all relevant information in this theory regarding the current
- * model. Return false if a contradiction is discovered.
- */
- bool collectModelInfo(TheoryModel* m) override;
+ /** Collect model values in m based on the relevant terms given by termSet */
+ bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet) override;
private:
/** NotifyClass for equality engine */
/** The solver state of the theory of strings */
SolverState& d_state;
};/* class TheoryStrings::NotifyClass */
- /** propagate method */
- bool propagateLit(TNode literal);
/** compute care graph */
void computeCareGraph() override;
/**
projects / cvc5.git / commitdiff