renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively

8 files changed, 11 insertions, 274 deletions

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index af760e520..3bb7e3056 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -9,8 +9,8 @@ noinst_LTLIBRARIES = libbv.la
 
 libbv_la_SOURCES = \
 	theory_bv_utils.h \
-	bv_sat.h \
-	bv_sat.cpp \
+	bitblaster.h \
+	bitblaster.cpp \
 	bitblast_strategies.h \
 	bitblast_strategies.cpp \
 	theory_bv.h \
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index b579122e5..6871a5421 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -17,7 +17,7 @@
  **/
 
 #include "bitblast_strategies.h"
-#include "bv_sat.h"
+#include "bitblaster.h"
 #include "prop/sat_solver.h"
 #include "theory/booleans/theory_bool_rewriter.h"
 
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bitblaster.cpp
index ed3101459..60fc8f9c1 100644
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file bv_sat.cpp
+/*! \file bitblaster.cpp
  ** \verbatim
  ** Original author: lianah
  ** Major contributors: none
@@ -17,7 +17,7 @@
  ** 
  **/
 
-#include "bv_sat.h"
+#include "bitblaster.h"
 #include "theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "prop/cnf_stream.h"
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bitblaster.h
index 7016879a0..6de84fc01 100644
--- a/src/theory/bv/bv_sat.h
+++ b/src/theory/bv/bitblaster.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file bv_sat.h
+/*! \file bitblaster.h
  ** \verbatim
  ** Original author: lianah
  ** Major contributors: none
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BV__SAT_H
-#define __CVC4__BV__SAT_H
+#ifndef __CVC4__BITBLASTER_H
+#define __CVC4__BITBLASTER_H
 
 
 #include "expr/node.h"
@@ -155,4 +155,4 @@ private:
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__BV__SAT_H */
+#endif /* __CVC4__BITBLASTER_H */
diff --git a/src/theory/bv/bv_solver_types.cpp b/src/theory/bv/bv_solver_types.cpp
deleted file mode 100644
index 2589e5712..000000000
--- a/src/theory/bv/bv_solver_types.cpp
+++ /dev/null
@@ -1,78 +0,0 @@
-/*********************                                                        */
-/*! \file bv_sat.cpp
- ** \verbatim
- ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** 
- **/
-
-#include "bv_solver_types.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-#ifdef BV_MINISAT 
-using namespace BVMinisat; 
-SatLit neg(const SatLit& lit) {
-  return ~lit; 
-}
-
-SatLit mkLit(SatVar var) {
-  return BVMinisat::mkLit(var, false); 
-}
-
-SatVar mkVar(SatLit lit) {
-  return BVMinisat::var(lit); 
-}
-bool   polarity(SatLit lit) {
-  return !(BVMinisat::sign(lit)); 
-} 
-
-
-std::string toStringLit(SatLit lit) {
-  std::ostringstream os;
-  os << (polarity(lit) ? "" : "-") << var(lit) + 1;
-  return os.str(); 
-}
-#endif
-
-#ifdef BV_PICOSAT
-
-SatLit mkLit(SatVar var) {
-  return var;
-}
-SatVar mkVar(SatLit lit) {
-  return (lit > 0 ? lit : -lit); 
-}
-bool   polarity(SatLit lit) {
-  return (lit > 0); 
-}
-
-SatLit neg(const SatLit& lit) {
-   return -lit; 
-}
-
-std::string toStringLit(SatLit lit) {
-  std::ostringstream os;
-  os << (lit < 0 ? "-" : "") << lit;
-  return os.str(); 
-}
-
-
-#endif  
-
-}
-}
-}
diff --git a/src/theory/bv/bv_solver_types.h b/src/theory/bv/bv_solver_types.h
deleted file mode 100644
index fb99ae4c6..000000000
--- a/src/theory/bv/bv_solver_types.h
+++ /dev/null
@@ -1,185 +0,0 @@
-//*********************                                                        */
-/*! \file bv_solver_types.h
- ** \verbatim
- ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Definitions of the SatSolver literal and clause types 
- **
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__BV__SOLVER__TYPES_H 
-#define __CVC4__BV__SOLVER__TYPES_H 
-
-#define BV_MINISAT
-//#define BV_PICOSAT
-
-#ifdef BV_MINISAT  /* BV_MINISAT if we are using the minisat solver for the theory of bitvectors*/
-#include "theory/bv/bvminisat/core/Solver.h"
-#include "theory/bv/bvminisat/core/SolverTypes.h"
-#include "theory/bv/bvminisat/simp/SimpSolver.h"
-#endif   /* BV_MINISAT */
-
-#ifdef BV_PICOSAT  /* BV_PICOSAT */
-#include "picosat/picosat.h"
-#endif  /* BV_PICOSAT */
-
-#include "expr/node.h"
-#include <vector>
-#include <list>
-#include <iostream>
-#include <math.h>
-#include <ext/hash_map>
-#include "context/cdlist.h"
-#include "util/stats.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-#endif /* BV_MINISAT */
-
-
-
-// #ifdef BV_PICOSAT /* BV_PICOSAT */
-// /** 
-//  * PICOSAT type-definitions
-//  * 
-//  * 
-//  */
-
-// typedef int SatVar; 
-// typedef int SatLit; 
-
-// std::string toStringLit(SatLit lit); 
-
-
-// SatLit neg(const SatLit& lit); 
-
-// struct SatLitHash {
-//   static size_t hash (const SatLit& lit) {
-//     return (size_t) lit;
-//   }
-  
-// };
-
-// struct SatLitHashFunction {
-//   size_t operator()(SatLit lit) const {
-//     return (size_t) lit; 
-//   }
-// };
-
-// struct SatLitLess{
-//   static bool compare(const SatLit& x, const SatLit& y)
-//   {
-//     return x < y;
-//   }
-// };
-
-// #endif /* BV_PICOSAT */
-
-// #ifdef BV_PICOSAT  /* BV_PICOSAT */
-
-// /** 
-//  * Some helper functions that should be defined for each SAT solver supported
-//  * 
-//  * 
-//  * @return 
-//  */
-
-// SatLit mkLit(SatVar var);
-// SatVar mkVar(SatLit lit);
-// bool   polarity(SatLit lit); 
-
-
-// /** 
-//  * Wrapper to create the impression of a SatSolver class for Picosat
-//  * which is written in C
-//  */
-
-// class SatSolver: public SatSolverInterface {
-//   int d_varCount;
-//   bool d_started;
-// public:
-//   SatSolver() :
-//     d_varCount(0),
-//     d_started(false)
-//   {
-//     picosat_init(); /// call constructor
-//     picosat_enable_trace_generation(); // required for unsat cores
-//   }
-  
-//   ~SatSolver() {
-//     picosat_reset(); 
-//   }
-
-//   void   addClause(const SatClause* cl) {
-//     Assert (cl);
-//     const SatClause& clause = *cl; 
-//     for (unsigned i = 0; i < clause.size(); ++i ) {
-//       picosat_add(clause[i]); 
-//     }
-//     picosat_add(0); // ends clause
-//   }
-  
-//   bool   solve () {
-//     if(d_started) {
-//       picosat_remove_learned(100);
-//     }
-//     int res = picosat_sat(-1); // no decision limit
-//     // 0 UNKNOWN, 10 SATISFIABLE and 20 UNSATISFIABLE
-//     d_started = true; 
-//     Assert (res == 10 || res == 20); 
-//     return res == 10; 
-//   }
-  
-//   bool   solve(const context::CDList<SatLit> & assumps) {
-//     context::CDList<SatLit>::const_iterator it = assumps.begin();
-//     for (; it!= assumps.end(); ++it) {
-//       picosat_assume(*it); 
-//     }
-//     return solve (); 
-//   }
-  
-//   SatVar newVar() { return ++d_varCount; }
-
-//   void   setUnremovable(SatLit lit) {}; 
-
-//   SatClause* getUnsatCore() {
-//     const int* failedAssumption = picosat_failed_assumptions();
-//     Assert(failedAssumption);
-
-//     SatClause* unsatCore = new SatClause();
-//     while (*failedAssumption != 0) {
-//       SatLit lit = *failedAssumption;
-//       unsatCore->addLiteral(neg(lit));
-//       ++failedAssumption; 
-//     }
-//     unsatCore->sort(); 
-//     return unsatCore; 
-//   }
-// }; 
-
-
-// #endif  /* BV_PICOSAT */
-
-
-
-
-} /* bv namespace */ 
-
-} /* theory namespace */
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4__BV__SOLVER__TYPES_H */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 07eb69c26..d005e9473 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -20,7 +20,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/valuation.h"
-#include "theory/bv/bv_sat.h"
+#include "theory/bv/bitblaster.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index bbc7a8f72..081fa7c2a 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -21,7 +21,7 @@
 #include <cxxtest/TestSuite.h>
 
 #include "theory/theory.h"
-#include "theory/bv/bv_sat.h"
+#include "theory/bv/bitblaster.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "context/context.h"