diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-02-07 15:00:41 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-07 15:00:41 -0800 |
commit | 7d325a44dcfce54dd9195b7ee49fb93a1aed3a06 (patch) | |
tree | 4701b7f24cb8a9a696b99242c23668b17c819236 /src/prop/sat_solver_factory.cpp | |
parent | b661071c238ea32e72ee6bddbff65f38328dd345 (diff) |
Cleanup Cryptominisat header. (#1561)
Clang formatted sat_solver_factor.cpp
Diffstat (limited to 'src/prop/sat_solver_factory.cpp')
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 27e2daf11..135fc300d 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -16,6 +16,8 @@ #include "prop/sat_solver_factory.h" +// Cryptominisat header has to come first since there are name clashes for +// var_Undef, l_True, ... (static const in Cryptominisat vs. #define in Minisat) #include "prop/cryptominisat.h" #include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" @@ -23,19 +25,29 @@ namespace CVC4 { namespace prop { -BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name) { +BVSatSolverInterface* SatSolverFactory::createMinisat( + context::Context* mainSatContext, + StatisticsRegistry* registry, + const std::string& name) +{ return new BVMinisatSatSolver(registry, mainSatContext, name); } SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry, - const std::string& name) { -return new CryptoMinisatSolver(registry, name); + const std::string& name) +{ +#ifdef CVC4_USE_CRYPTOMINISAT + return new CryptoMinisatSolver(registry, name); +#else + Unreachable("CVC4 was not compiled with Cryptominisat support."); +#endif } - -DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) { +DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat( + StatisticsRegistry* registry) +{ return new MinisatSatSolver(registry); } -} /* CVC4::prop namespace */ -} /* CVC4 namespace */ +} // namespace prop +} // namespace CVC4 |