diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 14:22:38 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 14:22:38 +0000 |
commit | 1ed3b1803bd0a25c56a62d290cd5dcb64c5085ce (patch) | |
tree | f65a0b2ad744a5f2b6408c34319aad10c7d2f406 /src/prop/sat_solver_factory.cpp | |
parent | 9918f0e86a38f5fc8671ec6115eaac9b2c3b31d8 (diff) |
More cleaning up.
Diffstat (limited to 'src/prop/sat_solver_factory.cpp')
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp new file mode 100644 index 000000000..fbb244789 --- /dev/null +++ b/src/prop/sat_solver_factory.cpp @@ -0,0 +1,36 @@ +/********************* */ +/*! \file sat_solver_factory.h + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** 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 SAT Solver creation facility. + ** + ** SAT Solver. + **/ + +#include "prop/sat_solver_factory.h" +#include "prop/minisat/minisat.h" +#include "prop/bvminisat/bvminisat.h" + +using namespace CVC4; +using namespace prop; + +BVSatSolverInterface* SatSolverFactory::createMinisat() { + return new MinisatSatSolver(); +} + +DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { + return new DPLLMinisatSatSolver(); +} + + + + |