From fe2088f892af594765fc50d8cc9f2b4f87286b7c Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Tue, 15 May 2012 18:53:54 +0000 Subject: [PATCH] renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively --- src/theory/bv/Makefile.am | 4 +- src/theory/bv/bitblast_strategies.cpp | 2 +- src/theory/bv/{bv_sat.cpp => bitblaster.cpp} | 4 +- src/theory/bv/{bv_sat.h => bitblaster.h} | 8 +- src/theory/bv/bv_solver_types.cpp | 78 -------- src/theory/bv/bv_solver_types.h | 185 ------------------- src/theory/bv/theory_bv.cpp | 2 +- test/unit/theory/theory_bv_white.h | 2 +- 8 files changed, 11 insertions(+), 274 deletions(-) rename src/theory/bv/{bv_sat.cpp => bitblaster.cpp} (99%) rename src/theory/bv/{bv_sat.h => bitblaster.h} (97%) delete mode 100644 src/theory/bv/bv_solver_types.cpp delete mode 100644 src/theory/bv/bv_solver_types.h 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 similarity index 99% rename from src/theory/bv/bv_sat.cpp rename to 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 similarity index 97% rename from src/theory/bv/bv_sat.h rename to 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 -#include -#include -#include -#include -#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 & assumps) { -// context::CDList::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 #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" -- 2.30.2