diff options
Diffstat (limited to 'src/prop/sat_solver.h')
-rw-r--r-- | src/prop/sat_solver.h | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 4fe24fc60..898709c43 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -73,15 +73,33 @@ public: class BVSatSolverInterface: public SatSolver { public: + /** Interface for notifications */ + class Notify { + public: + + virtual ~Notify() {}; + + /** + * If the notify returns false, the solver will break out of whatever it's currently doing + * with an "unknown" answer. + */ + virtual bool notify(SatLiteral lit) = 0; + + /** + * Notify about a learnt clause. + */ + virtual void notify(SatClause& clause) = 0; +}; + + virtual void setNotify(Notify* notify) = 0; + virtual void markUnremovable(SatLiteral lit) = 0; virtual void getUnsatCore(SatClause& unsatCore) = 0; virtual void addMarkerLiteral(SatLiteral lit) = 0; - virtual bool getPropagations(std::vector<SatLiteral>& propagations) = 0; - - virtual void explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0; + virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0; virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; |