Merge branch 'main' into int_blasting_overflow

cmake/FindCoCoA.cmake

@@ -31,6 +31,24 @@ if(CoCoA_INCLUDE_DIR AND CoCoA_LIBRARIES)
   string(REGEX MATCH "[0-9]+\\.[0-9]+" CoCoA_VERSION "${CoCoA_VERSION}")
 
   check_system_version("CoCoA")
+
+  # This test checks whether CoCoA has been patched
+  try_compile(CoCoA_USABLE "${DEPS_BASE}/try_compile/CoCoA-EP"
+    "${CMAKE_CURRENT_LIST_DIR}/deps-utils/cocoa-test.cpp"
+    CMAKE_FLAGS
+      "-DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE}"
+      "-DINCLUDE_DIRECTORIES=${CoCoA_INCLUDE_DIR}"
+    LINK_LIBRARIES ${CoCoA_LIBRARIES} ${GMP_LIBRARIES} ${GMPXX_LIBRARIES}
+  )
+  if(NOT CoCoA_USABLE)
+    message(STATUS "The system version of CoCoA has not been patched.")
+    if(ENABLE_AUTO_DOWNLOAD)
+      message(STATUS "A patched version of CoCoA will be built for you.")
+    else()
+      message(STATUS "Use --auto-download to let us download and build a patched version of CoCoA for you.")
+    endif()
+    set(CoCoA_FOUND_SYSTEM FALSE)
+  endif()
 endif()
 
 if(NOT CoCoA_FOUND_SYSTEM)
