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/.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/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/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/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/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/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/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/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..ba11e70f02f 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) @@ -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/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..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); @@ -386,11 +390,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)); @@ -445,6 +448,7 @@ void symex_target_equationt::convert_assumptions( with_solver_hardness( decision_procedure, hardness_register_ssa(step_index, step)); } + step.converted = true; } ++step_index; } @@ -533,10 +537,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; } @@ -586,6 +588,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) @@ -620,33 +623,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 +647,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/CMakeLists.txt b/src/solvers/CMakeLists.txt index 744def4861b..5108e0b918c 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 @@ -12,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 @@ -47,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,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") @@ -109,7 +125,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 +155,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 ) 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/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); + } } } } 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 diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index 90f1f7b5983..e23cf2e4c97 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/src/solvers/flattening/bv_utils.cpp @@ -290,19 +290,120 @@ literalt bv_utilst::carry(literalt a, literalt b, literalt c) } } +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, - literalt &carry_out) + literalt carry_in) { PRECONDITION(sum.size() == op.size()); - carry_out=carry_in; + if(sum.empty() || !prop.has_set_to() || !prop.cnf_handled_well()) + { + literalt carry_out=carry_in; - for(std::size_t i=0; i &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)) @@ -729,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%. @@ -764,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( @@ -878,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( @@ -947,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: @@ -954,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( @@ -1185,6 +1305,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()); @@ -1205,7 +1335,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 diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h index 35a64eec59b..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. @@ -226,8 +228,7 @@ class bv_utilst void adder( bvt &sum, const bvt &op, - literalt carry_in, - literalt &carry_out); + literalt carry_in); void adder_no_overflow( bvt &sum, @@ -246,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 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) 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_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() 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 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());