• 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
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Aignet

Aignet-simplify-marked-with-tracking

Signature

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

mark — Marks AIG nodes that are to be tracked: they are not necessarily preserved, but we want to know their mappings if they are.

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

lits — Specifies literals to be tracked (again not necessarily preserved), ordered. They will be added as outputs ot 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. This is provided so that users may provide output numbers for these literals as hints to transformations.
    Guard (lit-listp lits).

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.

Definitions and Theorems

Function: aignet-simplify-marked-with-tracking

(defun
 aignet-simplify-marked-with-tracking
 (aignet bitarr mark assum-lits
         lits litarr copy config state)
 (declare (xargs :stobjs (aignet bitarr mark litarr copy state)))
 (declare (xargs :guard (and (lit-listp assum-lits)
                             (lit-listp lits))))
 (declare (xargs :guard (and (<= (bits-length bitarr)
                                 (num-fanins aignet))
                             (<= (bits-length mark)
                                 (num-fanins aignet))
                             (aignet-lit-listp lits 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 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-for-marked-ids 0 mark aignet2))
    (marked-outs (num-outs aignet2))
    (aignet2 (aignet-add-outs lits aignet2))
    ((mv aignet2 state)
     (apply-m-assumption-n-output-transforms!
          assum-outs (- preserved-outs assum-outs)
          aignet2 config state))
    (litarr (resize-lits (num-fanins aignet)
                         litarr))
    (copy (resize-lits (num-fanins aignet) copy))
    (copy
     (aignet-map-outputs-by-lit-list lits marked-outs aignet2 copy))
    (copy (aignet-map-outputs-by-bitarr
               0 preserved-outs aignet2 mark 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))
    (aignet (aignet-raw-copy-fanins-top aignet2 aignet)))
   (mv aignet2 aignet litarr copy state))))

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-state)
              (aignet-simplify-marked-with-tracking
                   aignet bitarr mark assum-lits
                   lits 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-state)
    (aignet-simplify-marked-with-tracking
         aignet bitarr mark assum-lits
         lits 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-state)
      (aignet-simplify-marked-with-tracking
           aignet bitarr mark assum-lits
           lits 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-state)
              (aignet-simplify-marked-with-tracking
                   aignet bitarr mark assum-lits
                   lits 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-state)
              (aignet-simplify-marked-with-tracking
                   aignet bitarr mark assum-lits
                   lits litarr copy config state)))
            (b* ((fanins (+ 1 (fanin-count aignet))))
                (implies (and (<= (len bitarr) fanins)
                              (<= (len mark) fanins)
                              (aignet-lit-listp lits aignet))
                         (equal (len new-copy) fanins)))))

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-state)
          (aignet-simplify-marked-with-tracking
               aignet bitarr mark assum-lits
               lits litarr copy config state)))
        (implies (equal 1 (nth n bitarr))
                 (aignet-litp (nth-lit n new-copy)
                              new-aignet))))

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

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

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

(defthm aignet-litp-of-aignet-simplify-marked-with-tracking-lits
        (b* (((mv ?new-aignet
                  ?new-litarr ?new-copy ?new-state)
              (aignet-simplify-marked-with-tracking
                   aignet bitarr mark assum-lits
                   lits litarr copy config state)))
            (implies (member (nfix n) (lit-list-vars lits))
                     (aignet-litp (nth-lit n new-copy)
                                  new-aignet))))

Theorem: aignet-litp-of-aignet-simplify-marked-with-tracking-assum-lits

(defthm
     aignet-litp-of-aignet-simplify-marked-with-tracking-assum-lits
     (b* (((mv ?new-aignet
               ?new-litarr ?new-copy ?new-state)
           (aignet-simplify-marked-with-tracking
                aignet bitarr mark assum-lits
                lits litarr copy config state)))
         (implies (member (nfix n)
                          (lit-list-vars assum-lits))
                  (aignet-litp (nth-lit n new-litarr)
                               new-aignet))))

Theorem: aignet-litp-of-aignet-simplify-marked-with-tracking-lits-when-originally-0

(defthm
 aignet-litp-of-aignet-simplify-marked-with-tracking-lits-when-originally-0
 (b* (((mv ?new-aignet
           ?new-litarr ?new-copy ?new-state)
       (aignet-simplify-marked-with-tracking
            aignet bitarr mark assum-lits
            lits litarr copy config state)))
     (implies (equal (nth-lit n litarr) 0)
              (aignet-litp (nth-lit n new-litarr)
                           new-aignet))))

Theorem: aignet-litp-of-aignet-simplify-marked-with-tracking-copies-when-originally-0

(defthm
 aignet-litp-of-aignet-simplify-marked-with-tracking-copies-when-originally-0
 (b* (((mv ?new-aignet
           ?new-litarr ?new-copy ?new-state)
       (aignet-simplify-marked-with-tracking
            aignet bitarr mark assum-lits
            lits litarr copy config state)))
     (implies (equal (nth-lit n copy) 0)
              (aignet-litp (nth-lit n new-copy)
                           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-state)
       (aignet-simplify-marked-with-tracking
            aignet bitarr mark assum-lits
            lits litarr copy config state)))
     (implies (nth-lit-equiv copy nil)
              (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-state)
       (aignet-simplify-marked-with-tracking
            aignet bitarr mark assum-lits
            lits litarr copy config state)))
     (implies (nth-lit-equiv litarr nil)
              (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-state)
              (aignet-simplify-marked-with-tracking
                   aignet bitarr mark assum-lits
                   lits litarr copy config state)))
            (equal (w new-state) (w state))))