Merge branch 'main' into proof-new

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

@@ -26,8 +26,9 @@ runs:
         # only work for the specific CI Python version.
         rm -rf ${{ inputs.build-dir }}/install/lib/python*
 
-        # Copy COPYING file to install directory
+        # Copy COPYING file and licenses directory to install directory
         cp COPYING ${{ inputs.build-dir }}/install/
+        cp -r licenses ${{ inputs.build-dir }}/install/
 
         # Create ZIP file
         pushd ${{ inputs.build-dir }}

.github/actions/package-python-wheel-macos/action.yml

@@ -10,7 +10,7 @@ inputs:
 runs:
   using: composite
   steps:
-    - uses: actions/setup-python@v4
+    - uses: actions/setup-python@v5
       if: runner.os == 'macOS'
       with:
         python-version: ${{ inputs.python-version }}

COPYING

@@ -52,16 +52,23 @@ The following file contains third-party software.
 
 The copyright and licensing information of this file is in its header.
 
-cvc5 incorporates MiniSat code (see src/prop/minisat and src/prop/bvminisat),
-excluded from the above copyright.  See src/prop/minisat/LICENSE and
-src/prop/bvminisat/LICENSE for copyright and licensing information.
+cvc5 incorporates MiniSat code (see src/prop/minisat),
+excluded from the above copyright. See licenses/minisat-LICENSE
+for copyright and licensing information.
 
 cvc5 by default links against The GNU Multiple Precision (GMP) Arithmetic
-Library, which is licensed under GNU LGPL v3. See the file
+Library, which is licensed under GNU LGPL v3.  See the file
 licenses/lgpl-3.0.txt for a copy of that license.  Note that according to the
 terms of the LGPL, both cvc5's source, and the combined work (cvc5 linked with
 GMP) may (and do) remain under the more permissive modified BSD license.
 
