More cleaning up.

2 files changed, 18 insertions, 18 deletions

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index ede18c585..1ec81a4f6 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -57,16 +57,16 @@ SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
                     Minisat::sign(lit));
 }
 
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
-  if(res) return SatValTrue;
-  else return SatValFalse;
+SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
+  if(res) return SAT_VALUE_TRUE;
+  else return SAT_VALUE_FALSE;
 }
 
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
-  if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue;
-  if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown;
+SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
+  if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
+  if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
   Assert(res == (Minisat::lbool((uint8_t)1)));
-  return SatValFalse;
+  return SAT_VALUE_FALSE;
 }
 
 
@@ -121,7 +121,7 @@ SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) {
 }
 
 
-SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
+SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
   Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
   if(resource == 0) {
     d_minisat->budgetOff();
@@ -130,14 +130,14 @@ SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
   }
   Minisat::vec<Minisat::Lit> empty;
   unsigned long conflictsBefore = d_minisat->conflicts;
-  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+  SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
   d_minisat->clearInterrupt();
   resource = d_minisat->conflicts - conflictsBefore;
   Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
   return result;
 }
 
-SatLiteralValue DPLLMinisatSatSolver::solve() {
+SatValue DPLLMinisatSatSolver::solve() {
   d_minisat->budgetOff();
   return toSatLiteralValue(d_minisat->solve());
 }
@@ -147,11 +147,11 @@ void DPLLMinisatSatSolver::interrupt() {
   d_minisat->interrupt();
 }
 
-SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) {
+SatValue DPLLMinisatSatSolver::value(SatLiteral l) {
   return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
 }
 
-SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
+SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
   return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
 }
 
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index dc06753ab..549c0b679 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -44,8 +44,8 @@ public:
   static SatVariable     toSatVariable(Minisat::Var var);
   static Minisat::Lit    toMinisatLit(SatLiteral lit);
   static SatLiteral      toSatLiteral(Minisat::Lit lit);
-  static SatLiteralValue toSatLiteralValue(bool res);
-  static SatLiteralValue toSatLiteralValue(Minisat::lbool res);
+  static SatValue toSatLiteralValue(bool res);
+  static SatValue toSatLiteralValue(Minisat::lbool res);
 
   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
   static void  toSatClause    (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);
@@ -56,14 +56,14 @@ public:
 
   SatVariable newVar(bool theoryAtom = false);
 
-  SatLiteralValue solve();
-  SatLiteralValue solve(long unsigned int&);
+  SatValue solve();
+  SatValue solve(long unsigned int&);
 
   void interrupt();
 
-  SatLiteralValue value(SatLiteral l);
+  SatValue value(SatLiteral l);
 
-  SatLiteralValue modelValue(SatLiteral l);
+  SatValue modelValue(SatLiteral l);
 
   bool properExplanation(SatLiteral lit, SatLiteral expl) const;