Avoid redundant variables and clauses in the propositional encoding

.clang-format

@@ -71,7 +71,7 @@ SpacesInCStyleCastParentheses: 'false'
 SpacesInContainerLiterals: 'false'
 SpacesInParentheses: 'false'
 SpacesInSquareBrackets: 'false'
-Standard: c++11
+Standard: c++17
 TabWidth: '2'
 UseTab: Never
 ---

.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

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()
 

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:
    ```

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

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"

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"
 )
 

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}
+)

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"
 )
 

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

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:$@ $^

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

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())

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;
   }