diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-09 12:44:03 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-09 12:44:03 -0600 |
| commit | b1f4694c582a315feccb4c0c7e1a683583ff29e8 (patch) | |
| tree | 9f18c1564867206a4abbd1bb51dcb190359cd5c7 /src/decision/decision_engine.h | |
| parent | 59cd96a33b8f32405be2a20fc8230efc33b8dcdc (diff) | |
Make decision engine independent of AssertionsPipeline (#5626)
This PR makes decision engine independent of AssertionsPipeline, which consequently allows some of the key PropEngine interfaces to be consolidated. It also modifies PropEngine to take TrustNode for assertLemma, which is the first step for making PropEngine manage proofs from TheoryEngine.
This is in preparation for modifying the interplay between PropEngine, TheoryEngine, TheoryPreprocessor, and new proposed SAT relevancy heuristic.
There are no intended behavior changes in this PR.
Marking "major" since this impacts several current directions (including proof-new integration, lazy theory preprocessing, SAT relevancy).
Diffstat (limited to 'src/decision/decision_engine.h')
| -rw-r--r-- | src/decision/decision_engine.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 52e1e2d1a..afa16397d 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -24,7 +24,6 @@ #include "base/output.h" #include "decision/decision_strategy.h" #include "expr/node.h" -#include "preprocessing/assertion_pipeline.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" @@ -142,9 +141,12 @@ class DecisionEngine { // External World helping us help the Strategies /** - * Add a list of assertions from an AssertionPipeline. + * Add a list of assertions, as well as lemmas coming from preprocessing + * (ppLemmas) and pairwise the skolems they constrain (ppSkolems). */ - void addAssertions(const preprocessing::AssertionPipeline& assertions); + void addAssertions(const std::vector<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& ppSkolems); // Interface for Strategies to use stuff stored in Decision Engine // (which was possibly requested by them on initialization) |