Adds the simplify and nclauses methods to some SAT solvers.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1584 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp
index 581bf2f21f3f48aa8123ff08d4058c71594079a0..ab0eeb0ad26ee92869734e3c0eb30b15279e35ff 100644 (file)
--- a/src/sat/MinisatCore.cpp
+++ b/src/sat/MinisatCore.cpp
@@ -88,6 +88,19 @@ namespace BEEV
       printf("CPU time              : %g s\n", cpu_time);
     }
 
+  template <class T>
+    int MinisatCore<T>::nClauses()
+  {
+    return s->nClauses();
+  }
+
+  template <class T>
+    bool MinisatCore<T>::simplify()
+  {
+    s->simplify();
+  }
+
+
 
   // I was going to make SimpSolver and Solver instances of this template.
   // But I'm not so sure now because I don't understand what eliminate() does in the simp solver.

diff --git a/src/sat/MinisatCore.h b/src/sat/MinisatCore.h
index 6259305e95f15bc65c3e76159742b46dd470c801..e81ce5ba4581304520c0013ab4a35864b3fcc573 100644 (file)
--- a/src/sat/MinisatCore.h
+++ b/src/sat/MinisatCore.h
@@ -51,6 +51,8 @@ namespace BEEV
     virtual lbool true_literal() {return ((uint8_t)0);}
     virtual lbool false_literal()  {return ((uint8_t)1);}
     virtual lbool undef_literal()  {return ((uint8_t)2);}
+
+    virtual int nClauses();
   };
 }
 ;

diff --git a/src/sat/SATSolver.h b/src/sat/SATSolver.h
index af0df23a214193ff5f89ac73939faa117c4980af..10913624429a6c181f31f7bad79d450344b67d4d 100644 (file)
--- a/src/sat/SATSolver.h
+++ b/src/sat/SATSolver.h
@@ -71,6 +71,18 @@ namespace BEEV
     virtual void setFrozen(Var x)
     {}
 
+    virtual int nClauses()
+    {
+      std::cerr << "Not yet implemented.";
+      exit(1);
+    }
+
+    virtual bool simplify()
+    {
+      std::cerr << "Not yet implemented.";
+      exit(1);
+
+    }
   };
 };
 #endif