Merge remote-tracking branch 'upstream/main'

contrib/install-rare-rewrites

@@ -17,11 +17,13 @@ cat << EOF > $REWRITE_SIG
 (include "../theories/Arrays.eo")
 (include "../theories/Arith.eo")
 (include "../theories/Reals.eo")
-(include "../theories/Transcendentals.eo")
 (include "../theories/BitVectors.eo")
 (include "../theories/Strings.eo")
 (include "../theories/Sets.eo")
 
+(include "../expert/theories/Sets.eo")
+(include "../expert/theories/Transcendentals.eo")
+
 EOF
 
 echo "(check-sat)" | $cvc5 -o rare-db --force-logic=ALL --produce-proofs --proof-granularity=dsl-rewrite | sed '$ d' >> $REWRITE_SIG

include/cvc5/cvc5_proof_rule.h

@@ -3029,6 +3029,70 @@ enum ENUM(ProofRewriteRule)
    * \endverbatim
    */
   EVALUE(MACRO_STR_EQ_LEN_UNIFY),
+
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Strings -- Strings overlap split contains**
+   *
+   * .. math::
+   *   \mathit{str.contains}(\mathit{str.++}(t_1, t_2, t_3), s) =
+   *   \mathit{str.contains}(t_1, s) \vee \mathit{str.contains}(t_3, s)
+   *
+   * :math:`t_2` has no forward overlap with :math:`s` and :math:`s` has no
+   * forward overlap with :math:`t_2`. For details see
+   * :math:`\texttt{Word::hasOverlap}` in :cvc5src:`theory/strings/word.h`.
+   * \endverbatim
+   */
+  EVALUE(STR_OVERLAP_SPLIT_CTN),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Strings -- Strings overlap endpoints contains**
+   *
+   * .. math::
+   *   \mathit{str.contains}(\mathit{str.++}(t_1, t_2, t_3), s) =
+   *   \mathit{str.contains}(t_2, s)
+   *
+   * where :math:`s` is `:math:\mathit{str.++}(s_1, s_2, s_3)`,
+   * :math:`t_1` has no forward overlap with :math:`s_1` and
+   * :math:`t_3` has no reverse overlap with :math:`s_3`.
+   * For details see :math:`\texttt{Word::hasOverlap}` in
+   * :cvc5src:`theory/strings/word.h`.
+   *
+   * \endverbatim
+   */
+  EVALUE(STR_OVERLAP_ENDPOINTS_CTN),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Strings -- Strings overlap endpoints indexof**
+   *
+   * .. math::
+   *   \mathit{str.indexof}(\mathit{str.++}(t_1, t_2), s, n) =
+   *   \mathit{str.indexof}(t_1, s, n)
+   *
+   * where :math:`s` is `:math:\mathit{str.++}(s_1, s_2)` and
+   * :math:`t_2` has no reverse overlap with :math:`s_2`.
+   * For details see :math:`\texttt{Word::hasOverlap}` in
+   * :cvc5src:`theory/strings/word.h`.
+   * \endverbatim
+   */
+  EVALUE(STR_OVERLAP_ENDPOINTS_INDEXOF),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Strings -- Strings overlap endpoints replace**
+   *
+   * .. math::
+   *   \mathit{str.replace}(\mathit{str.++}(t_1, t_2, t_3), s, r) =
+   *   \mathit{str.++}(t_1, \mathit{str.replace}(t_2, s, r) t_3)
+   *
+   * where :math:`s` is `:math:\mathit{str.++}(s_1, s_2, s_3)`,
+   * :math:`t_1` has no forward overlap with :math:`s_1` and
+   * :math:`t_3` has no reverse overlap with :math:`s_3`.
+   * For details see :math:`\texttt{Word::hasOverlap}` in
+   * :cvc5src:`theory/strings/word.h`.
+   *
+   * \endverbatim
+   */
+  EVALUE(STR_OVERLAP_ENDPOINTS_REPLACE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Strings -- string indexof regex evaluation**
@@ -3369,6 +3433,22 @@ enum ENUM(ProofRewriteRule)
   EVALUE(ARITH_ABS_INT_GT),
   /** Auto-generated from RARE rule arith-abs-real-gt */
   EVALUE(ARITH_ABS_REAL_GT),
+  /** Auto-generated from RARE rule arith-geq-ite-lift */
+  EVALUE(ARITH_GEQ_ITE_LIFT),
+  /** Auto-generated from RARE rule arith-gt-ite-lift */
+  EVALUE(ARITH_GT_ITE_LIFT),
+  /** Auto-generated from RARE rule arith-leq-ite-lift */
+  EVALUE(ARITH_LEQ_ITE_LIFT),
+  /** Auto-generated from RARE rule arith-lt-ite-lift */
+  EVALUE(ARITH_LT_ITE_LIFT),
+  /** Auto-generated from RARE rule arith-min-lt1 */
+  EVALUE(ARITH_MIN_LT1),
+  /** Auto-generated from RARE rule arith-min-lt2 */
+  EVALUE(ARITH_MIN_LT2),
+  /** Auto-generated from RARE rule arith-max-geq1 */
+  EVALUE(ARITH_MAX_GEQ1),
+  /** Auto-generated from RARE rule arith-max-geq2 */
+  EVALUE(ARITH_MAX_GEQ2),
   /** Auto-generated from RARE rule array-read-over-write */
   EVALUE(ARRAY_READ_OVER_WRITE),
   /** Auto-generated from RARE rule array-read-over-write2 */

proofs/eo/cpc/Cpc.eo

@@ -62,20 +62,18 @@
 (include "./rules/Arrays.eo")
 (include "./rules/Uf.eo")
 (include "./rules/Arith.eo")
-(include "./theories/FloatingPoints.eo")
-(include "./rules/Transcendentals.eo")
 (include "./rules/BitVectors.eo")
 (include "./rules/Strings.eo")
 (include "./rules/Sets.eo")
-(include "./theories/Bags.eo")
-(include "./theories/FiniteFields.eo")
+(include "./rules/ArithBvConv.eo")
 (include "./rules/Quantifiers.eo")
 (include "./rules/Datatypes.eo")
-(include "./theories/SepLogic.eo")
 (include "./rules/Rewrites.eo")
 
 (include "./programs/PolyNorm.eo")
 
+(include "./expert/CpcExpert.eo")
+
 ; disclaimer: >
 ;   All symbols prefixed by @ are not part of the SMT-LIB standard
 ;   and are used to model cvc5's internal symbols, including its skolems,
@@ -90,17 +88,10 @@
 ;   @var is an alias of eo::var to ensure the cpc proof does not use eo::var.
 (define @var ((s String) (T Type)) (eo::var s T))
 
-; disclaimer: this function is not in SMT-LIB.
-(declare-const fmf.card (-> Type Int Bool))
-; disclaimer: this function is not in SMT-LIB.
-(declare-const fmf.combined_card (-> Int Bool))
-(declare-type @ho-elim-sort (Type))
-(declare-const @fmf-fun-sort (-> (! Type :var T :implicit) T Type))
-
 ; program: $run_evaluate
 ; args:
 ; - t S: The term to evaluate.
-; conclusion: The result of evaluating t.
+; return: The result of evaluating t.
 (program $run_evaluate ((T Type) (S Type) 
                        (x T) (y T) (z S) (ys S :list)
                        (b Bool) (n Int) (m Int)
@@ -172,6 +163,8 @@
                                                  (eo::extract ex (eo::add r (eo::len ey)) (eo::len ex)))
                                              )
                                            ))))
