Mark a subset of inputs and registers that, when assigned the same values
as in the input assignment, produce the same value on the given
(aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state) → (mv new-inmasks new-regmasks new-mark new-state)
Function:
(defun aignet-vals-sat-care-masks-rec (id inmasks regmasks invals regvals vals mark aignet state) (declare (xargs :stobjs (inmasks regmasks invals regvals vals mark aignet state))) (declare (xargs :guard (natp id))) (declare (xargs :guard (and (id-existsp id aignet) (non-exec (equal vals (aignet-record-vals nil invals regvals aignet))) (not (equal (id->type id aignet) (out-type))) (<= (num-ins aignet) (bits-length inmasks)) (<= (num-regs aignet) (bits-length regmasks)) (<= (num-ins aignet) (bits-length invals)) (<= (num-regs aignet) (bits-length regvals)) (< id (bits-length vals)) (< id (bits-length mark))))) (let ((__function__ 'aignet-vals-sat-care-masks-rec)) (declare (ignorable __function__)) (b* (((when (eql 1 (get-bit id mark))) (mv inmasks regmasks mark state)) (mark (set-bit id 1 mark))) (aignet-case (id->type id aignet) :in (if (eql 1 (id->regp id aignet)) (b* ((regmasks (set-bit (ci-id->ionum id aignet) 1 regmasks))) (mv inmasks regmasks mark state)) (b* ((inmasks (set-bit (ci-id->ionum id aignet) 1 inmasks))) (mv inmasks regmasks mark state))) :out (mv inmasks regmasks mark state) :const (mv inmasks regmasks mark state) :gate (b* ((val (mbe :logic (id-eval id invals regvals aignet) :exec (get-bit id vals))) (f0 (gate-id->fanin0 id aignet)) (f1 (gate-id->fanin1 id aignet)) ((when (or (eql val 1) (eql (id->regp id aignet) 1))) (b* (((mv inmasks regmasks mark state) (aignet-vals-sat-care-masks-rec (lit-id f0) inmasks regmasks invals regvals vals mark aignet state))) (aignet-vals-sat-care-masks-rec (lit-id f1) inmasks regmasks invals regvals vals mark aignet state))) ((when (eql (mbe :logic (lit-eval f0 invals regvals aignet) :exec (aignet-eval-lit f0 vals)) 1)) (aignet-vals-sat-care-masks-rec (lit-id f1) inmasks regmasks invals regvals vals mark aignet state)) ((when (eql (mbe :logic (lit-eval f1 invals regvals aignet) :exec (aignet-eval-lit f1 vals)) 1)) (aignet-vals-sat-care-masks-rec (lit-id f0) inmasks regmasks invals regvals vals mark aignet state)) ((when (or (eql 1 (get-bit (lit-id f0) mark)) (eql 1 (get-bit (lit-id f1) mark)))) (mv inmasks regmasks mark state)) ((mv coinflip state) (random$ 2 state))) (if (eql 1 coinflip) (aignet-vals-sat-care-masks-rec (lit-id f1) inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-rec (lit-id f0) inmasks regmasks invals regvals vals mark aignet state)))))))
Theorem:
(defthm aignet-vals-sat-care-masks-normalize-input (implies (syntaxp (not (equal vals ''nil))) (equal (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals nil mark aignet state))))
Theorem:
(defthm aignet-vals-sat-care-masks-preserve-marks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (equal (nth n mark) 1) (equal (nth n new-mark) 1))))
Theorem:
(defthm aignet-vals-sat-care-masks-preserve-inmasks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (equal (nth n inmasks) 1) (equal (nth n new-inmasks) 1))))
Theorem:
(defthm aignet-vals-sat-care-masks-preserve-regmasks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (equal (nth n regmasks) 1) (equal (nth n new-regmasks) 1))))
Theorem:
(defthm inmasks-length-of-aignet-vals-sat-care-masks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (<= (num-ins aignet) (len inmasks)) (equal (len new-inmasks) (len inmasks)))))
Theorem:
(defthm regmasks-length-of-aignet-vals-sat-care-masks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (<= (num-regs aignet) (len regmasks)) (equal (len new-regmasks) (len regmasks)))))
Theorem:
(defthm mark-length-of-aignet-vals-sat-care-masks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (< (nfix id) (len mark)) (equal (len new-mark) (len mark)))))
Function:
(defun aignet-vals-sat-care-masks-mark-ok (node mark invals regvals aignet) (declare (xargs :non-executable t)) (prog2$ (acl2::throw-nonexec-error 'aignet-vals-sat-care-masks-mark-ok (list node mark invals regvals aignet)) (implies (equal (nth node mark) 1) (and (implies (equal (stype (car (lookup-id node aignet))) (and-stype)) (and (implies (equal (id-eval node invals regvals aignet) 1) (and (equal (nth (lit-id (fanin 0 (lookup-id node aignet))) mark) 1) (equal (nth (lit-id (fanin 1 (lookup-id node aignet))) mark) 1))) (implies (and (equal (id-eval node invals regvals aignet) 0) (not (and (equal (lit-eval (fanin 0 (lookup-id node aignet)) invals regvals aignet) 0) (equal (nth (lit-id (fanin 0 (lookup-id node aignet))) mark) 1)))) (and (equal (lit-eval (fanin 1 (lookup-id node aignet)) invals regvals aignet) 0) (equal (nth (lit-id (fanin 1 (lookup-id node aignet))) mark) 1))))) (implies (equal (stype (car (lookup-id node aignet))) (xor-stype)) (and (equal (nth (lit-id (fanin 0 (lookup-id node aignet))) mark) 1) (equal (nth (lit-id (fanin 1 (lookup-id node aignet))) mark) 1)))))))
Theorem:
(defthm aignet-vals-sat-care-masks-mark-invar-necc (implies (aignet-vals-sat-care-masks-mark-invar id mark invals regvals aignet) (implies (<= (nfix node) (nfix id)) (aignet-vals-sat-care-masks-mark-ok node mark invals regvals aignet))))
Theorem:
(defthm aignet-vals-sat-care-masks-mark-invar-rw (implies (and (aignet-vals-sat-care-masks-mark-invar id mark invals regvals aignet) (<= (nfix node) (nfix id)) (equal (nth node mark) 1)) (and (implies (equal (stype (car (lookup-id node aignet))) (and-stype)) (and (implies (equal (id-eval node invals regvals aignet) 1) (and (equal (nth (lit-id (fanin 0 (lookup-id node aignet))) mark) 1) (equal (nth (lit-id (fanin 1 (lookup-id node aignet))) mark) 1))) (implies (and (equal (id-eval node invals regvals aignet) 0) (equal (lit-eval (fanin 0 (lookup-id node aignet)) invals regvals aignet) 1)) (and (equal (lit-eval (fanin 1 (lookup-id node aignet)) invals regvals aignet) 0) (equal (nth (lit-id (fanin 1 (lookup-id node aignet))) mark) 1))) (implies (and (equal (id-eval node invals regvals aignet) 0) (not (equal (nth (lit-id (fanin 0 (lookup-id node aignet))) mark) 1))) (and (equal (lit-eval (fanin 1 (lookup-id node aignet)) invals regvals aignet) 0) (equal (nth (lit-id (fanin 1 (lookup-id node aignet))) mark) 1))) (implies (and (equal (id-eval node invals regvals aignet) 0) (equal (lit-eval (fanin 1 (lookup-id node aignet)) invals regvals aignet) 1)) (and (equal (lit-eval (fanin 0 (lookup-id node aignet)) invals regvals aignet) 0) (equal (nth (lit-id (fanin 0 (lookup-id node aignet))) mark) 1))) (implies (and (equal (id-eval node invals regvals aignet) 0) (not (equal (nth (lit-id (fanin 1 (lookup-id node aignet))) mark) 1))) (and (equal (lit-eval (fanin 0 (lookup-id node aignet)) invals regvals aignet) 0) (equal (nth (lit-id (fanin 0 (lookup-id node aignet))) mark) 1))))) (implies (equal (stype (car (lookup-id node aignet))) (xor-stype)) (and (equal (nth (lit-id (fanin 0 (lookup-id node aignet))) mark) 1) (equal (nth (lit-id (fanin 1 (lookup-id node aignet))) mark) 1))))))
Theorem:
(defthm aignet-vals-sat-care-masks-mark-invar-when-lesser-id (implies (and (aignet-vals-sat-care-masks-mark-invar id mark invals regvals aignet) (<= (nfix id2) (nfix id))) (aignet-vals-sat-care-masks-mark-invar id2 mark invals regvals aignet)))
Theorem:
(defthm aignet-vals-sat-care-masks-mark-invar-of-mark-greater-id (implies (and (aignet-vals-sat-care-masks-mark-invar id mark invals regvals aignet) (< (nfix id) (nfix id2))) (aignet-vals-sat-care-masks-mark-invar id (update-nth id2 1 mark) invals regvals aignet)))
Theorem:
(defthm aignet-vals-sat-care-masks-preserves-marks-above-id (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (< (nfix id) (nfix node)) (equal (nth node new-mark) (nth node mark)))))
Theorem:
(defthm aignet-vals-sat-care-masks-marks-id (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (equal (nth id new-mark) 1)))
Theorem:
(defthm aignet-vals-sat-care-masks-mark-ok-of-update-mark (implies (and (aignet-vals-sat-care-masks-mark-ok node mark invals regvals aignet) (not (equal (nfix id) (nfix node)))) (aignet-vals-sat-care-masks-mark-ok node (update-nth id 1 mark) invals regvals aignet)))
Theorem:
(defthm aignet-vals-sat-care-masks-mark-ok-preserved (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (aignet-vals-sat-care-masks-mark-ok node mark invals regvals aignet) (aignet-vals-sat-care-masks-mark-ok node new-mark invals regvals aignet))))
Theorem:
(defthm aignet-vals-sat-care-masks-mark-invar-preserved (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (aignet-vals-sat-care-masks-mark-invar id mark invals regvals aignet) (aignet-vals-sat-care-masks-mark-invar id new-mark invals regvals aignet))))
Theorem:
(defthm aignet-marked-inputs-are-masked-necc (implies (aignet-marked-inputs-are-masked mark inmasks aignet) (implies (and (< (nfix n) (num-ins aignet)) (equal 1 (nth (fanin-count (lookup-stype n :pi aignet)) mark))) (equal (nth n inmasks) 1))))
Theorem:
(defthm aignet-marked-inputs-are-masked-of-update-non-input (implies (and (aignet-marked-inputs-are-masked mark inmasks aignet) (not (equal (stype (car (lookup-id id aignet))) :pi))) (aignet-marked-inputs-are-masked (update-nth id 1 mark) inmasks aignet)))
Theorem:
(defthm aignet-vals-sat-care-masks-preserves-marked-inputs-masked (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (aignet-marked-inputs-are-masked mark inmasks aignet) (aignet-marked-inputs-are-masked new-mark new-inmasks aignet))))
Theorem:
(defthm aignet-marked-regs-are-masked-necc (implies (aignet-marked-regs-are-masked mark regmasks aignet) (implies (and (< (nfix n) (num-regs aignet)) (equal 1 (nth (fanin-count (lookup-stype n :reg aignet)) mark))) (equal (nth n regmasks) 1))))
Theorem:
(defthm aignet-marked-regs-are-masked-of-update-non-input (implies (and (aignet-marked-regs-are-masked mark regmasks aignet) (not (equal (stype (car (lookup-id id aignet))) :reg))) (aignet-marked-regs-are-masked (update-nth id 1 mark) regmasks aignet)))
Theorem:
(defthm aignet-vals-sat-care-masks-preserves-marked-regs-masked (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (aignet-marked-regs-are-masked mark regmasks aignet) (aignet-marked-regs-are-masked new-mark new-regmasks aignet))))
Theorem:
(defthm vals-equiv-under-masks-necc (implies (vals-equiv-under-masks masks invals1 invals2) (implies (equal (nth n masks) 1) (equal (nth n invals1) (nth n invals2)))))
Theorem:
(defthm aignet-vals-sat-care-masks-rec-invariants-imply-counterexample-holds-under-masks (implies (and (aignet-vals-sat-care-masks-mark-invar max-id mark invals regvals aignet) (aignet-marked-inputs-are-masked mark inmasks aignet) (aignet-marked-regs-are-masked mark regmasks aignet) (vals-equiv-under-masks inmasks invals invals1) (vals-equiv-under-masks regmasks regvals regvals1) (equal (nth id mark) 1) (not (equal (id->type id aignet) (out-type))) (<= (nfix id) (nfix max-id))) (equal (id-eval id invals regvals aignet) (id-eval id invals1 regvals1 aignet))))
Theorem:
(defthm aignet-vals-sat-care-masks-rec-counterexample-under-masks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (and (vals-equiv-under-masks new-inmasks invals invals1) (vals-equiv-under-masks new-regmasks regvals regvals1) (aignet-vals-sat-care-masks-mark-invar id mark invals regvals aignet) (aignet-marked-inputs-are-masked mark inmasks aignet) (aignet-marked-regs-are-masked mark regmasks aignet) (not (equal (id->type id aignet) (out-type)))) (equal (id-eval id invals1 regvals1 aignet) (id-eval id invals regvals aignet)))))
Theorem:
(defthm aignet-vals-sat-care-masks-rec-counterexample-under-masks-lit-eval (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (implies (and (vals-equiv-under-masks new-inmasks invals invals1) (vals-equiv-under-masks new-regmasks regvals regvals1) (aignet-vals-sat-care-masks-mark-invar id mark invals regvals aignet) (aignet-marked-inputs-are-masked mark inmasks aignet) (aignet-marked-regs-are-masked mark regmasks aignet) (not (equal (id->type id aignet) (out-type))) (equal (lit-id x) (nfix id))) (equal (lit-eval x invals1 regvals1 aignet) (lit-eval x invals regvals aignet)))))
Theorem:
(defthm w-state-of-aignet-vals-sat-care-masks-rec (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state))) (equal (w new-state) (w state))))
Theorem:
(defthm aignet-vals-sat-care-masks-rec-of-nfix-id (equal (aignet-vals-sat-care-masks-rec (nfix id) inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state)))
Theorem:
(defthm aignet-vals-sat-care-masks-rec-nat-equiv-congruence-on-id (implies (nat-equiv id id-equiv) (equal (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-rec id-equiv inmasks regmasks invals regvals vals mark aignet state))) :rule-classes :congruence)
Theorem:
(defthm aignet-vals-sat-care-masks-rec-of-node-list-fix-aignet (equal (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark (node-list-fix aignet) state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state)))
Theorem:
(defthm aignet-vals-sat-care-masks-rec-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-rec id inmasks regmasks invals regvals vals mark aignet-equiv state))) :rule-classes :congruence)