From fe30804ae981fcbd6ae795db120741dcffc1ef01 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 7 Nov 2014 18:59:36 -0500 Subject: [PATCH] Remove some dead code. --- src/Makefile.am | 3 - src/prop/bvminisat/bvminisat.h | 1 - src/prop/minisat/minisat.h | 1 - src/prop/options | 3 - src/prop/options_handlers.h | 47 ------------- src/prop/sat_solver_factory.cpp | 17 ----- src/prop/sat_solver_factory.h | 5 -- src/prop/sat_solver_registry.cpp | 60 ---------------- src/prop/sat_solver_registry.h | 115 ------------------------------- 9 files changed, 252 deletions(-) delete mode 100644 src/prop/options_handlers.h delete mode 100644 src/prop/sat_solver_registry.cpp delete mode 100644 src/prop/sat_solver_registry.h diff --git a/src/Makefile.am b/src/Makefile.am index a04b86bee..2acefc577 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -100,9 +100,6 @@ libcvc4_la_SOURCES = \ prop/sat_solver_types.h \ prop/sat_solver_factory.h \ prop/sat_solver_factory.cpp \ - prop/sat_solver_registry.h \ - prop/sat_solver_registry.cpp \ - prop/options_handlers.h \ smt/smt_engine.cpp \ smt/smt_engine_check_proof.cpp \ smt/smt_engine.h \ diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index c7ee2e0b7..fea437565 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -21,7 +21,6 @@ #pragma once #include "prop/sat_solver.h" -#include "prop/sat_solver_registry.h" #include "prop/bvminisat/simp/SimpSolver.h" #include "context/cdo.h" diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 3d3cea356..96893fe41 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -19,7 +19,6 @@ #pragma once #include "prop/sat_solver.h" -#include "prop/sat_solver_registry.h" #include "prop/minisat/simp/SimpSolver.h" namespace CVC4 { diff --git a/src/prop/options b/src/prop/options index 71091d2b5..8189d61f8 100644 --- a/src/prop/options +++ b/src/prop/options @@ -5,9 +5,6 @@ module PROP "prop/options.h" SAT layer -option - --show-sat-solvers void :handler CVC4::prop::showSatSolvers :handler-include "prop/options_handlers.h" - show all available SAT solvers - option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) less_equal(1.0) sets the frequency of random decisions in the sat solver (P=0.0 by default) option satRandomSeed random-seed --random-seed=S uint32_t :default 0 :read-write diff --git a/src/prop/options_handlers.h b/src/prop/options_handlers.h deleted file mode 100644 index 8ed53a3f5..000000000 --- a/src/prop/options_handlers.h +++ /dev/null @@ -1,47 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** 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 ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__PROP__OPTIONS_HANDLERS_H -#define __CVC4__PROP__OPTIONS_HANDLERS_H - -#include "prop/sat_solver_factory.h" -#include -#include - -namespace CVC4 { -namespace prop { - -inline void showSatSolvers(std::string option, SmtEngine* smt) { - std::vector solvers; - SatSolverFactory::getSolverIds(solvers); - printf("Available SAT solvers: "); - for (unsigned i = 0; i < solvers.size(); ++ i) { - if (i > 0) { - printf(", "); - } - printf("%s", solvers[i].c_str()); - } - printf("\n"); - exit(0); -} - -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PROP__OPTIONS_HANDLERS_H */ diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 3d3e76205..98b8fce47 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -15,16 +15,12 @@ **/ #include "prop/sat_solver_factory.h" -#include "prop/sat_solver_registry.h" #include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" namespace CVC4 { namespace prop { -template class SatSolverConstructor; -template class SatSolverConstructor; - BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) { return new BVMinisatSatSolver(mainSatContext, name); } @@ -33,18 +29,5 @@ DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { return new MinisatSatSolver(); } -SatSolver* SatSolverFactory::create(const char* name) { - SatSolverConstructorInterface* constructor = SatSolverRegistry::getConstructor(name); - if (constructor) { - return constructor->construct(); - } else { - return NULL; - } -} - -void SatSolverFactory::getSolverIds(std::vector& solvers) { - SatSolverRegistry::getSolverIds(solvers); -} - } /* CVC4::prop namespace */ } /* CVC4 namespace */ diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 009622212..34776c245 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -31,11 +31,6 @@ public: static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = ""); static DPLLSatSolverInterface* createDPLLMinisat(); - static SatSolver* create(const char* id); - - /** Get the solver ids that are available */ - static void getSolverIds(std::vector& solvers); - };/* class SatSolverFactory */ }/* CVC4::prop namespace */ diff --git a/src/prop/sat_solver_registry.cpp b/src/prop/sat_solver_registry.cpp deleted file mode 100644 index 5cf79699f..000000000 --- a/src/prop/sat_solver_registry.cpp +++ /dev/null @@ -1,60 +0,0 @@ -/********************* */ -/*! \file sat_solver_registry.cpp - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief This class transforms a sequence of formulas into clauses. - ** - ** This class takes a sequence of formulas. - ** It outputs a stream of clauses that is propositionally - ** equi-satisfiable with the conjunction of the formulas. - ** This stream is maintained in an online fashion. - ** - ** Compile time registration of SAT solvers with the SAT solver factory - **/ - -#include "prop/sat_solver_registry.h" -#include "sstream" - -using namespace std; -using namespace CVC4; -using namespace prop; - -SatSolverConstructorInterface* SatSolverRegistry::getConstructor(string id) { - SatSolverRegistry* registry = getInstance(); - registry_type::const_iterator find = registry->d_solvers.find(id); - if (find == registry->d_solvers.end()) { - return NULL; - } else { - return find->second; - } -} - -void SatSolverRegistry::getSolverIds(std::vector& solvers) { - SatSolverRegistry* registry = getInstance(); - registry_type::const_iterator it = registry->d_solvers.begin(); - registry_type::const_iterator it_end = registry->d_solvers.end(); - for (; it != it_end; ++ it) { - solvers.push_back(it->first); - } -} - -SatSolverRegistry* SatSolverRegistry::getInstance() { - static SatSolverRegistry registry; - return ®istry; -} - -SatSolverRegistry::~SatSolverRegistry() { - registry_type::const_iterator it = d_solvers.begin(); - registry_type::const_iterator it_end = d_solvers.end(); - for (; it != it_end; ++ it) { - delete it->second; - } - d_solvers.clear(); -} diff --git a/src/prop/sat_solver_registry.h b/src/prop/sat_solver_registry.h deleted file mode 100644 index 7a326d6c8..000000000 --- a/src/prop/sat_solver_registry.h +++ /dev/null @@ -1,115 +0,0 @@ -/********************* */ -/*! \file sat_solver_registry.h - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief This class transforms a sequence of formulas into clauses. - ** - ** This class takes a sequence of formulas. - ** It outputs a stream of clauses that is propositionally - ** equi-satisfiable with the conjunction of the formulas. - ** This stream is maintained in an online fashion. - ** - ** Compile time registration of SAT solvers with the SAT solver factory - **/ - -#pragma once - -#include "cvc4_private.h" - -#include -#include -#include -#include "prop/sat_solver.h" -#include "prop/sat_solver_factory.h" - -namespace CVC4 { -namespace prop { - -/** - * Interface for SAT solver constructors. Solvers should declare an instantiation of the - * SatSolverConstructor interface below. - */ -class SatSolverConstructorInterface { -public: - virtual ~SatSolverConstructorInterface() {} - virtual SatSolver* construct() = 0; -}; - -/** - * Registry containing all the registered SAT solvers. - */ -class SatSolverRegistry { - - typedef std::map registry_type; - - /** Map from ids to solver constructors */ - registry_type d_solvers; - - /** Nobody can create the registry, there can be only one! */ - SatSolverRegistry() {} - - /** - * Register a SAT solver with the registry. The Constructor type should be a subclass - * of the SatSolverConstructor. - */ - template - size_t registerSolver(const char* id) { - int status; - char* demangled = abi::__cxa_demangle(id, 0, 0, &status); - d_solvers[demangled] = new Constructor(); - free(demangled); - return d_solvers.size(); - } - - /** Get the instance of the registry */ - static SatSolverRegistry* getInstance(); - -public: - - /** Destructor */ - ~SatSolverRegistry(); - - /** - * Returns the constructor for the given SAT solver. - */ - static SatSolverConstructorInterface* getConstructor(std::string id); - - /** Get the ids of the available solvers */ - static void getSolverIds(std::vector& solvers); - - /** The Constructors are friends, since they need to register */ - template - friend class SatSolverConstructor; - -}; - -/** - * Declare an instance of this class with the SAT solver in order to put it in the registry. - */ -template -class SatSolverConstructor : public SatSolverConstructorInterface { - - /** Static solver id we use for initialization */ - static const size_t s_solverId; - -public: - - /** Constructs the solver */ - SatSolver* construct() { - return new Solver(); - } - -}; - -template -const size_t SatSolverConstructor::s_solverId = SatSolverRegistry::getInstance()->registerSolver(typeid(Solver).name()); - -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ -- 2.30.2