+      (($run_evaluate (str.replace_all x y z))
+                                          ($str_eval_replace_all x y z))
       (($run_evaluate (str.prefixof x y)) (eo::define ((ex ($run_evaluate x)))
                                           (eo::define ((ey ($run_evaluate y)))
                                           (eo::define ((r (eo::extract ey 0 (eo::add (eo::len ex) -1))))

proofs/eo/cpc/expert/CpcExpert.eo

@@ -0,0 +1,38 @@
+; =============================================================================
+;
+; This is porition of CPC that is not supported under cvc5's safe options. It
+; should *not* be included in proofs emitted by safe builds of cvc5 or when
+; --safe-options is enabled. All proofs emitted in such cases will never
+; reference any of the symbols or proof rules defined in this subdirectory.
+;
+; Note the theory definitions in this subdirectory are intended to cover *all* of
+; the experimental theory symbols that cvc5 supports. It also may contain proof
+; rules that are supported when experimental features are enabled, or definitions
+; that are works in progress.
+;
+; =============================================================================
+
+(include "./theories/Arith.eo")
+(include "./theories/Bags.eo")
+(include "./theories/FloatingPoints.eo")
+(include "./theories/FiniteFields.eo")
+(include "./theories/SepLogic.eo")
+(include "./rules/Transcendentals.eo")
+(include "./rules/Sets.eo")
+
+; disclaimer: this function is not in SMT-LIB.
+(declare-const fmf.card (-> Type Int Bool))
+; disclaimer: this function is not in SMT-LIB.
+(declare-const fmf.combined_card (-> Int Bool))
+
+; Used in the --ho-elim preprocessing pass
+(declare-type @ho-elim-sort (Type))
+(declare-const @fmf-fun-sort (-> (! Type :var T :implicit) T Type))
+
+; The arrays equal-range predicate.
+; disclaimer: This function is not in SMT-LIB.
+(declare-const eqrange (-> (! Type :var U :implicit) (! Type :var T :implicit) (! Type :var I :implicit)
+                           (Array U T) (Array U T) I I Bool))
+
+; Dataypes shared selector
+(declare-const @shared_selector (-> (! Type :opaque :var D) (! Type :opaque :var T) (! Int :opaque) D T))

proofs/eo/cpc/expert/rules/Sets.eo

@@ -0,0 +1,32 @@
+(include "../theories/Sets.eo")
+
+;;;;; ProofRewriteRule::SETS_FILTER_DOWN
+
+; rule: sets_filter_down
+; implements: ProofRewriteRule::SETS_FILTER_DOWN
+; premises:
+; - mem: A membership of element x into a set filter term.
+; conclusion: >
+;   The membership holds for the set for which we are filtering, and the
+;   predicate is true for x.
+(declare-rule sets_filter_down ((T Type) (P (-> T Bool)) (x T) (S (Set T)))
+  :premises ((set.member x (set.filter P S)))
+  :conclusion (and (set.member x S) (P x))
+)
+
+;;;;; ProofRewriteRule::SETS_FILTER_UP
+
+; rule: sets_filter_up
+; implements: ProofRewriteRule::SETS_FILTER_UP
+; args:
+; - P (-> T Bool): The predicate to filter on.
+; premises:
+; - mem: A membership of element x into a set term.
+; conclusion: >
+;   The membership into the same set, filtered by P, holds if and only if the
+;   predicate is true for x.
+(declare-rule sets_filter_up ((T Type) (P (-> T Bool)) (x T) (S (Set T)))
+  :premises ((set.member x S))
+  :args (P)
+  :conclusion (= (set.member x (set.filter P S)) (P x))
+)

proofs/eo/cpc/rules/Transcendentals.eo → proofs/eo/cpc/expert/rules/Transcendentals.eo

@@ -1,7 +1,8 @@
-(include "../theories/Builtin.eo")
 (include "../theories/Transcendentals.eo")
-(include "../programs/Arith.eo")
-(include "../programs/Utils.eo")
+
+(include "../../theories/Builtin.eo")
+(include "../../programs/Arith.eo")
+(include "../../programs/Utils.eo")
 
 ; Unhandled:
 ; ProofRule::ARITH_TRANS_PI

proofs/eo/cpc/expert/theories/Arith.eo

@@ -0,0 +1,14 @@
+(include "../../theories/Arith.eo")
+
+; The "integer-and" operator, see Zohar et al VMCAI 2022.
+; disclaimer: This function is not in SMT-LIB.
+(declare-const iand (-> Int Int Int Int))
+
+; skolems for virtual term substitution
+(declare-const @arith_vts_delta Real)
+(declare-const @arith_vts_delta_free Real)
+(declare-const @arith_vts_infinity (-> (! Type :var T) T))
+(declare-const @arith_vts_infinity_free (-> (! Type :var T) T))
+
+; used by --nl-cov
+(declare-const @indexed_root_predicate (-> Int Bool Real Bool))

proofs/eo/cpc/theories/Bags.eo → proofs/eo/cpc/expert/theories/Bags.eo

@@ -1,6 +1,6 @@
-(include "../programs/Utils.eo")
-(include "../theories/Builtin.eo")
-(include "../theories/Arith.eo")
+(include "../../programs/Utils.eo")
+(include "../../theories/Builtin.eo")
+(include "../../theories/Arith.eo")
 
 ; disclaimer: >
 ;   This sort is not in the SMT-LIB standard. All further

proofs/eo/cpc/theories/FiniteFields.eo → proofs/eo/cpc/expert/theories/FiniteFields.eo

@@ -1,4 +1,4 @@
-(include "../theories/Arith.eo")
+(include "../../theories/Arith.eo")
 
 ; disclaimer: >
 ;   This sort is not in the SMT-LIB standard. All further function

proofs/eo/cpc/theories/FloatingPoints.eo → proofs/eo/cpc/expert/theories/FloatingPoints.eo

@@ -1,6 +1,6 @@
-(include "../theories/Builtin.eo")
-(include "../theories/Arith.eo")
-(include "../theories/BitVectors.eo")
+(include "../../theories/Builtin.eo")
+(include "../../theories/Arith.eo")
+(include "../../theories/BitVectors.eo")
 
 ; note: We do not currently check whether the indices of this sort are positive.
 (declare-const FloatingPoint

proofs/eo/cpc/expert/theories/Sets.eo

@@ -0,0 +1,46 @@
+(include "../../programs/Utils.eo")
+(include "../../theories/Sets.eo")
+(include "../../theories/Builtin.eo")
+(include "../../theories/Arith.eo")
+(include "../../theories/Datatypes.eo")
+
+; Constants for the theory of sets.
+; note: type rule does not check the type is set.
+(declare-const set.universe (-> (! Type :var T) T))
+
+; Operators for the theory of sets.
+(declare-const set.complement (-> (! Type :var T :implicit) (Set T) (Set T)))
+(declare-const set.card (-> (! Type :var T :implicit) (Set T) Int))
+
+; Higher-order sets operators.
+(declare-const set.filter (-> (! Type :var T :implicit) (-> T Bool) (Set T) (Set T)))
+(declare-const set.all (-> (! Type :var T :implicit) (-> T Bool) (Set T) Bool))
+(declare-const set.some (-> (! Type :var T :implicit) (-> T Bool) (Set T) Bool))
+(declare-const set.map (-> (! Type :var T :implicit) (! Type :var U :implicit) (-> T U) (Set T) (Set U)))
+(declare-const set.fold (-> (! Type :var T :implicit) (! Type :var U :implicit) (-> T U U) U (Set T) U))
+
+; Experimental sets operators.
+(declare-const set.comprehension (-> (! Type :var T :implicit) @List Bool T (Set T)) :binder @list)
+
+; Relation operators.
+(declare-const rel.tclosure (-> (! Type :var T :implicit) (Set (Tuple T T)) (Set (Tuple T T))))
+(declare-const rel.transpose (-> (! Type :var T :implicit) (Set T) (Set ($nary_reverse T))))
+(declare-const rel.product (-> (! Type :var T :implicit) (! Type :var U :implicit) (Set T) (Set U) (Set (eo::list_concat Tuple T U))))
+(declare-const rel.join (-> (! Type :var T :implicit) (! Type :var U :implicit) (Set T) (Set U) (Set ($nary_join Tuple UnitTuple T U))))
+(declare-const rel.group (-> (! Type :var T :implicit) @List (Set T) (Set (Set T))))
+
+; Experimental relation operators.
+(declare-const rel.iden (-> (! Type :var T :implicit) (Set (Tuple T)) (Set (Tuple T T))))
+(declare-const rel.join_image (-> (! Type :var T :implicit) (Set (Tuple T T)) Int (Set (Tuple T))))
+
+; Skolems for the extended theory of sets.
+(declare-const @relations_group_part (-> (! Type :var T :implicit) (! (Set (Set T)) :opaque) T (Set T)))
+(declare-const @relations_group_part_element (-> (! Type :var T :implicit) (! (Set (Set T)) :opaque) (! (Set T) :opaque) T))
+
+; The following skolems are not yet incorporated into the signature:
+;SETS_CHOOSE
+;SETS_FOLD_CARD
+;SETS_FOLD_COMBINE
+;SETS_FOLD_ELEMENTS
+;SETS_FOLD_UNION
+;SETS_MAP_DOWN_ELEMENT

proofs/eo/cpc/theories/Transcendentals.eo → proofs/eo/cpc/expert/theories/Transcendentals.eo

@@ -1,4 +1,4 @@
-(include "../theories/Arith.eo")
+(include "../../theories/Arith.eo")
 
 ; Transcendental-specific operators of arithmetic.
 

proofs/eo/cpc/programs/Nary.eo

@@ -1,4 +1,4 @@
-(include "../programs/Utils.eo")
+(include "../theories/Arith.eo")
 
 ; =============================================
 ;  Right-associative null-terminated operators