(apply-n-output-comb-transform! n aignet transform state) → (mv new-aignet new-state)
Function:
(defun apply-n-output-comb-transform! (n aignet transform state) (declare (xargs :stobjs (aignet state))) (declare (xargs :guard (natp n))) (declare (xargs :guard (<= n (num-outs aignet)))) (let ((__function__ 'apply-n-output-comb-transform!)) (declare (ignorable __function__)) (mbe :logic (non-exec (apply-n-output-comb-transform n aignet nil transform state)) :exec (b* (((local-stobjs aignet2) (mv aignet aignet2 state)) ((mv aignet2 state) (apply-n-output-comb-transform n aignet aignet2 transform state)) ((mv aignet aignet2) (swap-stobjs aignet aignet2))) (mv aignet aignet2 state)))))