@@ -68,12 +86,12 @@ if(NOT CoCoA_FOUND_SYSTEM)
   ExternalProject_Add(
     CoCoA-EP
     ${COMMON_EP_CONFIG}
-    URL "http://cocoa.dima.unige.it/cocoa/cocoalib/tgz/CoCoALib-${CoCoA_VERSION}.tgz"
+    URL https://github.com/cvc5/cvc5-deps/blob/main/CoCoALib-${CoCoA_VERSION}.tgz?raw=true
     URL_HASH SHA256=f8bb227e2e1729e171cf7ac2008af71df25914607712c35db7bcb5a044a928c6
     # CoCoA requires C++14, but the check does not work with compilers that
     # default to C++17 or newer. The patch fixes the check.
     PATCH_COMMAND patch -p1 -d <SOURCE_DIR>
-        -i ${CMAKE_CURRENT_LIST_DIR}/deps-utils/CoCoALib-0.99800-trace.patch
+        -i ${CMAKE_CURRENT_LIST_DIR}/deps-utils/CoCoALib-${CoCoA_VERSION}-trace.patch
     BUILD_IN_SOURCE YES
     CONFIGURE_COMMAND ${SHELL} ./configure --prefix=<INSTALL_DIR> --with-libgmp=${GMP_LIBRARY}
         --with-cxx=${CMAKE_CXX_COMPILER} --with-cxxflags=${CoCoA_CXXFLAGS}

cmake/deps-utils/cocoa-test.cpp

@@ -0,0 +1,23 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Daniel Larraz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Checks whether CoCoA has been patched.
+ */
+#include <iostream>
+#include <CoCoA/TmpGPoly.H>
+
+int main()
+{
+    std::cout << "CoCoA::handlersEnabled = ";
+    std::cout << CoCoA::handlersEnabled << std::endl;
+    return 0;
+}

contrib/get-carcara-checker

@@ -0,0 +1,70 @@
+#!/usr/bin/env bash
+
+# utility function to download a file
+function download {
+  if [ -x "$(command -v wget)" ]; then
+    wget -c -O "$2" "$1"
+  elif [ -x "$(command -v curl)" ]; then
+    curl -L "$1" >"$2"
+  else
+    echo "Can't figure out how to download from web.  Please install wget or curl." >&2
+    exit 1
+  fi
+}
+
+CVC_DIR=$(dirname $(dirname "$0"))
+mkdir -p $CVC_DIR/deps
+pushd $CVC_DIR/deps
+
+BASE_DIR=`pwd`
+mkdir -p $BASE_DIR/tmp/
+
+###### Carcara
+CARCARA_DIR="$BASE_DIR/carcara"
+mkdir -p $CARCARA_DIR
+
+# download and unpack Carcara
+CARCARA_VERSION="e770994b5d981257d53a83d38a679fa98c144005"
+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
+
+# build carcara
+pushd $CARCARA_DIR
+cargo build --release
+mkdir -p $BASE_DIR/bin
+cp ./target/release/carcara $BASE_DIR/bin/carcara
+popd
+
+cat << EOF > $BASE_DIR/bin/cvc5-carcara-check.sh
+#!/usr/bin/env bash
+echo "=== Generate proof: \$@"
+echo "> \$2.alethe"
+$BASE_DIR/bin/cvc5-alethe-proof.sh \$@ > \$2.alethe
+echo "=== Check proof with Carcara"
+$BASE_DIR/bin/carcara-check.sh \$2.alethe \$2
+EOF
+chmod +x $BASE_DIR/bin/cvc5-carcara-check.sh
+
+cat << EOF > $BASE_DIR/bin/cvc5-alethe-proof.sh
+#!/usr/bin/env bash
+# call cvc5 and remove the first line of the output (should be "unsat")
+\$@ --dump-proofs --proof-format=alethe --proof-alethe-experimental | tail -n +2
+EOF
+chmod +x $BASE_DIR/bin/cvc5-alethe-proof.sh
+
+cat << EOF > $BASE_DIR/bin/carcara-check.sh
+#!/usr/bin/env bash
+$BASE_DIR/bin/carcara check --allow-int-real-subtyping --expand-let-bindings --ignore-unknown-rules \$@ > carcara.out
+cat carcara.out
+rm carcara.out
+EOF
+chmod +x $BASE_DIR/bin/carcara-check.sh
+
+echo ""
+echo "========== How to use Carcara =========="
+echo "Generate an Alethe proof with cvc5 (for terms printed without sharing, use --dag-thresh=0):"
+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>"

include/cvc5/cvc5.h

@@ -6113,7 +6113,7 @@ class CVC5_EXPORT Solver
    * `modes::ProofFormat::NONE` if the proof is from a component other than
    * `modes::ProofComponent::FULL`.
    * @param assertionNames Mapping between assertions and names, if they were
-   * given by the user.
+   * given by the user.  This is used by the Alethe proof format.
    * @return The string representation of the proof in the given format.
    */
   std::string proofToString(

proofs/eo/cpc/Cpc.eo

@@ -128,8 +128,8 @@
       (($run_evaluate (div_total x y))     (eo::define ((d ($run_evaluate y)))
                                              (eo::ite (eo::is_eq d 0) 0 (eo::zdiv ($run_evaluate x) d))))
       (($run_evaluate (mod x y))           (eo::zmod ($run_evaluate x) ($run_evaluate y)))
-      (($run_evaluate (mod_total x y))     (let ((ex ($run_evaluate x)))
-                                           (let ((ey ($run_evaluate y)))
+      (($run_evaluate (mod_total x y))     (eo::define ((ex ($run_evaluate x)))
+                                           (eo::define ((ey ($run_evaluate y)))
                                             (eo::ite (eo::is_eq ey 0) ex (eo::zmod ex ey)))))
       (($run_evaluate (to_real x))         (eo::to_q ($run_evaluate x)))
       (($run_evaluate (to_int x))          (eo::to_z ($run_evaluate x)))

proofs/eo/cpc/programs/Arith.eo

@@ -143,7 +143,7 @@
     (($poly_add (@poly (@mon a1 c1) p1) (@poly (@mon a2 c2) p2)) (eo::ite (eo::is_eq a1 a2)
                                                                   (eo::define ((ca (eo::add c1 c2)) (pa ($poly_add p1 p2)))
                                                                   ; check if cancels
-                                                                  (eo::ite (eo::is_eq ca 0.0) pa (eo::cons @poly (@mon a1 ca) pa)))
+                                                                  (eo::ite (eo::is_eq ca 0/1) pa (eo::cons @poly (@mon a1 ca) pa)))
                                                                 (eo::ite ($compare_var a1 a2)
                                                                   (eo::cons @poly (@mon a1 c1) ($poly_add p1 (@poly (@mon a2 c2) p2)))
                                                                   (eo::cons @poly (@mon a2 c2) ($poly_add (@poly (@mon a1 c1) p1) p2)))))
@@ -224,10 +224,10 @@
                                   ; if it is a constant, which can be tested if to_q is idempotent after the first
                                   (eo::ite (eo::is_eq aq (eo::to_q aq))
                                     ; if it is zero, it cancels, otherwise it is 1 with itself as coefficient
-                                    (eo::ite (eo::is_eq aq 0.0)
+                                    (eo::ite (eo::is_eq aq 0/1)
                                       @poly.zero
                                       (@poly (@mon 1 aq)))
-                                  (@poly (@mon (* a) 1.0)))))    ; introduces list
+                                  (@poly (@mon (* a) 1/1)))))    ; introduces list
   )
 )
 

proofs/eo/cpc/programs/Strings.eo

@@ -1130,10 +1130,10 @@
   (($str_re_includes r1 r1)                               true)
   (($str_re_includes r1 (str.to_re s1))                   ($str_eval_str_in_re s1 r1))
   (($str_re_includes (str.to_re s1) r1)                   false)
