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