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

Signature

(aignet-simplify-marked-with-tracking 
     aignet bitarr assum-lits 
     litmap litarr copy config state) 
 
  → 
(mv new-aignet new-litarr new-copy 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.

assum-lits — Guard (lit-listp assum-lits).

litmap — Specifies literals to be tracked, each list of literals labeled by a name (symbol). 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 assumption nodes in the old AIG to literals of the new AIG.

copy — Overwritten with the map from non-assumption 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-with-tracking

(defun aignet-simplify-marked-with-tracking
       (aignet bitarr assum-lits
               litmap litarr copy config state)
 (declare (xargs :stobjs (aignet bitarr litarr copy state)))
 (declare (xargs :guard (and (lit-listp assum-lits)
                             (named-lit-list-map-p litmap))))
 (declare
    (xargs :guard (and (<= (bits-length bitarr)
                           (num-fanins aignet))
                       (named-lit-list-map-aignet-okp litmap aignet)
                       (aignet-lit-listp assum-lits aignet))))
 (let ((__function__ 'aignet-simplify-marked-with-tracking))
  (declare (ignorable __function__))
  (b*
   (((local-stobjs aignet2)
     (mv aignet2
         aignet litarr copy litmap state))
    (aignet2 (aignet-raw-copy-fanins-top aignet aignet2))
    (aignet2 (aignet-add-outs assum-lits aignet2))
    (assum-outs (num-outs aignet2))
    (aignet2 (aignet-add-outs-for-marked-ids 0 bitarr aignet2))
    (preserved-outs (num-outs aignet2))
    (aignet2 (aignet-add-outs-from-lit-list-map litmap aignet2))
    (outmap (named-lit-list-map-to-output-range-map litmap))
    (outmap (list* (cons nil assum-outs)
                   (cons nil (- preserved-outs assum-outs))
                   outmap))
    ((mv aignet2 res-outmap state)
     (apply-m-assumption-n-output-transforms!
          assum-outs (- preserved-outs assum-outs)
          aignet2 config outmap state))
    (litarr (resize-lits 0 litarr))
    (litarr (resize-lits (num-fanins aignet)
                         litarr))
    (copy (resize-lits 0 copy))
    (copy (resize-lits (num-fanins aignet) copy))
    (copy (aignet-map-outputs-by-bitarr
               0 assum-outs aignet2 bitarr copy))
    (litarr
       (aignet-map-outputs-by-lit-list assum-lits 0 aignet2 litarr))
    (res-litmap
         (output-range-map-to-lit-list-map 0 res-outmap aignet2))
    (aignet (aignet-raw-copy-fanins-top aignet2 aignet)))
   (mv aignet2
       aignet litarr copy res-litmap state))))

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

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

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

(defthm stype-count-of-aignet-simplify-marked-with-tracking
  (b* (((mv ?new-aignet ?new-litarr
            ?new-copy ?new-litmap ?new-state)
        (aignet-simplify-marked-with-tracking
             aignet bitarr assum-lits
             litmap litarr copy 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-with-tracking-when-marked

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

Theorem: eval-of-aignet-simplify-marked-with-tracking-when-assumption

(defthm eval-of-aignet-simplify-marked-with-tracking-when-assumption
  (b* (((mv ?new-aignet ?new-litarr
            ?new-copy ?new-litmap ?new-state)
        (aignet-simplify-marked-with-tracking
             aignet bitarr assum-lits
             litmap litarr copy config state)))
    (implies (and (member-equal (nfix n)
                                (lit-list-vars assum-lits))
                  (no-duplicatesp-equal (lit-list-vars assum-lits)))
             (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-with-tracking

(defthm litarr-length-of-aignet-simplify-marked-with-tracking
  (b* (((mv ?new-aignet ?new-litarr
            ?new-copy ?new-litmap ?new-state)
        (aignet-simplify-marked-with-tracking
             aignet bitarr assum-lits
             litmap litarr copy config state)))
    (b* ((fanins (+ 1 (fanin-count aignet))))
      (implies (and (aignet-lit-listp assum-lits aignet))
               (equal (len new-litarr) fanins)))))

Theorem: copy-length-of-aignet-simplify-marked-with-tracking

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

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

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

Theorem: aignet-litp-of-aignet-simplify-marked-with-tracking-copy-entries

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

Theorem: aignet-litp-of-aignet-simplify-marked-with-tracking-litarr-entries

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

Theorem: aignet-copies-in-bounds-of-aignet-simplify-marked-with-tracking-copies

(defthm
 aignet-copies-in-bounds-of-aignet-simplify-marked-with-tracking-copies
 (b* (((mv ?new-aignet ?new-litarr
           ?new-copy ?new-litmap ?new-state)
       (aignet-simplify-marked-with-tracking
            aignet bitarr assum-lits
            litmap litarr copy config state)))
   (aignet-copies-in-bounds new-copy new-aignet)))

Theorem: aignet-copies-in-bounds-of-aignet-simplify-marked-with-tracking-litarr

(defthm
 aignet-copies-in-bounds-of-aignet-simplify-marked-with-tracking-litarr
 (b* (((mv ?new-aignet ?new-litarr
           ?new-copy ?new-litmap ?new-state)
       (aignet-simplify-marked-with-tracking
            aignet bitarr assum-lits
            litmap litarr copy config state)))
   (aignet-copies-in-bounds new-litarr new-aignet)))

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

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

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

(defthm aignet-simplify-marked-with-tracking-of-node-list-fix-aignet
  (equal (aignet-simplify-marked-with-tracking
              (node-list-fix aignet)
              bitarr assum-lits
              litmap litarr copy config state)
         (aignet-simplify-marked-with-tracking
              aignet bitarr assum-lits
              litmap litarr copy config state)))

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

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

Theorem: aignet-simplify-marked-with-tracking-of-lit-list-fix-assum-lits

(defthm
    aignet-simplify-marked-with-tracking-of-lit-list-fix-assum-lits
  (equal (aignet-simplify-marked-with-tracking
              aignet bitarr (lit-list-fix assum-lits)
              litmap litarr copy config state)
         (aignet-simplify-marked-with-tracking
              aignet bitarr assum-lits
              litmap litarr copy config state)))

Theorem: aignet-simplify-marked-with-tracking-lit-list-equiv-congruence-on-assum-lits

(defthm
 aignet-simplify-marked-with-tracking-lit-list-equiv-congruence-on-assum-lits
 (implies (satlink::lit-list-equiv assum-lits assum-lits-equiv)
          (equal (aignet-simplify-marked-with-tracking
                      aignet bitarr assum-lits
                      litmap litarr copy config state)
                 (aignet-simplify-marked-with-tracking
                      aignet bitarr assum-lits-equiv
                      litmap litarr copy config state)))
 :rule-classes :congruence)

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

(defthm
 aignet-simplify-marked-with-tracking-of-named-lit-list-map-fix-litmap
 (equal (aignet-simplify-marked-with-tracking
             aignet bitarr assum-lits
             (named-lit-list-map-fix litmap)
             litarr copy config state)
        (aignet-simplify-marked-with-tracking
             aignet bitarr assum-lits
             litmap litarr copy config state)))

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

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