		Search-engine friendly clone of the ACL2 documentation.

Observability-fix

Observability-split-supergate

Signature
(observability-split-supergate id config aignet) → (mv hyps rest)
Arguments: id — Guard (natp id).; config — Guard (observability-config-p config).
Returns: hyps — Type (lit-listp hyps).; rest — Type (lit-listp rest).

Definitions and Theorems

Function: observability-split-supergate

(defun observability-split-supergate (id config aignet)
 (declare (xargs :stobjs (aignet)))
 (declare (xargs :guard (and (natp id)
                             (observability-config-p config))))
 (declare (xargs :guard (and (id-existsp id aignet)
                             (not (equal (id->type id aignet)
                                         (out-type))))))
 (let ((__function__ 'observability-split-supergate))
  (declare (ignorable __function__))
  (b*
   ((full-size (count-gates-mark id aignet))
    ((local-stobjs aignet-refcounts)
     (mv hyps rest aignet-refcounts))
    (aignet-refcounts (resize-u32 (+ 1 (lnfix id))
                                  aignet-refcounts))
    ((mv lits &)
     (lit-collect-supergate (make-lit id 0)
                            t nil 1000 nil aignet-refcounts aignet))
    (- (cw "Observability supergate: ~x0 lits~%"
           (len lits)))
    ((mv hyps rest)
     (observability-split-supergate-aux
          lits config full-size aignet))
    (- (cw "Observability hyp lits: ~x0 concl: ~x1~%"
           (len hyps)
           (len rest))))
   (mv hyps rest aignet-refcounts))))

Theorem: lit-listp-of-observability-split-supergate.hyps

(defthm lit-listp-of-observability-split-supergate.hyps
  (b* (((mv ?hyps common-lisp::?rest)
        (observability-split-supergate id config aignet)))
    (lit-listp hyps))
  :rule-classes :rewrite)

Theorem: lit-listp-of-observability-split-supergate.rest

(defthm lit-listp-of-observability-split-supergate.rest
  (b* (((mv ?hyps common-lisp::?rest)
        (observability-split-supergate id config aignet)))
    (lit-listp rest))
  :rule-classes :rewrite)

Theorem: aignet-lit-listp-of-observability-split-supergate

(defthm aignet-lit-listp-of-observability-split-supergate
 (b* (((mv ?hyps common-lisp::?rest)
       (observability-split-supergate id config aignet)))
   (implies
        (and (aignet-idp id aignet)
             (not (equal (ctype (stype (car (lookup-id id aignet))))
                         :output)))
        (and (aignet-lit-listp hyps aignet)
             (aignet-lit-listp rest aignet)))))

Theorem: eval-of-observability-split-supergate

(defthm eval-of-observability-split-supergate
 (b* (((mv ?hyps common-lisp::?rest)
       (observability-split-supergate id config aignet)))
   (equal
        (b-and (aignet-eval-conjunction hyps invals regvals aignet)
               (aignet-eval-conjunction rest invals regvals aignet))
        (id-eval id invals regvals aignet))))

Theorem: observability-split-supergate-of-nfix-id

(defthm observability-split-supergate-of-nfix-id
  (equal (observability-split-supergate (nfix id)
                                        config aignet)
         (observability-split-supergate id config aignet)))

Theorem: observability-split-supergate-nat-equiv-congruence-on-id

(defthm observability-split-supergate-nat-equiv-congruence-on-id
 (implies
     (nat-equiv id id-equiv)
     (equal (observability-split-supergate id config aignet)
            (observability-split-supergate id-equiv config aignet)))
 :rule-classes :congruence)

Theorem: observability-split-supergate-of-observability-config-fix-config

(defthm
   observability-split-supergate-of-observability-config-fix-config
  (equal (observability-split-supergate
              id (observability-config-fix config)
              aignet)
         (observability-split-supergate id config aignet)))

Theorem: observability-split-supergate-observability-config-equiv-congruence-on-config

(defthm
 observability-split-supergate-observability-config-equiv-congruence-on-config
 (implies
     (observability-config-equiv config config-equiv)
     (equal (observability-split-supergate id config aignet)
            (observability-split-supergate id config-equiv aignet)))
 :rule-classes :congruence)

Theorem: observability-split-supergate-of-node-list-fix-aignet

(defthm observability-split-supergate-of-node-list-fix-aignet
 (equal
    (observability-split-supergate id config (node-list-fix aignet))
    (observability-split-supergate id config aignet)))

Theorem: observability-split-supergate-node-list-equiv-congruence-on-aignet

(defthm
 observability-split-supergate-node-list-equiv-congruence-on-aignet
 (implies
     (node-list-equiv aignet aignet-equiv)
     (equal (observability-split-supergate id config aignet)
            (observability-split-supergate id config aignet-equiv)))
 :rule-classes :congruence)