src/prop/sat_solver_registry.h

   1 /*********************                                                        */
   2 /*! \file sat_solver_registry.h
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Morgan Deters
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief This class transforms a sequence of formulas into clauses.
  13  **
  14  ** This class takes a sequence of formulas.
  15  ** It outputs a stream of clauses that is propositionally
  16  ** equi-satisfiable with the conjunction of the formulas.
  17  ** This stream is maintained in an online fashion.
  18  **
  19  ** Compile time registration of SAT solvers with the SAT solver factory
  20  **/
  21
  22 #pragma once
  23
  24 #include "cvc4_private.h"
  25
  26 #include <map>
  27 #include <string>
  28 #include <cxxabi.h>
  29 #include "prop/sat_solver.h"
  30 #include "prop/sat_solver_factory.h"
  31
  32 namespace CVC4 {
  33 namespace prop {
  34
  35 /**
  36  * Interface for SAT solver constructors. Solvers should declare an instantiation of the
  37  * SatSolverConstructor interface below.
  38  */
  39 class SatSolverConstructorInterface {
  40 public:
  41   virtual ~SatSolverConstructorInterface() {}
  42   virtual SatSolver* construct() = 0;
  43 };
  44
  45 /**
  46  * Registry containing all the registered SAT solvers.
  47  */
  48 class SatSolverRegistry {
  49
  50   typedef std::map<std::string, SatSolverConstructorInterface*> registry_type;
  51
  52   /** Map from ids to solver constructors */
  53   registry_type d_solvers;
  54
  55   /** Nobody can create the registry, there can be only one! */
  56   SatSolverRegistry() {}
  57
  58   /**
  59    * Register a SAT solver with the registry. The Constructor type should be a subclass
  60    * of the SatSolverConstructor.
  61    */
  62   template <typename Constructor>
  63   size_t registerSolver(const char* id) {
  64     int status;
  65     char* demangled = abi::__cxa_demangle(id, 0, 0, &status);
  66     d_solvers[demangled] = new Constructor();
  67     free(demangled);
  68     return d_solvers.size();
  69   }
  70
  71   /** Get the instance of the registry */
  72   static SatSolverRegistry* getInstance();
  73
  74 public:
  75
  76   /** Destructor */
  77   ~SatSolverRegistry();
  78
  79   /**
  80    * Returns the constructor for the given SAT solver.
  81    */
  82   static SatSolverConstructorInterface* getConstructor(std::string id);
  83
  84   /** Get the ids of the available solvers */
  85   static void getSolverIds(std::vector<std::string>& solvers);
  86
  87   /** The Constructors are friends, since they need to register */
  88   template<typename Solver>
  89   friend class SatSolverConstructor;
  90
  91 };
  92
  93 /**
  94  * Declare an instance of this class with the SAT solver in order to put it in the registry.
  95  */
  96 template<typename Solver>
  97 class SatSolverConstructor : public SatSolverConstructorInterface {
  98
  99   /** Static solver id we use for initialization */
 100   static const size_t s_solverId;
 101
 102 public:
 103
 104   /** Constructs the solver */
 105   SatSolver* construct() {
 106     return new Solver();
 107   }
 108
 109 };
 110
 111 template<typename Solver>
 112 const size_t SatSolverConstructor<Solver>::s_solverId = SatSolverRegistry::getInstance()->registerSolver<SatSolverConstructor>(typeid(Solver).name());
 113
 114 }/* CVC4::prop namespace */
 115 }/* CVC4 namespace */