• 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-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

• Aignet

Aignet-simplify-marked

Signature

(aignet-simplify-marked aignet bitarr litmap litarr config state) 
  → 
(mv new-aignet new-litarr new-litmap new-state)

Arguments

aignet — AIG to be transformed.

bitarr — Marks AIG nodes to be preserved: if bit N is set, node N will be copied.

litmap — Specifies literals to be tracked, each list of literals labeled by a name (symbol). They will be added as outputs to the transformed AIG after the nodes specified by bitarr and mark, i.e. the first literal will be set as the N+Mth output where N is the number of bits set in bitarr and N is the number set in mark. These names can be used in transform configurations as hints. The litmap resulting from the transforms will be returned -- this likely, but not necessarily, preserves the same named fields and the logical function of the literals, depending on the transforms used.
    Guard (named-lit-list-map-p litmap).

litarr — Overwritten with the map from nodes in the old AIG to literals of the new AIG.

config — Combinational transformation config.

Returns

new-litmap — Type (named-lit-list-map-p new-litmap).

Definitions and Theorems

Function: aignet-simplify-marked

(defun aignet-simplify-marked
       (aignet bitarr litmap litarr config state)
 (declare (xargs :stobjs (aignet bitarr litarr state)))
 (declare (xargs :guard (named-lit-list-map-p litmap)))
 (declare
   (xargs
        :guard (and (<= (bits-length bitarr)
                        (num-fanins aignet))
                    (named-lit-list-map-aignet-okp litmap aignet))))
 (let ((__function__ 'aignet-simplify-marked))
   (declare (ignorable __function__))
   (b* (((local-stobjs copy)
         (mv aignet copy litarr litmap state))
        ((mv aignet copy litarr new-litmap state)
         (aignet-simplify-marked-with-tracking
              aignet bitarr
              nil litmap copy litarr config state)))
     (mv aignet copy litarr new-litmap state))))

Theorem: named-lit-list-map-p-of-aignet-simplify-marked.new-litmap

(defthm named-lit-list-map-p-of-aignet-simplify-marked.new-litmap
  (b* (((mv ?new-aignet
            ?new-litarr ?new-litmap ?new-state)
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)))
    (named-lit-list-map-p new-litmap))
  :rule-classes :rewrite)

Theorem: stype-count-of-aignet-simplify-marked

(defthm stype-count-of-aignet-simplify-marked
  (b* (((mv ?new-aignet
            ?new-litarr ?new-litmap ?new-state)
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)))
    (and (equal (stype-count :pi new-aignet)
                (stype-count :pi aignet))
         (equal (stype-count :reg new-aignet)
                (stype-count :reg aignet))
         (equal (stype-count :po new-aignet) 0)
         (equal (stype-count :nxst new-aignet)
                0))))

Theorem: eval-of-aignet-simplify-marked

(defthm eval-of-aignet-simplify-marked
  (b* (((mv ?new-aignet
            ?new-litarr ?new-litmap ?new-state)
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)))
    (implies (and (equal 1 (nth n bitarr))
                  (<= (bits-length bitarr)
                      (num-fanins aignet)))
             (equal (lit-eval (nth-lit n new-litarr)
                              invals regvals new-aignet)
                    (id-eval n invals regvals aignet)))))

Theorem: litarr-length-of-aignet-simplify-marked

(defthm litarr-length-of-aignet-simplify-marked
  (b* (((mv ?new-aignet
            ?new-litarr ?new-litmap ?new-state)
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)))
    (let ((fanins (+ 1 (fanin-count aignet))))
      (implies (<= (len bitarr) fanins)
               (equal (len new-litarr) fanins)))))

Theorem: aignet-litp-of-aignet-simplify-marked-lits

(defthm aignet-litp-of-aignet-simplify-marked-lits
  (b* (((mv ?new-aignet
            ?new-litarr ?new-litmap ?new-state)
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)))
    (aignet-litp (nth-lit n new-litarr)
                 new-aignet)))

Theorem: named-lit-list-map-aignet-okp-of-aignet-simplify-marked

(defthm named-lit-list-map-aignet-okp-of-aignet-simplify-marked
  (b* (((mv ?new-aignet
            ?new-litarr ?new-litmap ?new-state)
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)))
    (named-lit-list-map-aignet-okp new-litmap new-aignet)))

Theorem: w-state-of-aignet-simplify-marked

(defthm w-state-of-aignet-simplify-marked
  (b* (((mv ?new-aignet
            ?new-litarr ?new-litmap ?new-state)
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)))
    (equal (w new-state) (w state))))

Theorem: aignet-simplify-marked-of-node-list-fix-aignet

(defthm aignet-simplify-marked-of-node-list-fix-aignet
 (equal (aignet-simplify-marked (node-list-fix aignet)
                                bitarr litmap litarr config state)
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)))

Theorem: aignet-simplify-marked-node-list-equiv-congruence-on-aignet

(defthm aignet-simplify-marked-node-list-equiv-congruence-on-aignet
 (implies
   (node-list-equiv aignet aignet-equiv)
   (equal
        (aignet-simplify-marked aignet
                                bitarr litmap litarr config state)
        (aignet-simplify-marked aignet-equiv
                                bitarr litmap litarr config state)))
 :rule-classes :congruence)

Theorem: aignet-simplify-marked-of-named-lit-list-map-fix-litmap

(defthm aignet-simplify-marked-of-named-lit-list-map-fix-litmap
 (equal
      (aignet-simplify-marked aignet
                              bitarr (named-lit-list-map-fix litmap)
                              litarr config state)
      (aignet-simplify-marked aignet
                              bitarr litmap litarr config state)))

Theorem: aignet-simplify-marked-named-lit-list-map-equiv-congruence-on-litmap

(defthm
 aignet-simplify-marked-named-lit-list-map-equiv-congruence-on-litmap
 (implies
  (named-lit-list-map-equiv litmap litmap-equiv)
  (equal (aignet-simplify-marked aignet
                                 bitarr litmap litarr config state)
         (aignet-simplify-marked aignet bitarr
                                 litmap-equiv litarr config state)))
 :rule-classes :congruence)