Merge branch 'main' of https://github.com/cvc5/cvc5 into strMacroRew-…

…1210

.github/workflows/package_pypi.yml

@@ -30,6 +30,7 @@ jobs:
             os: ubuntu-latest
             arch: aarch64
             shell: bash
+            cibw_skip: "cp37-* pp37-*"
           - name: macos-x86_64
             os: macos-13
             macos-target: 10.13
@@ -87,10 +88,14 @@ jobs:
         mkdir -p build/src/api/python
         if [ "${{ matrix.gpl }}" == "true" ]; then
           sed -e 's/^name="cvc5"$/name="cvc5-gpl"/' \
+              -e 's/^\(description=".*\)"/\1 (GPL version)"/' \
+              -e 's/^\(readme = {text = ".*\)\(", content-type = "text\/plain"\)/\1 (GPL version)\2/' \
               -e 's/^license = {text = "/license = {text = "GPL-2.0-or-later AND GPL-3.0-or-later AND /' \
               ./src/api/python/pyproject.toml > ./build/src/api/python/pyproject.toml
         else
-          cp src/api/python/pyproject.toml build/src/api/python/
+          sed -e 's/^\(description=".*\)"/\1 (BSD version)"/' \
+              -e 's/^\(readme = {text = ".*\)\(", content-type = "text\/plain"\)/\1 (BSD version)\2/' \
+              ./src/api/python/pyproject.toml > ./build/src/api/python/pyproject.toml
         fi
         echo "::endgroup::"
 
@@ -101,11 +106,11 @@ jobs:
       run: echo "bin=$(cygpath -m $(dirname $(which gcc)))" >> $GITHUB_OUTPUT
 
     - name: Build wheels
-      uses: pypa/cibuildwheel@v2.17.0
+      uses: pypa/cibuildwheel@v2.22.0
       with:
         package-dir: ./build/src/api/python/
       env:
-        CIBW_SKIP: "cp36-* pp*-win* *-win32 *-manylinux_i686 *-musllinux_*"
+        CIBW_SKIP: "cp36-* pp*-win* *-win32 *-manylinux_i686 *-musllinux_* ${{ matrix.cibw_skip }}"
         CIBW_ARCHS_LINUX: "${{ matrix.arch }}"
         CIBW_BEFORE_ALL_LINUX: bash ./contrib/cibw/before_all_linux.sh ${{ matrix.gpl }}
         CIBW_BEFORE_ALL_MACOS: bash ./contrib/cibw/before_all_macos.sh ${{ matrix.gpl }}

CMakeLists.txt

@@ -97,6 +97,7 @@ cvc5_option(ENABLE_COMP_INC_TRACK
             "Enable optimizations for incremental SMT-COMP tracks")
 cvc5_option(ENABLE_DEBUG_SYMBOLS  "Enable debug symbols")
 cvc5_option(ENABLE_MUZZLE         "Suppress ALL non-result output")
+cvc5_option(ENABLE_SAFE_MODE      "Enable safe mode")
 cvc5_option(ENABLE_STATISTICS     "Enable statistics")
 cvc5_option(ENABLE_TRACING        "Enable tracing")
 cvc5_option(ENABLE_UNIT_TESTING   "Enable unit testing")
@@ -518,6 +519,10 @@ if(ENABLE_TRACING)
   add_definitions(-DCVC5_TRACING)
 endif()
 
+if(ENABLE_SAFE_MODE)
+  add_definitions(-DCVC5_SAFE_MODE)
+endif()
+
 if(ENABLE_STATISTICS)
   add_definitions(-DCVC5_STATISTICS_ON)
 endif()
@@ -745,7 +750,11 @@ message("")
 if(ENABLE_COMP_INC_TRACK)
   print_config("Build profile             " "${CVC5_BUILD_PROFILE_STRING} (incremental)")
 else()
-  print_config("Build profile             " "${CVC5_BUILD_PROFILE_STRING}")
+  if (ENABLE_SAFE_MODE)
+    print_config("Build profile             " "${CVC5_BUILD_PROFILE_STRING} (safe mode)")
+  else()
+    print_config("Build profile             " "${CVC5_BUILD_PROFILE_STRING}")
+  endif()
 endif()
 message("")
 print_config("Assertions                " ${ENABLE_ASSERTIONS})

configure.sh

@@ -131,6 +131,7 @@ pyvenv=default
 java_bindings=default
 editline=default
 build_shared=ON
+safe_mode=default
 static_binary=default
 statistics=default
 tracing=default
@@ -336,6 +337,7 @@ do
          testing)         buildtype=Testing;;
          competition)     buildtype=Competition;;
          competition-inc) buildtype=Competition; comp_inc=ON;;
+         safe-mode)       buildtype=Production; safe_mode=ON;;
          *)               die "invalid build type (try -h)";;
        esac
        ;;
@@ -369,6 +371,8 @@ fi
   && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
 [ $comp_inc != default ] \
   && cmake_opts="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
+[ $safe_mode != default ] \
+  && cmake_opts="$cmake_opts -DENABLE_SAFE_MODE=$safe_mode"
 [ $coverage != default ] \
   && cmake_opts="$cmake_opts -DENABLE_COVERAGE=$coverage"
 [ $debug_symbols != default ] \

contrib/get-ethos-checker

@@ -26,7 +26,7 @@ EO_DIR="$BASE_DIR/ethos-checker"
 mkdir -p $EO_DIR
 
 # download and unpack ethos
-ETHOS_VERSION="ffd697b162e556883ed26958b052a5b8ad7bdc77"
+ETHOS_VERSION="7b9ea06ab3c5e39b66366396cd216e3f8637c64e"
 download "https://github.com/cvc5/ethos/archive/$ETHOS_VERSION.tar.gz" $BASE_DIR/tmp/ethos.tgz
 tar --strip 1 -xzf $BASE_DIR/tmp/ethos.tgz -C $EO_DIR