1 files changed, 1 insertions, 123 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 61c67ed5f..f18335048 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -26,135 +26,13 @@
 #include "util/options.h"
 #include "util/stats.h"
 #include "context/cdlist.h"
+#include "prop/sat_solver_types.h"
 
 namespace CVC4 {
 namespace prop {
 
 class TheoryProxy; 
 
-/**
- * Boolean values of the SAT solver.
- */
-enum SatValue {
-  SAT_VALUE_UNKNOWN,
-  SAT_VALUE_TRUE, 
-  SAT_VALUE_FALSE 
-};
-
-/**
- * A variable of the SAT solver.
- */
-typedef uint64_t SatVariable; 
-
-/**
- * Undefined SAT solver variable.
- */
-const SatVariable undefSatVariable = SatVariable(-1); 
-
-/**
- * A SAT literal is a variable or an negated variable.
- */
-class SatLiteral {
-
-  /**
-   * The value holds the variable and a bit noting if the variable is negated.
-   */
-  uint64_t d_value;
-
-public:
-
-  /**
-   * Construct an undefined SAT literal.
-   */
-  SatLiteral()
-  : d_value(undefSatVariable)
-  {}
-  
-  /**
-   * Construct a literal given a possible negated variable.
-   */
-  SatLiteral(SatVariable var, bool negated = false) {
-    d_value = var + var + (int)negated;
-  }
-
-  /**
-   * Returns the variable of the literal.
-   */
-  SatVariable getSatVariable() const {
-    return d_value >> 1;
-  }
-
-  /**
-   * Returns true if the literal is a negated variable.
-   */
-  bool isNegated() const {
-    return d_value & 1;
-  }
-
-  /**
-   * Negate the given literal.
-   */
-  SatLiteral operator ~ () const {
-    return SatLiteral(getSatVariable(), !isNegated()); 
-  }
-
-  /**
-   * Compare two literals for equality.
-   */
-  bool operator == (const SatLiteral& other) const {
-    return d_value == other.d_value; 
-  }
-
-  /**
-   * Compare two literals for dis-equality.
-   */
-  bool operator != (const SatLiteral& other) const {
-    return !(*this == other); 
-  }
-
-  /**
-   * Returns a string representation of the literal.
-   */
-  std::string toString() const {
-    std::ostringstream os;
-    os << (isNegated()? "~" : "") << getSatVariable() << " ";
-    return os.str();
-  }
-
-  /**
-   * Returns the hash value of a literal.
-   */
-  size_t hash() const {
-    return (size_t)d_value;
-  }
-
-  /**
-   * Returns true if the literal is undefined.
-   */
-  bool isNull() const {
-    return getSatVariable() == undefSatVariable;
-  }
-};
-
-/**
- * A constant representing a undefined literal.
- */
-const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);  
-
-/**
- * Helper for hashing the literals.
- */
-struct SatLiteralHashFunction {
-  inline size_t operator() (const SatLiteral& literal) const {
-    return literal.hash();
-  }
-};
-
-/**
- * A SAT clause is a vector of literals.
- */
-typedef std::vector<SatLiteral> SatClause;
-
 class SatSolver {
 
 public: