(svtv-run-squash-dontcares svtv inalist &key (boolvars 't) (skip 'nil) (quiet 'nil) (simplify 'nil)) → *
Function:
(defun svtv-run-squash-dontcares-fn (svtv inalist boolvars skip quiet simplify) (declare (xargs :guard (svtv-p svtv))) (let ((__function__ 'svtv-run-squash-dontcares)) (declare (ignorable __function__)) (b* (((svtv svtv) svtv) (inalist (ec-call (svex-env-fix$inline inalist))) ((with-fast inalist)) (svtv.inmasks (make-fast-alist svtv.inmasks)) (keys (alist-keys inalist)) (boolmasks (hons-copy (and boolvars (svar-boolmasks-limit-to-bound-vars keys svtv.inmasks)))) (outs (b* (((unless (consp skip)) svtv.outexprs) (outkeys (difference (mergesort (svex-alist-keys svtv.outexprs)) (mergesort skip)))) (fal-extract outkeys svtv.outexprs))) (othervars (svexlist-collect-vars (svex-alist-vals outs))) (othervars-env (pairlis$ othervars (replicate (len othervars) 0))) (othervars-boolmasks (pairlis$ othervars (replicate (len othervars) -1))) (res (mbe :logic (svex-alist-eval-for-symbolic outs (append (svex-env-fix inalist) othervars-env) (cons (cons ':vars (append (alist-keys svtv.inmasks) othervars)) (cons (cons ':boolmasks (append boolmasks othervars-boolmasks)) (cons (cons ':simplify simplify) 'nil)))) :exec (svex-alist-eval outs (append (svex-env-fix inalist) othervars-env))))) (and (not quiet) (progn$ (cw "~%SVTV Inputs:~%") (svtv-print-alist inalist) (cw "~%SVTV Outputs:~%") (svtv-print-alist res) (cw "~%"))) res)))
Theorem:
(defthm svtv-run-squash-dontcares-fn-of-svtv-fix-svtv (equal (svtv-run-squash-dontcares-fn (svtv-fix svtv) inalist boolvars skip quiet simplify) (svtv-run-squash-dontcares-fn svtv inalist boolvars skip quiet simplify)))
Theorem:
(defthm svtv-run-squash-dontcares-fn-svtv-equiv-congruence-on-svtv (implies (svtv-equiv svtv svtv-equiv) (equal (svtv-run-squash-dontcares-fn svtv inalist boolvars skip quiet simplify) (svtv-run-squash-dontcares-fn svtv-equiv inalist boolvars skip quiet simplify))) :rule-classes :congruence)