1 files changed, 50 insertions, 0 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 679b9da8c..195323755 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -16,10 +16,60 @@
 #ifndef __CVC4__PROP__SAT_H
 #define __CVC4__PROP__SAT_H
 
+#define __CVC4_USE_MINISAT
+
+#ifdef __CVC4_USE_MINISAT
+
+#include "prop/minisat/core/Solver.h"
+#include "prop/minisat/core/SolverTypes.h"
+
 namespace CVC4 {
 namespace prop {
 
+/** The solver we are using */
+typedef minisat::Solver SatSolver;
+
+/** Type of the SAT variables */
+typedef minisat::Var SatVariable;
+
+/** Type of the Sat literals */
+typedef minisat::Lit SatLiteral;
+
+/** Type of the SAT clauses */
+typedef minisat::vec<SatLiteral> SatClause;
+
+/**
+ * Returns the variable of the literal.
+ * @param lit the literal
+ */
+inline SatVariable literalToVariable(SatLiteral lit) {
+  return minisat::var(lit);
+}
+
+inline bool literalSign(SatLiteral lit) {
+  return minisat::sign(lit);
+}
+
+inline std::ostream& operator << (std::ostream& out, SatLiteral lit) {
+  const char * s = (literalSign(lit)) ? "~" : " ";
+  out << s << literalToVariable(lit);
+  return out;
+}
+
+inline std::ostream& operator << (std::ostream& out, const SatClause& clause) {
+  out << "clause:";
+  for(int i = 0; i < clause.size(); ++i) {
+    out << " " << clause[i];
+  }
+  out << ";";
+  return out;
+}
+
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
+#endif
+
+
 #endif /* __CVC4__PROP__SAT_H */