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.h | |
parent | 9918f0e86a38f5fc8671ec6115eaac9b2c3b31d8 (diff) |
More cleaning up.
Diffstat (limited to 'src/prop/sat_solver_factory.h')
-rw-r--r-- | src/prop/sat_solver_factory.h | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h new file mode 100644 index 000000000..09d66b8d4 --- /dev/null +++ b/src/prop/sat_solver_factory.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file sat_solver_factory.h + ** \verbatim + ** Original author: dejan + ** 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. + ** + ** SAT Solver creation facility + **/ + +#pragma once + +#include "cvc4_public.h" + +#include "prop/sat_solver.h" + +namespace CVC4 { +namespace prop { + +class SatSolverFactory { +public: + static BVSatSolverInterface* createMinisat(); + static DPLLSatSolverInterface* createDPLLMinisat(); +}; + +} +} + + + |