diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 587 |
1 files changed, 17 insertions, 570 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 23a41a0bb..8a3c32fd8 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -74,18 +74,19 @@ TheoryStrings::TheoryStrings(context::Context* c, d_im(*this, c, u, d_state, d_sk_cache, out), d_pregistered_terms_cache(u), d_registered_terms_cache(u), - d_preproc(&d_sk_cache, u), - d_extf_infer_cache(c), d_functionsTerms(c), - d_has_extf(c, false), d_has_str_code(false), d_bsolver(c, u, d_state, d_im), d_csolver(c, u, d_state, d_im, d_sk_cache, d_bsolver), + d_esolver(nullptr), d_regexp_solver(*this, d_state, d_im, c, u), d_stringsFmf(c, u, valuation, d_sk_cache), d_strategy_init(false) { setupExtTheory(); + ExtTheory* extt = getExtTheory(); + d_esolver.reset(new ExtfSolver( + c, u, d_state, d_im, d_sk_cache, d_bsolver, d_csolver, extt)); getExtTheory()->addFunctionKind(kind::STRING_SUBSTR); getExtTheory()->addFunctionKind(kind::STRING_STRIDOF); getExtTheory()->addFunctionKind(kind::STRING_ITOS); @@ -221,172 +222,12 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var for( unsigned i=0; i<vars.size(); i++ ){ Node n = vars[i]; Trace("strings-subs") << " get subs for " << n << "..." << std::endl; - Node s = getCurrentSubstitutionFor(effort, n, exp[n]); + Node s = d_esolver->getCurrentSubstitutionFor(effort, n, exp[n]); subs.push_back(s); } return true; } -Node TheoryStrings::getCurrentSubstitutionFor(int effort, - Node n, - std::vector<Node>& exp) -{ - if (effort >= 3) - { - // model values - Node mv = d_valuation.getModel()->getRepresentative(n); - Trace("strings-subs") << " model val : " << mv << std::endl; - return mv; - } - Node nr = d_state.getRepresentative(n); - Node c = d_bsolver.explainConstantEqc(n, nr, exp); - if (!c.isNull()) - { - return c; - } - else if (effort >= 1 && n.getType().isString()) - { - Assert(effort < 3); - // normal forms - NormalForm& nfnr = d_csolver.getNormalForm(nr); - Node ns = d_csolver.getNormalString(nfnr.d_base, exp); - Trace("strings-subs") << " normal eqc : " << ns << " " << nfnr.d_base - << " " << nr << std::endl; - if (!nfnr.d_base.isNull()) - { - d_im.addToExplanation(n, nfnr.d_base, exp); - } - return ns; - } - return n; -} - -bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) -{ - Assert(d_extf_info_tmp.find(n) != d_extf_info_tmp.end()); - if (!d_extf_info_tmp[n].d_model_active) - { - // n is not active in the model, no need to reduce - return false; - } - //determine the effort level to process the extf at - // 0 - at assertion time, 1+ - after no other reduction is applicable - int r_effort = -1; - // polarity : 1 true, -1 false, 0 neither - int pol = 0; - Kind k = n.getKind(); - if (n.getType().isBoolean() && !d_extf_info_tmp[n].d_const.isNull()) - { - pol = d_extf_info_tmp[n].d_const.getConst<bool>() ? 1 : -1; - } - if (k == STRING_STRCTN) - { - if (pol == 1) - { - r_effort = 1; - } - else if (pol == -1) - { - if (effort == 2) - { - Node x = n[0]; - Node s = n[1]; - std::vector<Node> lexp; - Node lenx = d_state.getLength(x, lexp); - Node lens = d_state.getLength(s, lexp); - if (d_state.areEqual(lenx, lens)) - { - Trace("strings-extf-debug") - << " resolve extf : " << n - << " based on equal lengths disequality." << std::endl; - // We can reduce negative contains to a disequality when lengths are - // equal. In other words, len( x ) = len( s ) implies - // ~contains( x, s ) reduces to x != s. - if (!d_state.areDisequal(x, s)) - { - // len( x ) = len( s ) ^ ~contains( x, s ) => x != s - lexp.push_back(lenx.eqNode(lens)); - lexp.push_back(n.negate()); - Node xneqs = x.eqNode(s).negate(); - d_im.sendInference(lexp, xneqs, "NEG-CTN-EQL", true); - } - // this depends on the current assertions, so we set that this - // inference is context-dependent. - isCd = true; - return true; - } - else - { - r_effort = 2; - } - } - } - } - else - { - if (k == STRING_SUBSTR) - { - r_effort = 1; - } - else if (k != STRING_IN_REGEXP) - { - r_effort = 2; - } - } - if (effort != r_effort) - { - // not the right effort level to reduce - return false; - } - Node c_n = pol == -1 ? n.negate() : n; - Trace("strings-process-debug") - << "Process reduction for " << n << ", pol = " << pol << std::endl; - if (k == STRING_STRCTN && pol == 1) - { - Node x = n[0]; - Node s = n[1]; - // positive contains reduces to a equality - Node sk1 = - d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1"); - Node sk2 = - d_sk_cache.mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_POST, "sc2"); - Node eq = Rewriter::rewrite(x.eqNode(utils::mkNConcat(sk1, s, sk2))); - std::vector<Node> exp_vec; - exp_vec.push_back(n); - d_im.sendInference(d_empty_vec, exp_vec, eq, "POS-CTN", true); - Trace("strings-extf-debug") - << " resolve extf : " << n << " based on positive contain reduction." - << std::endl; - Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n - << " => " << eq << std::endl; - // context-dependent because it depends on the polarity of n itself - isCd = true; - } - else if (k != kind::STRING_CODE) - { - NodeManager* nm = NodeManager::currentNM(); - Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF - || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL - || k == STRING_STRREPLALL || k == STRING_LEQ || k == STRING_TOLOWER - || k == STRING_TOUPPER || k == STRING_REV); - std::vector<Node> new_nodes; - Node res = d_preproc.simplify(n, new_nodes); - Assert(res != n); - new_nodes.push_back(res.eqNode(n)); - Node nnlem = - new_nodes.size() == 1 ? new_nodes[0] : nm->mkNode(AND, new_nodes); - nnlem = Rewriter::rewrite(nnlem); - Trace("strings-red-lemma") - << "Reduction_" << effort << " lemma : " << nnlem << std::endl; - Trace("strings-red-lemma") << "...from " << n << std::endl; - d_im.sendInference(d_empty_vec, nnlem, "Reduction", true); - Trace("strings-extf-debug") - << " resolve extf : " << n << " based on reduction." << std::endl; - isCd = false; - } - return true; -} - ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS ///////////////////////////////////////////////////////////////////////////// @@ -880,36 +721,9 @@ void TheoryStrings::check(Effort e) { bool TheoryStrings::needsCheckLastEffort() { if( options::stringGuessModel() ){ - return d_has_extf.get(); - }else{ - return false; - } -} - -void TheoryStrings::checkExtfReductions( int effort ) { - // 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 = getExtTheory()->getActive(); - Trace("strings-process") << " checking " << extf.size() << " active extf" - << std::endl; - for( unsigned i=0; i<extf.size(); i++ ){ - Assert(!d_state.isInConflict()); - Node n = extf[i]; - Trace("strings-process") << " check " << n << ", active in model=" - << d_extf_info_tmp[n].d_model_active << std::endl; - // whether the reduction was context-dependent - bool isCd = false; - bool ret = doReduction(effort, n, isCd); - if (ret) - { - getExtTheory()->markReduced(extf[i], isCd); - if (d_im.hasProcessed()) - { - return; - } - } + return d_esolver->hasExtendedFunctions(); } + return false; } void TheoryStrings::checkMemberships() @@ -918,14 +732,17 @@ void TheoryStrings::checkMemberships() std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP); // maps representatives to regular expression memberships in that class std::map<Node, std::vector<Node> > assertedMems; + const std::map<Node, ExtfInfoTmp>& einfo = d_esolver->getInfo(); + std::map<Node, ExtfInfoTmp>::const_iterator it; for (unsigned i = 0; i < mems.size(); i++) { Node n = mems[i]; Assert(n.getKind() == STRING_IN_REGEXP); - Assert(d_extf_info_tmp.find(n) != d_extf_info_tmp.end()); - if (!d_extf_info_tmp[n].d_const.isNull()) + it = einfo.find(n); + Assert(it != einfo.end()); + if (!it->second.d_const.isNull()) { - bool pol = d_extf_info_tmp[n].d_const.getConst<bool>(); + bool pol = it->second.d_const.getConst<bool>(); Trace("strings-process-debug") << " add membership : " << n << ", pol = " << pol << std::endl; Node r = d_state.getRepresentative(n[0]); @@ -1158,377 +975,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { Trace("strings-pending-debug") << " Finished collect terms" << std::endl; } -void TheoryStrings::checkExtfEval( int effort ) { - Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl; - d_extf_info_tmp.clear(); - NodeManager* nm = NodeManager::currentNM(); - bool has_nreduce = false; - std::vector< Node > terms = getExtTheory()->getActive(); - for (const Node& n : terms) - { - // Setup information about n, including if it is equal to a constant. - ExtfInfoTmp& einfo = d_extf_info_tmp[n]; - Node r = d_state.getRepresentative(n); - einfo.d_const = d_bsolver.getConstantEqc(r); - // Get the current values of the children of n. - // Notice that we look up the value of the direct children of n, and not - // their free variables. In other words, given a term: - // t = (str.replace "B" (str.replace x "A" "B") "C") - // we may build the explanation that: - // ((str.replace x "A" "B") = "B") => t = (str.replace "B" "B" "C") - // instead of basing this on the free variable x: - // (x = "A") => t = (str.replace "B" (str.replace "A" "A" "B") "C") - // Although both allow us to infer t = "C", it is important to use the - // first kind of inference since it ensures that its subterms have the - // expected values. Otherwise, we may in rare cases fail to realize that - // the subterm (str.replace x "A" "B") does not currently have the correct - // value, say in this example that (str.replace x "A" "B") != "B". - std::vector<Node> exp; - std::vector<Node> schildren; - bool schanged = false; - for (const Node& nc : n) - { - Node sc = getCurrentSubstitutionFor(effort, nc, exp); - schildren.push_back(sc); - schanged = schanged || sc != nc; - } - // If there is information involving the children, attempt to do an - // inference and/or mark n as reduced. - Node to_reduce; - if (schanged) - { - Node sn = nm->mkNode(n.getKind(), schildren); - Trace("strings-extf-debug") - << "Check extf " << n << " == " << sn - << ", constant = " << einfo.d_const << ", effort=" << effort << "..." - << std::endl; - einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end()); - // inference is rewriting the substituted node - Node nrc = Rewriter::rewrite( sn ); - //if rewrites to a constant, then do the inference and mark as reduced - if( nrc.isConst() ){ - if( effort<3 ){ - getExtTheory()->markReduced( n ); - Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; - std::vector< Node > exps; - // The following optimization gets the "symbolic definition" of - // an extended term. The symbolic definition of a term t is a term - // t' where constants are replaced by their corresponding proxy - // variables. - // For example, if lsym is a proxy variable for "", then - // str.replace( lsym, lsym, lsym ) is the symbolic definition for - // str.replace( "", "", "" ). It is generally better to use symbolic - // definitions when doing cd-rewriting for the purpose of minimizing - // clauses, e.g. we infer the unit equality: - // str.replace( lsym, lsym, lsym ) == "" - // instead of making this inference multiple times: - // x = "" => str.replace( x, x, x ) == "" - // y = "" => str.replace( y, y, y ) == "" - Trace("strings-extf-debug") << " get symbolic definition..." << std::endl; - Node nrs; - // only use symbolic definitions if option is set - if (options::stringInferSym()) - { - nrs = d_im.getSymbolicDefinition(sn, exps); - } - if( !nrs.isNull() ){ - Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl; - Node nrsr = Rewriter::rewrite(nrs); - // ensure the symbolic form is not rewritable - if (nrsr != nrs) - { - // we cannot use the symbolic definition if it rewrites - Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl; - nrs = Node::null(); - } - }else{ - Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl; - } - Node conc; - if( !nrs.isNull() ){ - Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl; - if (!d_state.areEqual(nrs, nrc)) - { - //infer symbolic unit - if( n.getType().isBoolean() ){ - conc = nrc==d_true ? nrs : nrs.negate(); - }else{ - conc = nrs.eqNode( nrc ); - } - einfo.d_exp.clear(); - } - }else{ - if (!d_state.areEqual(n, nrc)) - { - if( n.getType().isBoolean() ){ - if (d_state.areEqual(n, nrc == d_true ? d_false : d_true)) - { - einfo.d_exp.push_back(nrc == d_true ? n.negate() : n); - conc = d_false; - } - else - { - conc = nrc==d_true ? n : n.negate(); - } - }else{ - conc = n.eqNode( nrc ); - } - } - } - if( !conc.isNull() ){ - Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl; - d_im.sendInference( - einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true); - if (d_state.isInConflict()) - { - Trace("strings-extf-debug") << " conflict, return." << std::endl; - return; - } - } - }else{ - //check if it is already equal, if so, mark as reduced. Otherwise, do nothing. - if (d_state.areEqual(n, nrc)) - { - Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl; - einfo.d_model_active = false; - } - } - } - else - { - // if this was a predicate which changed after substitution + rewriting - if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n) - { - bool pol = einfo.d_const == d_true; - Node nrcAssert = pol ? nrc : nrc.negate(); - Node nAssert = pol ? n : n.negate(); - Assert(effort < 3); - einfo.d_exp.push_back(nAssert); - Trace("strings-extf-debug") << " decomposable..." << std::endl; - Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc - << ", const = " << einfo.d_const << std::endl; - // We send inferences internal here, which may help show unsat. - // However, we do not make a determination whether n can be marked - // reduced since this argument may be circular: we may infer than n - // can be reduced to something else, but that thing may argue that it - // can be reduced to n, in theory. - d_im.sendInternalInference( - einfo.d_exp, nrcAssert, effort == 0 ? "EXTF_d" : "EXTF_d-N"); - } - to_reduce = nrc; - } - } - else - { - to_reduce = n; - } - //if not reduced - if( !to_reduce.isNull() ){ - Assert(effort < 3); - if( effort==1 ){ - Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl; - } - checkExtfInference(n, to_reduce, einfo, effort); - if( Trace.isOn("strings-extf-list") ){ - Trace("strings-extf-list") << " * " << to_reduce; - if (!einfo.d_const.isNull()) - { - Trace("strings-extf-list") << ", const = " << einfo.d_const; - } - if( n!=to_reduce ){ - Trace("strings-extf-list") << ", from " << n; - } - Trace("strings-extf-list") << std::endl; - } - if (getExtTheory()->isActive(n) && einfo.d_model_active) - { - has_nreduce = true; - } - } - } - d_has_extf = has_nreduce; -} - -void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort ){ - if (in.d_const.isNull()) - { - return; - } - NodeManager* nm = NodeManager::currentNM(); - Trace("strings-extf-infer") << "checkExtfInference: " << n << " : " << nr - << " == " << in.d_const << std::endl; - - // add original to explanation - if (n.getType().isBoolean()) - { - // if Boolean, it's easy - in.d_exp.push_back(in.d_const.getConst<bool>() ? n : n.negate()); - } - else - { - // otherwise, must explain via base node - Node r = d_state.getRepresentative(n); - // explain using the base solver - d_bsolver.explainConstantEqc(n, r, in.d_exp); - } - - // d_extf_infer_cache stores whether we have made the inferences associated - // with a node n, - // this may need to be generalized if multiple inferences apply - - if (nr.getKind() == STRING_STRCTN) - { - Assert(in.d_const.isConst()); - bool pol = in.d_const.getConst<bool>(); - if ((pol && nr[1].getKind() == STRING_CONCAT) - || (!pol && nr[0].getKind() == STRING_CONCAT)) - { - // If str.contains( x, str.++( y1, ..., yn ) ), - // we may infer str.contains( x, y1 ), ..., str.contains( x, yn ) - // The following recognizes two situations related to the above reasoning: - // (1) If ~str.contains( x, yi ) holds for some i, we are in conflict, - // (2) If str.contains( x, yj ) already holds for some j, then the term - // str.contains( x, yj ) is irrelevant since it is satisfied by all models - // for str.contains( x, str.++( y1, ..., yn ) ). - - // Notice that the dual of the above reasoning also holds, i.e. - // If ~str.contains( str.++( x1, ..., xn ), y ), - // we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y ) - // This is also handled here. - if (d_extf_infer_cache.find(nr) == d_extf_infer_cache.end()) - { - d_extf_infer_cache.insert(nr); - - int index = pol ? 1 : 0; - std::vector<Node> children; - children.push_back(nr[0]); - children.push_back(nr[1]); - for (const Node& nrc : nr[index]) - { - children[index] = nrc; - Node conc = nm->mkNode(STRING_STRCTN, children); - conc = Rewriter::rewrite(pol ? conc : conc.negate()); - // check if it already (does not) hold - if (d_state.hasTerm(conc)) - { - if (d_state.areEqual(conc, d_false)) - { - // we are in conflict - d_im.sendInference(in.d_exp, conc, "CTN_Decompose"); - } - else if (getExtTheory()->hasFunctionKind(conc.getKind())) - { - // can mark as reduced, since model for n implies model for conc - getExtTheory()->markReduced(conc); - } - } - } - } - } - else - { - if (std::find(d_extf_info_tmp[nr[0]].d_ctn[pol].begin(), - d_extf_info_tmp[nr[0]].d_ctn[pol].end(), - nr[1]) - == d_extf_info_tmp[nr[0]].d_ctn[pol].end()) - { - Trace("strings-extf-debug") << " store contains info : " << nr[0] - << " " << pol << " " << nr[1] << std::endl; - // Store s (does not) contains t, since nr = (~)contains( s, t ) holds. - d_extf_info_tmp[nr[0]].d_ctn[pol].push_back(nr[1]); - d_extf_info_tmp[nr[0]].d_ctn_from[pol].push_back(n); - // Do transistive closure on contains, e.g. - // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ). - - // The following infers new (negative) contains based on the above - // reasoning, provided that ~contains( t, r ) does not - // already hold in the current context. We test this by checking that - // contains( t, r ) is not already asserted false in the current - // context. We also handle the case where contains( t, r ) is equivalent - // to t = r, in which case we check that t != r does not already hold - // in the current context. - - // Notice that form of the above inference is enough to find - // conflicts purely due to contains predicates. For example, if we - // have only positive occurrences of contains, then no conflicts due to - // contains predicates are possible and this schema does nothing. For - // example, note that contains( s, t ) and contains( t, r ) implies - // contains( s, r ), which we could but choose not to infer. Instead, - // we prefer being lazy: only if ~contains( s, r ) appears later do we - // infer ~contains( t, r ), which suffices to show a conflict. - bool opol = !pol; - for (unsigned i = 0, size = d_extf_info_tmp[nr[0]].d_ctn[opol].size(); - i < size; - i++) - { - Node onr = d_extf_info_tmp[nr[0]].d_ctn[opol][i]; - Node concOrig = - nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]); - Node conc = Rewriter::rewrite(concOrig); - // For termination concerns, we only do the inference if the contains - // does not rewrite (and thus does not introduce new terms). - if (conc == concOrig) - { - bool do_infer = false; - conc = conc.negate(); - bool pol = conc.getKind() != NOT; - Node lit = pol ? conc : conc[0]; - if (lit.getKind() == EQUAL) - { - do_infer = pol ? !d_state.areEqual(lit[0], lit[1]) - : !d_state.areDisequal(lit[0], lit[1]); - } - else - { - do_infer = !d_state.areEqual(lit, pol ? d_true : d_false); - } - if (do_infer) - { - std::vector<Node> exp_c; - exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end()); - Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i]; - Assert(d_extf_info_tmp.find(ofrom) != d_extf_info_tmp.end()); - exp_c.insert(exp_c.end(), - d_extf_info_tmp[ofrom].d_exp.begin(), - d_extf_info_tmp[ofrom].d_exp.end()); - d_im.sendInference(exp_c, conc, "CTN_Trans"); - } - } - } - } - else - { - // If we already know that s (does not) contain t, then n is redundant. - // For example, if str.contains( x, y ), str.contains( z, y ), and x=z - // are asserted in the current context, then str.contains( z, y ) is - // satisfied by all models of str.contains( x, y ) ^ x=z and thus can - // be ignored. - Trace("strings-extf-debug") << " redundant." << std::endl; - getExtTheory()->markReduced(n); - } - } - return; - } - - // If it's not a predicate, see if we can solve the equality n = c, where c - // is the constant that extended term n is equal to. - Node inferEq = nr.eqNode(in.d_const); - Node inferEqr = Rewriter::rewrite(inferEq); - Node inferEqrr = inferEqr; - if (inferEqr.getKind() == EQUAL) - { - // try to use the extended rewriter for equalities - inferEqrr = TheoryStringsRewriter::rewriteEqualityExt(inferEqr); - } - if (inferEqrr != inferEqr) - { - inferEqrr = Rewriter::rewrite(inferEqrr); - Trace("strings-extf-infer") << "checkExtfInference: " << inferEq - << " ...reduces to " << inferEqrr << std::endl; - d_im.sendInternalInference(in.d_exp, inferEqrr, "EXTF_equality_rew"); - } -} - void TheoryStrings::checkRegisterTermsPreNormalForm() { const std::vector<Node>& seqc = d_bsolver.getStringEqc(); @@ -1822,7 +1268,8 @@ Node TheoryStrings::ppRewrite(TNode atom) { if( !options::stringLazyPreproc() ){ //eager preprocess here std::vector< Node > new_nodes; - Node ret = d_preproc.processAssertion( atom, new_nodes ); + StringsPreprocess* p = d_esolver->getPreprocess(); + Node ret = p->processAssertion(atom, new_nodes); if( ret!=atom ){ Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; for( unsigned i=0; i<new_nodes.size(); i++ ){ @@ -1870,7 +1317,7 @@ void TheoryStrings::runInferStep(InferStep s, int effort) { case CHECK_INIT: d_bsolver.checkInit(); break; case CHECK_CONST_EQC: d_bsolver.checkConstantEquivalenceClasses(); break; - case CHECK_EXTF_EVAL: checkExtfEval(effort); 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_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break; @@ -1879,7 +1326,7 @@ void TheoryStrings::runInferStep(InferStep s, int effort) case CHECK_CODES: checkCodes(); break; case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break; case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break; - case CHECK_EXTF_REDUCTION: checkExtfReductions(effort); break; + case CHECK_EXTF_REDUCTION: d_esolver->checkExtfReductions(effort); break; case CHECK_MEMBERSHIP: checkMemberships(); break; case CHECK_CARDINALITY: checkCardinality(); break; default: Unreachable(); break; |