• 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

Signature

(aignet-simplify-marked aignet bitarr litarr config state) 
  → 
(mv new-aignet new-litarr 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.

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

config — Combinational transformation config.

Definitions and Theorems

Function: aignet-simplify-marked

(defun aignet-simplify-marked
       (aignet bitarr litarr config state)
       (declare (xargs :stobjs (aignet bitarr litarr state)))
       (declare (xargs :guard (<= (bits-length bitarr)
                                  (num-fanins aignet))))
       (let ((__function__ 'aignet-simplify-marked))
            (declare (ignorable __function__))
            (b* (((local-stobjs mark copy)
                  (mv mark aignet copy litarr state))
                 ((mv aignet copy litarr state)
                  (aignet-simplify-marked-with-tracking
                       aignet bitarr
                       mark nil nil copy litarr config state)))
                (mv mark aignet copy litarr state))))

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

(defthm
  stype-count-of-aignet-simplify-marked
  (b* (((mv ?new-aignet ?new-litarr ?new-state)
        (aignet-simplify-marked aignet bitarr 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-state)
        (aignet-simplify-marked aignet bitarr 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-state)
        (aignet-simplify-marked aignet bitarr 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-litarr-entries

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

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

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

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

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