Adding support for reading wrong assumptions

[satlib.git] / glucose-syrup / simp / SimpSolver.h

diff --git a/glucose-syrup/simp/SimpSolver.h b/glucose-syrup/simp/SimpSolver.h
index 5f457a8..c7dcff7 100644 (file)
--- a/glucose-syrup/simp/SimpSolver.h
+++ b/glucose-syrup/simp/SimpSolver.h
@@ -193,7 +193,7 @@ class SimpSolver : public Solver {
     bool          backwardSubsumptionCheck (bool verbose = false);
     bool          eliminateVar             (Var v);
     void          extendModel              ();
     bool          backwardSubsumptionCheck (bool verbose = false);
     bool          eliminateVar             (Var v);
     void          extendModel              ();

-
+    void       unsatExplanation();

     void          removeClause             (CRef cr,bool inPurgatory=false);
     bool          strengthenClause         (CRef cr, Lit l);
     void          cleanUpClauses           ();
     void          removeClause             (CRef cr,bool inPurgatory=false);
     bool          strengthenClause         (CRef cr, Lit l);
     void          cleanUpClauses           ();