-
Notifications
You must be signed in to change notification settings - Fork 269
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 and check-vs-2019-cmake-build-and-test CI jobs 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
9bf24e0
commit 8ad9e4a
Showing
8 changed files
with
142 additions
and
13 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,28 @@ | ||
| # 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 11 | ||
| CXX_STANDARD_REQUIRED true | ||
| 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 | ||
|
|
@@ -80,9 +85,11 @@ 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} | ||
|
|
||
| #include "satcheck_minisat2.h" | ||
| # include "satcheck_minisat2.h" | ||
|
|
||
| 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) | ||
|
|
@@ -77,7 +80,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) | ||
| { | ||
|
|
@@ -101,12 +108,20 @@ void satcheck_minisat2_baset<T>::clear_interrupt() | |
|
|
||
| const std::string satcheck_minisat_no_simplifiert::solver_text() | ||
| { | ||
| #ifdef HAVE_MERGESAT | ||
| return "MergeSat 4.0-rc without simplifier"; | ||
| #else | ||
| return "MiniSAT 2.2.1 without simplifier"; | ||
| #endif | ||
| } | ||
|
|
||
| const std::string satcheck_minisat_simplifiert::solver_text() | ||
| { | ||
| #ifdef HAVE_MERGESAT | ||
| return "MergeSat 4.0-rc with simplifier"; | ||
| #else | ||
| return "MiniSAT 2.2.1 with simplifier"; | ||
| #endif | ||
| } | ||
|
|
||
| template<typename T> | ||
|
|
@@ -314,6 +329,10 @@ 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; | ||
| #endif | ||
| } | ||
|
|
||
| template <typename T> | ||
|
|
||