Elab-mod-wiresearch-next-smartp
- Signature
(elab-mod-wiresearch-next-smartp wire pivotoffset
mininst maxinst smartp elab-mod)
→
*- Arguments
- wire — Guard (natp wire).
- pivotoffset — Guard (natp pivotoffset).
- mininst — Guard (natp mininst).
- maxinst — Guard (natp maxinst).
Definitions and Theorems
Function: elab-mod-wiresearch-next-smartp
(defun elab-mod-wiresearch-next-smartp
(wire pivotoffset
mininst maxinst smartp elab-mod)
(declare (xargs :stobjs (elab-mod)))
(declare (xargs :guard (and (natp wire)
(natp pivotoffset)
(natp mininst)
(natp maxinst))))
(declare
(xargs :guard (and (< (+ 1 mininst) maxinst)
(<= maxinst (elab-mod-ninsts elab-mod)))))
(let ((__function__ 'elab-mod-wiresearch-next-smartp))
(declare (ignorable __function__))
(b* (((when (not smartp)) t)
(dumbpivot (elab-mod-wiresearch-dumbpivot mininst maxinst))
(dumboffset (elab-mod->inst-wireoffset dumbpivot elab-mod)))
(if (< wire pivotoffset)
(<= pivotoffset dumboffset)
(<= dumboffset pivotoffset)))))
