all-non-gv-exec-ffn-symbs-tests

Included Books

all-non-gv-exec-ffn-symbs assert-equal must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "all-non-gv-exec-ffn-symbs")

include-book

(include-book "std/testing/assert-equal" :dir :system)

include-book

(include-book "std/testing/must-succeed-star" :dir :system)

same-member-equalmacro

(defmacro same-member-equal
  (x y)
  `(let ((x ,X) (y ,Y))
    (and (subsetp-equal x y) (subsetp-equal y x))))

other

(assert-equal (all-non-gv-exec-ffn-symbs 'x (w state)) nil)

other

(assert-equal (all-non-gv-exec-ffn-symbs ''4 (w state)) nil)

other

(assert-equal (all-non-gv-exec-ffn-symbs '(cons x y) (w state))
  nil)

other

(must-succeed* (defun f (x) (declare (xargs :verify-guards nil)) x)
  (defun g (x) (declare (xargs :verify-guards t)) x)
  (assert! (same-member-equal (all-non-gv-exec-ffn-symbs '(cons (f x) (g (f y)))
        (w state))
      '(f))))

other

(must-succeed* (defun mycar
    (x)
    (declare (xargs :verify-guards nil))
    (car x))
  (assert! (same-member-equal (all-non-gv-exec-ffn-symbs '(cons (mycar z) (len y))
        (w state))
      '(mycar)))
  (defun f
    (x)
    (mbe :logic (mycar x)
      :exec (if (consp x)
        (car x)
        nil)))
  (assert-equal (all-non-gv-exec-ffn-symbs (body 'f nil (w state))
      (w state))
    nil))

other

(must-succeed* (defun f (x) (declare (xargs :verify-guards nil)) x)
  (defun g
    (x)
    (declare (xargs :verify-guards t))
    (cons (ec-call (f x)) (len x)))
  (assert-equal (all-non-gv-exec-ffn-symbs (body 'g nil (w state))
      (w state))
    nil))