summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/inference_manager.cpp111
-rw-r--r--src/theory/strings/inference_manager.h35
-rw-r--r--src/theory/strings/theory_strings.cpp124
-rw-r--r--src/theory/strings/theory_strings.h28
4 files changed, 108 insertions, 190 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index dce038fbf..811c040f3 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -28,19 +28,17 @@ namespace CVC4 {
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));
@@ -49,14 +47,6 @@ InferenceManager::InferenceManager(context::Context* 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)
@@ -299,7 +289,7 @@ void InferenceManager::doPendingFacts()
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
@@ -308,13 +298,8 @@ void InferenceManager::doPendingFacts()
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();
@@ -392,68 +377,6 @@ void InferenceManager::doPendingLemmas()
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();
@@ -475,7 +398,6 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a,
{
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())
@@ -492,12 +414,12 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a,
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);
}
@@ -522,7 +444,6 @@ void InferenceManager::explain(TNode literal,
{
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;
@@ -530,14 +451,14 @@ void InferenceManager::explain(TNode literal,
{
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)
{
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 016891737..dc46f1683 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -29,6 +29,7 @@
#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 {
@@ -65,28 +66,20 @@ namespace strings {
* 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
@@ -292,23 +285,12 @@ class InferenceManager
// ------------------------------------------------- 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;
@@ -326,13 +308,6 @@ class InferenceManager
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
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 846f9240d..3e60cbc44 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -46,7 +46,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
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),
@@ -83,6 +83,8 @@ TheoryStrings::TheoryStrings(context::Context* c,
}
// 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() {
@@ -165,23 +167,6 @@ void TheoryStrings::notifySharedTerm(TNode t)
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")
@@ -252,24 +237,10 @@ void TheoryStrings::presolve() {
// 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
@@ -654,25 +625,68 @@ TrustNode TheoryStrings::expandDefinition(Node node)
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());
@@ -681,8 +695,10 @@ void TheoryStrings::check(Effort e) {
{
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() ){
@@ -726,7 +742,9 @@ void TheoryStrings::check(Effort e) {
++(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();
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index f4aa0675c..0f59e73dc 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -97,27 +97,33 @@ class TheoryStrings : public Theory {
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 */
@@ -171,8 +177,6 @@ class TheoryStrings : public Theory {
/** 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;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback