• 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
            • Aignet-constprop-sweep
            • Aignet-lit-constprop-init-and-sweep
            • Aignet-lit-constprop
            • Aignet-constprop-sweep-invar
            • Constprop-iter
            • Constprop-once
            • Constprop-core
            • Constprop!
            • Constprop-config
            • Aignet-constprop-stats
          • Apply-m-assumption-n-output-output-transform-default
          • Balance
          • Apply-n-output-comb-transform-default
          • Apply-comb-transform-default
          • 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
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Constprop

Aignet-constprop-sweep

Signature

(aignet-constprop-sweep n constmarks litclasses aignet 
                        constr-lit copy gatesimp strash aignet2) 
 
  → 
(mv new-copy new-constr-lit new-strash new-aignet2)

Arguments

n — Guard (posp n).

constr-lit — Guard (litp constr-lit).

gatesimp — Guard (gatesimp-p gatesimp).

Returns

new-constr-lit — Type (litp new-constr-lit).

Definitions and Theorems

Function: aignet-constprop-sweep

(defun aignet-constprop-sweep
       (n constmarks litclasses aignet
          constr-lit copy gatesimp strash aignet2)
 (declare
   (xargs
        :stobjs (constmarks litclasses aignet copy strash aignet2)))
 (declare (type (unsigned-byte 29) n)
          (type (unsigned-byte 6) gatesimp))
 (declare (xargs :guard (and (posp n)
                             (litp constr-lit)
                             (gatesimp-p gatesimp))))
 (declare
      (xargs :guard (and (<= n (num-fanins aignet))
                         (<= (num-fanins aignet)
                             (bits-length constmarks))
                         (<= (num-fanins aignet)
                             (lits-length litclasses))
                         (<= (num-fanins aignet)
                             (lits-length copy))
                         (equal (num-regs aignet)
                                (num-regs aignet2))
                         (equal (num-ins aignet)
                                (num-ins aignet2))
                         (fanin-litp constr-lit aignet2)
                         (aignet-copies-in-bounds copy aignet2)
                         (ec-call (litclasses-orderedp litclasses)))
             :split-types t))
 (let ((__function__ 'aignet-constprop-sweep))
   (declare (ignorable __function__))
   (b*
    ((n (lposfix n))
     ((when (mbe :logic (zp (- (num-fanins aignet) n))
                 :exec (eql (num-fanins aignet) n)))
      (mbe :logic (non-exec (mv copy (lit-fix constr-lit)
                                strash (node-list-fix aignet2)))
           :exec (mv copy constr-lit strash aignet2)))
     (type (id->type n aignet))
     ((when (eql type (gate-type)))
      (b*
       ((fanin0 (lit-copy (gate-id->fanin0 n aignet)
                          copy))
        (fanin1 (lit-copy (gate-id->fanin1 n aignet)
                          copy))
        ((mv lit strash aignet2)
         (if (eql (id->regp n aignet) 1)
             (aignet-hash-xor fanin0 fanin1 gatesimp strash aignet2)
           (aignet-hash-and fanin0 fanin1 gatesimp strash aignet2)))
        (copy (set-lit n lit copy))
        ((acl2::hintcontext :gate)))
       (aignet-constprop-sweep
            (1+ n)
            constmarks litclasses aignet constr-lit
            copy gatesimp strash aignet2)))
     ((unless (eql type (in-type)))
      (b* ((copy (set-lit n 0 copy))
           ((acl2::hintcontext :const)))
        (aignet-constprop-sweep
             (1+ n)
             constmarks litclasses aignet constr-lit
             copy gatesimp strash aignet2)))
     (norm-lit (id-normal-form n constmarks litclasses))
     (corresp-lit (get-lit n copy))
     ((when (eql (lit->var norm-lit) n))
      (b* ((copy (set-lit n corresp-lit copy))
           ((acl2::hintcontext :no-replace-in)))
        (aignet-constprop-sweep
             (1+ n)
             constmarks litclasses aignet constr-lit
             copy gatesimp strash aignet2)))
     (norm-copy (lit-copy norm-lit copy))
     (copy (set-lit n norm-copy copy))
     ((mv unequal-lit strash aignet2)
      (aignet-hash-xor corresp-lit
                       norm-copy gatesimp strash aignet2))
     ((mv next-constr-lit strash aignet2)
      (aignet-hash-and constr-lit (lit-negate unequal-lit)
                       gatesimp strash aignet2))
     ((acl2::hintcontext :replace-in)))
    (aignet-constprop-sweep (1+ n)
                            constmarks
                            litclasses aignet next-constr-lit
                            copy gatesimp strash aignet2))))

Theorem: litp-of-aignet-constprop-sweep.new-constr-lit

(defthm litp-of-aignet-constprop-sweep.new-constr-lit
  (b*
   (((mv ?new-copy ?new-constr-lit
         ?new-strash ?new-aignet2)
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2)))
   (litp new-constr-lit))
  :rule-classes :rewrite)

Theorem: aignet-extension-p-of-aignet-constprop-sweep

(defthm aignet-extension-p-of-aignet-constprop-sweep
 (aignet-extension-p
  (mv-nth
     3
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2))
  aignet2)
 :rule-classes :rewrite)

