		Search-engine friendly clone of the ACL2 documentation.

Observability-fix

Observability-fix-input-copies

Signature
(observability-fix-input-copies lit aignet copy strash aignet2 state) → (mv status new-copy new-strash new-aignet2 new-state)
Arguments: lit — Guard (litp lit).
Returns: status — Type (or (equal status :failed) (equal status :unsat) (equal status :sat)) .

Definitions and Theorems

Function: observability-fix-input-copies

(defun observability-fix-input-copies
       (lit aignet copy strash aignet2 state)
 (declare (xargs :stobjs (aignet copy strash aignet2 state)))
 (declare (xargs :guard (litp lit)))
 (declare
      (xargs :guard (and (fanin-litp lit aignet2)
                         (<= (num-fanins aignet)
                             (lits-length copy))
                         (<= (num-ins aignet) (num-ins aignet2))
                         (<= (num-regs aignet)
                             (num-regs aignet2))
                         (aignet-copies-in-bounds copy aignet2))))
 (let ((__function__ 'observability-fix-input-copies))
   (declare (ignorable __function__))
   (b*
    (((local-stobjs invals regvals inmasks regmasks)
      (mv invals regvals inmasks regmasks
          status copy strash aignet2 state))
     ((mv status
          invals regvals inmasks regmasks state)
      (aignet-lit-ipasir-sat-minimize
           lit invals
           regvals inmasks regmasks aignet2 state))
     (aignet2 (aignet-fix aignet2))
     ((unless (eql status :sat))
      (mv invals regvals inmasks regmasks
          status copy strash aignet2 state))
     ((mv copy strash aignet2)
      (observability-fixed-inputs 0 invals inmasks
                                  lit aignet copy (default-gatesimp)
                                  strash aignet2))
     ((mv copy strash aignet2)
      (observability-fixed-regs 0 regvals regmasks
                                lit aignet copy (default-gatesimp)
                                strash aignet2)))
    (mv invals regvals inmasks regmasks
        status copy strash aignet2 state))))

Theorem: return-type-of-observability-fix-input-copies.status

(defthm return-type-of-observability-fix-input-copies.status
  (b* (((mv ?status ?new-copy
            ?new-strash ?new-aignet2 ?new-state)
        (observability-fix-input-copies
             lit aignet copy strash aignet2 state)))
    (or (equal status :failed)
        (equal status :unsat)
        (equal status :sat)))
  :rule-classes
  ((:forward-chaining
        :trigger-terms
        ((mv-nth 0
                 (observability-fix-input-copies
                      lit
                      aignet copy strash aignet2 state))))))

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

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

Theorem: copy-length-of-observability-fix-input-copies

(defthm copy-length-of-observability-fix-input-copies
  (b* (((mv ?status ?new-copy
            ?new-strash ?new-aignet2 ?new-state)
        (observability-fix-input-copies
             lit aignet copy strash aignet2 state)))
    (implies (<= (num-fanins aignet) (len copy))
             (equal (len new-copy) (len copy)))))

Theorem: aignet-extension-p-of-observability-fix-input-copies

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

Theorem: stypes-preserved-of-observability-fix-input-copies

(defthm stypes-preserved-of-observability-fix-input-copies
  (b* (((mv ?status ?new-copy
            ?new-strash ?new-aignet2 ?new-state)
        (observability-fix-input-copies
             lit 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: non-input-copy-of-observability-fix-input-copies

(defthm non-input-copy-of-observability-fix-input-copies
  (b* (((mv ?status ?new-copy
            ?new-strash ?new-aignet2 ?new-state)
        (observability-fix-input-copies
             lit aignet copy strash aignet2 state)))
    (implies (not (equal (ctype (stype (car (lookup-id id aignet))))
                         (in-ctype)))
             (equal (nth-lit id new-copy)
                    (nth-lit id copy)))))

Theorem: pi-copy-of-observability-fix-input-copies

(defthm pi-copy-of-observability-fix-input-copies
 (b* (((mv ?status ?new-copy
           ?new-strash ?new-aignet2 ?new-state)
       (observability-fix-input-copies
            lit aignet copy strash aignet2 state)))
  (implies
   (and (< (nfix innum) (num-ins aignet))
        (aignet-litp lit aignet2)
        (aignet-copies-in-bounds copy aignet2)
        (<= (num-ins aignet) (num-ins aignet2))
        (equal 1
               (lit-eval lit some-invals some-regvals aignet2)))
   (equal
    (lit-eval (nth-lit (fanin-count (lookup-stype innum :pi aignet))
                       new-copy)
              some-invals some-regvals new-aignet2)
    (lit-eval (nth-lit (fanin-count (lookup-stype innum :pi aignet))
                       copy)
              some-invals some-regvals aignet2)))))

Theorem: reg-copy-of-observability-fix-input-copies

(defthm reg-copy-of-observability-fix-input-copies
 (b* (((mv ?status ?new-copy
           ?new-strash ?new-aignet2 ?new-state)
       (observability-fix-input-copies
            lit aignet copy strash aignet2 state)))
  (implies
   (and (< (nfix regnum) (num-regs aignet))
        (aignet-litp lit aignet2)
        (aignet-copies-in-bounds copy aignet2)
        (<= (num-regs aignet)
            (num-regs aignet2))
        (<= (num-ins aignet) (num-ins aignet2))
        (equal 1
               (lit-eval lit some-invals some-regvals aignet2)))
   (equal
       (lit-eval
            (nth-lit (fanin-count (lookup-stype regnum :reg aignet))
                     new-copy)
            some-invals some-regvals new-aignet2)
       (lit-eval
            (nth-lit (fanin-count (lookup-stype regnum :reg aignet))
                     copy)
            some-invals some-regvals aignet2)))))

Theorem: reg-copy-values-of-observability-fix-input-copies

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

Theorem: input-copy-values-of-observability-fix-input-copies

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

Theorem: observability-fix-input-copies-not-unsat-when-sat

(defthm observability-fix-input-copies-not-unsat-when-sat
  (b* (((mv ?status ?new-copy
            ?new-strash ?new-aignet2 ?new-state)
        (observability-fix-input-copies
             lit aignet copy strash aignet2 state)))
    (implies
         (and (equal (lit-eval lit some-invals some-regvals aignet2)
                     1)
              (aignet-litp lit aignet2))
         (not (equal status :unsat)))))

Theorem: w-state-of-observability-fix-input-copies

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

Theorem: observability-fix-input-copies-of-lit-fix-lit

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

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

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

Theorem: observability-fix-input-copies-of-node-list-fix-aignet

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

Theorem: observability-fix-input-copies-node-list-equiv-congruence-on-aignet

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

Theorem: observability-fix-input-copies-of-node-list-fix-aignet2

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

Theorem: observability-fix-input-copies-node-list-equiv-congruence-on-aignet2

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