1 /********************* */
2 /*! \file sat_solver_factory.h
4 ** Original author: lianah
6 ** Minor contributors (to current version):
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief SAT Solver creation facility.
19 #include "prop/sat_solver_factory.h"
20 #include "prop/sat_solver_registry.h"
21 #include "prop/minisat/minisat.h"
22 #include "prop/bvminisat/bvminisat.h"
27 template class SatSolverConstructor
<MinisatSatSolver
>;
28 template class SatSolverConstructor
<BVMinisatSatSolver
>;
30 BVSatSolverInterface
* SatSolverFactory::createMinisat() {
31 return new BVMinisatSatSolver();
34 DPLLSatSolverInterface
* SatSolverFactory::createDPLLMinisat() {
35 return new MinisatSatSolver();
38 SatSolver
* SatSolverFactory::create(const char* name
) {
39 SatSolverConstructorInterface
* constructor
= SatSolverRegistry::getConstructor(name
);
41 return constructor
->construct();
47 void SatSolverFactory::getSolverIds(std::vector
<std::string
>& solvers
) {
48 SatSolverRegistry::getSolverIds(solvers
);
51 } /* namespace CVC4::prop */
52 } /* namespace CVC4 */