diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-05-22 06:41:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-22 08:41:50 -0500 |
| commit | c531152e6a707b66b885e508ea61e2a67e195ccc (patch) | |
| tree | a18a2d342b03db1700a963470f2064cf3ac8d086 /src/prop/sat_solver_factory.cpp | |
| parent | ae33f11d0f4156b4d21b9e77f6df59ec0f9e8184 (diff) | |
Add support for SAT solver Kissat. (#4514)
Diffstat (limited to 'src/prop/sat_solver_factory.cpp')
| -rw-r--r-- | src/prop/sat_solver_factory.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 460ab3ece..8f18a6055 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -19,6 +19,7 @@ #include "prop/bvminisat/bvminisat.h" #include "prop/cadical.h" #include "prop/cryptominisat.h" +#include "prop/kissat.h" #include "prop/minisat/minisat.h" namespace CVC4 { @@ -58,5 +59,17 @@ SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry, #endif } +SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry, + const std::string& name) +{ +#ifdef CVC4_USE_KISSAT + KissatSolver* res = new KissatSolver(registry, name); + res->init(); + return res; +#else + Unreachable() << "CVC4 was not compiled with Kissat support."; +#endif +} + } // namespace prop } // namespace CVC4 |