diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-07 13:52:23 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-07 20:52:23 +0000 |
| commit | d3a160dee74b236cab32458fe8e5a3e653d28faf (patch) | |
| tree | 8ba0ca844cfccf2b310e0b63d682ed0aa3647c2f /src/theory/uf | |
| parent | 01cde22b7d69c1b1037cf1d536ca62becc3bd865 (diff) | |
Use `EnvObj` methods instead of `Theory` methods (#7144)
This removes the methods `getEnv()`, `options()`, `getSatContext()`, and
`getUserContext()` from the `Theory` class because they are now part of
`EnvObj`. Additionally, this commit converts the inference managers to
`EnvObj` because of there were some calls to retrieve the contexts from
`Theory` in those classes.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index bdc5304e4..07820a41d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -47,11 +47,11 @@ TheoryUF::TheoryUF(Env& env, : Theory(THEORY_UF, env, out, valuation, instanceName), d_thss(nullptr), d_ho(nullptr), - d_functionsTerms(getSatContext()), + d_functionsTerms(context()), d_symb(userContext(), instanceName), d_rewriter(logicInfo().isHigherOrder()), d_state(env, valuation), - d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false), + d_im(env, *this, d_state, d_pnm, "theory::uf::" + instanceName, false), d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true ); |