		Search-engine friendly clone of the ACL2 documentation.

Observability-fix

Observability-fix-lit

Signature
(observability-fix-lit lit config aignet copy strash aignet2 state) → (mv new-lit new-copy new-strash new-aignet2 new-aignet new-state)
Arguments: lit — Guard (litp lit).; config — Guard (observability-config-p config).
Returns: new-lit — Type (litp new-lit).

Definitions and Theorems

Function: observability-fix-lit

(defun observability-fix-lit
       (lit config aignet copy strash aignet2 state)
 (declare (xargs :stobjs (aignet copy strash aignet2 state)))
 (declare (xargs :guard (and (litp lit)
                             (observability-config-p config))))
 (declare (xargs :guard (and (fanin-litp lit aignet)
                             (aignet-copies-in-bounds copy aignet2)
                             (<= (num-ins aignet) (num-ins aignet2))
                             (<= (num-regs aignet)
                                 (num-regs aignet2)))))
 (let ((__function__ 'observability-fix-lit))
  (declare (ignorable __function__))
  (b*
   (((mv hyps rest)
     (observability-split-supergate (lit-id lit)
                                    config aignet))
    ((observability-config config))
    ((mv hyp concl aignet)
     (b*
      (((local-stobjs strash)
        (mv strash hyp concl aignet))
       ((mv hyp strash aignet)
        (aignet-build-wide-and hyps config.gatesimp strash aignet))
       ((mv concl strash aignet)
        (aignet-build-wide-and rest config.gatesimp strash aignet)))
      (mv strash hyp concl aignet)))
    (- (cw "Observability input: hyp size ~x0, concl ~x1~%"
           (count-gates-mark (lit-id hyp) aignet)
           (count-gates-mark (lit-id concl)
                             aignet)))
    (copy (resize-lits (num-fanins aignet) copy))
    (copy (aignet-copy-set-ins 0 aignet copy aignet2))
    (copy (aignet-copy-set-regs 0 aignet copy aignet2))
    ((mv conjunction copy strash aignet2 state)
     (observability-fix-hyp/concl
          hyp concl aignet copy
          config.gatesimp strash aignet2 state)))
   (mv (lit-negate-cond conjunction (lit-neg lit))
       copy strash aignet2 aignet state))))

Theorem: litp-of-observability-fix-lit.new-lit

(defthm litp-of-observability-fix-lit.new-lit
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (litp new-lit))
  :rule-classes :rewrite)

Theorem: aignet-extension-p-of-observability-fix-lit-1

(defthm aignet-extension-p-of-observability-fix-lit-1
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (aignet-extension-p new-aignet aignet)))

Theorem: stype-counts-of-observability-fix-lit-1

(defthm stype-counts-of-observability-fix-lit-1
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (implies (and (not (equal (stype-fix stype) (and-stype)))
                  (not (equal (stype-fix stype) (xor-stype))))
             (equal (stype-count stype new-aignet)
                    (stype-count stype aignet)))))

Theorem: aignet-extension-p-of-observability-fix-lit-2

(defthm aignet-extension-p-of-observability-fix-lit-2
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (aignet-extension-p new-aignet2 aignet2)))

Theorem: stype-counts-of-observability-fix-lit-2

(defthm stype-counts-of-observability-fix-lit-2
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (implies (and (not (equal (stype-fix stype) (and-stype)))
                  (not (equal (stype-fix stype) (xor-stype))))
             (equal (stype-count stype new-aignet2)
                    (stype-count stype aignet2)))))

Theorem: copy-length-of-observability-fix-lit

(defthm copy-length-of-observability-fix-lit
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (implies (aignet-litp lit aignet)
             (equal (len new-copy)
                    (num-fanins new-aignet)))))

Theorem: copies-in-bounds-of-observability-fix-lit

