		Search-engine friendly clone of the ACL2 documentation.

Fraig-config

Fraig-config-p

Recognizer for fraig-config structures.

Signature
(fraig-config-p x) → *

Definitions and Theorems

Function: fraig-config-p

(defun fraig-config-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'fraig-config-p))
  (declare (ignorable __function__))
  (and
   (consp x)
   (eq (car x) :fraig-config)
   (mbe
    :logic
    (and
     (alistp (cdr x))
     (equal
          (strip-cars (cdr x))
          '(initial-sim-words initial-sim-rounds
                              sim-words ipasir-limit
                              ipasir-recycle-count ctrex-queue-limit
                              ctrex-force-resim final-force-resim
                              random-seed-name outs-only
                              miters-only delete-class-on-fail
                              gatesimp level-limit
                              output-types save-candidate-equivs-as
                              remove-candidate-equivs)))
    :exec
    (fty::alist-with-carsp
         (cdr x)
         '(initial-sim-words initial-sim-rounds
                             sim-words ipasir-limit
                             ipasir-recycle-count ctrex-queue-limit
                             ctrex-force-resim final-force-resim
                             random-seed-name outs-only
                             miters-only delete-class-on-fail
                             gatesimp level-limit
                             output-types save-candidate-equivs-as
                             remove-candidate-equivs)))
   (b* ((initial-sim-words (cdr (std::da-nth 0 (cdr x))))
        (initial-sim-rounds (cdr (std::da-nth 1 (cdr x))))
        (sim-words (cdr (std::da-nth 2 (cdr x))))
        (ipasir-limit (cdr (std::da-nth 3 (cdr x))))
        (ipasir-recycle-count (cdr (std::da-nth 4 (cdr x))))
        (ctrex-queue-limit (cdr (std::da-nth 5 (cdr x))))
        (ctrex-force-resim (cdr (std::da-nth 6 (cdr x))))
        (final-force-resim (cdr (std::da-nth 7 (cdr x))))
        (random-seed-name (cdr (std::da-nth 8 (cdr x))))
        (outs-only (cdr (std::da-nth 9 (cdr x))))
        (miters-only (cdr (std::da-nth 10 (cdr x))))
        (delete-class-on-fail (cdr (std::da-nth 11 (cdr x))))
        (gatesimp (cdr (std::da-nth 12 (cdr x))))
        (level-limit (cdr (std::da-nth 13 (cdr x))))
        (output-types (cdr (std::da-nth 14 (cdr x))))
        (save-candidate-equivs-as (cdr (std::da-nth 15 (cdr x))))
        (remove-candidate-equivs (cdr (std::da-nth 16 (cdr x)))))
     (and (posp initial-sim-words)
          (posp initial-sim-rounds)
          (posp sim-words)
          (acl2::maybe-natp ipasir-limit)
          (acl2::maybe-natp ipasir-recycle-count)
          (acl2::maybe-natp ctrex-queue-limit)
          (booleanp ctrex-force-resim)
          (booleanp final-force-resim)
          (symbolp random-seed-name)
          (booleanp outs-only)
          (booleanp miters-only)
          (natp delete-class-on-fail)
          (gatesimp-p gatesimp)
          (natp level-limit)
          (fraig-output-type-map-p output-types)
          (symbolp save-candidate-equivs-as)
          (symbolp remove-candidate-equivs))))))

Theorem: consp-when-fraig-config-p

(defthm consp-when-fraig-config-p
  (implies (fraig-config-p x) (consp x))
  :rule-classes :compound-recognizer)