From 0d080430206880ffc19050acfa01aae1475f1978 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sun, 25 Mar 2012 20:12:07 +0000 Subject: [PATCH] sat_module.h,cpp -> sat_solver.h,cpp (as intended) --- src/prop/Makefile.am | 4 ++-- src/prop/cnf_stream.cpp | 4 ++-- src/prop/cnf_stream.h | 6 +++--- src/prop/minisat/core/Solver.cc | 2 +- src/prop/prop_engine.cpp | 2 +- src/prop/{sat_module.cpp => sat_solver.cpp} | 2 +- src/prop/{sat_module.h => sat_solver.h} | 10 ++++------ src/prop/theory_proxy.h | 2 +- src/theory/bv/bitblast_strategies.cpp | 2 +- src/theory/bv/bitblast_strategies.h | 2 +- src/theory/bv/bv_sat.cpp | 2 +- src/theory/bv/bv_sat.h | 2 +- 12 files changed, 19 insertions(+), 21 deletions(-) rename src/prop/{sat_module.cpp => sat_solver.cpp} (99%) rename src/prop/{sat_module.h => sat_solver.h} (97%) diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 02a6a4714..832255621 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -15,8 +15,8 @@ libprop_la_SOURCES = \ theory_proxy.cpp \ cnf_stream.h \ cnf_stream.cpp \ - sat_module.h \ - sat_module.cpp + sat_solver.h \ + sat_solver.cpp SUBDIRS = minisat bvminisat diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 676cc4c49..3a4fa781a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -44,7 +44,7 @@ namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool fullLitToNodeMap) : +CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, bool fullLitToNodeMap) : d_satSolver(satSolver), d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar) { @@ -66,7 +66,7 @@ void CnfStream::recordTranslation(TNode node, bool alwaysRecord) { } } -TseitinCnfStream::TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap) : +TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap) : CnfStream(satSolver, registrar, fullLitToNodeMap) { } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index af2ff2fcd..f75e74d63 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -65,7 +65,7 @@ public: protected: /** The SAT solver we will be using */ - SatSolverInterface *d_satSolver; + SatSolver *d_satSolver; TranslationCache d_translationCache; NodeCache d_nodeCache; @@ -190,7 +190,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - CnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); + CnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -290,7 +290,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); + TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); private: diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 65ec025b1..e5a6d32e1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/core/Solver.h" #include "prop/theory_proxy.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" #include "util/output.h" #include "expr/command.h" #include "proof/proof_manager.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 9d6a2c8f6..0fa13dc04 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -19,7 +19,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" diff --git a/src/prop/sat_module.cpp b/src/prop/sat_solver.cpp similarity index 99% rename from src/prop/sat_module.cpp rename to src/prop/sat_solver.cpp index 5e5b78b44..13f2498f2 100644 --- a/src/prop/sat_module.cpp +++ b/src/prop/sat_solver.cpp @@ -18,7 +18,7 @@ **/ #include "prop/prop_engine.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" #include "context/context.h" #include "theory/theory_engine.h" #include "expr/expr_stream.h" diff --git a/src/prop/sat_module.h b/src/prop/sat_solver.h similarity index 97% rename from src/prop/sat_module.h rename to src/prop/sat_solver.h index 9c49c7d67..56c6c2783 100644 --- a/src/prop/sat_module.h +++ b/src/prop/sat_solver.h @@ -96,12 +96,10 @@ struct SatLiteralHashFunction { typedef std::vector SatClause; - - -class SatSolverInterface { +class SatSolver { public: /** Virtual destructor to make g++ happy */ - virtual ~SatSolverInterface() { } + virtual ~SatSolver() { } /** Assert a clause in the solver. */ virtual void addClause(SatClause& clause, bool removable) = 0; @@ -134,7 +132,7 @@ public: }; -class BVSatSolverInterface: public SatSolverInterface { +class BVSatSolverInterface: public SatSolver { public: virtual SatLiteralValue solve(const context::CDList & assumptions) = 0; @@ -144,7 +142,7 @@ public: }; -class DPLLSatSolverInterface: public SatSolverInterface { +class DPLLSatSolverInterface: public SatSolver { public: virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 85dcae68b..2934bcad9 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -29,7 +29,7 @@ #include "util/options.h" #include "util/stats.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" namespace CVC4 { diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index 6cbec732c..c0855122e 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -18,7 +18,7 @@ #include "bitblast_strategies.h" #include "bv_sat.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" #include "theory/booleans/theory_bool_rewriter.h" using namespace CVC4::prop; diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h index c445af626..826b61d4f 100644 --- a/src/theory/bv/bitblast_strategies.h +++ b/src/theory/bv/bitblast_strategies.h @@ -23,7 +23,7 @@ #include "expr/node.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" namespace CVC4 { diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index d386fd4db..f580aee44 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -21,7 +21,7 @@ #include "theory_bv_utils.h" #include "theory/rewriter.h" #include "prop/cnf_stream.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" using namespace std; diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index 3ffc79b7a..c0f3b75ed 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -37,7 +37,7 @@ #include "util/stats.h" #include "bitblast_strategies.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" namespace CVC4 { -- 2.30.2