Update alfc version (cvc5#10910)

Updates to version where new evaluation primitives are available.

contrib/get-alf-checker

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

proofs/alf/cvc5/Cvc5.smt3

@@ -33,11 +33,11 @@
       ((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
+                                          (alf.ite (alf.and (alf.is_q ex) (alf.is_q ey)) res
+                                          (alf.ite (alf.and (alf.is_z ex) (alf.is_z ey)) res
+                                          (alf.ite (alf.and (alf.is_bin ex) (alf.is_bin ey)) res
+                                          (alf.ite (alf.and (alf.is_str ex) (alf.is_str ey)) res
+                                          (alf.ite (alf.and (alf.is_bool ex) (alf.is_bool 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)))
@@ -91,7 +91,7 @@
                                           (alf.ite (alf.is_neg en) -1
                                             (let ((ex (run_evaluate x)))
                                             (let ((exl (alf.len ex)))
-                                            (alf.ite ($compare_gt en exl) -1
+                                            (alf.ite (alf.gt en exl) -1
                                               (let ((exs (alf.extract ex n exl)))
                                               (let ((ey (run_evaluate y)))
                                               (let ((r (alf.find (alf.to_str exs) (alf.to_str ey))))

proofs/alf/cvc5/programs/Strings.smt3

@@ -36,7 +36,7 @@
 
 ; Return true if n is a valid code point [0, 196607].
 (define $str_is_code_point ((n Int))
-  (alf.ite ($is_z_literal n)
+  (alf.ite (alf.is_z n)
   (alf.ite ($compare_geq 196608 n)
     (alf.not (alf.is_neg n))
     false)
@@ -126,7 +126,7 @@
 ; Returns true if s is in regular expression r.
 ; Does not evaluate if s is not a string literal.
 (define $str_eval_str_in_re ((s String) (r RegLan))
-  (alf.ite ($is_str_literal s)
+  (alf.ite (alf.is_str s)
     ($str_eval_str_in_re_rec s 0 r @re.null)
     (str.in_re s r)))
 

proofs/alf/cvc5/programs/Utils.smt3

@@ -1,53 +1,10 @@
-; define: $is_bool_literal
-; args:
-; - x T: The term to inspect.
-; return: 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)))
-
-; define: $is_q_literal
-; args:
-; - x T: The term to inspect.
-; return: true if x is a rational literal.
-(define $is_q_literal ((T Type :implicit) (x T))
-  (alf.is_eq (alf.to_q x) x))
-
-; define: $is_z_literal
-; args:
-; - x T: The term to inspect.
-; return: true if x is a numeral literal.
-(define $is_z_literal ((T Type :implicit) (x T))
-  (alf.is_eq (alf.to_z x) x))
-
-; define: $is_bin_literal
-; args:
-; - x T: The term to inspect.
-; return: 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))
-
-; define: $is_str_literal
-; args:
-; - x T: The term to inspect.
-; return: true if x is a string literal.
-(define $is_str_literal ((T Type :implicit) (x T))
-  (alf.is_eq (alf.to_str x) x))
-
-; define: $compare_gt
-; args:
-; - x T: The first term to compare.
-; - y T: The second term to compare.
-; return: true if x > y, where x and y are assumed to be arithmetic values.
-(define $compare_gt ((T Type :implicit) (x T) (y T))
-  (alf.is_neg (alf.add (alf.neg x) y)))
-
 ; define: $compare_geq
 ; args:
 ; - x T: The first term to compare.
 ; - y T: The second term to compare.
 ; return: true if x >= y, where x and y are assumed to be arithmetic values.
 (define $compare_geq ((T Type :implicit) (x T) (y T))
-  (alf.not (alf.is_neg (alf.add (alf.neg y) x))))
+  (alf.ite (alf.is_eq x y) true (alf.gt x y)))
 
 (declare-type @Pair (Type Type))
 (declare-const @pair (-> (! Type :var U :implicit) (! Type :var T :implicit) U T (@Pair U T)))
@@ -70,7 +27,7 @@
 ;   children, where if we ask for the hash of the children in order and prefer
 ;   the ones where this compare returns true, then the term remains unchanged.
 (define $compare_var ((T Type :implicit) (U Type :implicit) (a T) (b U))
-  (alf.is_neg (alf.add (alf.hash b) (alf.neg (alf.hash a)))))
+  (alf.cmp b a))
 
 ; define: $tail
 ; args: