(aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state) → (mv new-aignet new-assum-lits new-pres-lits new-track-lits new-state)
Function:
(defun aignet-simplify-with-tracking (aignet assum-lits pres-lits track-lits config state) (declare (xargs :stobjs (aignet state))) (declare (xargs :guard (and (lit-listp assum-lits) (lit-listp pres-lits) (lit-listp track-lits)))) (declare (xargs :guard (and (aignet-lit-listp assum-lits aignet) (aignet-lit-listp pres-lits aignet) (aignet-lit-listp track-lits aignet)))) (let ((__function__ 'aignet-simplify-with-tracking)) (declare (ignorable __function__)) (b* (((local-stobjs aignet2) (mv aignet2 aignet new-assum-lits new-pres-lits new-track-lits state)) (aignet2 (aignet-raw-copy-fanins-top aignet aignet2)) (aignet2 (aignet-add-outs assum-lits aignet2)) (assum-outs (num-outs aignet2)) (aignet2 (aignet-add-outs pres-lits aignet2)) (preserved-outs (num-outs aignet2)) (aignet2 (aignet-add-outs track-lits aignet2)) (tracked-outs (num-outs aignet2)) ((mv aignet2 state) (apply-m-assumption-n-output-transforms! assum-outs (- preserved-outs assum-outs) aignet2 config state)) (lits (aignet-output-lits 0 aignet2)) (new-assum-lits (take assum-outs lits)) (new-pres-lits (take (- preserved-outs assum-outs) (nthcdr assum-outs lits))) (new-track-lits (take (- tracked-outs preserved-outs) (nthcdr preserved-outs lits))) (aignet (aignet-raw-copy-fanins-top aignet2 aignet))) (mv aignet2 aignet new-assum-lits new-pres-lits new-track-lits state))))
Theorem:
(defthm lit-listp-of-aignet-simplify-with-tracking.new-assum-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (lit-listp new-assum-lits)) :rule-classes :rewrite)
Theorem:
(defthm lit-listp-of-aignet-simplify-with-tracking.new-pres-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (lit-listp new-pres-lits)) :rule-classes :rewrite)
Theorem:
(defthm lit-listp-of-aignet-simplify-with-tracking.new-track-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (lit-listp new-track-lits)) :rule-classes :rewrite)
Theorem:
(defthm stype-count-of-aignet-simplify-with-tracking (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (and (equal (stype-count :pi new-aignet) (stype-count :pi aignet)) (equal (stype-count :reg new-aignet) (stype-count :reg aignet)) (equal (stype-count :po new-aignet) 0) (equal (stype-count :nxst new-aignet) 0))))
Theorem:
(defthm eval-of-aignet-simplify-with-tracking-when-preserved (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (implies (and (aignet-lit-listp pres-lits aignet) (equal (aignet-eval-conjunction assum-lits invals regvals aignet) 1)) (equal (lit-eval (nth n new-pres-lits) invals regvals new-aignet) (lit-eval (nth n pres-lits) invals regvals aignet)))))
Theorem:
(defthm eval-of-aignet-simplify-with-tracking-when-assumption (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (implies (aignet-lit-listp assum-lits aignet) (equal (lit-eval (nth n new-assum-lits) invals regvals new-aignet) (lit-eval (nth n assum-lits) invals regvals aignet)))))
Theorem:
(defthm aignet-lit-listp-of-aignet-simplify-with-tracking-pres-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (implies (aignet-lit-listp pres-lits aignet) (aignet-lit-listp new-pres-lits new-aignet))))
Theorem:
(defthm aignet-lit-listp-of-aignet-simplify-with-tracking-assum-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (implies (aignet-lit-listp assum-lits aignet) (aignet-lit-listp new-assum-lits new-aignet))))
Theorem:
(defthm aignet-lit-listp-of-aignet-simplify-with-tracking-track-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (implies (aignet-lit-listp track-lits aignet) (aignet-lit-listp new-track-lits new-aignet))))
Theorem:
(defthm len-of-aignet-simplify-with-tracking-pres-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (equal (len new-pres-lits) (len pres-lits))))
Theorem:
(defthm len-of-aignet-simplify-with-tracking-assum-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (equal (len new-assum-lits) (len assum-lits))))
Theorem:
(defthm len-of-aignet-simplify-with-tracking-track-lits (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (equal (len new-track-lits) (len track-lits))))
Theorem:
(defthm w-state-of-aignet-simplify-with-tracking (b* (((mv ?new-aignet ?new-assum-lits ?new-pres-lits ?new-track-lits ?new-state) (aignet-simplify-with-tracking aignet assum-lits pres-lits track-lits config state))) (equal (w new-state) (w state))))