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.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 79e54cac2..102f8051b 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -95,7 +95,7 @@ public:
* Notify about a learnt clause.
*/
virtual void notify(SatClause& clause) = 0;
-};
+ };
virtual void setNotify(Notify* notify) = 0;
@@ -105,6 +105,8 @@ public:
virtual void addMarkerLiteral(SatLiteral lit) = 0;
+ virtual SatValue propagate() = 0;
+
virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0;
virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback