Merge branch 'main' of https://github.com/cvc5/cvc5 into arithPfRcons

include/cvc5/cvc5_proof_rule.h

@@ -2786,24 +2786,53 @@ enum ENUM(ProofRewriteRule)
    * \endverbatim
    */
   EVALUE(DT_COLLAPSE_TESTER_SINGLETON),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Datatypes -- Macro constructor equality**
+   *
+   * .. math::
+   *   (t = s) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n)
+   *
+   * where :math:`t_1, \ldots, t_n` and :math:`s_1, \ldots, s_n` are subterms
+   * of :math:`t` and :math:`s` that occur at the same position respectively
+   * (beneath constructor applications), or alternatively
+   *
+   * .. math::
+   *   (t = s) = false
+   * 
+   * where :math:`t` and :math:`s` have subterms that occur in the same
+   * position (beneath constructor applications) that are distinct.
+   *
+   * \endverbatim
+   */
+  EVALUE(MACRO_DT_CONS_EQ),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Datatypes -- constructor equality**
    *
    * .. math::
    *   (c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) =
    *   (t_1 = s_1 \wedge \ldots \wedge t_n = s_n)
+   * 
+   * where :math:`c` is a constructor.
    *
-   * or alternatively
+   * \endverbatim
+   */
+  EVALUE(DT_CONS_EQ),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Datatypes -- constructor equality clash**
    *
    * .. math::
-   *   (c(t_1, \ldots, t_n) = d(s_1, \ldots, s_m)) = false
-   *
-   * where :math:`c` and :math:`d` are distinct constructors.
+   *   (t = s) = false
+   * 
+   * where :math:`t` and :math:`s` have subterms that occur in the same
+   * position (beneath constructor applications) that are distinct constructor
+   * applications.
    *
    * \endverbatim
    */
-  EVALUE(DT_CONS_EQ),
+  EVALUE(DT_CONS_EQ_CLASH),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Datatypes -- cycle**

proofs/eo/cpc/Cpc.eo

@@ -211,11 +211,11 @@
       (($run_evaluate (bvsge xb yb))       (eo::define ((ex ($bv_to_signed_int ($run_evaluate xb))))
                                            (eo::define ((ey ($bv_to_signed_int ($run_evaluate yb))))
                                              (eo::or (eo::gt ex ey) (eo::is_eq ex ey)))))
-      (($run_evaluate (repeat n xb))       ($bv_eval_repeat ($run_evaluate n) ($run_evaluate xb)))
+      (($run_evaluate (repeat n xb))       ($run_evaluate ($bv_unfold_repeat ($run_evaluate n) ($run_evaluate xb))))
       (($run_evaluate (sign_extend n xb))  (eo::define ((ex ($run_evaluate xb)))
-                                              (eo::concat ($bv_eval_repeat ($run_evaluate n) ($bv_sign_bit ex)) ex)))
+                                              (eo::concat ($run_evaluate ($bv_unfold_repeat ($run_evaluate n) ($bv_sign_bit ex))) ex)))
       (($run_evaluate (zero_extend n xb))  (eo::define ((ex ($run_evaluate xb)))
-                                              (eo::concat ($bv_eval_repeat ($run_evaluate n) #b0) ex)))
+                                              (eo::concat ($run_evaluate ($bv_unfold_repeat ($run_evaluate n) #b0)) ex)))
       (($run_evaluate (@bv n m))           (eo::to_bin ($run_evaluate m) ($run_evaluate n)))
       (($run_evaluate (@bvsize x))         ($bv_bitwidth (eo::typeof x)))
 

proofs/eo/cpc/programs/Arith.eo

@@ -106,7 +106,7 @@
 
 ; define: $arith_eval_int_pow_2
 ; args:
-; - x Int: The term to compute whether it is a power of two.
+; - x Int: The term to compute take as the exponent of two.
 ; return: >
 ;   two raised to the power of x. If x is not a numeral value, we return
 ;   the term (int.pow2 x).
@@ -140,3 +140,27 @@
   (eo::ite (eo::is_z x) 
     (eo::ite (eo::is_neg x) false ($arith_eval_int_is_pow_2_rec x))
     (int.ispow2 x)))
+
+
+; define: $arith_unfold_pow_rec
+; args:
+; - n Int: The number of times to multiply, expected to be a non-negative numeral.
+; - a T: The term to muliply.
+; return: The result of multiplying a, n times.
+(program $arith_unfold_pow_rec ((T Type) (n Int) (a T))
+  (Int T) T
+  (
+    (($arith_unfold_pow_rec 0 a)  1)
+    (($arith_unfold_pow_rec n a)  (eo::cons * a ($arith_unfold_pow_rec (eo::add n -1) a)))
+  )
+)
+
+; define: $arith_unfold_pow
+; args:
+; - n Int: The number of times to multiply.
+; - a T: The term to muliply.
+; return: The result of multiplying a, n times. If n is not a positive numeral, this returns (^ a n).
+(define $arith_unfold_pow ((T Type :implicit) (n Int) (a T))
+  (eo::ite (eo::and (eo::is_z n) (eo::not (eo::is_neg n)))
+    ($arith_unfold_pow_rec n a)
+    (^ a n)))

proofs/eo/cpc/programs/BitVectors.eo

@@ -23,29 +23,29 @@
       (eo::add (eo::neg ($arith_eval_int_pow_2 wm1)) z)
       z))))))
 