Theorem: aignet-constprop-sweep-preserves-copy-length

(defthm aignet-constprop-sweep-preserves-copy-length
  (b*
   (((mv ?new-copy ?new-constr-lit
         ?new-strash ?new-aignet2)
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2)))
   (implies (<= (num-fanins aignet) (len copy))
            (equal (len new-copy) (len copy)))))

Theorem: aignet-constprop-sweep-preserves-copies-in-bounds

(defthm aignet-constprop-sweep-preserves-copies-in-bounds
  (b*
   (((mv ?new-copy ?new-constr-lit
         ?new-strash ?new-aignet2)
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2)))
   (implies (aignet-copies-in-bounds copy aignet2)
            (aignet-copies-in-bounds new-copy new-aignet2))))

Theorem: stype-count-of-aignet-constprop-sweep

(defthm stype-count-of-aignet-constprop-sweep
  (b*
   (((mv ?new-copy ?new-constr-lit
         ?new-strash ?new-aignet2)
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2)))
   (implies (and (not (equal (stype-fix stype) :and))
                 (not (equal (stype-fix stype) :xor)))
            (equal (stype-count stype new-aignet2)
                   (stype-count stype aignet2)))))

Theorem: aignet-litp-constr-lit-of-aignet-constprop-sweep

(defthm aignet-litp-constr-lit-of-aignet-constprop-sweep
  (b*
   (((mv ?new-copy ?new-constr-lit
         ?new-strash ?new-aignet2)
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2)))
   (implies (and (aignet-litp constr-lit aignet2)
                 (aignet-copies-in-bounds copy aignet2))
            (aignet-litp new-constr-lit new-aignet2))))

Theorem: aignet-constprop-sweep-constr-lit-ok-implies-previous

(defthm aignet-constprop-sweep-constr-lit-ok-implies-previous
 (b*
  (((mv ?new-copy ?new-constr-lit
        ?new-strash ?new-aignet2)
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2)))
  (implies (and (equal 0
                       (lit-eval constr-lit invals regvals aignet2))
                (aignet-litp constr-lit aignet2)
                (aignet-copies-in-bounds copy aignet2))
           (equal (lit-eval new-constr-lit
                            invals regvals new-aignet2)
                  0))))

Theorem: aignet-constprop-sweep-invar-when-constr-of-aignet-constprop-sweep

(defthm
 aignet-constprop-sweep-invar-when-constr-of-aignet-constprop-sweep
 (b*
  (((mv ?new-copy ?new-constr-lit
        ?new-strash ?new-aignet2)
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2)))
  (implies (and (equal (lit-eval new-constr-lit
                                 invals regvals new-aignet2)
                       1)
                (aignet-constprop-sweep-invar
                     (pos-fix n)
                     invals regvals aignet copy aignet2)
                (aignet-constprop-sweep-cis-ok
                     invals regvals aignet copy aignet2)
                (aignet-copies-in-bounds copy aignet2)
                (equal (num-ins aignet2)
                       (num-ins aignet))
                (equal (num-regs aignet2)
                       (num-regs aignet)))
           (aignet-constprop-sweep-invar
                (+ 1 (fanin-count aignet))
                invals
                regvals aignet new-copy new-aignet2))))

Theorem: aignet-constprop-sweep-cis-ok-when-constr-of-aignet-constprop-sweep

(defthm
 aignet-constprop-sweep-cis-ok-when-constr-of-aignet-constprop-sweep
 (b*
  (((mv ?new-copy ?new-constr-lit
        ?new-strash ?new-aignet2)
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2)))
  (implies (and (equal (lit-eval new-constr-lit
                                 invals regvals new-aignet2)
                       1)
                (aignet-constprop-sweep-invar
                     (pos-fix n)
                     invals regvals aignet copy aignet2)
                (aignet-constprop-sweep-cis-ok
                     invals regvals aignet copy aignet2)
                (aignet-copies-in-bounds copy aignet2)
                (equal (num-ins aignet2)
                       (num-ins aignet))
                (equal (num-regs aignet2)
                       (num-regs aignet)))
           (aignet-constprop-sweep-cis-ok
                invals
                regvals aignet new-copy new-aignet2))))

Theorem: litclasses-invar-implies-constraint-satisfied-of-aignet-constprop-sweep

(defthm
 litclasses-invar-implies-constraint-satisfied-of-aignet-constprop-sweep
 (b*
  (((mv ?new-copy ?new-constr-lit
        ?new-strash ?new-aignet2)
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2)))
  (implies
       (and (litclasses-invar invals
                              regvals constmarks litclasses aignet)
            (aignet-constprop-sweep-invar
                 (pos-fix n)
                 invals regvals aignet copy aignet2)
            (aignet-constprop-sweep-cis-ok
                 invals regvals aignet copy aignet2)
            (equal (lit-eval constr-lit invals regvals aignet2)
                   1)
            (aignet-litp constr-lit aignet2)
            (aignet-copies-in-bounds copy aignet2)
            (equal (num-ins aignet2)
                   (num-ins aignet))
            (equal (num-regs aignet2)
                   (num-regs aignet)))
       (equal (lit-eval new-constr-lit
                        invals regvals new-aignet2)
              1))))

