summaryrefslogtreecommitdiff
path: root/src/prop/sat_solver.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/sat_solver.h')
-rw-r--r--src/prop/sat_solver.h6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 055efa413..add73eebe 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -76,6 +76,12 @@ public:
/** Check the satisfiability of the added clauses */
virtual SatValue solve(long unsigned int&) = 0;
+ /** Check satisfiability under assumptions */
+ virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
+ {
+ Unimplemented("Solving under assumptions not implemented");
+ };
+
/** Interrupt the solver */
virtual void interrupt() = 0;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback