Merge branch 'main' into int_blasting_overflow

.github/actions/add-package/action.yml

@@ -45,23 +45,6 @@ runs:
 
         # Create ZIP file
         pushd ${{ inputs.build-dir }}
-        if [[ "$RUNNER_OS" == "macOS" ]]; then
-          # Temporary workaround to make the cvc5 library included in release relocatable (see issue #10681)
-          if [ -f ./install/lib/libcvc5.dylib ]; then
-            install_name_tool -change "${{ inputs.build-dir }}/deps/lib/libpoly.0.dylib" @rpath/libpoly.0.dylib ./install/lib/libcvc5.dylib
-            install_name_tool -change "${{ inputs.build-dir }}/deps/lib/libpoly.0.dylib" @rpath/libpoly.0.dylib ./install/lib/libcvc5.1.dylib
-            install_name_tool -change "${{ inputs.build-dir }}/deps/lib/libpolyxx.0.dylib" @rpath/libpolyxx.0.dylib ./install/lib/libcvc5.dylib
-            install_name_tool -change "${{ inputs.build-dir }}/deps/lib/libpolyxx.0.dylib" @rpath/libpolyxx.0.dylib ./install/lib/libcvc5.1.dylib
-            install_name_tool -change "${{ inputs.build-dir }}/deps/lib/libgmp.10.dylib" @rpath/libgmp.10.dylib ./install/lib/libcvc5.dylib
-            install_name_tool -change "${{ inputs.build-dir }}/deps/lib/libgmp.10.dylib" @rpath/libgmp.10.dylib ./install/lib/libcvc5.1.dylib
-            if [ -f ./install/lib/libcln.dylib ]; then
-              install_name_tool -change "${{ inputs.build-dir }}/deps/lib/libcln.6.dylib" @rpath/libcln.6.dylib ./install/lib/libcvc5.dylib
-              install_name_tool -change "${{ inputs.build-dir }}/deps/lib/libcln.6.dylib" @rpath/libcln.6.dylib ./install/lib/libcvc5.1.dylib
-              install_name_tool -change "/usr/local/opt/gmp/lib/libgmp.10.dylib" @rpath/libgmp.10.dylib ./install/lib/libcln.dylib
-              install_name_tool -change "/usr/local/opt/gmp/lib/libgmp.10.dylib" @rpath/libgmp.10.dylib ./install/lib/libcln.6.dylib
-            fi
-          fi
-        fi
         mv install ${{ inputs.package-name }}
         zip -r ${{ inputs.package-name }} ${{ inputs.package-name }}
         popd

cmake/FindCLN.cmake

@@ -114,6 +114,11 @@ if(NOT CLN_FOUND_SYSTEM)
     endif()
   endif()
 
+  set(CLN_WITH_GMP)
+  if(NOT GMP_FOUND_SYSTEM)
+    set(CLN_WITH_GMP "--with-gmp=<INSTALL_DIR>")
+  endif()
+
   ExternalProject_Add(
     CLN-EP
     ${COMMON_EP_CONFIG}
@@ -122,7 +127,7 @@ if(NOT CLN_FOUND_SYSTEM)
     DOWNLOAD_NAME cln.tar.bz2
     CONFIGURE_COMMAND
       ${CONFIGURE_ENV} ${SHELL} <SOURCE_DIR>/configure
-        --prefix=<INSTALL_DIR> ${LINK_OPTS} --with-pic
+        --prefix=<INSTALL_DIR> ${LINK_OPTS} --with-pic ${CLN_WITH_GMP}
         ${CONFIGURE_OPTS}
     BUILD_BYPRODUCTS ${CLN_BYPRODUCTS}
   )
@@ -163,4 +168,11 @@ else()
   # These libraries are required to compile a program that
   # uses the cvc5 static library.
   install(FILES ${BUILD_BYPRODUCTS} TYPE ${LIB_BUILD_TYPE})
+
+  if(NOT SKIP_SET_RPATH AND BUILD_SHARED_LIBS AND APPLE)
+    foreach(CLN_DYLIB ${BUILD_BYPRODUCTS})
+      get_filename_component(CLN_DYLIB_NAME ${CLN_DYLIB} NAME)
+      update_rpath_macos(${CLN_DYLIB_NAME})
+    endforeach()
+  endif()
 endif()

cmake/FindGMP.cmake

@@ -181,4 +181,17 @@ else()
       FILES_MATCHING PATTERN libgmp*
     )
   endif()
