		Search-engine friendly clone of the ACL2 documentation.
Fgl-config
Fgl-config-p

Recognizer for fgl-config structures.
Signature
(fgl-config-p x) → *
Definitions and Theorems

Function: fgl-config-p
(defun fgl-config-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'fgl-config-p))
  (declare (ignorable __function__))
  (and
    (std::prod-consp x)
    (std::prod-consp (std::prod-car x))
    (std::prod-consp (std::prod-car (std::prod-car x)))
    (std::prod-consp (std::prod-cdr (std::prod-car x)))
    (std::prod-consp
         (std::prod-cdr (std::prod-cdr (std::prod-car x))))
    (std::prod-consp (std::prod-cdr x))
    (std::prod-consp (std::prod-car (std::prod-cdr x)))
    (std::prod-consp
         (std::prod-cdr (std::prod-car (std::prod-cdr x))))
    (std::prod-consp (std::prod-cdr (std::prod-cdr x)))
    (std::prod-consp
         (std::prod-cdr (std::prod-cdr (std::prod-cdr x))))
    (b*
     ((trace-rewrites
           (std::prod-car (std::prod-car (std::prod-car x))))
      (reclimit (std::prod-cdr (std::prod-car (std::prod-car x))))
      (make-ites (std::prod-car (std::prod-cdr (std::prod-car x))))
      (?rewrite-rule-table
           (std::prod-car
                (std::prod-cdr (std::prod-cdr (std::prod-car x)))))
      (?branch-merge-rules
           (std::prod-cdr
                (std::prod-cdr (std::prod-cdr (std::prod-car x)))))
      (function-modes
           (std::prod-car (std::prod-car (std::prod-cdr x))))
      (prof-enabledp
           (std::prod-car
                (std::prod-cdr (std::prod-car (std::prod-cdr x)))))
      (?sat-config
           (std::prod-cdr
                (std::prod-cdr (std::prod-car (std::prod-cdr x)))))
      (?sat-config-vacuity
           (std::prod-car (std::prod-cdr (std::prod-cdr x))))
      (toplevel-sat-check
           (std::prod-car
                (std::prod-cdr (std::prod-cdr (std::prod-cdr x)))))
      (skip-vacuity-check
           (std::prod-cdr
                (std::prod-cdr (std::prod-cdr (std::prod-cdr x))))))
     (and (booleanp trace-rewrites)
          (posp reclimit)
          (booleanp make-ites)
          (fgl-function-mode-alist-p function-modes)
          (booleanp prof-enabledp)
          (fgl-toplevel-sat-check-mode-p toplevel-sat-check)
          (booleanp skip-vacuity-check))))))