summaryrefslogtreecommitdiff
path: root/src/decision/decision_strategy.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/decision/decision_strategy.h')
-rw-r--r--src/decision/decision_strategy.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index bad80d4ef..d26b28eeb 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -19,6 +19,7 @@
#ifndef __CVC4__DECISION__DECISION_STRATEGY_H
#define __CVC4__DECISION__DECISION_STRATEGY_H
+#include "preprocessing/assertion_pipeline.h"
#include "prop/sat_solver_types.h"
#include "smt/term_formula_removal.h"
@@ -57,9 +58,8 @@ public:
bool needIteSkolemMap() override { return true; }
- virtual void addAssertions(const std::vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap) = 0;
+ virtual void addAssertions(
+ const preprocessing::AssertionPipeline& assertions) = 0;
};/* class ITEDecisionStrategy */
class RelevancyStrategy : public ITEDecisionStrategy {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback