diff options
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) |