diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-02-03 12:38:09 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-03 12:38:09 -0800 |
commit | ac998a45ae64c589aeb79c5fd72234468e40451c (patch) | |
tree | ade5266bbc0a5279ea76b4eb5c9d8a77e3ab967d /src/options | |
parent | a6c122da21b3d5b9c37d9ec670dec766eaff7001 (diff) |
Add BV solver bitblast. (#5851)
This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/bv_options.toml | 3 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 5 |
2 files changed, 6 insertions, 2 deletions
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 6a0ca913b..acb010a2e 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -236,6 +236,9 @@ header = "options/bv_options.h" default = "LAZY" help = "choose bit-vector solver, see --bv-solver=help" help_mode = "Bit-vector solvers." +[[option.mode.BITBLAST]] + name = "bitblast" + help = "Enables bitblasting solver." [[option.mode.LAZY]] name = "lazy" help = "Enables the lazy BV solver infrastructure." diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index fe37e9363..ac33d9c51 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -145,8 +145,9 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) throw OptionException(ss.str()); } - if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL - || m == SatSolverMode::KISSAT) + if (options::bvSolver() != options::BVSolver::BITBLAST + && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL + || m == SatSolverMode::KISSAT)) { if (options::bitblastMode() == options::BitblastMode::LAZY && options::bitblastMode.wasSetByUser()) |