		Search-engine friendly clone of the ACL2 documentation.

Substrings

Strsuffixp

Case-sensitive string suffix test.

(strsuffixp x y) determines if the string x is a suffix of the string y, in a case-sensitive manner.

Logically, we ask whether |x| < |y|, and whether

(equal (nthcdr (- |y| |x|) (explode x))
       (explode y))

But we use a more efficient implementation that avoids coercing the strings into lists; basically we ask if the last |x| characters of y are equal to x.

Corner case: we regard the empty string as a suffix of every other string. That is, (strsuffixp "" x) is always true.

Definitions and Theorems

Function: strsuffixp$inline

(defun strsuffixp$inline (x y)
  (declare (type string x y))
  (mbe :logic
       (let* ((xchars (explode x))
              (ychars (explode y))
              (xlen (len xchars))
              (ylen (len ychars)))
         (and (<= xlen ylen)
              (equal (nthcdr (- ylen xlen) (explode y))
                     (explode x))))
       :exec
       (let* ((xlen (length x)) (ylen (length y)))
         (and (<= xlen ylen)
              (strprefixp-impl x y 0 (- ylen xlen)
                               xlen ylen)))))

Theorem: strsuffixp-of-empty

(defthm strsuffixp-of-empty
  (strsuffixp "" y))

Theorem: streqv-implies-equal-strsuffixp-1

(defthm streqv-implies-equal-strsuffixp-1
  (implies (streqv x x-equiv)
           (equal (strsuffixp x y)
                  (strsuffixp x-equiv y)))
  :rule-classes (:congruence))

Theorem: streqv-implies-equal-strsuffixp-2

(defthm streqv-implies-equal-strsuffixp-2
  (implies (streqv y y-equiv)
           (equal (strsuffixp x y)
                  (strsuffixp x y-equiv)))
  :rule-classes (:congruence))