• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-with-tracking
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-marked
        • Aignet-complete-copy
        • Aignet-transforms
          • Aignet-output-ranges
          • Aignet-comb-transforms
            • Fraig
            • Parametrize
            • Observability-fix
            • Constprop
            • Apply-m-assumption-n-output-output-transform-default
            • Balance
            • Apply-n-output-comb-transform-default
            • Apply-comb-transform-default
            • Obs-constprop
              • Obs-constprop-config
                • Obs-constprop-config-fix
                • Obs-constprop-config-equiv
                • Make-obs-constprop-config
                • Obs-constprop-config->obs-hyp-max-size
                • Obs-constprop-config->obs-concl-min-size
                • Obs-constprop-config->constprop-iterations
                • Obs-constprop-config->obs-min-ratio
                • Obs-constprop-config->gatesimp
                • Change-obs-constprop-config
                • Obs-constprop-config-p
                • Obs-constprop!
              • Rewrite
              • Comb-transform
              • Abc-comb-simplify
              • Prune
              • Rewrite!
              • M-assumption-n-output-comb-transform->name
              • N-output-comb-transform->name
              • Comb-transform->name
              • N-output-comb-transformlist
              • M-assumption-n-output-comb-transformlist
              • Comb-transformlist
              • Apply-comb-transform
            • Aignet-m-assumption-n-output-transforms
            • Aignet-n-output-comb-transforms
          • Aignet-eval
          • Semantics
          • Aignet-read-aiger
          • Aignet-write-aiger
          • Aignet-abc-interface
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Std
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Obs-constprop-config

    Obs-constprop-config-p

    Recognizer for obs-constprop-config structures.

    Signature
    (obs-constprop-config-p x) → *

    Definitions and Theorems

    Function: obs-constprop-config-p

    (defun obs-constprop-config-p (x)
     (declare (xargs :guard t))
     (let ((__function__ 'obs-constprop-config-p))
      (declare (ignorable __function__))
      (and
       (consp x)
       (eq (car x) :obs-constprop-config)
       (mbe :logic
            (and (alistp (cdr x))
                 (equal (strip-cars (cdr x))
                        '(gatesimp constprop-iterations obs-hyp-max-size
                                   obs-concl-min-size obs-min-ratio)))
            :exec (fty::alist-with-carsp
                       (cdr x)
                       '(gatesimp constprop-iterations obs-hyp-max-size
                                  obs-concl-min-size obs-min-ratio)))
       (b* ((gatesimp (cdr (std::da-nth 0 (cdr x))))
            (constprop-iterations (cdr (std::da-nth 1 (cdr x))))
            (obs-hyp-max-size (cdr (std::da-nth 2 (cdr x))))
            (obs-concl-min-size (cdr (std::da-nth 3 (cdr x))))
            (obs-min-ratio (cdr (std::da-nth 4 (cdr x)))))
         (and (gatesimp-p gatesimp)
              (natp constprop-iterations)
              (acl2::maybe-natp obs-hyp-max-size)
              (acl2::maybe-natp obs-concl-min-size)
              (rationalp obs-min-ratio))))))

    Theorem: consp-when-obs-constprop-config-p

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