Records the register values for a satisfying assignment from an ipasir SAT check.
(aignet-get-ipasir-ctrex-regvals n regvals sat-lits aignet ipasir) → new-regvals
Function:
(defun aignet-get-ipasir-ctrex-regvals (n regvals sat-lits aignet ipasir) (declare (xargs :stobjs (regvals sat-lits aignet ipasir))) (declare (xargs :guard (natp n))) (declare (xargs :guard (and (sat-lits-wfp sat-lits aignet) (<= n (num-regs aignet)) (<= (num-regs aignet) (bits-length regvals)) (non-exec (equal (ipasir$a->status ipasir) :sat))))) (let ((__function__ 'aignet-get-ipasir-ctrex-regvals)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (num-regs aignet) (nfix n))) :exec (eql (num-regs aignet) n))) regvals) (id (regnum->id n aignet)) (sat-lit (aignet-id->sat-lit id sat-lits)) ((when (eql 0 sat-lit)) (aignet-get-ipasir-ctrex-regvals (1+ (lnfix n)) regvals sat-lits aignet ipasir)) (val (ipasir-val ipasir sat-lit)) ((unless val) (aignet-get-ipasir-ctrex-regvals (1+ (lnfix n)) regvals sat-lits aignet ipasir)) (regvals (set-bit n val regvals))) (aignet-get-ipasir-ctrex-regvals (1+ (lnfix n)) regvals sat-lits aignet ipasir))))
Theorem:
(defthm regvals-length-of-aignet-get-ipasir-ctrex-regvals (b* ((?new-regvals (aignet-get-ipasir-ctrex-regvals n regvals sat-lits aignet ipasir))) (implies (<= (num-regs aignet) (len regvals)) (equal (len new-regvals) (len regvals)))))
Theorem:
(defthm aignet-get-ipasir-ctrex-regvals-of-nfix-n (equal (aignet-get-ipasir-ctrex-regvals (nfix n) regvals sat-lits aignet ipasir) (aignet-get-ipasir-ctrex-regvals n regvals sat-lits aignet ipasir)))
Theorem:
(defthm aignet-get-ipasir-ctrex-regvals-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (aignet-get-ipasir-ctrex-regvals n regvals sat-lits aignet ipasir) (aignet-get-ipasir-ctrex-regvals n-equiv regvals sat-lits aignet ipasir))) :rule-classes :congruence)
Theorem:
(defthm aignet-get-ipasir-ctrex-regvals-of-node-list-fix-aignet (equal (aignet-get-ipasir-ctrex-regvals n regvals sat-lits (node-list-fix aignet) ipasir) (aignet-get-ipasir-ctrex-regvals n regvals sat-lits aignet ipasir)))
Theorem:
(defthm aignet-get-ipasir-ctrex-regvals-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-get-ipasir-ctrex-regvals n regvals sat-lits aignet ipasir) (aignet-get-ipasir-ctrex-regvals n regvals sat-lits aignet-equiv ipasir))) :rule-classes :congruence)