Theorem: aignet-constprop-sweep-preserves-past-copy-lits

(defthm aignet-constprop-sweep-preserves-past-copy-lits
  (b*
   (((mv ?new-copy ?new-constr-lit
         ?new-strash ?new-aignet2)
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2)))
   (implies (< (nfix m) (pos-fix n))
            (equal (nth-lit m new-copy)
                   (nth-lit m copy)))))

Theorem: aignet-constprop-sweep-of-pos-fix-n

(defthm aignet-constprop-sweep-of-pos-fix-n
 (equal
    (aignet-constprop-sweep (pos-fix n)
                            constmarks litclasses aignet
                            constr-lit copy gatesimp strash aignet2)
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2)))

Theorem: aignet-constprop-sweep-pos-equiv-congruence-on-n

(defthm aignet-constprop-sweep-pos-equiv-congruence-on-n
 (implies
  (pos-equiv n n-equiv)
  (equal
    (aignet-constprop-sweep n constmarks litclasses aignet
                            constr-lit copy gatesimp strash aignet2)
    (aignet-constprop-sweep n-equiv
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2)))
 :rule-classes :congruence)

Theorem: aignet-constprop-sweep-of-node-list-fix-aignet

(defthm aignet-constprop-sweep-of-node-list-fix-aignet
 (equal
    (aignet-constprop-sweep n constmarks
                            litclasses (node-list-fix aignet)
                            constr-lit copy gatesimp strash aignet2)
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2)))

Theorem: aignet-constprop-sweep-node-list-equiv-congruence-on-aignet

(defthm aignet-constprop-sweep-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal
    (aignet-constprop-sweep n constmarks litclasses aignet
                            constr-lit copy gatesimp strash aignet2)
    (aignet-constprop-sweep n constmarks
                            litclasses aignet-equiv constr-lit
                            copy gatesimp strash aignet2)))
 :rule-classes :congruence)

Theorem: aignet-constprop-sweep-of-lit-fix-constr-lit

(defthm aignet-constprop-sweep-of-lit-fix-constr-lit
 (equal
     (aignet-constprop-sweep n constmarks
                             litclasses aignet (lit-fix constr-lit)
                             copy gatesimp strash aignet2)
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2)))

Theorem: aignet-constprop-sweep-lit-equiv-congruence-on-constr-lit

(defthm aignet-constprop-sweep-lit-equiv-congruence-on-constr-lit
 (implies
  (lit-equiv constr-lit constr-lit-equiv)
  (equal
    (aignet-constprop-sweep n constmarks litclasses aignet
                            constr-lit copy gatesimp strash aignet2)
    (aignet-constprop-sweep n constmarks
                            litclasses aignet constr-lit-equiv
                            copy gatesimp strash aignet2)))
 :rule-classes :congruence)

Theorem: aignet-constprop-sweep-of-gatesimp-fix-gatesimp

(defthm aignet-constprop-sweep-of-gatesimp-fix-gatesimp
 (equal
     (aignet-constprop-sweep n constmarks litclasses aignet
                             constr-lit copy (gatesimp-fix gatesimp)
                             strash aignet2)
     (aignet-constprop-sweep n
                             constmarks litclasses aignet constr-lit
                             copy gatesimp strash aignet2)))

Theorem: aignet-constprop-sweep-gatesimp-equiv-congruence-on-gatesimp

(defthm aignet-constprop-sweep-gatesimp-equiv-congruence-on-gatesimp
 (implies
  (gatesimp-equiv gatesimp gatesimp-equiv)
  (equal
    (aignet-constprop-sweep n constmarks litclasses aignet
                            constr-lit copy gatesimp strash aignet2)
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp-equiv strash aignet2)))
 :rule-classes :congruence)

Theorem: aignet-constprop-sweep-of-node-list-fix-aignet2

(defthm aignet-constprop-sweep-of-node-list-fix-aignet2
 (equal
    (aignet-constprop-sweep n constmarks
                            litclasses aignet constr-lit copy
                            gatesimp strash (node-list-fix aignet2))
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2)))

Theorem: aignet-constprop-sweep-node-list-equiv-congruence-on-aignet2

(defthm aignet-constprop-sweep-node-list-equiv-congruence-on-aignet2
 (implies
  (node-list-equiv aignet2 aignet2-equiv)
  (equal
    (aignet-constprop-sweep n constmarks litclasses aignet
                            constr-lit copy gatesimp strash aignet2)
    (aignet-constprop-sweep n
                            constmarks litclasses aignet constr-lit
                            copy gatesimp strash aignet2-equiv)))
 :rule-classes :congruence)