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/theory/bv | |
| parent | 62f58d62c6c597eeb9cae5e08d74f21c4a5c5c40 (diff) | |
Add support for CaDiCaL as eager BV SAT solver. (#1675)
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index f8317cf15..25610af2b 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -44,8 +44,10 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - switch (options::bvSatSolver()) { - case SAT_SOLVER_MINISAT: { + switch (options::bvSatSolver()) + { + case SAT_SOLVER_MINISAT: + { prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat( d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); @@ -54,12 +56,15 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_satSolver = minisat; break; } + case SAT_SOLVER_CADICAL: + d_satSolver = prop::SatSolverFactory::createCadical( + smtStatisticsRegistry(), "EagerBitblaster"); + break; case SAT_SOLVER_CRYPTOMINISAT: d_satSolver = prop::SatSolverFactory::createCryptoMinisat( smtStatisticsRegistry(), "EagerBitblaster"); break; - default: - Unreachable("Unknown SAT solver type"); + default: Unreachable("Unknown SAT solver type"); } d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, |