From 0b5ab053092ea88fa6115edbe6f0fa1ba4b6288c Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 12 Mar 2012 00:12:51 +0000
Subject: [PATCH] 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
---
 src/sat/MinisatCore.cpp | 13 +++++++++++++
 src/sat/MinisatCore.h   |  2 ++
 src/sat/SATSolver.h     | 12 ++++++++++++
 3 files changed, 27 insertions(+)

diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp
index 581bf2f..ab0eeb0 100644
--- 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 6259305..e81ce5b 100644
--- 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 af0df23..1091362 100644
--- 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
-- 
2.47.3