diff options
Diffstat (limited to 'src/prop/sat_solver_registry.cpp')
-rw-r--r-- | src/prop/sat_solver_registry.cpp | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/src/prop/sat_solver_registry.cpp b/src/prop/sat_solver_registry.cpp new file mode 100644 index 000000000..01434bd80 --- /dev/null +++ b/src/prop/sat_solver_registry.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \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 + **/ + +#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 ®istry; +} + +SatSolverRegistry::~SatSolverRegistry() { + registry_type::const_iterator it = d_solvers.begin(); + registry_type::const_iterator it_end = d_solvers.begin(); + for (; it != it_end; ++ it) { + delete it->second; + } +} |