Add support for MergeSat #6439
There are no files selected for viewing
This file contains hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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) || 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 || defined SATCHECK_MERGESAT | ||
| // MergeSat is based on MiniSat2 and is invoked (with suitable defines/ifdefs) | ||
| // via satcheck_minisat2.{h,cpp} | ||
|
|
||
tautschnig marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| typedef satcheck_minisat_simplifiert satcheckt; | ||
| typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert; | ||
|
|
||
This file contains hidden or 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 <util/invariant.h> | ||
| #include <util/make_unique.h> | ||
| #include <util/threeval.h> | ||
|
|
||
| #include <minisat/core/Solver.h> | ||
| #include <minisat/simp/SimpSolver.h> | ||
|
|
||
tautschnig marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| #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-rc 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(); | ||
|
There was a problem hiding this comment. This is not required anymore. There was an issue with how incremental solving was implemented. The latest update of MergeSat has that fixed. Hence, feel free to drop this hunk! There was a problem hiding this comment. Thank you! I don't think we want to merge this PR before MergeSat 4.0 is released, so I suppose 4.0 will include this fix? There was a problem hiding this comment. Likely yes. On the other hand, I am not sure when I will release 4.0, i.. whether I wait for the SAT competition results or not. Hence, feel free to not wait. The major thing that will change is the default configuration of the solver - and the competition will help to identify which one to pick. |
||
| #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> | ||
|
|
||
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.