diff options
Diffstat (limited to 'src/decision/decision_engine.h')
| -rw-r--r-- | src/decision/decision_engine.h | 18 |
1 files changed, 4 insertions, 14 deletions
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 838e53b5a..c5325bc9a 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -24,11 +24,12 @@ #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" -#include "smt/term_formula_removal.h" #include "smt/smt_engine_scope.h" +#include "smt/term_formula_removal.h" using namespace std; using namespace CVC4::prop; @@ -173,21 +174,10 @@ public: /* return d_needIteSkolemMap.size() > 0; */ /* } */ - /* add a set of assertions */ - void addAssertions(const vector<Node> &assertions); - /** - * add a set of assertions, while providing a mapping between skolem - * variables and corresponding assertions. It is assumed that all - * assertions after assertionEnd were generated by ite - * removal. Hence, iteSkolemMap maps into only these. + * Add a list of assertions from an AssertionPipeline. */ - void addAssertions(const vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap); - - /* add a single assertion */ - void addAssertion(Node n); + void addAssertions(const preprocessing::AssertionPipeline& assertions); // Interface for Strategies to use stuff stored in Decision Engine // (which was possibly requested by them on initialization) |