diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:12:07 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:12:07 +0000 |
commit | 0d080430206880ffc19050acfa01aae1475f1978 (patch) | |
tree | b1334148abb7311eca1afcb00fdce69f606ac22f /src | |
parent | 426abc52a0f1631f2adee0eef845e3f8946c5088 (diff) |
sat_module.h,cpp -> sat_solver.h,cpp (as intended)
Diffstat (limited to 'src')
-rw-r--r-- | src/prop/Makefile.am | 4 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 4 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 2 | ||||
-rw-r--r-- | src/prop/sat_solver.cpp (renamed from src/prop/sat_module.cpp) | 2 | ||||
-rw-r--r-- | src/prop/sat_solver.h (renamed from src/prop/sat_module.h) | 10 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast_strategies.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_sat.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_sat.h | 2 |
12 files changed, 19 insertions, 21 deletions
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 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 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<SatLiteral> 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<SatLiteral> & 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 { |