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-lits lits inmasks regmasks invals regvals vals mark aignet state) → (mv new-inmasks new-regmasks new-mark new-state)
Function:
(defun aignet-vals-sat-care-masks-lits (lits inmasks regmasks invals regvals vals mark aignet state) (declare (xargs :stobjs (inmasks regmasks invals regvals vals mark aignet state))) (declare (xargs :guard (lit-listp lits))) (declare (xargs :guard (and (aignet-lit-listp lits aignet) (non-exec (equal vals (aignet-record-vals nil invals regvals aignet))) (<= (num-ins aignet) (bits-length inmasks)) (<= (num-regs aignet) (bits-length regmasks)) (<= (num-ins aignet) (bits-length invals)) (<= (num-regs aignet) (bits-length regvals)) (< (lits-max-id-val lits) (bits-length vals)) (< (lits-max-id-val lits) (bits-length mark))))) (let ((__function__ 'aignet-vals-sat-care-masks-lits)) (declare (ignorable __function__)) (b* (((when (atom lits)) (mv inmasks regmasks mark state)) ((mv inmasks regmasks mark state) (aignet-vals-sat-care-masks-rec (lit->var (car lits)) inmasks regmasks invals regvals vals mark aignet state))) (aignet-vals-sat-care-masks-lits (cdr lits) inmasks regmasks invals regvals vals mark aignet state))))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-normalize-input (implies (syntaxp (not (equal vals ''nil))) (equal (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals nil mark aignet state))))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-preserve-marks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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-lits-preserve-inmasks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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-lits-preserve-regmasks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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-lits (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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-lits (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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-lits (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state))) (implies (< (lits-max-id-val lits) (len mark)) (equal (len new-mark) (len mark)))))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-preserves-marks-above-id (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state))) (implies (< (lits-max-id-val lits) (nfix node)) (equal (nth node new-mark) (nth node mark)))))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-marks-id (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state))) (implies (member (lit-fix lit) (lit-list-fix lits)) (equal (nth (lit->var lit) new-mark) 1))))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-mark-ok-preserved (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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-lits-mark-invar-preserved (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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-vals-sat-care-masks-lits-preserves-marked-inputs-masked (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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-vals-sat-care-masks-lits-preserves-marked-regs-masked (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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 aignet-vals-sat-care-masks-lits-counterexample-under-masks (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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 (lits-max-id-val lits) mark invals regvals aignet) (aignet-marked-inputs-are-masked mark inmasks aignet) (aignet-marked-regs-are-masked mark regmasks aignet) (member-equal (lit-fix lit) (lit-list-fix lits))) (equal (id-eval (lit->var lit) invals1 regvals1 aignet) (id-eval (lit->var lit) invals regvals aignet)))))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-counterexample-under-masks-lit-eval (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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 (lits-max-id-val lits) mark invals regvals aignet) (aignet-marked-inputs-are-masked mark inmasks aignet) (aignet-marked-regs-are-masked mark regmasks aignet) (member-equal (lit-fix lit) (lit-list-fix lits))) (equal (lit-eval lit invals1 regvals1 aignet) (lit-eval lit invals regvals aignet)))))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-counterexample-under-masks-aignet-eval-conjunction (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits 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 (lits-max-id-val lits) mark invals regvals aignet) (aignet-marked-inputs-are-masked mark inmasks aignet) (aignet-marked-regs-are-masked mark regmasks aignet) (subsetp-equal (lit-list-fix lits1) (lit-list-fix lits))) (equal (aignet-eval-conjunction lits1 invals1 regvals1 aignet) (aignet-eval-conjunction lits1 invals regvals aignet)))))
Theorem:
(defthm w-state-of-aignet-vals-sat-care-masks-lits (b* (((mv ?new-inmasks ?new-regmasks ?new-mark ?new-state) (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state))) (equal (w new-state) (w state))))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-of-lit-list-fix-lits (equal (aignet-vals-sat-care-masks-lits (lit-list-fix lits) inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state)))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-lit-list-equiv-congruence-on-lits (implies (satlink::lit-list-equiv lits lits-equiv) (equal (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-lits lits-equiv inmasks regmasks invals regvals vals mark aignet state))) :rule-classes :congruence)
Theorem:
(defthm aignet-vals-sat-care-masks-lits-of-node-list-fix-aignet (equal (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark (node-list-fix aignet) state) (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state)))
Theorem:
(defthm aignet-vals-sat-care-masks-lits-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet state) (aignet-vals-sat-care-masks-lits lits inmasks regmasks invals regvals vals mark aignet-equiv state))) :rule-classes :congruence)