Filtering...

prove-dollar-tests

books/tools/prove-dollar-tests

Included Books

prove-dollar assert-bang-stobj must-eval-to-t must-fail
other
(in-package "ACL2")
include-book
(include-book "prove-dollar")
include-book
(include-book "std/testing/assert-bang-stobj" :dir :system)
include-book
(include-book "std/testing/must-eval-to-t" :dir :system)
include-book
(include-book "std/testing/must-fail" :dir :system)
must-succeed-pimacro
(defmacro must-succeed-pi
  (form)
  `(local (must-eval-to-t ,FORM)))
must-fail-pimacro
(defmacro must-fail-pi
  (form)
  `(local (must-fail (must-eval-to-t ,FORM))))
other
(must-succeed-pi (prove$ '(equal x x)))
other
(must-succeed-pi (prove$ '(equal (append (append x y) z) (append x y z))
    :instructions '(induct prove prove)))
other
(must-fail-pi (prove$ '(equal (append (append x y) z) (append x y z))
    :instructions '(induct prove)))
other
(must-fail-pi (prove$ '(equal x y) :with-output (:off summary)))
other
(must-fail-pi (prove$ '(equal (append (append x y) x y x y x y x y)
      (append x y x y x y x y x y))
    :time-limit 5/4))
other
(must-fail-pi (prove$ '(equal (append (append x y) x y x y x y x y)
      (append x y x y x y x y x y))
    :step-limit 1000))
other
(must-fail-pi (prove$ '(and (equal (append (append x y) x y x y x y x y)
        (append x y x y x y x y x y))
      (equal (append (append x y) x y x y x)
        (append x y x y x y x y x)))
    :otf-flg t
    :hints '(("Goal" :use ((:theorem (equal x x)))))
    :time-limit 3
    :with-output nil))
first-success-timefunction
(defun first-success-time
  (termlist time-limit state)
  (declare (xargs :mode :program :stobjs state))
  (cond ((endp termlist) (value nil))
    (t (er-let* ((result (prove$ (car termlist) :time-limit time-limit)))
        (cond (result (value (car termlist)))
          (t (first-success-time (cdr termlist) time-limit state)))))))
local
(local (must-eval-to (first-success-time '((equal x y) (equal (append (append x y) x y x y x y x y)
          (append x y x y x y x y x y))
        (equal (append (append x y) z) (append x y z))
        (equal u u))
      2
      state)
    '(equal (append (append x y) z) (append x y z))))
first-success-stepfunction
(defun first-success-step
  (termlist step-limit state)
  (declare (xargs :mode :program :stobjs state))
  (cond ((endp termlist) (value nil))
    (t (er-let* ((result (prove$ (car termlist) :step-limit step-limit)))
        (cond (result (value (car termlist)))
          (t (first-success-step (cdr termlist) step-limit state)))))))
local
(local (must-eval-to (first-success-step '((equal x y) (equal (append (append x y) x y x y x y x y)
          (append x y x y x y x y x y))
        (equal (append (append x y) z) (append x y z))
        (equal u u))
      1000
      state)
    '(equal (append (append x y) z) (append x y z))))
other
(must-succeed-pi (prove$ t))
other
(must-succeed-pi (er-let* ((val (prove$ '(equal x y)))) (value (null val))))
other
(must-fail (prove$ t :hints 17))
other
(must-fail (prove$ '(t)))
other
(must-succeed-pi (prove$ '(let ((w 1))
      (equal (car (cons x y)) x))))
other
(must-succeed-pi (let ((time-limit nil))
    (prove$ '(equal (car (cons x y)) x) :time-limit time-limit)))