diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8b71df31b..3e807c3ac 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -58,8 +58,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_eagerSolver(d_state), d_termReg(d_state, d_statistics, d_pnm), d_extTheoryCb(), - d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), - d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), d_im), + d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), + d_extTheory(d_extTheoryCb, context(), userContext(), d_im), d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), @@ -77,8 +77,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_csolver, d_esolver, d_statistics), - d_regexp_elim(options::regExpElimAgg(), d_pnm, getUserContext()), - d_stringsFmf(getSatContext(), getUserContext(), valuation, d_termReg) + d_regexp_elim(options::regExpElimAgg(), d_pnm, userContext()), + d_stringsFmf(context(), userContext(), valuation, d_termReg) { d_termReg.finishInit(&d_im); @@ -370,7 +370,7 @@ bool TheoryStrings::collectModelInfoType( argVal = nfe.d_nf[0][0]; } Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0]; - Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal)); + Node c = rewrite(nm->mkNode(SEQ_UNIT, argVal)); pure_eq_assign[eqc] = c; Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") "; m->getEqualityEngine()->addTerm(c); @@ -914,7 +914,7 @@ void TheoryStrings::checkCodes() Trace("strings-code-debug") << "Get proxy variable for " << c << std::endl; Node cc = nm->mkNode(kind::STRING_TO_CODE, c); - cc = Rewriter::rewrite(cc); + cc = rewrite(cc); Assert(cc.isConst()); Node cp = d_termReg.ensureProxyVariableFor(c); Node vc = nm->mkNode(STRING_TO_CODE, cp); @@ -958,7 +958,7 @@ void TheoryStrings::checkCodes() Node eqn = c1[0].eqNode(c2[0]); // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); - deq = Rewriter::rewrite(deq); + deq = rewrite(deq); d_im.addPendingPhaseRequirement(deq, false); std::vector<Node> emptyVec; d_im.sendInference(emptyVec, inj_lem, InferenceId::STRINGS_CODE_INJ); |