diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-22 14:12:23 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-22 19:12:23 +0000 |
| commit | 7295b8da3f77d0121ab0215a7f309dab90b02854 (patch) | |
| tree | 3ea57fb04d3a279460b5df4634c0bd13c40e2652 /src/prop/theory_proxy.cpp | |
| parent | 5c09e3f6e14f92b3c66b260837bd460973b4cc57 (diff) | |
Reorganizing use of skolem definition manager in prop engine (#6415)
Towards setting up the proper callbacks into the new justification heuristic.
Moves ownership of skolem definition manager from TheoryProxy to PropEngine.
Diffstat (limited to 'src/prop/theory_proxy.cpp')
| -rw-r--r-- | src/prop/theory_proxy.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 98a76ae1a..43f91f732 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -24,6 +24,7 @@ #include "proof/cnf_proof.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" +#include "prop/skolem_def_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -34,7 +35,8 @@ namespace prop { TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, - DecisionEngine* decisionEngine, + decision::DecisionEngine* decisionEngine, + SkolemDefManager* skdm, context::Context* context, context::UserContext* userContext, ProofNodeManager* pnm) @@ -44,7 +46,7 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, d_theoryEngine(theoryEngine), d_queue(context), d_tpp(*theoryEngine, userContext, pnm), - d_skdm(new SkolemDefManager(context, userContext)) + d_skdm(skdm) { } |