From 2ddd85b53d6dedbd03b30533c1f826cd774f1149 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Mar 2022 11:37:38 +0000 Subject: [PATCH 01/19] Build using C++17 This raises the minimum GCC version supported to 7 (see https://gcc.gnu.org/projects/cxx-status.html#cxx17). Add -Wno-register to silence warnings about the use of the `register` storage class by older flex versions (as present on macOS). CMake doesn't know about C++ 17 until version 3.8, so we need to hard-code the necessary command-line options. --- .clang-format | 2 +- CMakeLists.txt | 9 ++------- COMPILING.md | 2 +- scripts/bash-autocomplete/extract_switches.sh | 2 +- scripts/glucose_CMakeLists.txt | 2 -- scripts/minisat2_CMakeLists.txt | 2 -- src/common | 12 ++++++------ src/config.inc | 2 +- src/solvers/CMakeLists.txt | 7 ++----- 9 files changed, 14 insertions(+), 26 deletions(-) diff --git a/.clang-format b/.clang-format index fdd2d857fcd..6b5af452210 100644 --- a/.clang-format +++ b/.clang-format @@ -71,7 +71,7 @@ SpacesInCStyleCastParentheses: 'false' SpacesInContainerLiterals: 'false' SpacesInParentheses: 'false' SpacesInSquareBrackets: 'false' -Standard: c++11 +Standard: c++17 TabWidth: '2' UseTab: Never --- diff --git a/CMakeLists.txt b/CMakeLists.txt index 8945f9429c6..2b239c41e03 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -72,10 +72,9 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR set(CMAKE_CXX_FLAGS_RELEASE "-O2") set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g") # Enable lots of warnings - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++17 -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wno-register -Wswitch-enum") elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") - # This would be the place to enable warnings for Windows builds, although - # config.inc doesn't seem to do that currently + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /std:c++17 /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF ") # Include Git Bash Environment (rqeuired for download_project (patch)) find_package(Git) @@ -180,16 +179,12 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR endif() function(cprover_default_properties) - set(CBMC_CXX_STANDARD 11) - set(CBMC_CXX_STANDARD_REQUIRED true) set(CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening") set_target_properties( ${ARGN} PROPERTIES - CXX_STANDARD ${CBMC_CXX_STANDARD} - CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED} XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY}) endfunction() diff --git a/COMPILING.md b/COMPILING.md index 3fb133a1be3..eec73be1c95 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -152,7 +152,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. ``` dnf install gcc gcc-c++ flex bison curl patch ``` - Note that you need g++ version 5.0 or newer. + Note that you need g++ version 7.0 or newer. On Amazon Linux and similar distributions, do as root: ``` diff --git a/scripts/bash-autocomplete/extract_switches.sh b/scripts/bash-autocomplete/extract_switches.sh index c876e420af7..06a480fa925 100755 --- a/scripts/bash-autocomplete/extract_switches.sh +++ b/scripts/bash-autocomplete/extract_switches.sh @@ -6,7 +6,7 @@ set -e cd `dirname $0` echo "Compiling the helper file to extract the raw list of parameters from cbmc" -g++ -E -dM -std=c++11 -I../../src ../../src/cbmc/cbmc_parse_options.cpp -o macros.c +g++ -E -dM -std=c++17 -I../../src ../../src/cbmc/cbmc_parse_options.cpp -o macros.c echo CBMC_OPTIONS >> macros.c echo "Converting the raw parameter list to the format required by autocomplete scripts" diff --git a/scripts/glucose_CMakeLists.txt b/scripts/glucose_CMakeLists.txt index b2116ce91f4..2faee91eeb9 100644 --- a/scripts/glucose_CMakeLists.txt +++ b/scripts/glucose_CMakeLists.txt @@ -9,8 +9,6 @@ add_library(glucose-condensed set_target_properties( glucose-condensed PROPERTIES - CXX_STANDARD 11 - CXX_STANDARD_REQUIRED true XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) diff --git a/scripts/minisat2_CMakeLists.txt b/scripts/minisat2_CMakeLists.txt index 71e39ff35b4..2192d1f3e09 100644 --- a/scripts/minisat2_CMakeLists.txt +++ b/scripts/minisat2_CMakeLists.txt @@ -10,8 +10,6 @@ add_library(minisat2-condensed set_target_properties( minisat2-condensed PROPERTIES - CXX_STANDARD 11 - CXX_STANDARD_REQUIRED true XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) diff --git a/src/common b/src/common index d6de5219be7..7ddf92fa5e0 100644 --- a/src/common +++ b/src/common @@ -34,11 +34,11 @@ endif CP_CFLAGS = -MMD -MP CXXFLAGS ?= -Wall -O2 ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),) - CP_CXXFLAGS += -MMD -MP -mmacosx-version-min=10.15 -std=c++11 -stdlib=libc++ + CP_CXXFLAGS += -MMD -MP -mmacosx-version-min=10.15 -std=c++17 -stdlib=libc++ LINKFLAGS += -mmacosx-version-min=10.15 -stdlib=libc++ LINKNATIVE += -mmacosx-version-min=10.15 -stdlib=libc++ else - CP_CXXFLAGS += -MMD -MP -std=c++11 + CP_CXXFLAGS += -MMD -MP -std=c++17 endif ifeq ($(filter -O%,$(CXXFLAGS)),) CP_CXXFLAGS += -O2 @@ -102,13 +102,13 @@ else ifeq ($(BUILD_ENV_),Cygwin) CFLAGS ?= -Wall -O2 CXXFLAGS ?= -Wall -O2 CP_CFLAGS = -MMD -MP - CP_CXXFLAGS += -MMD -MP -std=c++11 -U__STRICT_ANSI__ + CP_CXXFLAGS += -MMD -MP -std=c++17 -U__STRICT_ANSI__ # Cygwin-g++ has problems with statically linking exception code. # If linking fails, remove -static. - LINKFLAGS = -static -std=c++11 + LINKFLAGS = -static -std=c++17 LINKLIB = ar rcT $@ $^ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) - LINKNATIVE = $(HOSTCXX) -std=c++11 -o $@ $^ -static + LINKNATIVE = $(HOSTCXX) -std=c++17 -o $@ $^ -static ifeq ($(origin CC),default) #CC = gcc CC = x86_64-w64-mingw32-gcc @@ -133,7 +133,7 @@ else ifeq ($(BUILD_ENV_),MSVC) DEPEXT = .dep EXEEXT = .exe CFLAGS ?= /W3 /O2 /GF - CXXFLAGS ?= /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF + CXXFLAGS ?= /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++17 CP_CFLAGS = CP_CXXFLAGS += LINKLIB = lib /NOLOGO /OUT:$@ $^ diff --git a/src/config.inc b/src/config.inc index d523ee6b6b4..d39a1efdcc6 100644 --- a/src/config.inc +++ b/src/config.inc @@ -5,7 +5,7 @@ BUILD_ENV = AUTO ifeq ($(BUILD_ENV),MSVC) #CXXFLAGS += /Wall /WX else - CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wswitch-enum + CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wno-register -Wswitch-enum endif ifeq ($(CPROVER_WITH_PROFILING),1) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 744def4861b..36ca596ff64 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -1,6 +1,3 @@ -set(CMAKE_CXX_STANDARD 11) -set(CMAKE_CXX_STANDARD_REQUIRED true) - # We may use one of several different solver libraries. # The following files wrap the chosen solver library. # We remove them all from the solver-library sources list, and then add the @@ -109,7 +106,7 @@ elseif("${sat_impl}" STREQUAL "cadical") download_project(PROJ cadical URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz PATCH_COMMAND true - COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14 + COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++17 URL_MD5 b44874501a175106424f4bd5de29aa59 ) @@ -139,7 +136,7 @@ elseif("${sat_impl}" STREQUAL "ipasir-cadical") download_project(PROJ cadical URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz PATCH_COMMAND true - COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14 + COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++17 URL_MD5 b44874501a175106424f4bd5de29aa59 ) From 2cd58ded5b61f510ea45e7dc794e24627983a621 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Thu, 6 May 2021 00:02:08 +0200 Subject: [PATCH 02/19] 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 | 2 +- scripts/mergesat_CMakeLists.txt | 28 ++++++++++++++ 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 | 40 ++++++++++++++++++-- 8 files changed, 154 insertions(+), 12 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 fe9f7edb259..d15e2d435b3 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -224,7 +224,7 @@ jobs: run: | mkdir build cd build - cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ + cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl=mergesat - name: Check that doc task works run: | cd build diff --git a/scripts/mergesat_CMakeLists.txt b/scripts/mergesat_CMakeLists.txt new file mode 100644 index 00000000000..b2f5c0cf03c --- /dev/null +++ b/scripts/mergesat_CMakeLists.txt @@ -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} +) diff --git a/src/Makefile b/src/Makefile index 92afa0ba26b..1ef934462d5 100644 --- a/src/Makefile +++ b/src/Makefile @@ -139,6 +139,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 = 4.0-rc +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 d39a1efdcc6..ba11e70f02f 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-3.0 #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 36ca596ff64..5108e0b918c 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} @@ -78,9 +78,28 @@ if("${sat_impl}" STREQUAL "minisat2") 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("${sat_impl}" STREQUAL "mergesat") + message(STATUS "Building solvers with MergeSat") + + download_project(PROJ mergesat + URL https://github.com/conp-solutions/mergesat/archive/4.0-rc.tar.gz + PATCH_COMMAND true + COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/mergesat_CMakeLists.txt CMakeLists.txt + URL_MD5 069c0d4f69723847055c3491cff5940e + ) + + 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("${sat_impl}" STREQUAL "glucose") message(STATUS "Building solvers with glucose") diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 85800d1473c..f0ab16bc9e2 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) @@ -74,6 +89,7 @@ SRC = $(BOOLEFORCE_SRC) \ $(GLUCOSE_SRC) \ $(LINGELING_SRC) \ $(MINISAT2_SRC) \ + $(MERGESAT_SRC) \ $(IPASIR_SRC) \ $(MINISAT_SRC) \ $(PICOSAT_SRC) \ @@ -229,6 +245,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 @@ -244,6 +285,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) @@ -262,7 +304,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 c7175fa414c..2ee3ac9edde 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 @@ -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; diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 25a82e6f8df..8f0f72a6b26 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) @@ -77,7 +80,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) { @@ -101,12 +108,20 @@ void satcheck_minisat2_baset::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 @@ -257,6 +272,14 @@ propt::resultt satcheck_minisat2_baset::do_prop_solve() #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. + ((Minisat::Solver *)solver.get())->reset_constrain_clause(); +#endif + if(solver_result == l_True) { log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom; @@ -314,6 +337,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 From 31ec09cc40993d85549a0aa5a03cee01efa23da6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Aug 2022 12:52:45 +0000 Subject: [PATCH 03/19] Use CaDiCaL configuration tweaked for CBMC Testing thousands of configuration this appeared to improve performance. --- src/solvers/sat/satcheck_cadical.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/solvers/sat/satcheck_cadical.cpp b/src/solvers/sat/satcheck_cadical.cpp index 567f03aeb3f..3ca60bd95e3 100644 --- a/src/solvers/sat/satcheck_cadical.cpp +++ b/src/solvers/sat/satcheck_cadical.cpp @@ -136,7 +136,19 @@ void satcheck_cadicalt::set_assignment(literalt a, bool value) satcheck_cadicalt::satcheck_cadicalt(message_handlert &message_handler) : cnf_solvert(message_handler), solver(new CaDiCaL::Solver()) { - solver->set("quiet", 1); + bool ok; + ok = solver->set("quiet", 1); + CHECK_RETURN(ok); + ok = solver->set("chrono", 2); + CHECK_RETURN(ok); + ok = solver->set("cover", 1); + CHECK_RETURN(ok); + ok = solver->set("target", 0); + CHECK_RETURN(ok); + ok = solver->set("vivify", 0); + CHECK_RETURN(ok); + ok = solver->set("seed", 3); + CHECK_RETURN(ok); } satcheck_cadicalt::~satcheck_cadicalt() From 0f70d2992b8aff03dfc24165ab6e4c8deaf7c2d4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2022 08:26:06 +0000 Subject: [PATCH 04/19] propt::l_set_to: avoid duplicate work Avoid calling `lcnf` with constants when the actual solving back-end will just filter them out. --- src/solvers/prop/prop.h | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h index 65a5f362464..a9dbb0c32ee 100644 --- a/src/solvers/prop/prop.h +++ b/src/solvers/prop/prop.h @@ -44,13 +44,20 @@ class propt virtual void l_set_to(literalt a, bool value) { - set_equal(a, const_literal(value)); + if(value) + lcnf({a}); + else + lcnf({!a}); } void l_set_to_true(literalt a) - { l_set_to(a, true); } + { + lcnf({a}); + } void l_set_to_false(literalt a) - { l_set_to(a, false); } + { + lcnf({!a}); + } // constraints void lcnf(literalt l0, literalt l1) From c5b30b8426784ca61c7a2319de7b81154c1aa0e4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 14 Jul 2022 13:53:15 +0000 Subject: [PATCH 05/19] Cleanup the API of bv_utilst::adder Don't make every caller create an uninitialised literal. --- src/solvers/flattening/bv_utils.cpp | 32 +++++++++++++---------------- src/solvers/flattening/bv_utils.h | 5 ++--- 2 files changed, 16 insertions(+), 21 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 90f1f7b5983..32f6de15e7b 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -290,20 +290,21 @@ literalt bv_utilst::carry(literalt a, literalt b, literalt c) } } -void bv_utilst::adder( +literalt bv_utilst::adder( bvt &sum, const bvt &op, - literalt carry_in, - literalt &carry_out) + literalt carry_in) { PRECONDITION(sum.size() == op.size()); - carry_out=carry_in; + literalt carry_out = carry_in; for(std::size_t i=0; i Date: Thu, 7 Jul 2022 08:29:21 +0000 Subject: [PATCH 06/19] Don't generate unnecessary fresh symbols for the GOTO trace We can safely record the values of expressions by adding `expr == expr` as constraints in order to be able to fetch and display them in the GOTO trace. This was already being done for declarations. Introducing new symbols just adds unnecessary variables to the formula. --- .../pointers-conversions/pointer_to_int.desc | 2 +- src/goto-symex/build_goto_trace.cpp | 19 +++----- src/goto-symex/symex_target_equation.cpp | 47 ++++--------------- src/solvers/smt2/smt2_conv.cpp | 25 +++++----- 4 files changed, 27 insertions(+), 66 deletions(-) diff --git a/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc b/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc index f9cfae9d67e..7c1f2188317 100644 --- a/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc +++ b/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG pointer_to_int.c --trace \[main\.assertion\.1\] line \d+ expected result == -1: success: SUCCESS diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 6830f352344..2296f917836 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -351,10 +351,12 @@ void build_goto_trace( goto_trace_step.io_id = SSA_step.io_id; goto_trace_step.formatted = SSA_step.formatted; goto_trace_step.called_function = SSA_step.called_function; - goto_trace_step.function_arguments = SSA_step.converted_function_arguments; - for(auto &arg : goto_trace_step.function_arguments) - arg = decision_procedure.get(arg); + for(const auto &arg : SSA_step.converted_function_arguments) + { + goto_trace_step.function_arguments.push_back( + simplify_expr(decision_procedure.get(arg), ns)); + } // update internal field for specific variables in the counterexample update_internal_field(SSA_step, goto_trace_step, ns); @@ -391,15 +393,8 @@ void build_goto_trace( for(const auto &j : SSA_step.converted_io_args) { - if(j.is_constant() || j.id() == ID_string_constant) - { - goto_trace_step.io_args.push_back(j); - } - else - { - exprt tmp = decision_procedure.get(j); - goto_trace_step.io_args.push_back(tmp); - } + goto_trace_step.io_args.push_back( + simplify_expr(decision_procedure.get(j), ns)); } if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto()) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 8c97da8e1b1..09365b72cfb 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -620,33 +620,18 @@ void symex_target_equationt::convert_function_calls( { if(!step.ignore) { - and_exprt::operandst conjuncts; step.converted_function_arguments.reserve(step.ssa_function_arguments.size()); for(const auto &arg : step.ssa_function_arguments) { - if(arg.is_constant() || - arg.id()==ID_string_constant) - step.converted_function_arguments.push_back(arg); - else + if(!arg.is_constant() && arg.id() != ID_string_constant) { - const irep_idt identifier="symex::args::"+std::to_string(argument_count++); - symbol_exprt symbol(identifier, arg.type()); - - equal_exprt eq(arg, symbol); + equal_exprt eq{arg, arg}; merge_irep(eq); - - decision_procedure.set_to(eq, true); - conjuncts.push_back(eq); - step.converted_function_arguments.push_back(symbol); + decision_procedure.set_to_true(eq); } + step.converted_function_arguments.push_back(arg); } - with_solver_hardness( - decision_procedure, - [step_index, &conjuncts, &step](solver_hardnesst &hardness) { - hardness.register_ssa( - step_index, conjunction(conjuncts), step.source.pc); - }); } ++step_index; } @@ -659,32 +644,16 @@ void symex_target_equationt::convert_io(decision_proceduret &decision_procedure) { if(!step.ignore) { - and_exprt::operandst conjuncts; for(const auto &arg : step.io_args) { - if(arg.is_constant() || - arg.id()==ID_string_constant) - step.converted_io_args.push_back(arg); - else + if(!arg.is_constant() && arg.id() != ID_string_constant) { - const irep_idt identifier = - "symex::io::" + std::to_string(io_count++); - symbol_exprt symbol(identifier, arg.type()); - - equal_exprt eq(arg, symbol); + equal_exprt eq{arg, arg}; merge_irep(eq); - - decision_procedure.set_to(eq, true); - conjuncts.push_back(eq); - step.converted_io_args.push_back(symbol); + decision_procedure.set_to_true(eq); } + step.converted_io_args.push_back(arg); } - with_solver_hardness( - decision_procedure, - [step_index, &conjuncts, &step](solver_hardnesst &hardness) { - hardness.register_ssa( - step_index, conjunction(conjuncts), step.source.pc); - }); } ++step_index; } diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index f720cf54bb8..ba3524d792d 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -297,14 +297,6 @@ exprt smt2_convt::get(const exprt &expr) const if(it!=identifier_map.end()) return it->second.value; } - else if(expr.id()==ID_member) - { - const member_exprt &member_expr=to_member_expr(expr); - exprt tmp=get(member_expr.struct_op()); - if(tmp.is_nil()) - return nil_exprt(); - return member_exprt(tmp, member_expr.get_component_name(), expr.type()); - } else if(expr.id() == ID_literal) { auto l = to_literal_expr(expr).get_literal(); @@ -323,14 +315,17 @@ exprt smt2_convt::get(const exprt &expr) const } else if(expr.is_constant()) return expr; - else if(const auto &array = expr_try_dynamic_cast(expr)) + else if(expr.has_operands()) { - exprt array_copy = *array; - for(auto &element : array_copy.operands()) + exprt copy = expr; + for(auto &op : copy.operands()) { - element = get(element); + exprt eval_op = get(op); + if(eval_op.is_nil()) + return nil_exprt{}; + op = std::move(eval_op); } - return array_copy; + return copy; } return nil_exprt(); @@ -4641,7 +4636,9 @@ void smt2_convt::set_to(const exprt &expr, bool value) const irep_idt &identifier= to_symbol_expr(equal_expr.lhs()).get_identifier(); - if(identifier_map.find(identifier)==identifier_map.end()) + if( + identifier_map.find(identifier) == identifier_map.end() && + equal_expr.lhs() != equal_expr.rhs()) { identifiert &id=identifier_map[identifier]; CHECK_RETURN(id.type.is_nil()); From 99095936e7a4cbe80b9b27316be1b4bd9562c0ae Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 11 Jul 2022 13:00:16 +0000 Subject: [PATCH 07/19] Optimise propositional encoding of object_size Avoid creating equalities over the postponed bitvector when the object literals trivially aren't equal, and directly encode bitwise equality when the object literals are trivially equal (and stop searching for a matching object). In all other cases, avoid unnecessary Tseitin variables to encode the postponed bitvector equality. --- src/solvers/flattening/bv_pointers.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 0e10621a8f3..6e2be1ded4f 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -958,9 +958,26 @@ void bv_pointerst::do_postponed( PRECONDITION(size_bv.size() == postponed.bv.size()); literalt l1=bv_utils.equal(bv, saved_bv); + if(l1.is_true()) + { + for(std::size_t i = 0; i < postponed.bv.size(); ++i) + prop.set_equal(postponed.bv[i], size_bv[i]); + break; + } + else if(l1.is_false()) + continue; +#define COMPACT_OBJECT_SIZE_EQ +#ifndef COMPACT_OBJECT_SIZE_EQ literalt l2=bv_utils.equal(postponed.bv, size_bv); prop.l_set_to_true(prop.limplies(l1, l2)); +#else + for(std::size_t i = 0; i < postponed.bv.size(); ++i) + { + prop.lcnf({!l1, !postponed.bv[i], size_bv[i]}); + prop.lcnf({!l1, postponed.bv[i], !size_bv[i]}); + } +#endif } } else From 9d66549c0728f5c015a0e8d8f942c7d4c1cf5a18 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 11 Jul 2022 13:04:53 +0000 Subject: [PATCH 08/19] bv_utilst::equal: stop early when the result will be false There is no need to create any further bit-level equalities when the result will be false anyway. On aws-c-common/aws_hash_iter_next, this reduces the number of Boolean variables from 2291304 to 584628, and the time spent in CaDiCaL from 191 seconds to 22 seconds. --- src/solvers/flattening/bv_utils.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 32f6de15e7b..e1c63515aa0 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -1181,6 +1181,16 @@ literalt bv_utilst::equal(const bvt &op0, const bvt &op1) return equal_const(op0, op1); #endif + // If the eventual result would be "false" anyway, avoid constructing + // equalities that would end up not affecting the satisfiability of the + // formula (effectively doing preprocessing steps that the SAT solver would + // otherwise have to undertake). + for(std::size_t i = 0; i < op0.size(); i++) + { + if(op0[i] != op1[i] && op0[i].var_no() == op1[i].var_no()) + return const_literal(false); + } + bvt equal_bv; equal_bv.resize(op0.size()); From 5fe1967a71d6d93cff324541f0d70e6b566dc85e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2022 08:33:03 +0000 Subject: [PATCH 09/19] Use set_to_true in convert_decls This avoids creating a variable that is equal to the truth value of the equality. While at it, also add a call to merge_irep to clean up the equality expression that was created. --- src/goto-symex/symex_target_equation.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 09365b72cfb..5f6e4d5092a 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -386,11 +386,10 @@ void symex_target_equationt::convert_decls( { if(step.is_decl() && !step.ignore && !step.converted) { - // The result is not used, these have no impact on - // the satisfiability of the formula. - decision_procedure.handle(step.cond_expr); - decision_procedure.handle( - equal_exprt{step.ssa_full_lhs, step.ssa_full_lhs}); + decision_procedure.set_to_true(step.cond_expr); + equal_exprt eq{step.ssa_full_lhs, step.ssa_full_lhs}; + merge_irep(eq); + decision_procedure.set_to_true(eq); step.converted = true; with_solver_hardness( decision_procedure, hardness_register_ssa(step_index, step)); From 856bcd4b5d9dc031d5f351cff13136534e8469b5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2022 08:35:37 +0000 Subject: [PATCH 10/19] convert_assertions: do not attempt to re-convert assumptions convert_assumptions already took care of the conversion, and we can just use the resulting literal to force that to true. --- src/goto-symex/symex_target_equation.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 5f6e4d5092a..3e4f0cea87a 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -444,6 +444,7 @@ void symex_target_equationt::convert_assumptions( with_solver_hardness( decision_procedure, hardness_register_ssa(step_index, step)); } + step.converted = true; } ++step_index; } @@ -532,10 +533,8 @@ void symex_target_equationt::convert_assertions( } else if(step.is_assume()) { - decision_procedure.set_to_true(step.cond_expr); - - with_solver_hardness( - decision_procedure, hardness_register_ssa(step_index, step)); + PRECONDITION(step.converted); + decision_procedure.set_to_true(step.cond_handle); } ++step_index; } @@ -585,6 +584,7 @@ void symex_target_equationt::convert_assertions( } else if(step.is_assume()) { + PRECONDITION(step.converted); // the assumptions have been converted before // avoid deep nesting of ID_and expressions if(assumption.id()==ID_and) From ffa00d77d8987a3af67bd9c447812cac1be7c96a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2022 08:36:43 +0000 Subject: [PATCH 11/19] Symex target equation: convert assignments first Converting assignments (equalities) permits the optimisation of re-using variables generated for a right-hand side to represent the left-hand side. Consequently, no free variables need to be introduced for those left-hand sides when the symbol is seen. If converting, e.g., guards before assignments, no such optimisation is possible. --- src/goto-symex/symex_target_equation.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 3e4f0cea87a..a75662bd841 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -332,9 +332,13 @@ void symex_target_equationt::convert_without_assertions( hardness.register_ssa_size(SSA_steps.size()); }); - convert_guards(decision_procedure); + // The order matters here: the decision procedure may be able to re-use + // variables obtained from constructing the right-hand side of an assignment + // for the left-hand side. Those left-hand sides might then appear in guards + // or assumptions, so do assignments and decls before any of the others. convert_assignments(decision_procedure); convert_decls(decision_procedure); + convert_guards(decision_procedure); convert_assumptions(decision_procedure); convert_goto_instructions(decision_procedure); convert_function_calls(decision_procedure); From ba0d94cb6a466ab2491edef32bffb402e0578c93 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2022 08:39:58 +0000 Subject: [PATCH 12/19] Reduce variable equivalences unnecessarily generated by set_literals There is no need to call set_literals for `A == A`, and if we end up in set_literals via another code path we can still avoid generating the trivially-true equality of `l == l`. --- src/solvers/flattening/boolbv.cpp | 8 +++++--- src/solvers/flattening/boolbv_map.cpp | 6 +++++- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 63b986794bc..ee01da8d8d9 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -489,10 +489,12 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr) const bvt &bv1=convert_bv(expr.rhs()); - const irep_idt &identifier= - to_symbol_expr(expr.lhs()).get_identifier(); + if(expr.rhs() != expr.lhs()) + { + const irep_idt &identifier = to_symbol_expr(expr.lhs()).get_identifier(); - map.set_literals(identifier, type, bv1); + map.set_literals(identifier, type, bv1); + } if(freeze_all) set_frozen(bv1); diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp index 9c1b2747948..7cf972ec599 100644 --- a/src/solvers/flattening/boolbv_map.cpp +++ b/src/solvers/flattening/boolbv_map.cpp @@ -110,7 +110,11 @@ void boolbv_mapt::set_literals( INVARIANT( bit < map_entry.literal_map.size(), "bit index shall be within bounds"); - prop.set_equal(map_entry.literal_map[bit], literal); + if(map_entry.literal_map[bit] != literal) + { + // this branch should be avoided wherever possible + prop.set_equal(map_entry.literal_map[bit], literal); + } } } } From 872cab4253a7d25ec4479a9861547f5ab1d5691a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jul 2022 08:43:00 +0000 Subject: [PATCH 13/19] Remove bv_utils::set_equal as it ought to be avoided Instead of the dance of creating free variables and then setting them equal to the result of some circuit just pass in the known output signals and create the circuit using those directly. --- src/solvers/flattening/bv_utils.cpp | 7 --- src/solvers/flattening/bv_utils.h | 2 - src/solvers/flattening/equality.cpp | 8 ++- src/solvers/prop/prop.h | 1 + src/solvers/refinement/refine_arithmetic.cpp | 7 ++- src/solvers/sat/cnf.cpp | 58 ++++++++++++++++++++ src/solvers/sat/cnf.h | 1 + unit/solvers/bdd/miniBDD/miniBDD.cpp | 5 ++ 8 files changed, 77 insertions(+), 12 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index e1c63515aa0..d998d9d6007 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -28,13 +28,6 @@ literalt bv_utilst::is_one(const bvt &bv) return prop.land(is_zero(tmp), bv[0]); } -void bv_utilst::set_equal(const bvt &a, const bvt &b) -{ - PRECONDITION(a.size() == b.size()); - for(std::size_t i=0; ifirst.first]; const bvt &bv2=eq_bvs[it->first.second]; - prop.set_equal(bv_utils.equal(bv1, bv2), it->second); + bvt equal_bv; + equal_bv.resize(bv1.size()); + + for(std::size_t i = 0; i < bv1.size(); i++) + equal_bv[i] = prop.lequal(bv1[i], bv2[i]); + + prop.gate_bv_and(equal_bv, it->second); } } diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h index a9dbb0c32ee..adef03c07c4 100644 --- a/src/solvers/prop/prop.h +++ b/src/solvers/prop/prop.h @@ -32,6 +32,7 @@ class propt virtual literalt land(literalt a, literalt b)=0; virtual literalt lor(literalt a, literalt b)=0; virtual literalt land(const bvt &bv)=0; + virtual void gate_bv_and(const bvt &bv, literalt output) = 0; virtual literalt lor(const bvt &bv)=0; virtual literalt lxor(literalt a, literalt b)=0; virtual literalt lxor(const bvt &bv)=0; diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index d8241c7b0b8..8410269630d 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -270,7 +270,8 @@ void bv_refinementt::check_SAT(approximationt &a) UNREACHABLE; CHECK_RETURN(r.size()==res.size()); - bv_utils.set_equal(r, res); + for(std::size_t i = 0; i < r.size(); i++) + prop.set_equal(r[i], res[i]); } } else if(type.id()==ID_signedbv || @@ -338,7 +339,9 @@ void bv_refinementt::check_SAT(approximationt &a) else UNREACHABLE; - bv_utils.set_equal(r, a.result_bv); + CHECK_RETURN(r.size() == a.result_bv.size()); + for(std::size_t i = 0; i < r.size(); i++) + prop.set_equal(r[i], a.result_bv[i]); } else UNREACHABLE; diff --git a/src/solvers/sat/cnf.cpp b/src/solvers/sat/cnf.cpp index a485751708c..e49ec9d4b12 100644 --- a/src/solvers/sat/cnf.cpp +++ b/src/solvers/sat/cnf.cpp @@ -196,6 +196,64 @@ literalt cnft::land(const bvt &bv) return literal; } +/// Tseitin encoding of conjunction between multiple literals +/// \param bv: Any number of inputs to the AND gate +/// \param output: Output signal of the circuit +void cnft::gate_bv_and(const bvt &bv, literalt output) +{ + if(bv.empty()) + { + lcnf({output}); + return; + } + if(bv.size() == 1) + { + lcnf(bv[0], !output); + lcnf(!bv[0], output); + return; + } + if(bv.size() == 2) + { + gate_and(bv[0], bv[1], output); + return; + } + + for(const auto &l : bv) + { + if(l.is_false()) + { + lcnf({!output}); + return; + } + } + + if(is_all(bv, const_literal(true))) + { + lcnf({output}); + return; + } + + bvt new_bv = eliminate_duplicates(bv); + + bvt lits(2); + lits[1] = neg(output); + + for(const auto &l : new_bv) + { + lits[0] = pos(l); + lcnf(lits); + } + + lits.clear(); + lits.reserve(new_bv.size() + 1); + + for(const auto &l : new_bv) + lits.push_back(neg(l)); + + lits.push_back(pos(output)); + lcnf(lits); +} + /// Tseitin encoding of disjunction between multiple literals /// \par parameters: Any number of inputs to the OR gate /// \return Output signal of the OR gate as literal diff --git a/src/solvers/sat/cnf.h b/src/solvers/sat/cnf.h index 58c0d6efa75..a4c441f1ec1 100644 --- a/src/solvers/sat/cnf.h +++ b/src/solvers/sat/cnf.h @@ -28,6 +28,7 @@ class cnft:public propt virtual literalt land(literalt a, literalt b) override; virtual literalt lor(literalt a, literalt b) override; virtual literalt land(const bvt &bv) override; + void gate_bv_and(const bvt &bv, literalt output) override; virtual literalt lor(const bvt &bv) override; virtual literalt lxor(const bvt &bv) override; virtual literalt lxor(literalt a, literalt b) override; diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index c3292761576..a068ef5693d 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -82,6 +82,11 @@ class bdd_propt : public propt return to_literal(result); } + void gate_bv_and(const bvt &bv, literalt output) override + { + UNREACHABLE; + } + literalt lor(const bvt &bv) override { mini_bddt result = mgr.False(); From 4e1e64f54469f0b487aad01381e75e9482c2349a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 8 Jul 2022 11:45:59 +0000 Subject: [PATCH 14/19] Revert "Remove bv_utils::set_equal as it ought to be avoided" This reverts commit 90ba9f9d2c0e61287723199f06304becd5a4d24d. --- src/solvers/flattening/bv_utils.cpp | 7 +++ src/solvers/flattening/bv_utils.h | 2 + src/solvers/flattening/equality.cpp | 8 +-- src/solvers/prop/prop.h | 1 - src/solvers/refinement/refine_arithmetic.cpp | 7 +-- src/solvers/sat/cnf.cpp | 58 -------------------- src/solvers/sat/cnf.h | 1 - unit/solvers/bdd/miniBDD/miniBDD.cpp | 5 -- 8 files changed, 12 insertions(+), 77 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index d998d9d6007..e1c63515aa0 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -28,6 +28,13 @@ literalt bv_utilst::is_one(const bvt &bv) return prop.land(is_zero(tmp), bv[0]); } +void bv_utilst::set_equal(const bvt &a, const bvt &b) +{ + PRECONDITION(a.size() == b.size()); + for(std::size_t i=0; ifirst.first]; const bvt &bv2=eq_bvs[it->first.second]; - bvt equal_bv; - equal_bv.resize(bv1.size()); - - for(std::size_t i = 0; i < bv1.size(); i++) - equal_bv[i] = prop.lequal(bv1[i], bv2[i]); - - prop.gate_bv_and(equal_bv, it->second); + prop.set_equal(bv_utils.equal(bv1, bv2), it->second); } } diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h index adef03c07c4..a9dbb0c32ee 100644 --- a/src/solvers/prop/prop.h +++ b/src/solvers/prop/prop.h @@ -32,7 +32,6 @@ class propt virtual literalt land(literalt a, literalt b)=0; virtual literalt lor(literalt a, literalt b)=0; virtual literalt land(const bvt &bv)=0; - virtual void gate_bv_and(const bvt &bv, literalt output) = 0; virtual literalt lor(const bvt &bv)=0; virtual literalt lxor(literalt a, literalt b)=0; virtual literalt lxor(const bvt &bv)=0; diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index 8410269630d..d8241c7b0b8 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -270,8 +270,7 @@ void bv_refinementt::check_SAT(approximationt &a) UNREACHABLE; CHECK_RETURN(r.size()==res.size()); - for(std::size_t i = 0; i < r.size(); i++) - prop.set_equal(r[i], res[i]); + bv_utils.set_equal(r, res); } } else if(type.id()==ID_signedbv || @@ -339,9 +338,7 @@ void bv_refinementt::check_SAT(approximationt &a) else UNREACHABLE; - CHECK_RETURN(r.size() == a.result_bv.size()); - for(std::size_t i = 0; i < r.size(); i++) - prop.set_equal(r[i], a.result_bv[i]); + bv_utils.set_equal(r, a.result_bv); } else UNREACHABLE; diff --git a/src/solvers/sat/cnf.cpp b/src/solvers/sat/cnf.cpp index e49ec9d4b12..a485751708c 100644 --- a/src/solvers/sat/cnf.cpp +++ b/src/solvers/sat/cnf.cpp @@ -196,64 +196,6 @@ literalt cnft::land(const bvt &bv) return literal; } -/// Tseitin encoding of conjunction between multiple literals -/// \param bv: Any number of inputs to the AND gate -/// \param output: Output signal of the circuit -void cnft::gate_bv_and(const bvt &bv, literalt output) -{ - if(bv.empty()) - { - lcnf({output}); - return; - } - if(bv.size() == 1) - { - lcnf(bv[0], !output); - lcnf(!bv[0], output); - return; - } - if(bv.size() == 2) - { - gate_and(bv[0], bv[1], output); - return; - } - - for(const auto &l : bv) - { - if(l.is_false()) - { - lcnf({!output}); - return; - } - } - - if(is_all(bv, const_literal(true))) - { - lcnf({output}); - return; - } - - bvt new_bv = eliminate_duplicates(bv); - - bvt lits(2); - lits[1] = neg(output); - - for(const auto &l : new_bv) - { - lits[0] = pos(l); - lcnf(lits); - } - - lits.clear(); - lits.reserve(new_bv.size() + 1); - - for(const auto &l : new_bv) - lits.push_back(neg(l)); - - lits.push_back(pos(output)); - lcnf(lits); -} - /// Tseitin encoding of disjunction between multiple literals /// \par parameters: Any number of inputs to the OR gate /// \return Output signal of the OR gate as literal diff --git a/src/solvers/sat/cnf.h b/src/solvers/sat/cnf.h index a4c441f1ec1..58c0d6efa75 100644 --- a/src/solvers/sat/cnf.h +++ b/src/solvers/sat/cnf.h @@ -28,7 +28,6 @@ class cnft:public propt virtual literalt land(literalt a, literalt b) override; virtual literalt lor(literalt a, literalt b) override; virtual literalt land(const bvt &bv) override; - void gate_bv_and(const bvt &bv, literalt output) override; virtual literalt lor(const bvt &bv) override; virtual literalt lxor(const bvt &bv) override; virtual literalt lxor(literalt a, literalt b) override; diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index a068ef5693d..c3292761576 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -82,11 +82,6 @@ class bdd_propt : public propt return to_literal(result); } - void gate_bv_and(const bvt &bv, literalt output) override - { - UNREACHABLE; - } - literalt lor(const bvt &bv) override { mini_bddt result = mgr.False(); From 9cb2d84c6b650131d37f0b487ac97a8139c7cbcc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 14 Jul 2022 13:53:50 +0000 Subject: [PATCH 15/19] Playing with the adder encoding: no carry variables This reduces the number of Boolean variables at the expense of introducing more clauses. No measurable difference with CaDiCaL, minor slowdown with MiniSat. --- src/solvers/flattening/bv_utils.cpp | 86 +++++++++++++++++++++++++++-- 1 file changed, 81 insertions(+), 5 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index e1c63515aa0..355e930e4e1 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -297,14 +297,90 @@ literalt bv_utilst::adder( { PRECONDITION(sum.size() == op.size()); - literalt carry_out = carry_in; - - for(std::size_t i=0; i Date: Thu, 14 Jul 2022 18:33:59 +0000 Subject: [PATCH 16/19] Fix and enable COMPACT_LT_LE, needs re-eval --- src/solvers/flattening/bv_utils.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 355e930e4e1..001aea7547e 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -1287,7 +1287,7 @@ literalt bv_utilst::equal(const bvt &op0, const bvt &op1) // Saves space but slows the solver // There is a variant that uses the xor as an auxiliary that should improve both -// #define COMPACT_LT_OR_LE +#define COMPACT_LT_OR_LE From f20a3329b5f41db6f85a5ede3f7a2a79ac8ea42b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 14 Jul 2022 21:50:24 +0000 Subject: [PATCH 17/19] No unnecessary carry --- src/solvers/flattening/bv_utils.cpp | 58 +++++++++++++++++++++-------- src/solvers/flattening/bv_utils.h | 2 +- 2 files changed, 43 insertions(+), 17 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 001aea7547e..865a1140261 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -290,7 +290,37 @@ literalt bv_utilst::carry(literalt a, literalt b, literalt c) } } -literalt bv_utilst::adder( +static literalt carry_out_of_sum( + propt &prop, + const bvt &op0, + const bvt &op1, + const bvt &sum) +{ + literalt a = op0.back(); + literalt b = op1.back(); + literalt s = sum.back(); + + const auto const_count = + a.is_constant() + b.is_constant() + s.is_constant(); + + if(const_count >= 2 || true) + { + return + prop.lor( + prop.land(a, b), + prop.land(!s, prop.lor(a, b))); + } + + literalt c = prop.new_variable(); + + // TODO + assert(false); + prop.lcnf({a, b, s, c}); + + return c; +} + +void bv_utilst::adder( bvt &sum, const bvt &op, literalt carry_in) @@ -305,8 +335,6 @@ literalt bv_utilst::adder( { sum[i] = full_adder(sum[i], op[i], carry_out, carry_out); } - - return carry_out; } else { @@ -376,10 +404,6 @@ literalt bv_utilst::adder( prop.lcnf({!sum[i], !first_op[i], !op[i], !sum[i-1], first_op[i-1]}); prop.lcnf({!sum[i], !first_op[i], !op[i], !sum[i-1], op[i-1]}); } - - return prop.lor( - prop.land(first_op.back(), op.back()), - prop.land(!sum.back(), prop.lor(first_op.back(), op.back()))); } } @@ -418,8 +442,7 @@ bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, bool subtract) bvt result=op0; bvt tmp_op1=subtract?inverted(op1):op1; - // we ignore the carry-out - (void)adder(result, tmp_op1, carry_in); + adder(result, tmp_op1, carry_in); return result; } @@ -431,8 +454,7 @@ bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, literalt subtract) bvt result=op0; - // we ignore the carry-out - (void)adder(result, op1_sign_applied, subtract); + adder(result, op1_sign_applied, subtract); return result; } @@ -452,7 +474,8 @@ bvt bv_utilst::saturating_add_sub( bvt add_sub_result = op0; bvt tmp_op1 = subtract ? inverted(op1) : op1; - literalt carry_out = adder(add_sub_result, tmp_op1, carry_in); + adder(add_sub_result, tmp_op1, carry_in); + literalt carry_out = carry_out_of_sum(prop, op0, tmp_op1, add_sub_result); bvt result; result.reserve(add_sub_result.size()); @@ -572,8 +595,7 @@ void bv_utilst::adder_no_overflow( literalt sign_the_same= prop.lequal(sum[sum.size()-1], tmp_op[tmp_op.size()-1]); - // we ignore the carry-out - (void)adder(sum, tmp_op, const_literal(subtract)); + adder(sum, tmp_op, const_literal(subtract)); // result of addition in sum prop.l_set_to_false( @@ -584,14 +606,18 @@ void bv_utilst::adder_no_overflow( INVARIANT( rep == representationt::UNSIGNED, "representation has either value signed or unsigned"); - literalt carry_out = adder(sum, tmp_op, const_literal(subtract)); + bvt op0 = sum; + adder(sum, tmp_op, const_literal(subtract)); + literalt carry_out = carry_out_of_sum(prop, op0, tmp_op, sum); prop.l_set_to(carry_out, subtract); } } void bv_utilst::adder_no_overflow(bvt &sum, const bvt &op) { - literalt carry_out = adder(sum, op, const_literal(false)); + bvt op0 = sum; + adder(sum, op, const_literal(false)); + literalt carry_out = carry_out_of_sum(prop, op0, op, sum); prop.l_set_to_false(carry_out); // enforce no overflow } diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h index 1e9f58099cf..2b018233455 100644 --- a/src/solvers/flattening/bv_utils.h +++ b/src/solvers/flattening/bv_utils.h @@ -223,7 +223,7 @@ class bv_utilst protected: propt ∝ - literalt adder( + void adder( bvt &sum, const bvt &op, literalt carry_in); From ec0e36c5f8505d98aa76e2dd36c9df5b8ecacb35 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 14 Jul 2022 22:00:58 +0000 Subject: [PATCH 18/19] Enable Wallace Tree multiplier --- src/solvers/flattening/bv_utils.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 865a1140261..15547d86dfe 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -798,7 +798,8 @@ bvt bv_utilst::wallace_tree(const std::vector &pps) bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1) { - #if 1 +//#ifndef SATCHECK_CADICAL +#if 0 bvt op0=_op0, op1=_op1; if(is_constant(op1)) @@ -827,7 +828,7 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1) } return product; - #else +#else // Wallace tree multiplier. This is disabled, as runtimes have // been observed to go up by 5%-10%, and on some models even by 20%. @@ -862,8 +863,7 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1) return zeros(op0.size()); else return wallace_tree(pps); - - #endif +#endif } bvt bv_utilst::unsigned_multiplier_no_overflow( From 07378c7a1d3079a1d6251913a75f6ecc95d94b39 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Jul 2022 09:48:04 +0000 Subject: [PATCH 19/19] Cache expensive circuits for given input bvts This makes solving trivial in presence of temporary intermediate variables. --- src/solvers/flattening/bv_utils.cpp | 28 +++++++++++++++++++++++++--- src/solvers/flattening/bv_utils.h | 7 +++++++ 2 files changed, 32 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 15547d86dfe..e23cf2e4c97 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -976,13 +976,23 @@ bvt bv_utilst::multiplier( const bvt &op1, representationt rep) { + auto cache_entry = + circuit_cache[{ID_mult, rep}].insert({{op0, op1}, {bvt{}}}); + if(!cache_entry.second) + return cache_entry.first->second[0]; + switch(rep) { - case representationt::SIGNED: return signed_multiplier(op0, op1); - case representationt::UNSIGNED: return unsigned_multiplier(op0, op1); + case representationt::SIGNED: + cache_entry.first->second[0] = signed_multiplier(op0, op1); + case representationt::UNSIGNED: + cache_entry.first->second[0] = unsigned_multiplier(op0, op1); } - UNREACHABLE; + // multiplication is commutative + circuit_cache[{ID_mult, rep}][{op1, op0}] = {cache_entry.first->second}; + + return cache_entry.first->second[0]; } bvt bv_utilst::multiplier_no_overflow( @@ -1045,6 +1055,15 @@ void bv_utilst::divider( { PRECONDITION(prop.has_set_to()); + auto cache_entry = + circuit_cache[{ID_div, rep}].insert({{op0, op1}, {bvt{}, bvt{}}}); + if(!cache_entry.second) + { + result = cache_entry.first->second[0]; + remainer = cache_entry.first->second[1]; + return; + } + switch(rep) { case representationt::SIGNED: @@ -1052,6 +1071,9 @@ void bv_utilst::divider( case representationt::UNSIGNED: unsigned_divider(op0, op1, result, remainer); break; } + + cache_entry.first->second[0] = result; + cache_entry.first->second[1] = remainer; } void bv_utilst::unsigned_divider( diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h index 2b018233455..e487c220489 100644 --- a/src/solvers/flattening/bv_utils.h +++ b/src/solvers/flattening/bv_utils.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + // Shares variables between var == const tests for registered variables. // Gives ~15% memory savings on some programs using constant arrays // but seems to give a run-time penalty. @@ -245,6 +247,11 @@ class bv_utilst bvt cond_negate_no_overflow(const bvt &bv, const literalt cond); bvt wallace_tree(const std::vector &pps); + + using circuit_cachet = std::map< + std::pair, + std::map, std::vector>>; + circuit_cachet circuit_cache; }; #endif // CPROVER_SOLVERS_FLATTENING_BV_UTILS_H