diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 21 |
1 files changed, 8 insertions, 13 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c526decf1..8b71df31b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -50,21 +50,16 @@ struct SeqModelVarAttributeId }; using SeqModelVarAttribute = expr::Attribute<SeqModelVarAttributeId, Node>; -TheoryStrings::TheoryStrings(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm), +TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_STRINGS, env, out, valuation), d_notify(*this), d_statistics(), - d_state(c, u, d_valuation), + d_state(env, d_valuation), d_eagerSolver(d_state), - d_termReg(d_state, d_statistics, pnm), + d_termReg(d_state, d_statistics, d_pnm), d_extTheoryCb(), - d_extTheory(d_extTheoryCb, c, u, out), - d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm), + d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), + d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), d_im), d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), @@ -82,8 +77,8 @@ TheoryStrings::TheoryStrings(context::Context* c, d_csolver, d_esolver, d_statistics), - d_regexp_elim(options::regExpElimAgg(), pnm, u), - d_stringsFmf(c, u, valuation, d_termReg) + d_regexp_elim(options::regExpElimAgg(), d_pnm, getUserContext()), + d_stringsFmf(getSatContext(), getUserContext(), valuation, d_termReg) { d_termReg.finishInit(&d_im); |