diff options
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/solver_state.cpp | 31 | ||||
| -rw-r--r-- | src/theory/strings/solver_state.h | 10 | ||||
| -rw-r--r-- | src/theory/strings/term_registry.cpp | 21 | ||||
| -rw-r--r-- | src/theory/strings/term_registry.h | 3 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 144 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 18 |
6 files changed, 127 insertions, 100 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index a554ac595..8634478fd 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -27,11 +27,10 @@ namespace strings { SolverState::SolverState(context::Context* c, context::UserContext* u, - eq::EqualityEngine& ee, Valuation& v) : d_context(c), d_ucontext(u), - d_ee(ee), + d_ee(nullptr), d_eeDisequalities(c), d_valuation(v), d_conflict(c, false), @@ -48,19 +47,25 @@ 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)) + if (d_ee->hasTerm(t)) { - return d_ee.getRepresentative(t); + return d_ee->getRepresentative(t); } return t; } -bool SolverState::hasTerm(Node a) const { return d_ee.hasTerm(a); } +bool SolverState::hasTerm(Node a) const { return d_ee->hasTerm(a); } bool SolverState::areEqual(Node a, Node b) const { @@ -70,7 +75,7 @@ bool SolverState::areEqual(Node a, Node b) const } else if (hasTerm(a) && hasTerm(b)) { - return d_ee.areEqual(a, b); + return d_ee->areEqual(a, b); } return false; } @@ -83,17 +88,17 @@ bool SolverState::areDisequal(Node a, Node b) const } else if (hasTerm(a) && hasTerm(b)) { - Node ar = d_ee.getRepresentative(a); - Node br = d_ee.getRepresentative(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); + || 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; } +eq::EqualityEngine* SolverState::getEqualityEngine() const { return d_ee; } const context::CDList<Node>& SolverState::getDisequalityList() const { @@ -105,7 +110,7 @@ void SolverState::eqNotifyNewClass(TNode t) Kind k = t.getKind(); if (k == STRING_LENGTH || k == STRING_TO_CODE) { - Node r = d_ee.getRepresentative(t[0]); + Node r = d_ee->getRepresentative(t[0]); EqcInfo* ei = getOrMakeEqcInfo(r); if (k == STRING_LENGTH) { @@ -317,14 +322,14 @@ void SolverState::separateByLength( NodeManager* nm = NodeManager::currentNM(); for (const Node& eqc : n) { - Assert(d_ee.getRepresentative(eqc) == eqc); + Assert(d_ee->getRepresentative(eqc) == eqc); TypeNode tnEqc = eqc.getType(); EqcInfo* ei = getOrMakeEqcInfo(eqc, false); Node lt = ei ? ei->d_lengthTerm : Node::null(); if (!lt.isNull()) { lt = nm->mkNode(STRING_LENGTH, lt); - Node r = d_ee.getRepresentative(lt); + Node r = d_ee->getRepresentative(lt); std::pair<Node, TypeNode> lkey(r, tnEqc); if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end()) { diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index 8d3162b38..0322abdb7 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -46,9 +46,13 @@ class SolverState public: SolverState(context::Context* c, context::UserContext* u, - eq::EqualityEngine& ee, 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 */ @@ -186,8 +190,8 @@ class SolverState context::Context* d_context; /** Pointer to the user context object used by the theory of strings. */ context::UserContext* d_ucontext; - /** Reference to equality engine of the theory of strings. */ - eq::EqualityEngine& d_ee; + /** 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. diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index f28db4c35..71b45915f 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -37,12 +37,10 @@ typedef expr::Attribute<StringsProxyVarAttributeId, bool> StringsProxyVarAttribute; TermRegistry::TermRegistry(SolverState& s, - eq::EqualityEngine& ee, OutputChannel& out, SequencesStatistics& statistics, ProofNodeManager* pnm) : d_state(s), - d_ee(ee), d_out(out), d_statistics(statistics), d_hasStrCode(false), @@ -129,6 +127,7 @@ void TermRegistry::preRegisterTerm(TNode n) { return; } + eq::EqualityEngine* ee = d_state.getEqualityEngine(); d_preregisteredTerms.insert(n); Trace("strings-preregister") << "TheoryString::preregister : " << n << std::endl; @@ -156,15 +155,15 @@ void TermRegistry::preRegisterTerm(TNode n) ss << "Equality between regular expressions is not supported"; throw LogicException(ss.str()); } - d_ee.addTriggerEquality(n); + ee->addTriggerEquality(n); return; } else if (k == STRING_IN_REGEXP) { d_out.requirePhase(n, true); - d_ee.addTriggerPredicate(n); - d_ee.addTerm(n[0]); - d_ee.addTerm(n[1]); + ee->addTriggerPredicate(n); + ee->addTerm(n[0]); + ee->addTerm(n[1]); return; } else if (k == STRING_TO_CODE) @@ -196,17 +195,17 @@ void TermRegistry::preRegisterTerm(TNode n) } } } - d_ee.addTerm(n); + ee->addTerm(n); } else if (tn.isBoolean()) { // Get triggered for both equal and dis-equal - d_ee.addTriggerPredicate(n); + ee->addTriggerPredicate(n); } else { // Function applications/predicates - d_ee.addTerm(n); + ee->addTerm(n); } // Set d_functionsTerms stores all function applications that are // relevant to theory combination. Notice that this is a subset of @@ -216,7 +215,7 @@ void TermRegistry::preRegisterTerm(TNode n) // Concatenation terms do not need to be considered here because // their arguments have string type and do not introduce any shared // terms. - if (n.hasOperator() && d_ee.isFunctionKind(k) && k != STRING_CONCAT) + if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT) { d_functionsTerms.push_back(n); } @@ -313,7 +312,7 @@ void TermRegistry::registerType(TypeNode tn) { // preregister the empty word for the type Node emp = Word::mkEmptyWord(tn); - if (!d_ee.hasTerm(emp)) + if (!d_state.hasTerm(emp)) { preRegisterTerm(emp); } diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 2048abec1..45fb40073 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -50,7 +50,6 @@ class TermRegistry public: TermRegistry(SolverState& s, - eq::EqualityEngine& ee, OutputChannel& out, SequencesStatistics& statistics, ProofNodeManager* pnm); @@ -220,8 +219,6 @@ class TermRegistry uint32_t d_cardSize; /** Reference to the solver state of the theory of strings. */ SolverState& d_state; - /** Reference to equality engine of the theory of strings. */ - eq::EqualityEngine& d_ee; /** Reference to the output channel of the theory of strings. */ OutputChannel& d_out; /** Reference to the statistics for the theory of strings/sequences. */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0ad887d2f..b23765313 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -43,9 +43,8 @@ TheoryStrings::TheoryStrings(context::Context* c, : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm), d_notify(*this), d_statistics(), - d_equalityEngine(d_notify, c, "theory::strings::ee", true), - d_state(c, u, d_equalityEngine, d_valuation), - d_termReg(d_state, d_equalityEngine, out, d_statistics, nullptr), + 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_rewriter(&d_statistics.d_rewrites), @@ -67,30 +66,6 @@ TheoryStrings::TheoryStrings(context::Context* c, d_statistics), d_stringsFmf(c, u, valuation, d_termReg) { - bool eagerEval = options::stringEagerEval(); - // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::STRING_LENGTH, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_CONCAT, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_TO_CODE, eagerEval); - d_equalityEngine.addFunctionKind(kind::SEQ_UNIT, eagerEval); - - // extended functions - d_equalityEngine.addFunctionKind(kind::STRING_STRCTN, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_LEQ, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_UPDATE, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_ITOS, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_STOI, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_STRREPL, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_STRREPLALL, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER, eagerEval); - d_equalityEngine.addFunctionKind(kind::STRING_REV, eagerEval); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -113,26 +88,63 @@ TheoryStrings::~TheoryStrings() { } TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; } -std::string TheoryStrings::identify() const -{ - return std::string("TheoryStrings"); -} -eq::EqualityEngine* TheoryStrings::getEqualityEngine() + +bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi) { - return &d_equalityEngine; + esi.d_notify = &d_notify; + esi.d_name = "theory::strings::ee"; + return true; } + void TheoryStrings::finishInit() { + Assert(d_equalityEngine != nullptr); + // witness is used to eliminate str.from_code d_valuation.setUnevaluatedKind(WITNESS); + + bool eagerEval = options::stringEagerEval(); + // The kinds we are treating as function application in congruence + d_equalityEngine->addFunctionKind(kind::STRING_LENGTH, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_CONCAT, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_IN_REGEXP, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_TO_CODE, eagerEval); + d_equalityEngine->addFunctionKind(kind::SEQ_UNIT, eagerEval); + // extended functions + d_equalityEngine->addFunctionKind(kind::STRING_STRCTN, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_LEQ, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_SUBSTR, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_UPDATE, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_ITOS, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_STOI, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_STRIDOF, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_STRREPL, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval); + 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 +{ + return std::string("TheoryStrings"); } bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { - Assert(d_equalityEngine.hasTerm(x)); - Assert(d_equalityEngine.hasTerm(y)); - if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){ - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS); + Assert(d_equalityEngine->hasTerm(x)); + Assert(d_equalityEngine->hasTerm(y)); + if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS) + && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS)) + { + TNode x_shared = + d_equalityEngine->getTriggerTermRepresentative(x, THEORY_STRINGS); + TNode y_shared = + d_equalityEngine->getTriggerTermRepresentative(y, THEORY_STRINGS); EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ return true; @@ -141,14 +153,10 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { return false; } -void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_equalityEngine.setMasterEqualityEngine(eq); -} - void TheoryStrings::addSharedTerm(TNode t) { Debug("strings") << "TheoryStrings::addSharedTerm(): " << t << " " << t.getType().isBoolean() << endl; - d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS); + d_equalityEngine->addTriggerTerm(t, THEORY_STRINGS); if (options::stringExp()) { d_esolver.addSharedTerm(t); @@ -157,12 +165,15 @@ void TheoryStrings::addSharedTerm(TNode t) { } EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) { - if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){ - if (d_equalityEngine.areEqual(a, 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)) { + if (d_equalityEngine->areDisequal(a, b, false)) + { // The terms are implied to be dis-equal return EQUALITY_FALSE; } @@ -251,7 +262,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) // Compute terms appearing in assertions and shared terms computeRelevantTerms(termSet); // assert the (relevant) portion of the equality engine to the model - if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) + if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) { Unreachable() << "TheoryStrings::collectModelInfo: failed to assert equality engine" @@ -670,14 +681,15 @@ void TheoryStrings::check(Effort e) { << "Theory of strings " << e << " effort check " << std::endl; if(Trace.isOn("strings-eqc")) { for( unsigned t=0; t<2; t++ ) { - eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine ); + eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine); Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl; while( !eqcs2_i.isFinished() ){ Node eqc = (*eqcs2_i); bool print = (t == 0 && eqc.getType().isStringLike()) || (t == 1 && !eqc.getType().isStringLike()); if (print) { - eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + eq::EqClassIterator eqc2_i = + eq::EqClassIterator(eqc, d_equalityEngine); Trace("strings-eqc") << "Eqc( " << eqc << " ) : { "; while( !eqc2_i.isFinished() ) { if( (*eqc2_i)!=eqc && (*eqc2_i).getKind()!=kind::EQUAL ){ @@ -779,20 +791,26 @@ void TheoryStrings::addCarePairs(TNodeTrie* t1, if( t2!=NULL ){ Node f1 = t1->getData(); Node f2 = t2->getData(); - if( !d_equalityEngine.areEqual( f1, f2 ) ){ + if (!d_equalityEngine->areEqual(f1, f2)) + { Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; vector< pair<TNode, TNode> > currentPairs; for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { TNode x = f1[k]; TNode y = f2[k]; - Assert(d_equalityEngine.hasTerm(x)); - Assert(d_equalityEngine.hasTerm(y)); - Assert(!d_equalityEngine.areDisequal(x, y, false)); + Assert(d_equalityEngine->hasTerm(x)); + Assert(d_equalityEngine->hasTerm(y)); + Assert(!d_equalityEngine->areDisequal(x, y, false)); Assert(!areCareDisequal(x, y)); - if( !d_equalityEngine.areEqual( x, y ) ){ - if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){ - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS); + if (!d_equalityEngine->areEqual(x, y)) + { + if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS) + && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS)) + { + TNode x_shared = d_equalityEngine->getTriggerTermRepresentative( + x, THEORY_STRINGS); + TNode y_shared = d_equalityEngine->getTriggerTermRepresentative( + y, THEORY_STRINGS); currentPairs.push_back(make_pair(x_shared, y_shared)); } } @@ -820,7 +838,8 @@ void TheoryStrings::addCarePairs(TNodeTrie* t1, std::map<TNode, TNodeTrie>::iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ - if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ + if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) + { if( !areCareDisequal(it->first, it2->first) ){ addCarePairs( &it->second, &it2->second, arity, depth+1 ); } @@ -833,7 +852,7 @@ void TheoryStrings::addCarePairs(TNodeTrie* t1, { for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data) { - if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false)) + if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) { if (!areCareDisequal(tt1.first, tt2.first)) { @@ -862,8 +881,9 @@ void TheoryStrings::computeCareGraph(){ std::vector< TNode > reps; bool has_trigger_arg = false; for( unsigned j=0; j<f1.getNumChildren(); j++ ){ - reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) ); - if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_STRINGS ) ){ + reps.push_back(d_equalityEngine->getRepresentative(f1[j])); + if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_STRINGS)) + { has_trigger_arg = true; } } @@ -889,7 +909,7 @@ void TheoryStrings::checkRegisterTermsPreNormalForm() const std::vector<Node>& seqc = d_bsolver.getStringEqc(); for (const Node& eqc : seqc) { - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine); while (!eqc_i.isFinished()) { Node n = (*eqc_i); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 2fb827429..500daac1f 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -70,20 +70,24 @@ class TheoryStrings : public Theory { const LogicInfo& logicInfo, ProofNodeManager* pnm); ~TheoryStrings(); + //--------------------------------- initialization + /** get the official theory rewriter of this theory */ + TheoryRewriter* getTheoryRewriter() override; + /** + * Returns true if we need an equality engine. If so, we initialize the + * information regarding how it should be setup. For details, see the + * documentation in Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(EeSetupInfo& esi) override; /** finish initialization */ void finishInit() override; - /** Get the theory rewriter of this class */ - TheoryRewriter* getTheoryRewriter() override; - /** Set the master equality engine */ - void setMasterEqualityEngine(eq::EqualityEngine* eq) override; + //--------------------------------- end initialization /** Identify this theory */ std::string identify() const override; /** Propagate */ void propagate(Effort e) override; /** Explain */ TrustNode explain(TNode literal) override; - /** Get the equality engine */ - eq::EqualityEngine* getEqualityEngine() override; /** Get current substitution */ bool getCurrentSubstitution(int effort, std::vector<Node>& vars, @@ -268,8 +272,6 @@ class TheoryStrings : public Theory { * theories is collected in this object. */ SequencesStatistics d_statistics; - /** Equaltity engine */ - eq::EqualityEngine d_equalityEngine; /** The solver state object */ SolverState d_state; /** The term registry for this theory */ |