diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-20 16:11:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-20 16:11:15 -0700 |
commit | 614670f98a9ab2d3cfcb9f364a1b06d78f63ebb0 (patch) | |
tree | 7dbdfbbae495fed26877c51267f6775f618f5d33 /src/prop/sat_solver_factory.h | |
parent | 62f58d62c6c597eeb9cae5e08d74f21c4a5c5c40 (diff) |
Add support for CaDiCaL as eager BV SAT solver. (#1675)
Diffstat (limited to 'src/prop/sat_solver_factory.h')
-rw-r--r-- | src/prop/sat_solver_factory.h | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index fac8c9083..8d6e405d8 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -16,7 +16,8 @@ #include "cvc4_private.h" -#pragma once +#ifndef __CVC4__PROP__SAT_SOLVER_FACTORY_H +#define __CVC4__PROP__SAT_SOLVER_FACTORY_H #include <string> #include <vector> @@ -28,17 +29,25 @@ namespace CVC4 { namespace prop { -class SatSolverFactory { -public: - +class SatSolverFactory +{ + public: static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name = ""); - static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry); + + static DPLLSatSolverInterface* createDPLLMinisat( + StatisticsRegistry* registry); + static SatSolver* createCryptoMinisat(StatisticsRegistry* registry, const std::string& name = ""); -};/* class SatSolverFactory */ + static SatSolver* createCadical(StatisticsRegistry* registry, + const std::string& name = ""); + +}; /* class SatSolverFactory */ + +} // namespace prop +} // namespace CVC4 -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ +#endif // __CVC4__PROP__SAT_SOLVER_FACTORY_H |