Recognizer for fgl-exhaustive-test-config structures.
(fgl-exhaustive-test-config-p x) → *
Function:
(defun fgl-exhaustive-test-config-p (x) (declare (xargs :guard t)) (let ((__function__ 'fgl-exhaustive-test-config-p)) (declare (ignorable __function__)) (and (consp x) (eq (car x) :fgl-exhaustive-test-config) (mbe :logic (and (alistp (cdr x)) (equal (strip-cars (cdr x)) '(ignore-pathcond ignore-constraint transform transform-config-override random-iters))) :exec (fty::alist-with-carsp (cdr x) '(ignore-pathcond ignore-constraint transform transform-config-override random-iters))) (b* ((ignore-pathcond (cdr (std::da-nth 0 (cdr x)))) (ignore-constraint (cdr (std::da-nth 1 (cdr x)))) (transform (cdr (std::da-nth 2 (cdr x)))) (?transform-config-override (cdr (std::da-nth 3 (cdr x)))) (random-iters (cdr (std::da-nth 4 (cdr x))))) (and (booleanp ignore-pathcond) (booleanp ignore-constraint) (booleanp transform) (acl2::maybe-natp random-iters))))))
Theorem:
(defthm consp-when-fgl-exhaustive-test-config-p (implies (fgl-exhaustive-test-config-p x) (consp x)) :rule-classes :compound-recognizer)