forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
MergeSat is a recent SAT solver that fits the MiniSat2 interface. Run the check-ubuntu-20_04-cmake-gcc CI job with MergeSat to continuously confirm that this configuration actually works. To use MergeSat as a proper SAT backend, some extensions might be dropped. Especially being able to print memory usage is not helpful for CBMC, but requires pulling in a new dependency. Signed-off-by: Norbert Manthey <[email protected]>
- Loading branch information
1 parent
a8de0b7
commit 705959e
Showing
8 changed files
with
210 additions
and
11 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| # CBMC only uses part of MergeSat. | ||
| # This CMakeLists is designed to build just the parts that are needed. | ||
|
|
||
| add_library(mergesat-condensed | ||
| minisat/core/Lookahead.cc | ||
| minisat/core/Solver.cc | ||
| minisat/simp/SimpSolver.cc | ||
| minisat/utils/ccnr.cc | ||
| minisat/utils/Options.cc | ||
| minisat/utils/System.cc | ||
| ) | ||
|
|
||
| set_target_properties( | ||
| mergesat-condensed | ||
| PROPERTIES | ||
| CXX_STANDARD 17 | ||
| CXX_STANDARD_REQUIRED true | ||
| CXX_EXTENSIONS OFF | ||
| XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" | ||
| ) | ||
|
|
||
| if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") | ||
| target_compile_options(mergesat-condensed PUBLIC /w) | ||
| endif() | ||
|
|
||
| target_include_directories(mergesat-condensed | ||
| PUBLIC | ||
| ${CMAKE_CURRENT_SOURCE_DIR} | ||
| ) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected] | |
| // #define SATCHECK_ZCHAFF | ||
| // #define SATCHECK_MINISAT1 | ||
| // #define SATCHECK_MINISAT2 | ||
| // #define SATCHECK_MERGESAT | ||
| // #define SATCHECK_GLUCOSE | ||
| // #define SATCHECK_BOOLEFORCE | ||
| // #define SATCHECK_PICOSAT | ||
|
|
@@ -39,6 +40,10 @@ Author: Daniel Kroening, [email protected] | |
| #define SATCHECK_MINISAT2 | ||
| #endif | ||
|
|
||
| #if defined(HAVE_MERGESAT) && !defined(SATCHECK_MERGESAT) | ||
| # define SATCHECK_MERGESAT | ||
| #endif | ||
|
|
||
| #if defined(HAVE_GLUCOSE) && !defined(SATCHECK_GLUCOSE) | ||
| #define SATCHECK_GLUCOSE | ||
| #endif | ||
|
|
@@ -71,7 +76,7 @@ Author: Daniel Kroening, [email protected] | |
| # include "satcheck_minisat.h" | ||
| #endif | ||
|
|
||
| #if defined SATCHECK_MINISAT2 | ||
| #if defined(SATCHECK_MINISAT2) || defined(SATCHECK_MERGESAT) | ||
| # include "satcheck_minisat2.h" | ||
| #endif | ||
|
|
||
|
|
@@ -110,7 +115,9 @@ typedef satcheck_booleforcet satcheck_no_simplifiert; | |
| typedef satcheck_minisat1t satcheckt; | ||
| typedef satcheck_minisat1t satcheck_no_simplifiert; | ||
|
|
||
| #elif defined SATCHECK_MINISAT2 | ||
| #elif defined SATCHECK_MINISAT2 || defined SATCHECK_MERGESAT | ||
| // MergeSat is based on MiniSat2 and is invoked (with suitable defines/ifdefs) | ||
| // via satcheck_minisat2.{h,cpp} | ||
|
|
||
| typedef satcheck_minisat_simplifiert satcheckt; | ||
| typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert; | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -13,17 +13,20 @@ Author: Daniel Kroening, [email protected] | |
| # include <unistd.h> | ||
| #endif | ||
|
|
||
| #include <limits> | ||
|
|
||
| #include <util/invariant.h> | ||
| #include <util/make_unique.h> | ||
| #include <util/threeval.h> | ||
|
|
||
| #include <minisat/core/Solver.h> | ||
| #include <minisat/simp/SimpSolver.h> | ||
|
|
||
| #ifndef HAVE_MINISAT2 | ||
| #error "Expected HAVE_MINISAT2" | ||
| #include <cstdlib> | ||
| #include <limits> | ||
|
|
||
| // MergeSat is based on MiniSat2; variations in their API are handled via | ||
| // #ifdefs | ||
| #if !defined(HAVE_MINISAT2) && !defined(HAVE_MERGESAT) | ||
| # error "Expected HAVE_MINISAT2 or HAVE_MERGESAT" | ||
| #endif | ||
|
|
||
| void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest) | ||
|
|
@@ -91,7 +94,11 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value) | |
| try | ||
| { | ||
| add_variables(); | ||
| #ifdef HAVE_MERGESAT | ||
| solver->setPolarity(a.var_no(), value); | ||
| #else | ||
| solver->setPolarity(a.var_no(), value ? l_True : l_False); | ||
| #endif | ||
| } | ||
| catch(Minisat::OutOfMemoryException) | ||
| { | ||
|
|
@@ -115,12 +122,20 @@ void satcheck_minisat2_baset<T>::clear_interrupt() | |
|
|
||
| std::string satcheck_minisat_no_simplifiert::solver_text() const | ||
| { | ||
| #ifdef HAVE_MERGESAT | ||
| return "MergeSat 4.0-rc4 without simplifier"; | ||
| #else | ||
| return "MiniSAT 2.2.1 without simplifier"; | ||
| #endif | ||
| } | ||
|
|
||
| std::string satcheck_minisat_simplifiert::solver_text() const | ||
| { | ||
| #ifdef HAVE_MERGESAT | ||
| return "MergeSat 4.0-rc4 with simplifier"; | ||
| #else | ||
| return "MiniSAT 2.2.1 with simplifier"; | ||
| #endif | ||
| } | ||
|
|
||
| template<typename T> | ||
|
|
@@ -271,6 +286,15 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve(const bvt &assumptions) | |
|
|
||
| #endif | ||
|
|
||
| #ifdef HAVE_MERGESAT | ||
| // We do not actually use MergeSat's "constrain" clauses at the moment, but | ||
| // MergeSat internally still uses them to track UNSAT. To make sure we | ||
| // aren't stuck with "UNSAT" in incremental calls the status needs to be | ||
| // reset. | ||
| // See also https://github.com/conp-solutions/mergesat/pull/124 | ||
| ((Minisat::Solver *)solver.get())->reset_constrain_clause(); | ||
| #endif | ||
|
|
||
| if(solver_result == l_True) | ||
| { | ||
| log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom; | ||
|
|
@@ -328,6 +352,15 @@ satcheck_minisat2_baset<T>::satcheck_minisat2_baset( | |
| solver(util_make_unique<T>()), | ||
| time_limit_seconds(0) | ||
| { | ||
| #ifdef HAVE_MERGESAT | ||
| if constexpr(std::is_same<T, Minisat::SimpSolver>::value) | ||
| { | ||
| solver->grow_iterations = false; | ||
| // limit the amount of work spent in simplification; the optimal value needs | ||
| // to be found via benchmarking | ||
| solver->nr_max_simp_cls = 1000000; | ||
| } | ||
| #endif | ||
| } | ||
|
|
||
| template <typename T> | ||
|
|
||