Remove some dead code.

8 files changed, 0 insertions, 249 deletions

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 <string>
-#include <vector>
-
-namespace CVC4 {
-namespace prop {
-
-inline void showSatSolvers(std::string option, SmtEngine* smt) {
-  std::vector<std::string> 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<MinisatSatSolver>;
-template class SatSolverConstructor<BVMinisatSatSolver>;
-
 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<std::string>& 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<std::string>& 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<std::string>& 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 &registry;
-}
-
-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 <map>
-#include <string>
-#include <cxxabi.h>
-#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<std::string, SatSolverConstructorInterface*> 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 <typename Constructor>
-  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<std::string>& solvers);
-
-  /** The Constructors are friends, since they need to register */
-  template<typename Solver>
-  friend class SatSolverConstructor;
-
-};
-
-/**
- * Declare an instance of this class with the SAT solver in order to put it in the registry.
- */
-template<typename Solver>
-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<typename Solver>
-const size_t SatSolverConstructor<Solver>::s_solverId = SatSolverRegistry::getInstance()->registerSolver<SatSolverConstructor>(typeid(Solver).name());
-
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */