From 705959ec99b8963ec47463d11ddef55d82d62325 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Thu, 6 May 2021 00:02:08 +0200 Subject: [PATCH] Add support for MergeSat 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 --- .github/workflows/pull-request-checks.yaml | 55 ++++++++++++++++++++++ scripts/mergesat_CMakeLists.txt | 29 ++++++++++++ src/Makefile | 9 ++++ src/config.inc | 7 ++- src/solvers/CMakeLists.txt | 25 ++++++++-- src/solvers/Makefile | 44 ++++++++++++++++- src/solvers/sat/satcheck.h | 11 ++++- src/solvers/sat/satcheck_minisat2.cpp | 41 ++++++++++++++-- 8 files changed, 210 insertions(+), 11 deletions(-) create mode 100644 scripts/mergesat_CMakeLists.txt diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index d3e728fb4a66..69b85e80c633 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -267,6 +267,61 @@ jobs: exit 1 fi + # This job takes approximately 29 to 42 minutes + check-ubuntu-20_04-cmake-gcc-mergesat: + runs-on: ubuntu-20.04 + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + - name: Fetch dependencies + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 + - name: Confirm z3 solver is available and log the version installed + run: z3 --version + - name: Download cvc-5 from the releases page and make sure it can be deployed + run: | + wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux + chmod u+x cvc5 + mv cvc5 /usr/local/bin + cvc5 --version + - name: Prepare ccache + uses: actions/cache@v3 + with: + path: .ccache + key: ${{ runner.os }}-20.04-Release-mergesat-${{ github.ref }}-${{ github.sha }}-PR + restore-keys: | + ${{ runner.os }}-20.04-Release-mergesat-${{ github.ref }} + ${{ runner.os }}-20.04-Release-mergesat + - name: ccache environment + run: | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV + - name: Configure using CMake + run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="mergesat;cadical" + - name: Check that doc task works + run: ninja -C build doc + - name: Zero ccache stats and limit in size + run: ccache -z --max-size=500M + - name: Build with Ninja + run: ninja -C build -j2 + - name: Print ccache stats + run: ccache -s + - name: Checking completeness of help output + run: scripts/check_help.sh build/bin + - name: Check if package building works + run: | + cd build + ninja package + ls *.deb + - name: Run tests + run: cd build; ctest . -V -L CORE -j2 + # This job takes approximately 34 to 38 minutes check-ubuntu-22_04-make-clang: runs-on: ubuntu-22.04 diff --git a/scripts/mergesat_CMakeLists.txt b/scripts/mergesat_CMakeLists.txt new file mode 100644 index 000000000000..e798eefce158 --- /dev/null +++ b/scripts/mergesat_CMakeLists.txt @@ -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} +) diff --git a/src/Makefile b/src/Makefile index c5b377c9c0d8..c9d86eeca92a 100644 --- a/src/Makefile +++ b/src/Makefile @@ -167,6 +167,15 @@ minisat2-download: @(cd ../minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch) @rm minisat2_2.2.1.orig.tar.gz +mergesat_version = v4.0-rc4 +mergesat-download: + @echo "Downloading MergeSat $(mergesat_version)" + @$(DOWNLOADER) https://github.com/conp-solutions/mergesat/archive/$(mergesat_version).tar.gz + @$(TAR) xfz $(mergesat_version).tar.gz + @rm -Rf ../mergesat + @mv mergesat-$(mergesat_version) ../mergesat + @$(RM) $(mergesat_version).tar.gz + cudd-download: @echo "Downloading Cudd 3.0.0" @$(DOWNLOADER) https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download cudd-3.0.0.tar.gz diff --git a/src/config.inc b/src/config.inc index d83f625abdf4..1ea7f0a46849 100644 --- a/src/config.inc +++ b/src/config.inc @@ -30,12 +30,13 @@ endif #BOOLEFORCE = ../../booleforce-0.4 #MINISAT = ../../MiniSat-p_v1.14 #MINISAT2 = ../../minisat-2.2.1 +#MERGESAT = ../../mergesat-4.0-rc1 #IPASIR = ../../ipasir #GLUCOSE = ../../glucose-syrup #CADICAL = ../../cadical # select default solver to be minisat2 if no other is specified -ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(CADICAL),) +ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(MERGESAT)$(PICOSAT)$(CADICAL),) MINISAT2 = ../../minisat-2.2.1 endif @@ -63,6 +64,10 @@ ifneq ($(MINISAT2),) CP_CXXFLAGS += -DSATCHECK_MINISAT2 endif +ifneq ($(MERGESAT),) + CP_CXXFLAGS += -DSATCHECK_MERGESAT +endif + ifneq ($(GLUCOSE),) CP_CXXFLAGS += -DSATCHECK_GLUCOSE endif diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 14d00cb94ee9..4e831142d7f8 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -9,7 +9,7 @@ set(chaff_source set(minisat_source ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_minisat.cpp ) -set(minisat2_source +set(minisat2_mergesat_source ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_minisat2.cpp ) set(glucose_source @@ -44,7 +44,7 @@ file(GLOB_RECURSE sources "*.cpp" "*.h") list(REMOVE_ITEM sources ${chaff_source} ${minisat_source} - ${minisat2_source} + ${minisat2_mergesat_source} ${glucose_source} ${squolem2_source} ${cudd_source} @@ -81,7 +81,7 @@ foreach(SOLVER ${sat_impl}) SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS ) - target_sources(solvers PRIVATE ${minisat2_source}) + target_sources(solvers PRIVATE ${minisat2_mergesat_source}) target_link_libraries(solvers minisat2-condensed) elseif("${SOLVER}" STREQUAL "system-minisat2") @@ -98,6 +98,25 @@ foreach(SOLVER ${sat_impl}) else() message(FATAL_ERROR "Unable to find header file for preinstalled minisat2") endif() + elseif("${SOLVER}" STREQUAL "mergesat") + message(STATUS "Building solvers with MergeSat") + + download_project(PROJ mergesat + URL https://github.com/conp-solutions/mergesat/archive/v4.0-rc4.tar.gz + PATCH_COMMAND true + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/mergesat_CMakeLists.txt CMakeLists.txt + URL_MD5 aba2a8d6867d0b77f9cefac8515c2d72 + ) + + add_subdirectory(${mergesat_SOURCE_DIR} ${mergesat_BINARY_DIR}) + + target_compile_definitions(solvers PUBLIC + SATCHECK_MERGESAT HAVE_MERGESAT __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS + ) + + target_sources(solvers PRIVATE ${minisat2_mergesat_source}) + + target_link_libraries(solvers mergesat-condensed) elseif("${SOLVER}" STREQUAL "glucose") message(STATUS "Building solvers with glucose") diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 64f606312af4..970be4a945b5 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -22,6 +22,21 @@ ifneq ($(MINISAT2),) CLEANFILES += $(MINISAT2_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MINISAT2_LIB)) endif +ifneq ($(MERGESAT),) + # MergeSat is based on MiniSat2 and is invoked (with suitable defines/ifdefs) + # via satcheck_minisat2.{h,cpp} + MERGESAT_SRC=sat/satcheck_minisat2.cpp + MERGESAT_INCLUDE=-I $(MERGESAT) + MERGESAT_LIB=$(MERGESAT)/minisat/core/Lookahead$(OBJEXT) \ + $(MERGESAT)/minisat/core/Solver$(OBJEXT) \ + $(MERGESAT)/minisat/simp/SimpSolver$(OBJEXT) \ + $(MERGESAT)/minisat/utils/ccnr$(OBJEXT) \ + $(MERGESAT)/minisat/utils/Options$(OBJEXT) \ + $(MERGESAT)/minisat/utils/System$(OBJEXT) + CP_CXXFLAGS += -DHAVE_MERGESAT -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS + CLEANFILES += $(MERGESAT_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MERGESAT_LIB)) +endif + ifneq ($(IPASIR),) IPASIR_SRC=sat/satcheck_ipasir.cpp IPASIR_INCLUDE=-I $(IPASIR) @@ -75,6 +90,7 @@ SRC = $(BOOLEFORCE_SRC) \ $(GLUCOSE_SRC) \ $(LINGELING_SRC) \ $(MINISAT2_SRC) \ + $(MERGESAT_SRC) \ $(IPASIR_SRC) \ $(MINISAT_SRC) \ $(PICOSAT_SRC) \ @@ -232,6 +248,31 @@ $(MINISAT2)/minisat/core/Solver$(OBJEXT): $(MINISAT2)/minisat/core/Solver.cc endif endif +ifneq ($(MERGESAT),) +ifeq ($(BUILD_ENV_),MSVC) +sat/satcheck_minisat2$(OBJEXT): sat/satcheck_minisat2.cpp + $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ + +$(MERGESAT)/minisat/core/Lookahead$(OBJEXT): $(MERGESAT)/minisat/core/Lookahead.cc + $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ + +$(MERGESAT)/minisat/core/Solver$(OBJEXT): $(MERGESAT)/minisat/core/Solver.cc + $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ + +$(MERGESAT)/minisat/simp/SimpSolver$(OBJEXT): $(MERGESAT)/minisat/simp/SimpSolver.cc + $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ + +$(MERGESAT)/minisat/utils/ccnr$(OBJEXT): $(MERGESAT)/minisat/utils/ccnr.cc + $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ + +$(MERGESAT)/minisat/utils/Options$(OBJEXT): $(MERGESAT)/minisat/utils/Options.cc + $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ + +$(MERGESAT)/minisat/utils/System$(OBJEXT): $(MERGESAT)/minisat/utils/System.cc + $(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@ +endif +endif + ifneq ($(GLUCOSE),) ifeq ($(BUILD_ENV_),MSVC) sat/satcheck_glucose$(OBJEXT): sat/satcheck_glucose.cpp @@ -247,6 +288,7 @@ endif INCLUDES += -I .. \ $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \ + $(MERGESAT_INCLUDE) \ $(IPASIR_INCLUDE) \ $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \ $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) $(CADICAL_INCLUDE) @@ -265,7 +307,7 @@ endif endif SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \ - $(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \ + $(MINISAT2_LIB) $(MERGESAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \ $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) $(CADICAL_LIB) SOLVER_OBJS = $(filter %$(OBJEXT), $(SOLVER_LIB)) diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h index 733896086aa3..c9dfafe69573 100644 --- a/src/solvers/sat/satcheck.h +++ b/src/solvers/sat/satcheck.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com // #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, kroening@kroening.com #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, kroening@kroening.com # 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; diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 2c9799cc7009..b269fb2893e5 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com # include #endif -#include - #include #include #include @@ -22,8 +20,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#ifndef HAVE_MINISAT2 -#error "Expected HAVE_MINISAT2" +#include +#include + +// 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 &dest) @@ -91,7 +94,11 @@ void satcheck_minisat2_baset::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::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 @@ -271,6 +286,15 @@ propt::resultt satcheck_minisat2_baset::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::satcheck_minisat2_baset( solver(util_make_unique()), time_limit_seconds(0) { +#ifdef HAVE_MERGESAT + if constexpr(std::is_same::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