diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 19:42:25 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 19:42:25 +0000 |
commit | 6fdc62f34bb1d04b84dfd628ec16335b8f02385e (patch) | |
tree | 44755057990ad99f6f47904a0201d33c9be18c9c /src/prop/sat_solver_registry.h | |
parent | 1ed3b1803bd0a25c56a62d290cd5dcb64c5085ce (diff) |
Global registry of SAT solvers, where they are registered at compile time. The available SAT solvers can be seen with the --show-sat-solvers option.
Diffstat (limited to 'src/prop/sat_solver_registry.h')
-rw-r--r-- | src/prop/sat_solver_registry.h | 118 |
1 files changed, 118 insertions, 0 deletions
diff --git a/src/prop/sat_solver_registry.h b/src/prop/sat_solver_registry.h new file mode 100644 index 000000000..df1cf86f8 --- /dev/null +++ b/src/prop/sat_solver_registry.h @@ -0,0 +1,118 @@ +/********************* */ +/*! \file sat_solver_registry.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters, dejan + ** Minor contributors (to current version): barrett, cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 instantiatiation 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 SatSolverConstrutor. + */ + 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()); + +} +} + |