-  (($str_re_includes (re.range s1 s2) (re.range s3 s4))   (let ((z1 (eo::to_z s1)))
-                                                          (let ((z2 (eo::to_z s2)))
-                                                          (let ((z3 (eo::to_z s3)))
-                                                          (let ((z4 (eo::to_z s4)))
+  (($str_re_includes (re.range s1 s2) (re.range s3 s4))   (eo::define ((z1 (eo::to_z s1)))
+                                                          (eo::define ((z2 (eo::to_z s2)))
+                                                          (eo::define ((z3 (eo::to_z s3)))
+                                                          (eo::define ((z4 (eo::to_z s4)))
                                                           (eo::requires (eo::is_neg z1) false
                                                           (eo::requires (eo::is_neg z2) false
                                                           (eo::requires (eo::is_neg z3) false

proofs/eo/cpc/rules/Arith.eo

@@ -33,7 +33,7 @@
 (program $arith_mk_zero ((T Type))
   (Type) T
   (
-    (($arith_mk_zero Real) 0.0)
+    (($arith_mk_zero Real) 0/1)
     (($arith_mk_zero Int)  0)
   )
 )

proofs/eo/cpc/rules/Transcendentals.eo

@@ -58,7 +58,7 @@
 ;   is one.
 (declare-rule arith_trans_exp_zero ((x Real))
   :args (x)
-  :conclusion (= (= x 0.0) (= (exp x) 1.0))
+  :conclusion (= (= x 0/1) (= (exp x) 1/1))
 )
 
 ; rule: arith_trans_sine_bounds

src/api/java/io/github/cvc5/Solver.java

@@ -2765,6 +2765,27 @@ public String proofToString(Proof proof, ProofFormat format)
 
   private native String proofToString(long pointer, long proofs, int format);
 
+  /**
+   * Prints a proof into a string with a slected proof format mode.
+   * Other aspects of printing are taken from the solver options.
+   *
+   * @api.note This method is experimental and may change in future versions.
+   *
+   * @param proof A proof.
+   * @param format The proof format used to print the proof. Must be
+   * `PROOF_FORMAT_NONE` if the proof is from a component other than
+   * `PROOF_COMPONENT_FULL`.
+   * @param assertionNames Mapping between assertions and names, if they were
+   * given by the user.  This is used by the Alethe proof format.
+   * @return The proof printed in the current format.
+   */
+  public String proofToString(Proof proof, ProofFormat format, Map assertionNames)
+  {
+    return proofToString(pointer, proof.getPointer(), format.getValue(), assertionNames);
+  }
+
+  private native String proofToString(long pointer, long proofs, int format, Map assertionNames);
+
   /**
    * Get the value of the given term in the current model.
    *

src/api/java/jni/solver.cpp

@@ -744,6 +744,74 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_Solver_proofToString__JJI(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     io_github_cvc5_Solver
+ * Method:    proofToString
+ * Signature: (JJILjava/util/Map;)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL
+Java_io_github_cvc5_Solver_proofToString__JJILjava_util_Map_2(
+    JNIEnv* env,
+    jobject,
+    jlong pointer,
+    jlong proofPointer,
+    jint pfvalue,
+    jobject assertionNames)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  modes::ProofFormat pf = static_cast<modes::ProofFormat>(pfvalue);
+  Proof* proof = reinterpret_cast<Proof*>(proofPointer);
+
+  jclass c_map = env->GetObjectClass(assertionNames);
+  jmethodID id_entrySet =
+      env->GetMethodID(c_map, "entrySet", "()Ljava/util/Set;");
+
+  jclass c_entryset = env->FindClass("java/util/Set");
+  jmethodID id_iterator =
+      env->GetMethodID(c_entryset, "iterator", "()Ljava/util/Iterator;");
+
+  jclass c_iterator = env->FindClass("java/util/Iterator");
+  jmethodID id_hasNext = env->GetMethodID(c_iterator, "hasNext", "()Z");
+  jmethodID id_next =
+      env->GetMethodID(c_iterator, "next", "()Ljava/lang/Object;");
+
+  jclass c_entry = env->FindClass("java/util/Map$Entry");
+  jmethodID id_getKey =
+      env->GetMethodID(c_entry, "getKey", "()Ljava/lang/Object;");
+  jmethodID id_getValue =
+      env->GetMethodID(c_entry, "getValue", "()Ljava/lang/Object;");
+
+  jclass c_term = env->FindClass("io/github/cvc5/Term");
+  jmethodID id_getPointer = env->GetMethodID(c_term, "getPointer", "()J");
+
+  jobject obj_entrySet = env->CallObjectMethod(assertionNames, id_entrySet);
+  jobject obj_iterator = env->CallObjectMethod(obj_entrySet, id_iterator);
+
+  std::map<Term, std::string> namesMap;
+
+  while ((bool)env->CallBooleanMethod(obj_iterator, id_hasNext))
+  {
+    jobject entry = env->CallObjectMethod(obj_iterator, id_next);
+
+    jobject key = env->CallObjectMethod(entry, id_getKey);
+    jstring value = (jstring)env->CallObjectMethod(entry, id_getValue);
+
+    jlong termPointer = (jlong)env->CallObjectMethod(key, id_getPointer);
+    Term term = *reinterpret_cast<Term*>(termPointer);
+
+    const char* termName = (env)->GetStringUTFChars(value, 0);
+    std::string termNameString = std::string(termName);
+    (env)->ReleaseStringUTFChars(value, termName);
+
+    namesMap.insert(std::pair{term, termNameString});
+  }
+
+  std::string proofStr = solver->proofToString(*proof, pf, namesMap);
+  return env->NewStringUTF(proofStr.c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
 /*
  * Class:     io_github_cvc5_Solver
  * Method:    getValue

src/api/python/cvc5.pxd

@@ -454,7 +454,7 @@ cdef extern from "<cvc5/cvc5.h>" namespace "cvc5":
         Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars,
                            vector[Term]& terms, bint glbl) except +
         vector[Proof] getProof(ProofComponent c) except +
-        string proofToString(Proof proof, ProofFormat format) except +
+        string proofToString(Proof proof, ProofFormat format, const map[Term, string]& assertionNames) except +
         vector[Term] getLearnedLiterals(LearnedLitType type) except +
         vector[Term] getAssertions() except +
         string getInfo(const string& flag) except +

src/api/python/cvc5.pxi

@@ -14,6 +14,7 @@ from libcpp.pair cimport pair
 from libcpp.set cimport set as c_set
 from libcpp.string cimport string
 from libcpp.vector cimport vector
+from libcpp.map cimport map
 
 from cvc5 cimport cout
 from cvc5 cimport stringstream
@@ -3591,7 +3592,8 @@ cdef class Solver:
         return proofs
 
     def proofToString(self, proof,
-                      format = ProofFormat.DEFAULT):
+                      format = ProofFormat.DEFAULT,
+                      assertionNames = {}):
         """
             Prints proof into a string with a selected proof format mode.
             Other aspects of printing are taken from the solver options.
@@ -3603,11 +3605,18 @@ cdef class Solver:
                           :py:meth:`getProof()`.
             :param format: The proof format used to print the proof.  Must be
                           "None" if the proof is not a full proof.
+            :param assertionNames: Mapping between assertions and names, if
+                                   they were  given by the user.  This is used
+                                   by the Alethe proof format.
 
             :return: The proof printed in the current format.
         """
+        cdef map[c_Term, string] assertionMap
+        for k in assertionNames:
+            assertionMap[(<Term> k).cterm] = assertionNames[k].encode('utf-8')
         return self.csolver.proofToString((<Proof?> proof).cproof,
-                                         <c_ProofFormat> format.value)
+                                         <c_ProofFormat> format.value,
+                                         assertionMap)
 
     def getLearnedLiterals(self, type = LearnedLitType.INPUT):
         """

src/api/python/pyproject.toml

@@ -1,7 +1,10 @@
 [build-system]
 requires = [
     "setuptools>=66.1.0",
+    # Avoid issue #268: https://github.com/pypa/distutils/issues/268
     "setuptools!=70.2.0; os_name == 'nt'",
+    # Avoid issue #283: https://github.com/pypa/distutils/issues/283
+    "setuptools<72.2.0; implementation_name == 'pypy'",
     "Cython>=3"
 ]
 build-backend = "setuptools.build_meta"

src/options/smt_options.toml

@@ -126,12 +126,19 @@ name   = "SMT Layer"
   help_mode  = "proof modes."
 [[option.mode.OFF]]
   name = "off"
+  help = "Do not produce proofs."
 [[option.mode.PP_ONLY]]
   name = "pp-only"
+  help = "Only produce proofs for preprocessing."
 [[option.mode.SAT]]
   name = "sat-proof"
+  help = "Produce proofs for preprocessing and for the SAT solver."
 [[option.mode.FULL]]
   name = "full-proof"
+  help = "Produce full proofs of preprocessing, SAT and theory lemmas."
+[[option.mode.FULL_STRICT]]
+  name = "full-proof-strict"
+  help = "Produce full proofs of preprocessing, SAT and theory lemmas. Additionally disable techniques that will lead to incomplete proofs."
 
 [[option]]
   name       = "checkProofs"