+cvc5 also links against the CaDiCaL library
+(https://github.com/arminbiere/cadical), which is licensed under
+the MIT license.
+See https://raw.githubusercontent.com/arminbiere/cadical/master/LICENSE
+for copyright and licensing information.  Linking cvc5 against
+this library does not affect the license terms of the cvc5 code.
+
 The implementation of the floating point solver in cvc5 depends on symfpu
 (https://github.com/martin-cs/symfpu) written by Martin Brain.
 See https://raw.githubusercontent.com/martin-cs/symfpu/CVC4/LICENSE for
@@ -70,7 +77,6 @@ copyright and licensing information.
 cvc5 optionally links against the following libraries:
 
   ABC                (https://bitbucket.org/alanmi/abc)
-  CaDiCaL            (https://github.com/arminbiere/cadical)
   CryptoMiniSat      (https://github.com/msoos/cryptominisat)
   LibPoly            (https://github.com/SRI-CSL/libpoly)
   libedit            (https://thrysoee.dk/editline)

INSTALL.rst

@@ -118,13 +118,16 @@ versions; more recent versions should be compatible.
 - `GNU C and C++ (gcc and g++, >= 7) <https://gcc.gnu.org>`_
   or `Clang (>= 5) <https://clang.llvm.org>`_
 - `CMake >= 3.9 <https://cmake.org>`_
-- `Python >= 3.6 and <= 3.10 <https://www.python.org>`_
+- `Python >= 3.6 <https://www.python.org>`_
   + module `tomli <https://pypi.org/project/tomli/>`_
   + module `pyparsing <https://pypi.org/project/pyparsing/>`_
 - `GMP v6.3 (GNU Multi-Precision arithmetic library) <https://gmplib.org>`_
 - `CaDiCaL (SAT solver) <https://github.com/arminbiere/cadical>`_
 - `SymFPU <https://github.com/martin-cs/symfpu/tree/CVC4>`_
 
+For Python, to install these dependencies automatically, please use:
+
+  - `pip install -r contrib/requirements_build.txt`
 
 CaDiCaL (SAT solver)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -258,6 +261,10 @@ Dependencies for Language Bindings
   - `pytest <https://docs.pytest.org/en/6.2.x/>`_
   - The source for the `pythonic API <(https://github.com/cvc5/cvc5_pythonic_api)>`.
 
+For Python, to install these depedencies automatically, please use:
+
+  - `pip install -r contrib/requirements_python_dev.txt`
+
 If configured with ``--pythonic-path=PATH``, the build system will expect the Pythonic API's source to be at ``PATH``.
 Otherwise, if configured with ``--auto-download``, the build system will download it.
 

cmake/FindCLN.cmake

@@ -44,7 +44,7 @@ if(NOT CLN_FOUND_SYSTEM)
   fail_if_cross_compiling("Windows" "" "CLN" "autoconf fails")
   fail_if_cross_compiling("" "arm" "CLN" "syntax error in configure")
 
-  set(CLN_VERSION "1.3.6")
+  set(CLN_VERSION "1.3.7")
   string(REPLACE "." "-" CLN_TAG ${CLN_VERSION})
 
   find_program(AUTORECONF autoreconf)
@@ -56,7 +56,7 @@ if(NOT CLN_FOUND_SYSTEM)
     CLN-EP
     ${COMMON_EP_CONFIG}
     URL "https://www.ginac.de/CLN/cln.git/?p=cln.git\\\;a=snapshot\\\;h=cln_${CLN_TAG}\\\;sf=tgz"
-    URL_HASH SHA1=71d02b90ef0575f06b7bafb8690f73e8064d8228
+    URL_HASH SHA1=bd6dec17cf1088bdd592794d9239d47c752cf3da
     DOWNLOAD_NAME cln.tgz
     CONFIGURE_COMMAND
       ${CMAKE_COMMAND} -E chdir <SOURCE_DIR> ./autogen.sh

contrib/get-alf-checker

@@ -24,7 +24,7 @@ ALFC_DIR="$BASE_DIR/alf-checker"
 mkdir -p $ALFC_DIR
 
 # download and unpack ALFC
-ALF_VERSION="b51d495b4871dc0c4e4f68e579a504cec288b022"
+ALF_VERSION="57b34b6b5c130eb44332149b110bed130b3281e3"
 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
 

contrib/packaging_python/mk_clean_wheel.sh

@@ -40,7 +40,8 @@ source ./$ENVDIR/bin/activate
 
 # install packages
 pip install -q --upgrade pip setuptools auditwheel
-pip install -q Cython pytest tomli scikit-build flex pyparsing 
+pip install -r contrib/requirements_build.txt
+pip install -r contrib/requirements_python_dev.txt
 if [ "$(uname)" == "Darwin" ]; then
     # Mac version of auditwheel
     pip install -q delocate
@@ -59,6 +60,8 @@ rm -rf build_wheel/
 echo "Building pycvc5 wheel"
 
 pushd build_wheel
+# Copy the license files to be included in the wheel
+cmake --build . --target cvc5_python_licenses
 if [ -z "$PLATFORM" ] ; then
   python ../contrib/packaging_python/mk_wheel.py bdist_wheel -d dist
 else

contrib/packaging_python/mk_wheel.py

@@ -113,9 +113,13 @@ def build_extension(self, ext):
     version=get_cvc5_version(),
     long_description='Python bindings for cvc5',
     url='https://github.com/cvc5/cvc5',
-    license='BSD-3-Clause',
+    license = "BSD-3-Clause AND LGPL-3.0-or-later AND MIT",
+    # BSD-3-Clause      : cvc5 library and Python API
+    # LGPL-3.0-or-later : LibPoly and GMP
+    # MIT               : Pythonic API
     zip_safe=False,
     ext_modules=[CMakeExtension('cvc5')],
     cmdclass=dict(build_ext=CMakeBuild),
-    tests_require=['pytest']
+    tests_require=['pytest'],
+    license_files = ['COPYING', 'licenses/*'],
 )

contrib/requirements_build.txt

@@ -0,0 +1,2 @@
+tomli
+pyparsing

contrib/requirements_python_dev.txt

@@ -0,0 +1,3 @@
+Cython
+pytest
+scikit-build

docs/api/python/python.rst

@@ -47,7 +47,7 @@ Before building and installing, the following dependencies should be installed,
 .. code:: bash
 
   brew install cmake python gmp java
-  pip3 install cython tomli scikit-build pyparsing
+  pip3 install -r contrib/requirements_python_dev.txt
 
 
 Then `cvc5` can be installed from source as follows:

include/cvc5/cvc5.h

@@ -4642,11 +4642,15 @@ class CVC5_EXPORT Solver
    * @param format The proof format used to print the proof.  Must be
    * `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.
    * @return The string representation of the proof in the given format.
    */
   std::string proofToString(
       Proof proof,
-      modes::ProofFormat format = modes::ProofFormat::DEFAULT) const;
+      modes::ProofFormat format = modes::ProofFormat::DEFAULT,
+      const std::map<cvc5::Term, std::string>& assertionNames =
+          std::map<cvc5::Term, std::string>()) const;
 
   /**
    * Get a list of learned literals that are entailed by the current set of

include/cvc5/cvc5_proof_rule.h

@@ -1322,7 +1322,7 @@ enum ENUM(ProofRule) : uint32_t
    *
    * .. math::
    *
-   *   \inferruleSC{-\mid F, y_1=z_1,\dots, y_n=z_n}
+   *   \inferruleSC{-\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)}
    *   {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}}
    *   {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables}
    *
@@ -1395,21 +1395,29 @@ enum ENUM(ProofRule) : uint32_t
    * \mathit{index},b)` is null, in other words, neither is a prefix of the
    * other. Note it may be the case that one side of the equality denotes the
    * empty string.
+   * 
+   * This rule is used exclusively for strings.
    *
-   * Alternatively, if the equality is between sequences, this rule has the
-   * form:
+   * \endverbatim
+   */
+  EVALUE(CONCAT_CONFLICT),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Strings -- Core rules -- Concatenation conflict for disequal characters**
    *
    * .. math::
    *
    *   \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq s_1 \mid b}{\bot}
    *
-   * where t_1 and s_1 are constants of length one, or otherwise one side
-   * of the equality is the empty sequence and t_1 or s_1 corresponding to
+   * where $t_1$ and $s_1$ are constants of length one, or otherwise one side
+   * of the equality is the empty sequence and $t_1$ or $s_1$ corresponding to
    * that side is the empty sequence.
+   * 
+   * This rule is used exclusively for sequences.
    *
    * \endverbatim
    */
-  EVALUE(CONCAT_CONFLICT),
+  EVALUE(CONCAT_CONFLICT_DEQ),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Strings -- Core rules -- Concatenation split**
@@ -1768,7 +1776,7 @@ enum ENUM(ProofRule) : uint32_t
    * **Arithmetic -- Trichotomy of the reals**
    *
    * .. math::
-   *   \inferrule{A, B \mid C}{C}
+   *   \inferrule{A, B \mid -}{C}
    *
    * where :math:`\neg A, \neg B, C` are :math:`x < c, x = c, x > c` in some order.
    * Note that :math:`\neg` here denotes arithmetic negation, i.e., flipping :math:`\geq` to :math:`<` etc.

licenses/minisat-LICENSE

@@ -0,0 +1,21 @@
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+           Copyright (c) 2007-2010  Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a
+copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

proofs/alf/programs/Quantifiers.smt3

@@ -19,4 +19,3 @@
     ((substitute_list @list.nil @list.nil F)       F)
   )
 )
-

proofs/alf/rules/Booleans.smt3

@@ -3,44 +3,6 @@
 
 (include "../programs/Nary.smt3")
 
-; SCOPE
-(declare-rule scope
-  ((F Bool) (G Bool))
-  :assumption F
-  :premises (G)
-  :args ()
-  :conclusion (=> F G)
-)
-
-; `extract_antec F C`
-; returns the antecedant of F up to C,
-; e.g. returns (and G1 G2) when F is (=> G1 (=> G2 C)).
-(program extract_antec
-   ((C Bool) (F1 Bool) (F2 Bool))
-   (Bool Bool) Bool
-   (
-   ((extract_antec C C) true)
-   ((extract_antec (=> F1 F2) C) (alf.cons and F1 (extract_antec F2 C)))
-   )
-)
-
-(program run_process_scope
-   ((C Bool) (F Bool))
-   (Bool Bool) Bool
-   (
-   ((run_process_scope F false) (not (alf.from_list and (extract_antec F false))))
-   ((run_process_scope F C) (=> (alf.from_list and (extract_antec F C)) C))
-   )
-)
-
-; this rule processes the result of n scopes into the conclusion expected by ProofRule::SCOPE
-(declare-rule process_scope
-  ((C Bool) (F Bool))
-  :premises (F)
-  :args (C)
-  :conclusion (run_process_scope F C)
-)
-
 ; SPLIT
 (declare-rule split ((F Bool))
     :args (F)

proofs/alf/rules/Builtin.smt3

@@ -1,5 +1,43 @@
 (include "../theories/Builtin.smt3")
 
+; SCOPE
+(declare-rule scope
+  ((F Bool) (G Bool))
+  :assumption F
+  :premises (G)
+  :args ()
+  :conclusion (=> F G)
+)
+
+; `extract_antec F C`
+; returns the antecedant of F up to C,
+; e.g. returns (and G1 G2) when F is (=> G1 (=> G2 C)).
+(program extract_antec
+   ((C Bool) (F1 Bool) (F2 Bool))
+   (Bool Bool) Bool
+   (
+   ((extract_antec C C) true)
+   ((extract_antec (=> F1 F2) C) (alf.cons and F1 (extract_antec F2 C)))
+   )
+)
+
+(program run_process_scope
+   ((C Bool) (F Bool))
+   (Bool Bool) Bool
+   (
+   ((run_process_scope F false) (not (alf.from_list and (extract_antec F false))))
+   ((run_process_scope F C) (=> (alf.from_list and (extract_antec F C)) C))
+   )
+)
+
+; this rule processes the result of n scopes into the conclusion expected by ProofRule::SCOPE
+(declare-rule process_scope
+  ((C Bool) (F Bool))
+  :premises (F)
+  :args (C)
+  :conclusion (run_process_scope F C)
+)
+
 (declare-rule remove_term_formula_axiom ((T Type) (b Bool) (t1 T) (t2 T))
   :args ((ite b t1 t2))
   :conclusion

proofs/alf/rules/Quantifiers.smt3

@@ -34,8 +34,16 @@
       t
       (
         ; special case for witness
-        ((skolem (@k.QUANTIFIERS_SKOLEMIZE (exists (@list x) F) x)) (= t (witness x F)))
+        ((skolem (@k.QUANTIFIERS_SKOLEMIZE (exists (@list x) F) x)) (= t (witness (@list x) F)))
         ((skolem x)                                                 (= t x))
       )
    )
 )
+
+; B is the formula to apply to
+; vs is a list of variables to substitution for the variable list ts
+; Note we don't currently check whether this is valid renaming.
+(declare-rule alpha_equiv ((B Bool) (vs @List) (ts @List))
+  :args (B vs ts)
+  :conclusion (= B (substitute_list vs ts B))
+)