diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-10 09:29:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-10 16:29:09 +0200 |
commit | ac8cf53b07eb29687850f2ae64007f9f2688c9ad (patch) | |
tree | f62bad43ed45557a88f3d81df3d76536ee69cc38 /src/theory/combination_engine.cpp | |
parent | ce1acb3e31769e1ccb66075fe3b2151acae58ce6 (diff) |
Unify top-level substitutions and model substitutions (#6499)
This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.
The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.
There is no reason to have these two things be separate.
Diffstat (limited to 'src/theory/combination_engine.cpp')
-rw-r--r-- | src/theory/combination_engine.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 4b04188f1..33300ead8 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -29,9 +29,11 @@ namespace cvc5 { namespace theory { CombinationEngine::CombinationEngine(TheoryEngine& te, + Env& env, const std::vector<Theory*>& paraTheories, ProofNodeManager* pnm) : d_te(te), + d_env(env), d_valuation(&te), d_pnm(pnm), d_logicInfo(te.getLogicInfo()), @@ -51,7 +53,8 @@ CombinationEngine::CombinationEngine(TheoryEngine& te, d_eemanager.reset( new EqEngineManagerDistributed(d_te, *d_sharedSolver.get())); // make the distributed model manager - d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get())); + d_mmanager.reset( + new ModelManagerDistributed(d_te, d_env, *d_eemanager.get())); } else { |