diff options
-rw-r--r-- | src/prop/cryptominisat.h | 45 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 26 |
2 files changed, 22 insertions, 49 deletions
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index bb2f47783..fca2c7aa1 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -87,46 +87,7 @@ public: Statistics d_statistics; }; -} // CVC4::prop -} // CVC4 -#else // CVC4_USE_CRYPTOMINISAT - -namespace CVC4 { -namespace prop { - -class CryptoMinisatSolver : public SatSolver { - -public: - CryptoMinisatSolver(StatisticsRegistry* registry, - const std::string& name = "") { Unreachable(); } - /** Assert a clause in the solver. */ - ClauseId addClause(SatClause& clause, bool removable) { - Unreachable(); - } - - /** Return true if the solver supports native xor resoning */ - bool nativeXor() { Unreachable(); } - - /** Add a clause corresponding to rhs = l1 xor .. xor ln */ - ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { - Unreachable(); - } - - SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); } - SatVariable trueVar() { Unreachable(); } - SatVariable falseVar() { Unreachable(); } - SatValue solve() { Unreachable(); } - SatValue solve(long unsigned int&) { Unreachable(); } - void interrupt() { Unreachable(); } - SatValue value(SatLiteral l) { Unreachable(); } - SatValue modelValue(SatLiteral l) { Unreachable(); } - unsigned getAssertionLevel() const { Unreachable(); } - bool ok() const { return false;}; - - -};/* class CryptoMinisatSolver */ -} // CVC4::prop -} // CVC4 - -#endif // CVC4_USE_CRYPTOMINISAT +} // namespace prop +} // namespace CVC4 +#endif // CVC4_USE_CRYPTOMINISAT 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 |