(defthm copies-in-bounds-of-observability-fix-lit
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (implies (and (aignet-copies-in-bounds copy aignet2)
                  (aignet-litp lit aignet)
                  (<= (num-ins aignet) (num-ins aignet2))
                  (<= (num-regs aignet)
                      (num-regs aignet2)))
             (and (aignet-copies-in-bounds new-copy new-aignet2)
                  (aignet-litp new-lit new-aignet2)))))

Theorem: eval-of-observability-fix-lit

(defthm eval-of-observability-fix-lit
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (implies (and (aignet-copies-in-bounds copy aignet2)
                  (aignet-litp lit aignet)
                  (<= (num-ins aignet) (num-ins aignet2))
                  (<= (num-regs aignet)
                      (num-regs aignet2)))
             (equal (lit-eval new-lit invals regvals new-aignet2)
                    (lit-eval lit invals regvals aignet)))))

Theorem: w-state-of-observability-fix-lit

(defthm w-state-of-observability-fix-lit
  (b* (((mv ?new-lit ?new-copy ?new-strash
            ?new-aignet2 ?new-aignet ?new-state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))
    (equal (w new-state) (w state))))

Theorem: observability-fix-lit-of-lit-fix-lit

(defthm observability-fix-lit-of-lit-fix-lit
 (equal
     (observability-fix-lit (lit-fix lit)
                            config aignet copy strash aignet2 state)
     (observability-fix-lit lit config
                            aignet copy strash aignet2 state)))

Theorem: observability-fix-lit-lit-equiv-congruence-on-lit

(defthm observability-fix-lit-lit-equiv-congruence-on-lit
 (implies
  (lit-equiv lit lit-equiv)
  (equal
     (observability-fix-lit lit
                            config aignet copy strash aignet2 state)
     (observability-fix-lit lit-equiv config
                            aignet copy strash aignet2 state)))
 :rule-classes :congruence)

Theorem: observability-fix-lit-of-observability-config-fix-config

(defthm observability-fix-lit-of-observability-config-fix-config
 (equal (observability-fix-lit lit (observability-config-fix config)
                               aignet copy strash aignet2 state)
        (observability-fix-lit lit config
                               aignet copy strash aignet2 state)))

Theorem: observability-fix-lit-observability-config-equiv-congruence-on-config

(defthm
 observability-fix-lit-observability-config-equiv-congruence-on-config
 (implies
  (observability-config-equiv config config-equiv)
  (equal
     (observability-fix-lit lit
                            config aignet copy strash aignet2 state)
     (observability-fix-lit lit config-equiv
                            aignet copy strash aignet2 state)))
 :rule-classes :congruence)

Theorem: observability-fix-lit-of-node-list-fix-aignet

(defthm observability-fix-lit-of-node-list-fix-aignet
  (equal (observability-fix-lit lit config (node-list-fix aignet)
                                copy strash aignet2 state)
         (observability-fix-lit lit config
                                aignet copy strash aignet2 state)))

Theorem: observability-fix-lit-node-list-equiv-congruence-on-aignet

(defthm observability-fix-lit-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal
     (observability-fix-lit lit
                            config aignet copy strash aignet2 state)
     (observability-fix-lit lit config aignet-equiv
                            copy strash aignet2 state)))
 :rule-classes :congruence)

Theorem: observability-fix-lit-of-node-list-fix-aignet2

(defthm observability-fix-lit-of-node-list-fix-aignet2
  (equal (observability-fix-lit lit config aignet
                                copy strash (node-list-fix aignet2)
                                state)
         (observability-fix-lit lit config
                                aignet copy strash aignet2 state)))

Theorem: observability-fix-lit-node-list-equiv-congruence-on-aignet2

(defthm observability-fix-lit-node-list-equiv-congruence-on-aignet2
 (implies
  (node-list-equiv aignet2 aignet2-equiv)
  (equal
     (observability-fix-lit lit
                            config aignet copy strash aignet2 state)
     (observability-fix-lit lit config aignet
                            copy strash aignet2-equiv state)))
 :rule-classes :congruence)