• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-with-tracking
      • Aignet-complete-copy
      • Aignet-eval
      • Semantics
      • Aignet-transforms
      • Aignet-simplify-marked
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Aignet

Aignet-complete-copy

Copy an aignet, "normalizing" the order of nodes

Signature

(aignet-complete-copy aignet 
                      &key (gatesimp '(default-gatesimp)) 
                      (aignet2 'aignet2)) 
 
  → 
aignet2

Arguments

gatesimp — Guard (gatesimp-p gatesimp).

Copies aignet into aignet2, in the following order:

• Primary inputs
• Registers
• Gates
• Primary outputs
• Next states

Every node in the original aignet has a copy in aignet2, so no particular pruning is done. However, if strashing or a higher level of simplification is used than was used when constructing the original aignet, there may be fewer nodes.

Definitions and Theorems

Function: aignet-complete-copy-fn

(defun
 aignet-complete-copy-fn
 (aignet gatesimp aignet2)
 (declare (xargs :stobjs (aignet aignet2)))
 (declare (xargs :guard (gatesimp-p gatesimp)))
 (let
  ((__function__ 'aignet-complete-copy))
  (declare (ignorable __function__))
  (b*
   (((local-stobjs copy strash)
     (mv copy strash aignet2)))
   (aignet-complete-copy-aux aignet copy gatesimp strash aignet2))))

Theorem: normalize-aignet-complete-copy

(defthm normalize-aignet-complete-copy
        (implies (syntaxp (equal aignet2 ''nil))
                 (equal (aignet-complete-copy aignet
                                              :gatesimp gatesimp
                                              :aignet2 aignet2)
                        (aignet-complete-copy aignet
                                              :gatesimp gatesimp
                                              :aignet2 nil))))

Theorem: eval-output-of-aignet-complete-copy

(defthm
  eval-output-of-aignet-complete-copy
  (b* ((aignet2 (aignet-complete-copy aignet
                                      :gatesimp gatesimp)))
      (equal (lit-eval (fanin 0 (lookup-stype n (po-stype) aignet2))
                       invals regvals aignet2)
             (lit-eval (fanin 0 (lookup-stype n (po-stype) aignet))
                       invals regvals aignet))))

Theorem: eval-nxst-of-aignet-complete-copy

(defthm eval-nxst-of-aignet-complete-copy
        (b* ((aignet2 (aignet-complete-copy aignet
                                            :gatesimp gatesimp)))
            (equal (lit-eval (lookup-reg->nxst n aignet2)
                             invals regvals aignet2)
                   (lit-eval (lookup-reg->nxst n aignet)
                             invals regvals aignet))))

Theorem: num-outs-of-aignet-complete-copy

(defthm
  num-outs-of-aignet-complete-copy
  (equal (stype-count :po (aignet-complete-copy aignet
                                                :gatesimp gatesimp))
         (stype-count :po aignet)))

Theorem: num-regs-of-aignet-complete-copy

(defthm
 num-regs-of-aignet-complete-copy
 (equal (stype-count :reg (aignet-complete-copy aignet
                                                :gatesimp gatesimp))
        (stype-count :reg aignet)))

Theorem: comb-equiv-of-aignet-complete-copy

(defthm comb-equiv-of-aignet-complete-copy
        (comb-equiv (aignet-complete-copy aignet
                                          :gatesimp gatesimp)
                    aignet))

Theorem: aignet-complete-copy-fn-of-node-list-fix-aignet

(defthm aignet-complete-copy-fn-of-node-list-fix-aignet
        (equal (aignet-complete-copy-fn (node-list-fix aignet)
                                        gatesimp aignet2)
               (aignet-complete-copy-fn aignet gatesimp aignet2)))

Theorem: aignet-complete-copy-fn-node-list-equiv-congruence-on-aignet

(defthm
 aignet-complete-copy-fn-node-list-equiv-congruence-on-aignet
 (implies
    (node-list-equiv aignet aignet-equiv)
    (equal (aignet-complete-copy-fn aignet gatesimp aignet2)
           (aignet-complete-copy-fn aignet-equiv gatesimp aignet2)))
 :rule-classes :congruence)

Theorem: aignet-complete-copy-fn-of-gatesimp-fix-gatesimp

(defthm
     aignet-complete-copy-fn-of-gatesimp-fix-gatesimp
     (equal (aignet-complete-copy-fn aignet (gatesimp-fix gatesimp)
                                     aignet2)
            (aignet-complete-copy-fn aignet gatesimp aignet2)))

Theorem: aignet-complete-copy-fn-gatesimp-equiv-congruence-on-gatesimp

(defthm
 aignet-complete-copy-fn-gatesimp-equiv-congruence-on-gatesimp
 (implies
    (gatesimp-equiv gatesimp gatesimp-equiv)
    (equal (aignet-complete-copy-fn aignet gatesimp aignet2)
           (aignet-complete-copy-fn aignet gatesimp-equiv aignet2)))
 :rule-classes :congruence)

Theorem: aignet-complete-copy-fn-of-node-list-fix-aignet2

(defthm
 aignet-complete-copy-fn-of-node-list-fix-aignet2
 (equal
   (aignet-complete-copy-fn aignet gatesimp (node-list-fix aignet2))
   (aignet-complete-copy-fn aignet gatesimp aignet2)))

Theorem: aignet-complete-copy-fn-node-list-equiv-congruence-on-aignet2

(defthm
 aignet-complete-copy-fn-node-list-equiv-congruence-on-aignet2
 (implies
    (node-list-equiv aignet2 aignet2-equiv)
    (equal (aignet-complete-copy-fn aignet gatesimp aignet2)
           (aignet-complete-copy-fn aignet gatesimp aignet2-equiv)))
 :rule-classes :congruence)