From 31717bf7c014bf1971cabcc9b871de5818278126 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Aug 2020 13:36:59 -0500 Subject: Make sets and strings solver states inherit from TheoryState (#4918) This is towards the new standard for theory solvers. This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager. Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class). --- src/theory/strings/inference_manager.cpp | 4 +- src/theory/strings/solver_state.cpp | 66 +------------------------------- src/theory/strings/solver_state.h | 50 +----------------------- src/theory/strings/theory_strings.cpp | 8 ++-- 4 files changed, 10 insertions(+), 118 deletions(-) (limited to 'src/theory/strings') diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 88cf6d958..a8ebd921a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -171,7 +171,7 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma) // only keep stats if we process it here d_statistics.d_inferences << ii.d_id; d_out.conflict(conf); - d_state.setConflict(); + d_state.notifyInConflict(); return; } Trace("strings-infer-debug") << "...as lemma" << std::endl; @@ -435,7 +435,7 @@ void InferenceManager::assertPendingFact(Node atom, bool polarity, Node exp) Trace("strings-pending") << "Process pending conflict " << pc << std::endl; Node conflictNode = mkExplain(a); - d_state.setConflict(); + d_state.notifyInConflict(); Trace("strings-conflict") << "CONFLICT: Eager prefix : " << conflictNode << std::endl; ++(d_statistics.d_conflictsEagerPrefix); diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 8634478fd..fd0f0174f 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -28,13 +28,7 @@ namespace strings { SolverState::SolverState(context::Context* c, context::UserContext* u, Valuation& v) - : d_context(c), - d_ucontext(u), - d_ee(nullptr), - d_eeDisequalities(c), - d_valuation(v), - d_conflict(c, false), - d_pendingConflict(c) + : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflict(c) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); } @@ -47,59 +41,6 @@ SolverState::~SolverState() } } -void SolverState::finishInit(eq::EqualityEngine* ee) -{ - Assert(ee != nullptr); - d_ee = ee; -} - -context::Context* SolverState::getSatContext() const { return d_context; } -context::UserContext* SolverState::getUserContext() const { return d_ucontext; } - -Node SolverState::getRepresentative(Node t) const -{ - if (d_ee->hasTerm(t)) - { - return d_ee->getRepresentative(t); - } - return t; -} - -bool SolverState::hasTerm(Node a) const { return d_ee->hasTerm(a); } - -bool SolverState::areEqual(Node a, Node b) const -{ - if (a == b) - { - return true; - } - else if (hasTerm(a) && hasTerm(b)) - { - return d_ee->areEqual(a, b); - } - return false; -} - -bool SolverState::areDisequal(Node a, Node b) const -{ - if (a == b) - { - return false; - } - else if (hasTerm(a) && hasTerm(b)) - { - Node ar = d_ee->getRepresentative(a); - Node br = d_ee->getRepresentative(b); - return (ar != br && ar.isConst() && br.isConst()) - || d_ee->areDisequal(ar, br, false); - } - Node ar = getRepresentative(a); - Node br = getRepresentative(b); - return ar != br && ar.isConst() && br.isConst(); -} - -eq::EqualityEngine* SolverState::getEqualityEngine() const { return d_ee; } - const context::CDList& SolverState::getDisequalityList() const { return d_eeDisequalities; @@ -199,7 +140,7 @@ EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake) return nullptr; } -TheoryModel* SolverState::getModel() const { return d_valuation.getModel(); } +TheoryModel* SolverState::getModel() { return d_valuation.getModel(); } void SolverState::addEndpointsToEqcInfo(Node t, Node concat, Node eqc) { @@ -286,9 +227,6 @@ bool SolverState::isEqualEmptyWord(Node s, Node& emps) return false; } -void SolverState::setConflict() { d_conflict = true; } -bool SolverState::isInConflict() const { return d_conflict; } - void SolverState::setPendingConflictWhen(Node conf) { if (!conf.isNull() && d_pendingConflict.get().isNull()) diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index 0322abdb7..fc27b847b 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -39,7 +39,7 @@ namespace strings { * (2) Whether the set of assertions is in conflict. * (3) Equivalence class information as in the class above. */ -class SolverState +class SolverState : public TheoryState { typedef context::CDList NodeList; @@ -48,35 +48,7 @@ class SolverState context::UserContext* u, Valuation& v); ~SolverState(); - /** - * Finish initialize, ee is a pointer to the official equality engine - * of theory of strings. - */ - void finishInit(eq::EqualityEngine* ee); - /** Get the SAT context */ - context::Context* getSatContext() const; - /** Get the user context */ - context::UserContext* getUserContext() const; //-------------------------------------- equality information - /** - * Get the representative of t in the equality engine of this class, or t - * itself if it is not registered as a term. - */ - Node getRepresentative(Node t) const; - /** Is t registered as a term in the equality engine of this class? */ - bool hasTerm(Node a) const; - /** - * Are a and b equal according to the equality engine of this class? Also - * returns true if a and b are identical. - */ - bool areEqual(Node a, Node b) const; - /** - * Are a and b disequal according to the equality engine of this class? Also - * returns true if the representative of a and b are distinct constants. - */ - bool areDisequal(Node a, Node b) const; - /** get equality engine */ - eq::EqualityEngine* getEqualityEngine() const; /** * Get the list of disequalities that are currently asserted to the equality * engine. @@ -92,14 +64,6 @@ class SolverState void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); //-------------------------------------- end notifications for equalities //------------------------------------------ conflicts - /** - * Set that the current state of the solver is in conflict. This should be - * called immediately after a call to conflict(...) on the output channel of - * the theory of strings. - */ - void setConflict(); - /** Are we currently in conflict? */ - bool isInConflict() const; /** set pending conflict * * If conf is non-null, this is called when conf is a conjunction of literals @@ -153,7 +117,7 @@ class SolverState */ EqcInfo* getOrMakeEqcInfo(Node eqc, bool doMake = true); /** Get pointer to the model object of the Valuation object */ - TheoryModel* getModel() const; + TheoryModel* getModel(); /** add endpoints to eqc info * @@ -186,21 +150,11 @@ class SolverState private: /** Common constants */ Node d_zero; - /** Pointer to the SAT context object used by the theory of strings. */ - context::Context* d_context; - /** Pointer to the user context object used by the theory of strings. */ - context::UserContext* d_ucontext; - /** Pointer to equality engine of the theory of strings. */ - eq::EqualityEngine* d_ee; /** * The (SAT-context-dependent) list of disequalities that have been asserted * to the equality engine above. */ NodeList d_eeDisequalities; - /** Reference to the valuation of the theory of strings */ - Valuation& d_valuation; - /** Are we in conflict? */ - context::CDO d_conflict; /** The pending conflict if one exists */ context::CDO d_pendingConflict; /** Map from representatives to their equivalence class information */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c78e8dc2a..6d81c742a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -81,6 +81,8 @@ TheoryStrings::TheoryStrings(context::Context* c, // add checkers d_sProofChecker.registerTo(pc); } + // use the state object as the official theory state + d_theoryState = &d_state; } TheoryStrings::~TheoryStrings() { @@ -126,8 +128,6 @@ void TheoryStrings::finishInit() d_equalityEngine->addFunctionKind(kind::STRING_TOLOWER, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_TOUPPER, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_REV, eagerEval); - - d_state.finishInit(d_equalityEngine); } std::string TheoryStrings::identify() const @@ -196,7 +196,7 @@ bool TheoryStrings::propagate(TNode literal) { // Propagate out bool ok = d_out->propagate(literal); if (!ok) { - d_state.setConflict(); + d_state.notifyInConflict(); } return ok; } @@ -762,7 +762,7 @@ void TheoryStrings::conflict(TNode a, TNode b){ if (!d_state.isInConflict()) { Debug("strings-conflict") << "Making conflict..." << std::endl; - d_state.setConflict(); + d_state.notifyInConflict(); TrustNode conflictNode = explain(a.eqNode(b)); Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode.getNode() -- cgit v1.2.3