• 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
  • Math
  • Testing-utilities

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