-; define: $bv_eval_repeat_rec
+; define: $bv_unfold_repeat_rec
 ; args:
 ; - n Int: The number of times to repeat, expected to be a non-negative numeral.
-; - b (BitVec m): The bitvector term, expected to be a binary constant.
-; return: The result of repeating b n times.
-(program $bv_eval_repeat_rec ((m Int) (n Int) (b (BitVec m)))
+; - b (BitVec m): The bitvector term.
+; return: The result of concatenating b n times.
+(program $bv_unfold_repeat_rec ((m Int) (n Int) (b (BitVec m)))
   (Int (BitVec m)) (BitVec (eo::mul n m))
   (
-    (($bv_eval_repeat_rec 0 b)  (eo::to_bin 0 0))
-    (($bv_eval_repeat_rec n b)  (eo::concat b ($bv_eval_repeat_rec (eo::add n -1) b)))
+    (($bv_unfold_repeat_rec 0 b)  (eo::to_bin 0 0))
+    (($bv_unfold_repeat_rec n b)  (eo::cons concat b ($bv_unfold_repeat_rec (eo::add n -1) b)))
   )
 )
 
-; define: $bv_eval_repeat
+; define: $bv_unfold_repeat
 ; args:
 ; - n Int: The number of times to repeat, expected to be a non-negative numeral.
-; - b (BitVec m): The bitvector term, expected to be a binary constant.
+; - b (BitVec m): The bitvector term.
 ; return: >
-;   The result of repeating b n times. If n is not a numeral or is negative,
+;   The result of concatenating b n times. If n is not a numeral or is negative,
 ;   this returns the term (repeat n b).
-(define $bv_eval_repeat ((m Int :implicit) (n Int) (b (BitVec m)))
+(define $bv_unfold_repeat ((m Int :implicit) (n Int) (b (BitVec m)))
   (eo::ite (eo::and (eo::is_z n) (eo::not (eo::is_neg n)))
-    ($bv_eval_repeat_rec n b)
+    ($bv_unfold_repeat_rec n b)
     (repeat n b)))
 
 ; program: $bv_get_first_const_child

proofs/eo/cpc/programs/Datatypes.eo

@@ -0,0 +1,75 @@
+(include "../theories/Datatypes.eo")
+
+; program: $dt_get_constructors
+; args:
+; - T Type: The datatype to get the constructors for.
+; return: The list of constructors of T, as a eo::List.
+; note: >
+;   (Unit) tuples are treated as a special case of datatypes with a single
+;   constructor. Parametric datatypes must reference the type constructor to
+;   extract their constructors.
+(program $dt_get_constructors ((D Type) (T Type) (c T) (T1 Type) (T2 Type :list) (DC (-> Type Type)))
+  (Type) eo::List
+  (
+    (($dt_get_constructors (Tuple T1 T2)) (eo::cons eo::List::cons tuple eo::List::nil))
+    (($dt_get_constructors UnitTuple)     (eo::cons eo::List::cons tuple.unit eo::List::nil))
+    (($dt_get_constructors (DC T))        ($dt_get_constructors DC))   ; user-defined parameteric datatypes, traverse
+    (($dt_get_constructors D)             (eo::dt_constructors D))     ; ordinary user-defined datatypes
+  )
+)
+
+; program: $tuple_get_selectors_rec
+; args:
+; - T Type: The tuple type to get the selectors for.
+; - n Int: The number of component types we have processed so far.
+; return: The list of selectors of T, as a eo::List.
+; note: >
+;   Tuples use a special selector tuple.select indexed by an integer, which is
+;   why they require a special method here.
+(program $tuple_get_selectors_rec ((D Type) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int))
+  (Type Int) Bool
+  (
+    (($tuple_get_selectors_rec UnitTuple n)     eo::List::nil)
+    (($tuple_get_selectors_rec (Tuple T1 T2) n) (eo::cons eo::List::cons (tuple.select n) ($tuple_get_selectors_rec T2 (eo::add n 1))))
+  )
+)
+
+; program: $dt_get_selectors
+; args:
+; - D Type: The type to get the selectors for.
+; - c T: The constructor of D.
+; return: The list of selectors of c, as a eo::List.
+; note: >
+;   (Unit) tuples are treated as a special case of datatypes whose selectors are
+;   tuple.select indexed by an integer, which requires the above method.
+(program $dt_get_selectors ((D Type) (T Type) (c Type) (T1 Type) (T2 Type :list))
+  (Type T) eo::List
+  (
+    (($dt_get_selectors (Tuple T1 T2) tuple)  ($tuple_get_selectors_rec (Tuple T1 T2) 0))
+    (($dt_get_selectors UnitTuple tuple.unit) eo::List::nil)
+    (($dt_get_selectors D c)                  (eo::dt_selectors c)) ; user-defined datatypes
+  )
+)
+
+; define: $dt_is_cons
+; args:
+; - t T: The term in question.
+; return: true iff t is a constructor symbol.
+(define $dt_is_cons ((T Type :implicit) (t T))
+  (eo::is_z (eo::list_len eo::List::cons (eo::dt_selectors t))))
+
+; define: $dt_arg_nth
+; args:
+; - t T: The term to inspect, expected to be a constructor application.
+; - n Int: The index of the argument to get.
+; return: >
+;   The nth argument of t.
+(program $dt_arg_nth ((T Type) (U Type) (V Type) (W Type) (t T) (n Int) (t1 V) (t2 W :list))
+  (T Int) U
+  (
+    ; for tuples, use nth on tuple as an n-ary constructor
+    (($dt_arg_nth (tuple t1 t2) n)  (eo::list_nth tuple (tuple t1 t2) n))
+    ; otherwise we get the argument list
+    (($dt_arg_nth t n)              (eo::list_nth @list ($get_arg_list t) n))
+  )
+)

proofs/eo/cpc/programs/Utils.eo

@@ -21,6 +21,19 @@
 (declare-const @list.nil @List)
 (declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
 
+; program: $get_fun
+; args:
+; - t S: The term to inspect.
+; return: >
+;   The function at the head of the application of t, or t itself if it is not
+;   an application.
+(program $get_fun ((T Type) (S Type) (U Type) (f (-> T S)) (x T) (y S))
+  (S) U
+  (
+    (($get_fun (f x))  ($get_fun f))
+    (($get_fun y)      y)
+  )
+)
 
 ; program: $get_arg_list_rec
 ; args:
@@ -45,8 +58,6 @@
 ;   list if t is not a function application.
 (define $get_arg_list ((T Type :implicit) (t T)) ($get_arg_list_rec t @list.nil))
 
-
-
 ; program: $is_app
 ; args:
 ; - f (-> T U): The function.

proofs/eo/cpc/rules/Arith.eo

@@ -348,3 +348,18 @@
   :args (t)
   :conclusion ($arith_reduction_pred t)
 )
+
+;;;;; ProofRewriteRule::ARITH_POW_ELIM
+
+; rule: arith-pow-elim
+; implements: ProofRewriteRule::ARITH_POW_ELIM
+; args:
+; - eq Bool: The equality to prove with this rule.
+; requires: n is integral, and b is the multiplication of a, n times.
+; conclusion: the equality between a and b.
+(declare-rule arith-pow-elim ((T Type) (a T) (n T) (b T))
+  :args ((= (^ a n) b))
+  :requires (((eo::to_q (eo::to_z n)) (eo::to_q n))
+             (($singleton_elim ($arith_unfold_pow (eo::to_z n) a)) b))
+  :conclusion (= (^ a n) b)
+)

proofs/eo/cpc/rules/Arrays.eo

@@ -21,7 +21,7 @@
 ; conclusion: The index of the store is equal to the selected index.
 (declare-rule arrays_read_over_write_contra ((T Type) (U Type) (i T) (j T) (e U) (a (Array T U)))
   :premises ((not (= (select (store a i e) j) (select a j))))
-  :conclusion (= i j)
+  :conclusion (= j i)
 )
 
 ; rule: arrays_read_over_write_1

proofs/eo/cpc/rules/BitVectors.eo

@@ -1,6 +1,20 @@
 (include "../programs/BitVectors.eo")
 
-; ---------------- ProofRewriteRule::BV_BITWISE_SLICING
+;;;;; ProofRewriteRule::BV_REPEAT_ELIM
+
+; rule: bv-repeat-elim
+; implements: ProofRewriteRule::BV_REPEAT_ELIM
+; args:
+; - eq Bool: The equality to prove with this rule.
+; requires: b is the concatenation of a, n times.
+; conclusion: the equality between a and b.
+(declare-rule bv-repeat-elim ((k1 Int) (k2 Int) (n Int) (a (BitVec k1)) (b (BitVec k2)))
+  :args ((= (repeat n a) b))
+  :requires ((($singleton_elim ($bv_unfold_repeat n a)) b))
+  :conclusion (= (repeat n a) b)
+)
+
+;;;;; ProofRewriteRule::BV_BITWISE_SLICING
 
 ; program: $bv_mk_bitwise_slicing_rec
 ; args:
@@ -84,7 +98,7 @@
   :conclusion (= a b)
 )
 
-; ---------------- ProofRewriteRule::BV_BITBLAST_STEP
+;;;;; ProofRule::BV_BITBLAST_STEP
 
 ; program: $bv_mk_bitblast_step_eq
 ; args: