Merge branch 'main' into fix-lazypfchain

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

@@ -9,11 +9,13 @@ inputs:
     description: token to upload package to latest
   github-token-release:
     description: token to upload package to release
+  shell:
+    default: bash
 runs:
   using: composite
   steps:
     - name: Create ZIP file
-      shell: bash
+      shell: ${{ inputs.shell }}
       run: |
         echo "::group::Create ZIP file"
         # Run 'make install' on build directory
@@ -41,7 +43,7 @@ runs:
         echo "::endgroup::"
 
     - name: install pyGithub
-      shell: bash
+      shell: ${{ inputs.shell }}
       run: |
         python3 -m pip install pyGithub
 

.github/actions/install-dependencies/action.yml

@@ -74,6 +74,7 @@ runs:
           mingw-w64-x86_64-cmake
           mingw-w64-x86_64-gcc
           mingw-w64-x86_64-gmp
+          zip
 
     - name: Set up num_proc variable for Linux and Windows
       if: runner.os == 'Linux' || runner.os == 'Windows'

.github/workflows/ci.yml

@@ -69,6 +69,7 @@ jobs:
             windows-build: true
             shell: 'msys2 {0}'
             check-examples: true
+            package-name: cvc5-Win64
             exclude_regress: 1-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
 
@@ -78,7 +79,6 @@ jobs:
             cache-key: production-win64-cross
             strip-bin: x86_64-w64-mingw32-strip
             windows-build: true
-            package-name: cvc5-Win64
 
           - name: ubuntu:production-clang
             os: ubuntu-20.04
@@ -181,6 +181,7 @@ jobs:
         # when using GITHUB_TOKEN, no further workflows are triggered
         github-token-latest: ${{ secrets.GITHUB_TOKEN }}
         github-token-release: ${{ secrets.ACTION_USER_TOKEN }}
+        shell: ${{ matrix.shell }}
 
     - name: Create and add static package to latest and release
       if: matrix.package-name && (github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/'))
@@ -191,6 +192,7 @@ jobs:
         # when using GITHUB_TOKEN, no further workflows are triggered
         github-token-latest: ${{ secrets.GITHUB_TOKEN }}
         github-token-release: ${{ secrets.ACTION_USER_TOKEN }}
+        shell: ${{ matrix.shell }}
 
   update-pr:
     runs-on: ubuntu-latest

.github/workflows/package_pypi.yml

@@ -97,7 +97,7 @@ jobs:
         # Use delvewheel on windows
         CIBW_BEFORE_BUILD_WINDOWS: "pip install delvewheel"
         CIBW_REPAIR_WHEEL_COMMAND_WINDOWS: >
-          delvewheel repair -w {dest_dir} {wheel} --add-path "${{ github.workspace }}\install\lib;${{ steps.mingw64-path.outputs.bin }}"
+          delvewheel repair -w {dest_dir} {wheel} --add-path "${{ github.workspace }}\install\bin;${{ steps.mingw64-path.outputs.bin }}"
         CIBW_ENVIRONMENT_LINUX: >
           LD_LIBRARY_PATH="$(pwd)/install/lib64:$LD_LIBRARY_PATH"
         CIBW_ENVIRONMENT_MACOS: >

INSTALL.rst

@@ -186,6 +186,16 @@ LibPoly >= v0.1.13 (Optional polynomial library)
 nonlinear reasoning. It can be downloaded and built automatically. Configure
 cvc5 with ``configure.sh --poly`` to build with this dependency.
 
+CoCoA (Optional computer algebra library)
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+`CoCoA <https://cocoa.dima.unige.it/cocoa/>`_ is required for some non-linear
+reasoning and for finite field reasoning. We use a patched version of it, so we
+recommend downloading it using the ``--auto-download`` configuration flag,
+which applies our patch automatically. It is included in the build through the
+``--cocoa`` configuration flag.
+
+CoCoA is covered by the GPLv3 license. See below for the ramifications of this.
 
 CLN >= v1.3 (Class Library for Numbers)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

include/cvc5/cvc5.h

@@ -3532,7 +3532,7 @@ class CVC5_EXPORT Proof
    * @return The proof rewrite rule used by the root step of the proof.
    *
    * @exception raises an exception if `getRule()` does not return
-   * `DSL_REWRITE`.
+   * `DSL_REWRITE` or `THEORY_REWRITE`.
    */
   ProofRewriteRule getRewriteRule() const;
 

include/cvc5/cvc5_proof_rule.h

@@ -291,7 +291,7 @@ enum ENUM(ProofRule) : uint32_t
    * .. math::
    *   \inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F}
    * 
