diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-05 15:12:57 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-05 15:12:57 -0600 |
commit | bbba915f44f9e75eaa6238a10ba667643dacb00b (patch) | |
tree | 981c352e9aae8c96539374e98065101ee3835b28 /src/prop/prop_engine.h | |
parent | d26ee67911fedfef966a0e4d64ffda02007d65a0 (diff) |
Move ownership of DecisionEngine into PropEngine. (#3850)
This is in preparation of fixing the issue we currently have with reset-assertions.
This also removes a competition hack for QF_LRA.
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r-- | src/prop/prop_engine.h | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 061fbbca6..707244ff5 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -27,6 +27,7 @@ #include "expr/expr_stream.h" #include "expr/node.h" #include "options/options.h" +#include "preprocessing/assertion_pipeline.h" #include "proof/proof_manager.h" #include "util/resource_manager.h" #include "util/result.h" @@ -60,9 +61,8 @@ class PropEngine * Create a PropEngine with a particular decision and theory engine. */ PropEngine(TheoryEngine*, - DecisionEngine*, context::Context* satContext, - context::Context* userContext, + context::UserContext* userContext, std::ostream* replayLog, ExprStream* replayStream); @@ -105,6 +105,12 @@ class PropEngine TNode from = TNode::null()); /** + * Pass a list of assertions from an AssertionPipeline to the decision engine. + */ + void addAssertionsToDecisionEngine( + const preprocessing::AssertionPipeline& assertions); + + /** * If ever n is decided upon, it must be in the given phase. This * occurs *globally*, i.e., even if the literal is untranslated by * user pop and retranslated, it keeps this phase. The associated @@ -223,7 +229,7 @@ class PropEngine TheoryEngine* d_theoryEngine; /** The decision engine we will be using */ - DecisionEngine* d_decisionEngine; + std::unique_ptr<DecisionEngine> d_decisionEngine; /** The context */ context::Context* d_context; |