+  if(NOT SKIP_SET_RPATH AND BUILD_SHARED_LIBS AND APPLE)
+    install(CODE "
+      file(GLOB GMP_DYLIBS \"\${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/libgmp*.dylib\")
+      foreach(GMP_DYLIB \${GMP_DYLIBS})
+        execute_process(COMMAND \${CMAKE_COMMAND}
+          -DRPATH=@loader_path
+          -DINSTALL_NAME_TOOL=${CMAKE_INSTALL_NAME_TOOL}
+          -DDYLIB_PATH=\${GMP_DYLIB}
+          -DDEPS_BASE=${DEPS_BASE}
+          -P ${CMAKE_SOURCE_DIR}/cmake/update_rpath_macos.cmake)
+      endforeach()
+    ")
+  endif()
 endif()

cmake/FindPoly.cmake

@@ -242,4 +242,11 @@ else()
   # These libraries are required to compile a program that
   # uses the cvc5 static library.
   install(FILES ${BUILD_BYPRODUCTS} TYPE ${LIB_BUILD_TYPE})
+
+  if(NOT SKIP_SET_RPATH AND BUILD_SHARED_LIBS AND APPLE)
+    foreach(POLY_DYLIB ${BUILD_BYPRODUCTS})
+      get_filename_component(POLY_DYLIB_NAME ${POLY_DYLIB} NAME)
+      update_rpath_macos(${POLY_DYLIB_NAME})
+    endforeach()
+  endif()
 endif()

cmake/Helpers.cmake

@@ -278,3 +278,12 @@ macro(copy_file_from_src filename)
     DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
   )
 endmacro()
+
+macro(update_rpath_macos dylibname)
+  install(CODE "execute_process(COMMAND \${CMAKE_COMMAND}
+    -DRPATH=@loader_path
+    -DINSTALL_NAME_TOOL=${CMAKE_INSTALL_NAME_TOOL}
+    -DDYLIB_PATH=\${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/${dylibname}
+    -DDEPS_BASE=${DEPS_BASE}
+    -P ${CMAKE_SOURCE_DIR}/cmake/update_rpath_macos.cmake)")
+endmacro()

cmake/update_rpath_macos.cmake

@@ -0,0 +1,57 @@
+# If RPATH is provided, add it unless it already exists
+if(RPATH)
+   # otool -l output is in the format:
+   #      cmd LC_RPATH
+   # cmdsize XX
+   #      path <path> (offset YY)
+  execute_process(
+    COMMAND otool -l "${DYLIB_PATH}"
+    COMMAND grep LC_RPATH -A2
+    OUTPUT_VARIABLE RPATH_OUTPUT
+  )
+  if(NOT "${RPATH_OUTPUT}" MATCHES "${RPATH}")
+    execute_process(
+      COMMAND ${INSTALL_NAME_TOOL} -add_rpath ${RPATH} ${DYLIB_PATH}
+    )
+  endif()
+endif()
+
+# Get install name
+execute_process(
+  COMMAND otool -D "${DYLIB_PATH}"
+  OUTPUT_VARIABLE INSTALL_NAME_OUTPUT
+  OUTPUT_STRIP_TRAILING_WHITESPACE
+)
+# otool -D output is in the format:
+# libname.dylib:
+#   /full/path/to/libname.n.dylib
+# Extract the second line which contains the actual install name
+string(REPLACE "\n" ";" INSTALL_NAME_LIST "${INSTALL_NAME_OUTPUT}")
+list(GET INSTALL_NAME_LIST 1 INSTALL_NAME)
+
+if("${INSTALL_NAME}" MATCHES "${DEPS_BASE}/lib")
+  # Replace ${DEPS_BASE}/lib with @rpath
+  string(REPLACE "${DEPS_BASE}/lib" "@rpath" NEW_INSTALL_NAME "${INSTALL_NAME}")
+  execute_process(
+    COMMAND ${INSTALL_NAME_TOOL} -id ${NEW_INSTALL_NAME} ${DYLIB_PATH}
+  )
+endif()
+
+# Get all dependencies and replace ${DEPS_BASE}/lib with @rpath
+execute_process(
+  COMMAND otool -L ${DYLIB_PATH}
+  OUTPUT_VARIABLE OTOOL_OUTPUT
+  OUTPUT_STRIP_TRAILING_WHITESPACE
+)
+string(REPLACE "\n" ";" OTOOL_LINES "${OTOOL_OUTPUT}")
+# Discard the first line which is the path to ${DYLIB_PATH}
+list(REMOVE_AT OTOOL_LINES 0)
+foreach(LINE ${OTOOL_LINES})
+  if(LINE MATCHES "${DEPS_BASE}/lib/")
+    string(REGEX REPLACE "^[ \t]*([^ \t]+).*" "\\1" LIB_PATH "${LINE}")
+    string(REPLACE "${DEPS_BASE}/lib" "@rpath" LIB_RPATH "${LIB_PATH}")
+    execute_process(
+      COMMAND ${INSTALL_NAME_TOOL} -change ${LIB_PATH} ${LIB_RPATH} ${DYLIB_PATH}
+    )
+  endif()
+endforeach()

contrib/get-carcara-checker

@@ -24,9 +24,10 @@ CARCARA_DIR="$BASE_DIR/carcara"
 mkdir -p $CARCARA_DIR
 
 # download and unpack Carcara
-CARCARA_VERSION="e770994b5d981257d53a83d38a679fa98c144005"
+CARCARA_VERSION="d434d5caa0f2dad65aaa9ac9c20817af53004088"
 download "https://github.com/hanielb/carcara/archive/$CARCARA_VERSION.tar.gz" $BASE_DIR/tmp/carcara.tgz
 tar --strip 1 -xzf $BASE_DIR/tmp/carcara.tgz -C $CARCARA_DIR
+rm $BASE_DIR/tmp/carcara.tgz
 
 # build carcara
 pushd $CARCARA_DIR
@@ -67,4 +68,4 @@ echo "  $CVC_DIR/deps/bin/cvc5-alethe-proof.sh cvc5 <input file> <options>"
 echo "Check a proof:"
 echo "  $CVC_DIR/deps/bin/carcara-check.sh <proof file> <input file>"
 echo "Run cvc5 and check the generated proof:"
-echo "  $CVC_DIR/deps/bin/cvc5-carcara-check.sh cvc5 <input file> <options>"
+echo "  $CVC_DIR/deps/bin/cvc5-carcara-check.sh cvc5 <input file> <options>"

include/cvc5/cvc5_proof_rule.h

@@ -489,8 +489,7 @@ enum ENUM(ProofRule)
    *   \inferrule{C_1 \mid C_2}{C_2}
    *
    * where
-   * the set representations of :math:`C_1` and :math:`C_2` are the same and the
-   * number of literals in :math:`C_2` is the same of that of :math:`C_1`.
+   * the multiset representations of :math:`C_1` and :math:`C_2` are the same.
    * \endverbatim
    */
   EVALUE(REORDERING),

src/CMakeLists.txt

@@ -1470,6 +1470,11 @@ target_include_directories(cvc5
 # DLLs into the runtime path (by default "bin")
 install(TARGETS cvc5 EXPORT cvc5-targets)
 
+if(NOT SKIP_SET_RPATH AND BUILD_SHARED_LIBS AND APPLE)
+  update_rpath_macos(libcvc5.dylib)
+  update_rpath_macos(libcvc5.${CVC5_SOVERSION}.dylib)
+endif()
+
 if(BUILD_SHARED_LIBS)
   set_target_properties(cvc5 PROPERTIES SOVERSION ${CVC5_SOVERSION})
 endif()

src/options/theory_options.toml

@@ -26,12 +26,30 @@ name   = "Theory Layer"
 
 [[option]]
   name       = "condenseFunctionValues"
-  category   = "expert"
+  category   = "common"
   long       = "condense-function-values"
   type       = "bool"
   default    = "true"
   help       = "condense values for functions in models rather than explicitly representing them"
 
+[[option]]
+  name       = "defaultFunctionValueMode"
+  category   = "common"
+  long       = "default-function-value-mode=MODE"
+  type       = "DefaultFunctionValueMode"
+  default    = "FIRST"
+  help       = "mode for choosing default values for functions"
+  help_mode  = "Defines mode for choosing default values for functions."
+[[option.mode.FIRST]]
+  name = "first"
+  help = "The default value is equal to the value of the first application found of that function when applicable, or the first enumerated term otherwise."
+[[option.mode.FIRST_ENUM]]
+  name = "first-enum"
+  help = "The default value is equal to the first enumerated value of its range type."
+[[option.mode.HOLE]]
+  name = "hole"
+  help = "The default value is equal to a distinguished variable."
+
 [[option]]
   name       = "relevanceFilter"
   category   = "expert"

src/preprocessing/passes/real_to_int.cpp

@@ -218,18 +218,21 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
 PreprocessingPassResult RealToInt::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  // this pass is refutation unsound, "unsat" will be "unknown"
-  assertionsToPreprocess->markRefutationUnsound();
   std::vector<Node> var_eq;
   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     Node a = (*assertionsToPreprocess)[i];
     Node ac = realToIntInternal(a, d_cache, var_eq);
-    Trace("real-to-int") << "Converted " << a << " to " << ac << std::endl;
-    assertionsToPreprocess->replace(i, rewrite(ac));
-    if (assertionsToPreprocess->isInConflict())
+    if (ac != a)
     {
-      return PreprocessingPassResult::CONFLICT;
+      // this pass is refutation unsound, "unsat" will be "unknown"
+      assertionsToPreprocess->markRefutationUnsound();
+      Trace("real-to-int") << "Converted " << a << " to " << ac << std::endl;
+      assertionsToPreprocess->replace(i, rewrite(ac));
+      if (assertionsToPreprocess->isInConflict())
+      {
+        return PreprocessingPassResult::CONFLICT;
+      }
     }
   }
   return PreprocessingPassResult::NO_CONFLICT;