(fraig-record-sat-ctrex-rec id mark aignet2 sat-lits ipasir ctrex-eval) → (mv new-mark new-ctrex-eval)
Function:
(defun fraig-record-sat-ctrex-rec (id mark aignet2 sat-lits ipasir ctrex-eval) (declare (xargs :stobjs (mark aignet2 sat-lits ipasir ctrex-eval))) (declare (xargs :guard (natp id))) (declare (xargs :guard (and (id-existsp id aignet2) (<= (num-fanins aignet2) (bits-length ctrex-eval)) (<= (num-fanins aignet2) (bits-length mark)) (non-exec (eq (ipasir$a->status ipasir) :sat)) (sat-lits-wfp sat-lits aignet2)))) (let ((__function__ 'fraig-record-sat-ctrex-rec)) (declare (ignorable __function__)) (b* (((when (eql 1 (get-bit id mark))) (mv mark ctrex-eval)) (slot0 (id->slot id 0 aignet2)) (slot1 (id->slot id 1 aignet2)) (type (snode->type slot0)) (regp (snode->regp slot1)) (sat-val (b* ((has-sat-lit (aignet-id-has-sat-var id sat-lits)) ((unless has-sat-lit) nil) (sat-lit (aignet-id->sat-lit id sat-lits))) (ipasir-val ipasir sat-lit)))) (aignet-case type regp :pi (b* (((unless sat-val) (raise "Got to a primary input and had no assigned sat literal value.") (mv mark ctrex-eval)) (ctrex-eval (set-bit id sat-val ctrex-eval)) (mark (set-bit id 1 mark))) (mv mark ctrex-eval)) :reg (b* (((unless sat-val) (raise "Got to a register and had no assigned sat literal value.") (mv mark ctrex-eval)) (ctrex-eval (set-bit id sat-val ctrex-eval)) (mark (set-bit id 1 mark))) (mv mark ctrex-eval)) :co (progn$ (raise "Unexpectedly encountered a PO node") (mv mark ctrex-eval)) :const (mv mark ctrex-eval) :gate (b* ((fanin0 (snode->fanin slot0)) (fanin1 (snode->fanin slot1)) ((mv mark ctrex-eval) (fraig-record-sat-ctrex-rec (lit-id fanin0) mark aignet2 sat-lits ipasir ctrex-eval)) ((mv mark ctrex-eval) (fraig-record-sat-ctrex-rec (lit-id fanin1) mark aignet2 sat-lits ipasir ctrex-eval)) (fanin0-val (aignet-eval-lit fanin0 ctrex-eval)) (fanin1-val (aignet-eval-lit fanin1 ctrex-eval)) (computed-val (if (eql 1 (snode->regp slot1)) (b-xor fanin0-val fanin1-val) (b-and fanin0-val fanin1-val))) (ctrex-eval (set-bit id computed-val ctrex-eval)) (mark (set-bit id 1 mark))) (mbe :logic (mv mark ctrex-eval) :exec (b* (((unless (or (not sat-val) (eql computed-val sat-val))) (raise "Inconsistent values in satisfying assignment") (mv mark ctrex-eval))) (mv mark ctrex-eval))))))))
Theorem:
(defthm mark-length-of-fraig-record-sat-ctrex-rec (b* (((mv ?new-mark ?new-ctrex-eval) (fraig-record-sat-ctrex-rec id mark aignet2 sat-lits ipasir ctrex-eval))) (implies (and (<= (num-fanins aignet2) (len mark)) (<= (nfix id) (fanin-count aignet2))) (equal (len new-mark) (len mark)))))
Theorem:
(defthm eval-length-of-fraig-record-sat-ctrex-rec (b* (((mv ?new-mark ?new-ctrex-eval) (fraig-record-sat-ctrex-rec id mark aignet2 sat-lits ipasir ctrex-eval))) (implies (and (<= (+ 1 (fanin-count aignet2)) (len ctrex-eval)) (<= (nfix id) (fanin-count aignet2))) (equal (len new-ctrex-eval) (len ctrex-eval)))))
Theorem:
(defthm fraig-record-sat-ctrex-rec-of-nfix-id (equal (fraig-record-sat-ctrex-rec (nfix id) mark aignet2 sat-lits ipasir ctrex-eval) (fraig-record-sat-ctrex-rec id mark aignet2 sat-lits ipasir ctrex-eval)))
Theorem:
(defthm fraig-record-sat-ctrex-rec-nat-equiv-congruence-on-id (implies (nat-equiv id id-equiv) (equal (fraig-record-sat-ctrex-rec id mark aignet2 sat-lits ipasir ctrex-eval) (fraig-record-sat-ctrex-rec id-equiv mark aignet2 sat-lits ipasir ctrex-eval))) :rule-classes :congruence)