(fraig-minimize-sat-ctrex-rec id ctrex-relevant aignet2 ctrex-eval state) → (mv new-ctrex-relevant new-state)
Function:
(defun fraig-minimize-sat-ctrex-rec (id ctrex-relevant aignet2 ctrex-eval state) (declare (xargs :stobjs (ctrex-relevant aignet2 ctrex-eval state))) (declare (xargs :guard (natp id))) (declare (xargs :guard (and (id-existsp id aignet2) (<= (num-fanins aignet2) (bits-length ctrex-eval)) (<= (num-fanins aignet2) (bits-length ctrex-relevant))))) (let ((__function__ 'fraig-minimize-sat-ctrex-rec)) (declare (ignorable __function__)) (b* (((when (eql 1 (get-bit id ctrex-relevant))) (mv ctrex-relevant state)) (ctrex-relevant (set-bit id 1 ctrex-relevant)) (slot0 (id->slot id 0 aignet2)) (slot1 (id->slot id 1 aignet2)) (type (snode->type slot0)) ((unless (eql type (gate-type))) (mv ctrex-relevant state)) (fanin0 (snode->fanin slot0)) (fanin1 (snode->fanin slot1)) ((when (or (eql 1 (snode->regp slot1)) (eql 1 (get-bit id ctrex-eval)))) (b* (((mv ctrex-relevant state) (fraig-minimize-sat-ctrex-rec (lit-id fanin0) ctrex-relevant aignet2 ctrex-eval state))) (fraig-minimize-sat-ctrex-rec (lit-id fanin1) ctrex-relevant aignet2 ctrex-eval state))) ((when (eql 1 (aignet-eval-lit fanin0 ctrex-eval))) (fraig-minimize-sat-ctrex-rec (lit-id fanin1) ctrex-relevant aignet2 ctrex-eval state)) ((when (eql 1 (aignet-eval-lit fanin1 ctrex-eval))) (fraig-minimize-sat-ctrex-rec (lit-id fanin0) ctrex-relevant aignet2 ctrex-eval state)) ((when (or (eql 1 (get-bit (lit-id fanin0) ctrex-relevant)) (eql 1 (get-bit (lit-id fanin1) ctrex-relevant)))) (mv ctrex-relevant state)) ((mv coin state) (random$ 2 state)) ((when (eql coin 0)) (fraig-minimize-sat-ctrex-rec (lit-id fanin0) ctrex-relevant aignet2 ctrex-eval state))) (fraig-minimize-sat-ctrex-rec (lit-id fanin1) ctrex-relevant aignet2 ctrex-eval state))))
Theorem:
(defthm ctrex-relevant-length-of-fraig-minimize-sat-ctrex-rec (b* (((mv ?new-ctrex-relevant ?new-state) (fraig-minimize-sat-ctrex-rec id ctrex-relevant aignet2 ctrex-eval state))) (implies (and (<= (num-fanins aignet2) (len ctrex-relevant)) (<= (nfix id) (fanin-count aignet2))) (equal (len new-ctrex-relevant) (len ctrex-relevant)))))
Theorem:
(defthm w-state-of-fraig-minimize-sat-ctrex-rec (b* (((mv ?new-ctrex-relevant ?new-state) (fraig-minimize-sat-ctrex-rec id ctrex-relevant aignet2 ctrex-eval state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-minimize-sat-ctrex-rec-of-nfix-id (equal (fraig-minimize-sat-ctrex-rec (nfix id) ctrex-relevant aignet2 ctrex-eval state) (fraig-minimize-sat-ctrex-rec id ctrex-relevant aignet2 ctrex-eval state)))
Theorem:
(defthm fraig-minimize-sat-ctrex-rec-nat-equiv-congruence-on-id (implies (nat-equiv id id-equiv) (equal (fraig-minimize-sat-ctrex-rec id ctrex-relevant aignet2 ctrex-eval state) (fraig-minimize-sat-ctrex-rec id-equiv ctrex-relevant aignet2 ctrex-eval state))) :rule-classes :congruence)