-   * where the DSL rewrite rule with the given identifier is
+   * where `id` is a `ProofRewriteRule` whose definition in the RARE DSL is
    * :math:`\forall x_1 \dots x_n. (G_1 \wedge G_n) \Rightarrow G`
    * where for :math:`i=1, \dots n`, we have that :math:`F_i = \sigma(G_i)`
    * and :math:`F = \sigma(G)` where :math:`\sigma` is the substitution
@@ -305,6 +305,23 @@ enum ENUM(ProofRule) : uint32_t
    * \endverbatim
    */
   EVALUE(DSL_REWRITE),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Other theory rewrite rules**
+   *
+   * .. math::
+   *   \inferrule{- \mid id, t}{t = t'}
+   *
+   * where `id` is the `ProofRewriteRule` of the theory rewrite rule which
+   * transforms :math:`t` to :math `t'`.
+   * 
+   * In contrast to `DSL_REWRITE`, theory rewrite rules used by this proof
+   * rule are not necessarily expressible in RARE. Each rule that can be used
+   * in this proof rule are documented explicitly in cases within the
+   * `ProofRewriteRule` enum.
+   * \endverbatim
+   */
+  EVALUE(THEORY_REWRITE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Builtin theory -- Annotation**
@@ -2278,11 +2295,24 @@ enum ENUM(ProofRule) : uint32_t
  * This enumeration represents the rewrite rules used in a rewrite proof. Some
  * of the rules are internal ad-hoc rewrites, while others are rewrites
  * specified by the RARE DSL. This enumeration is used as the first argument to
- * the :cpp:enumerator:`DSL_REWRITE <cvc5::ProofRule::DSL_REWRITE>` proof rule.
+ * the :cpp:enumerator:`DSL_REWRITE <cvc5::ProofRule::DSL_REWRITE>` proof rule
+ * and the :cpp:enumerator:`DSL_REWRITE <cvc5::ProofRule::THEORY_REWRITE>` proof
+ * rule.
  */
 enum ENUM(ProofRewriteRule) : uint32_t
 {
   EVALUE(NONE),
+  // Custom theory rewrites.
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Quantifiers -- Exists elimination**
+   *
+   * .. math::
+   *   \exists x_1\dots x_n.\> F = \neg \forall x_1\dots x_n.\> \neg F
+   *
+   * \endverbatim
+   */
+  EVALUE(EXISTS_ELIM),
   // RARE rules
   // ${rules}$
   /** Auto-generated from RARE rule arith-plus-zero */

proofs/alf/cvc5/Cvc5.smt3

@@ -60,7 +60,15 @@
     (S) S
     (
       ; core
-      ((run_evaluate (= x y))             (alf.is_eq (run_evaluate x) (run_evaluate y))) ; FIXME
+      ((run_evaluate (= x y))             (let ((ex (run_evaluate x)))
+                                          (let ((ey (run_evaluate y)))
+                                          (let ((res (alf.is_eq ex ey)))
+                                          (alf.ite (alf.and ($is_q_literal ex) ($is_q_literal ey)) res
+                                          (alf.ite (alf.and ($is_z_literal ex) ($is_z_literal ey)) res
+                                          (alf.ite (alf.and ($is_bin_literal ex) ($is_bin_literal ey)) res
+                                          (alf.ite (alf.and ($is_str_literal ex) ($is_str_literal ey)) res
+                                          (alf.ite (alf.and ($is_bool_literal ex) ($is_bool_literal ey)) res
+                                            (= ex ey))))))))))
       ((run_evaluate (not b))             (alf.not (run_evaluate b)))
       ((run_evaluate (ite b x y))         (alf.ite (run_evaluate b) (run_evaluate x) (run_evaluate y)))
       ((run_evaluate (or x ys))           (alf.or (run_evaluate x) (run_evaluate ys)))
@@ -113,7 +121,10 @@
                                           (let ((ey (run_evaluate y)))
                                           (let ((r (alf.find (alf.to_str ex) (alf.to_str ey))))
                                               (alf.ite (alf.is_neg r) r (alf.add n r))))))
+
       ; bitvectors
+      ((run_evaluate (bvnot xb))          (alf.not (run_evaluate xb)))
+      ((run_evaluate (bvneg xb))          (alf.neg (run_evaluate xb)))
       ((run_evaluate (bvadd xb ybs))      (alf.add (run_evaluate xb) (run_evaluate ybs)))
       ((run_evaluate (bvmul xb ybs))      (alf.mul (run_evaluate xb) (run_evaluate ybs)))
       ((run_evaluate (bvand xb ybs))      (alf.and (run_evaluate xb) (run_evaluate ybs)))
@@ -126,6 +137,7 @@
       ((run_evaluate (bvugt x y))         (run_evaluate (> (alf.to_z x) (alf.to_z y))))
       ((run_evaluate (bvuge x y))         (run_evaluate (>= (alf.to_z x) (alf.to_z y))))
       ((run_evaluate (@bv n m))           (alf.to_bin (run_evaluate m) (run_evaluate n)))
+      ((run_evaluate (@bvsize x))         ($bv_bitwidth (alf.typeof x)))
 
       ((run_evaluate z)                   z)
     )

proofs/alf/cvc5/programs/Utils.smt3

@@ -1,4 +1,16 @@
 
+; Returns true if x is a Boolean literal.
+(define $is_bool_literal ((T Type :implicit) (x T))
+  (alf.ite (alf.is_eq x true) true (alf.is_eq x false)))
+
+; Returns true if x is a rational literal.
+(define $is_q_literal ((T Type :implicit) (x T))
+  (alf.is_eq (alf.to_q x) x))
+
+; Returns true if x is a numeral literal.
+(define $is_z_literal ((T Type :implicit) (x T))
+  (alf.is_eq (alf.to_z x) x))
+
 ; Returns true if x is a binary literal.
 (define $is_bin_literal ((T Type :implicit) (x T))
   (alf.is_eq (alf.to_bin (alf.len x) x) x))

src/CMakeLists.txt

@@ -624,6 +624,8 @@ libcvc5_add_sources(
   theory/builtin/theory_builtin_rewriter.h
   theory/builtin/theory_builtin_type_rules.cpp
   theory/builtin/theory_builtin_type_rules.h
+  theory/builtin/theory_rewrite_proof_checker.cpp
+  theory/builtin/theory_rewrite_proof_checker.h
   theory/builtin/type_enumerator.cpp
   theory/builtin/type_enumerator.h
   theory/bv/bitblast/bitblast_proof_generator.cpp

src/api/cpp/cvc5.cpp

@@ -5048,8 +5048,11 @@ ProofRule Proof::getRule() const
 ProofRewriteRule Proof::getRewriteRule() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(this->getProofNode()->getRule() == ProofRule::DSL_REWRITE)
-      << "Expected `getRule()` to return `DSL_REWRITE`, got "
+  CVC5_API_CHECK(this->getProofNode()->getRule() == ProofRule::DSL_REWRITE
+                 || this->getProofNode()->getRule()
+                        == ProofRule::THEORY_REWRITE)
+      << "Expected `getRule()` to return `DSL_REWRITE` or `THEORY_REWRITE`, "
+         "got "
       << this->getProofNode()->getRule() << " instead.";
   //////// all checks before this line
   if (d_proof_node != nullptr)

src/api/cpp/cvc5_proof_rule_template.cpp

@@ -37,6 +37,7 @@ const char* toString(ProofRule rule)
     case ProofRule::ENCODE_PRED_TRANSFORM: return "ENCODE_PRED_TRANSFORM";
     case ProofRule::ANNOTATION: return "ANNOTATION";
     case ProofRule::DSL_REWRITE: return "DSL_REWRITE";
+    case ProofRule::THEORY_REWRITE: return "THEORY_REWRITE";
     case ProofRule::REMOVE_TERM_FORMULA_AXIOM:
       return "REMOVE_TERM_FORMULA_AXIOM";
     //================================================= Trusted rules
@@ -219,8 +220,10 @@ const char* toString(cvc5::ProofRewriteRule rule)
 {
   switch (rule)
   {
-    case ProofRewriteRule::NONE:
-      return "NONE";
+    case ProofRewriteRule::NONE: return "NONE";
+    //================================================= ad-hoc rules
+    case ProofRewriteRule::EXISTS_ELIM:
+      return "exists_elim";
       //================================================= RARE rules
       // clang-format off
       ${printer}$

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

@@ -59,7 +59,8 @@ public ProofRule getRule() throws CVC5ApiException
 
   /**
    * @return The proof rewrite rule used by the root step of the proof.
-   * @throws CVC5ApiException if `getRule()` does not return `DSL_REWRITE`.
+   * @throws CVC5ApiException if `getRule()` does not return `DSL_REWRITE`
+   *         or `THEORY_REWRITE`.
    */
   public ProofRewriteRule getRewriteRule() throws CVC5ApiException
   {

src/api/python/cvc5.pxi

@@ -5678,7 +5678,7 @@ cdef class Proof:
         """
             :return: The proof rewrite rule used by the root step of the proof.
                      Raises an exception if `getRule()` does not return
-                     `DSL_REWRITE`.
+                     `DSL_REWRITE` or `THEORY_REWRITE`.
         """
         return ProofRewriteRule(<int> self.cproof.getRewriteRule())
 

src/expr/skolem_manager.cpp

@@ -53,6 +53,7 @@ const char* toString(InternalSkolemId id)
     case InternalSkolemId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
     case InternalSkolemId::MBQI_INPUT: return "MBQI_INPUT";
     case InternalSkolemId::ABSTRACT_VALUE: return "ABSTRACT_VALUE";
+    case InternalSkolemId::QE_CLOSED_INPUT: return "QE_CLOSED_INPUT";
     default: return "?";
   }
 }

src/expr/skolem_manager.h

@@ -58,6 +58,8 @@ enum class InternalSkolemId
   MBQI_INPUT,
   /** abstract value for a term t */
   ABSTRACT_VALUE,
+  /** Input variables for quantifier elimination of closed formulas */
+  QE_CLOSED_INPUT
 };
 /** Converts an internal skolem function name to a string. */
 const char* toString(InternalSkolemId id);

src/options/main_options.toml

@@ -54,6 +54,7 @@ name   = "Driver"
 
 [[option]]
   name       = "seed"
+  alias      = ["random-seed"]
   category   = "common"
   short      = "s"
   long       = "seed=N"

src/options/uf_options.toml

@@ -67,6 +67,14 @@ name   = "Uninterpreted Functions Theory"
   default    = "true"
   help       = "do lambda lifting lazily"
 
+[[option]]
+  name       = "ufHoLambdaQe"
+  category   = "expert"
+  long       = "uf-lambda-qe"
+  type       = "bool"
+  default    = "false"
+  help       = "apply quantifier elimination eagerly when two lambdas are equated"
+
 [[option]]
   name       = "eagerArithBvConv"
   category   = "expert"

src/proof/alf/alf_node_converter.cpp

@@ -265,6 +265,18 @@ Node AlfNodeConverter::postConvert(Node n)
     args.insert(args.end(), n.begin(), n.end());
     return mkInternalApp("@list", args, tn);
   }
+  else if (k == Kind::APPLY_INDEXED_SYMBOLIC)
+  {
+    Kind okind = n.getOperator().getConst<GenericOp>().getKind();
+    if (okind == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
+    {
+      // This does not take a rounding mode, we change the smt2 syntax
+      // to distinguish this case, similar to the case in getOperatorOfTerm
+      // where it is processed as an indexed operator.
+      std::vector<Node> children(n.begin(), n.end());
+      return mkInternalApp("to_fp_bv", children, tn);
+    }
+  }
   else if (GenericOp::isIndexedOperatorKind(k))
   {
     // return app of?
@@ -343,8 +355,15 @@ Node AlfNodeConverter::maybeMkSkolemFun(Node k)
     }
     if (!app.isNull())
     {
-      // wrap in "skolem" operator
-      return mkInternalApp("skolem", {app}, k.getType());
+      // If it has no children, then we don't wrap in `(skolem ...)`, since it
+      // makes no difference for substitution. Moreover, it is important not
+      // to do this since bitvector concat uses @bv_empty as its nil terminator.
+      if (sfi == SkolemId::PURIFY || app.getNumChildren() > 0)
+      {
+        // wrap in "skolem" operator
+        return mkInternalApp("skolem", {app}, k.getType());
+      }
+      return app;
     }
   }
   return Node::null();
@@ -668,6 +687,7 @@ bool AlfNodeConverter::isHandledSkolemId(SkolemId id)
   {
     case SkolemId::PURIFY:
     case SkolemId::ARRAY_DEQ_DIFF:
+    case SkolemId::BV_EMPTY:
     case SkolemId::DIV_BY_ZERO:
     case SkolemId::INT_DIV_BY_ZERO:
     case SkolemId::MOD_BY_ZERO:

src/proof/alf/alf_printer.cpp

@@ -201,10 +201,10 @@ bool AlfPrinter::canEvaluate(Node n) const
         case Kind::CONST_INTEGER:
         case Kind::CONST_RATIONAL:
         case Kind::CONST_STRING:
+        case Kind::CONST_BITVECTOR:
         case Kind::ADD:
         case Kind::SUB:
         case Kind::NEG:
-        case Kind::EQUAL:
         case Kind::LT:
         case Kind::GT:
         case Kind::GEQ:
@@ -229,10 +229,21 @@ bool AlfPrinter::canEvaluate(Node n) const
         case Kind::BITVECTOR_ADD:
         case Kind::BITVECTOR_SUB:
         case Kind::BITVECTOR_NEG:
+        case Kind::BITVECTOR_NOT:
         case Kind::BITVECTOR_MULT:
         case Kind::BITVECTOR_AND:
         case Kind::BITVECTOR_OR:
         case Kind::CONST_BITVECTOR_SYMBOLIC: break;
+        case Kind::EQUAL:
+        {
+          TypeNode tn = cur[0].getType();
+          return tn.isBoolean() || tn.isReal() || tn.isInteger()
+                 || tn.isString() || tn.isBitVector();
+        }
+        break;
+        case Kind::BITVECTOR_SIZE:
+          // special case, evaluates no matter what is inside
+          continue;
         default:
           Trace("alf-printer-debug")
               << "Cannot evaluate " << cur.getKind() << std::endl;