Merge branch 'main' into uf_example

CMakeLists.txt

@@ -513,9 +513,6 @@ if(USE_CRYPTOMINISAT)
   # CryptoMiniSat requires pthreads support
   set(THREADS_PREFER_PTHREAD_FLAG ON)
   find_package(Threads REQUIRED)
-  if(THREADS_HAVE_PTHREAD_ARG)
-    add_c_cxx_flag(-pthread)
-  endif()
   find_package(CryptoMiniSat 5.8 REQUIRED)
   add_definitions(-DCVC5_USE_CRYPTOMINISAT)
 endif()

cmake/FindCoCoA.cmake

@@ -53,6 +53,11 @@ if(NOT CoCoA_FOUND_SYSTEM)
 
   get_target_property(GMP_LIBRARY GMP IMPORTED_LOCATION)
 
+  find_program(PATCH_BIN patch)
+  if(NOT PATCH_BIN)
+    message(FATAL_ERROR "Can not build CoCoA, missing binary for patch")
+  endif()
+
   ExternalProject_Add(
     CoCoA-EP
     ${COMMON_EP_CONFIG}

cmake/cvc5Config.cmake.in

@@ -17,6 +17,11 @@ set(CVC5_BINDINGS_JAVA @BUILD_BINDINGS_JAVA@)
 set(CVC5_BINDINGS_PYTHON @BUILD_BINDINGS_PYTHON@)
 set(CVC5_BINDINGS_PYTHON_VERSION @BUILD_BINDINGS_PYTHON_VERSION@)
 set(CVC5_USE_COCOA @USE_COCOA@)
+set(CVC5_USE_CRYPTOMINISAT @USE_CRYPTOMINISAT@)
+
+if (CVC5_USE_CRYPTOMINISAT)
+  find_package(Threads REQUIRED)
+endif()
 
 if(NOT TARGET cvc5::cvc5)
   include(${CMAKE_CURRENT_LIST_DIR}/cvc5Targets.cmake)

contrib/get-alf-checker

@@ -24,7 +24,7 @@ ALFC_DIR="$BASE_DIR/alf-checker"
 mkdir -p $ALFC_DIR
 
 # download and unpack ALFC
-ALF_VERSION="3c122c02bdb49d239223e683740da59f74816ba7"
+ALF_VERSION="da1903230c1d7cc5adbacb65d4eee602dcba93a0"
 download "https://github.com/cvc5/alfc/archive/$ALF_VERSION.tar.gz" $BASE_DIR/tmp/alfc.tgz
 tar --strip 1 -xzf $BASE_DIR/tmp/alfc.tgz -C $ALFC_DIR
 

docs/proofs/output_alf.rst

@@ -7,7 +7,7 @@ The ALF proof format is based on the SMT-LIB 3 language. An efficient C++ proof
 
 For a quick start, the cvc5 repository contains a :cvc5repo:`script <contrib/get-alf-checker>` which will download and install the ALF proof checker (alfc), and create scripts for generating proofs with cvc5 and checking them with the ALF proof checker.
 
-The AletheLF language is a meta-framework, meaning that the proof rules used by cvc5 are defined in signature files.   The signature files are contained within the cvc5 repository in this :cvc5repo:`directory <proofs/alf/Cvc5.smt3>`. Based on these signatures, cvc5 provides basic support for ALF proofs over all theories that it supports.
+The AletheLF language is a meta-framework, meaning that the proof rules used by cvc5 are defined in signature files.   The signature files are contained within the cvc5 repository in this :cvc5repo:`directory <proofs/alf/cvc5/Cvc5.smt3>`. Based on these signatures, cvc5 provides basic support for ALF proofs over all theories that it supports.
 
 Note that several proof rules in the internal calculus are not yet supported in ALF signatures.  Steps that use such rules are printed as `trust` steps in the ALF proof. A trust step proves an arbitrary formula with no provided justification. The ALF proof contains warnings for trust steps that indicate which internal proof rules were recorded as trust steps in the ALF proof.
 

include/cvc5/c/cvc5.h

@@ -343,7 +343,7 @@ bool cvc5_sort_is_string(Cvc5Sort sort);
  * @param sort The sort.
  * @return True if given sort is the regular expression sort.
  */
-bool cvc5_sort_is_reg_exp(Cvc5Sort sort);
+bool cvc5_sort_is_regexp(Cvc5Sort sort);
 
 /**
  * Determine if given sort is the rounding mode sort
@@ -531,7 +531,7 @@ Cvc5Sort cvc5_sort_get_uninterpreted_sort_constructor(Cvc5Sort sort);
  * @param sort The sort.
  * @return The underlying datatype of a datatype sort.
  */
-Cvc5Datatype* cvc5_sort_get_datatype(Cvc5Sort sort);
+Cvc5Datatype cvc5_sort_get_datatype(Cvc5Sort sort);
 
 /**
  * Instantiate a parameterized datatype sort or uninterpreted sort
@@ -782,7 +782,7 @@ uint32_t cvc5_sort_bv_get_size(Cvc5Sort sort);
  * @note The returned char* pointer is only valid until the next call to this
  *       function.
  */
-const char* cvc5_sort_ff_get_size();
+const char* cvc5_sort_ff_get_size(Cvc5Sort sort);
 
 /* Floating-point sort ------------------------------------------------- */