		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-minimize-sat-ctrex-rec

Signature
(fraig-minimize-sat-ctrex-rec id ctrex-relevant aignet2 ctrex-eval state) → (mv new-ctrex-relevant new-state)
Arguments: id — Guard (natp id).

Definitions and Theorems

Function: fraig-minimize-sat-ctrex-rec

(defun fraig-minimize-sat-ctrex-rec
       (id ctrex-relevant aignet2 ctrex-eval state)
 (declare (xargs :stobjs (ctrex-relevant aignet2 ctrex-eval state)))
 (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 ctrex-relevant)))))
 (let ((__function__ 'fraig-minimize-sat-ctrex-rec))
  (declare (ignorable __function__))
  (b*
   (((when (eql 1 (get-bit id ctrex-relevant)))
     (mv ctrex-relevant state))
    (ctrex-relevant (set-bit id 1 ctrex-relevant))
    (slot0 (id->slot id 0 aignet2))
    (slot1 (id->slot id 1 aignet2))
    (type (snode->type slot0))
    ((unless (eql type (gate-type)))
     (mv ctrex-relevant state))
    (fanin0 (snode->fanin slot0))
    (fanin1 (snode->fanin slot1))
    ((when (or (eql 1 (snode->regp slot1))
               (eql 1 (get-bit id ctrex-eval))))
     (b* (((mv ctrex-relevant state)
           (fraig-minimize-sat-ctrex-rec (lit-id fanin0)
                                         ctrex-relevant
                                         aignet2 ctrex-eval state)))
       (fraig-minimize-sat-ctrex-rec (lit-id fanin1)
                                     ctrex-relevant
                                     aignet2 ctrex-eval state)))
    ((when (eql 1 (aignet-eval-lit fanin0 ctrex-eval)))
     (fraig-minimize-sat-ctrex-rec (lit-id fanin1)
                                   ctrex-relevant
                                   aignet2 ctrex-eval state))
    ((when (eql 1 (aignet-eval-lit fanin1 ctrex-eval)))
     (fraig-minimize-sat-ctrex-rec (lit-id fanin0)
                                   ctrex-relevant
                                   aignet2 ctrex-eval state))
    ((when (or (eql 1
                    (get-bit (lit-id fanin0)
                             ctrex-relevant))
               (eql 1
                    (get-bit (lit-id fanin1)
                             ctrex-relevant))))
     (mv ctrex-relevant state))
    ((mv coin state) (random$ 2 state))
    ((when (eql coin 0))
     (fraig-minimize-sat-ctrex-rec (lit-id fanin0)
                                   ctrex-relevant
                                   aignet2 ctrex-eval state)))
   (fraig-minimize-sat-ctrex-rec (lit-id fanin1)
                                 ctrex-relevant
                                 aignet2 ctrex-eval state))))

Theorem: ctrex-relevant-length-of-fraig-minimize-sat-ctrex-rec

(defthm ctrex-relevant-length-of-fraig-minimize-sat-ctrex-rec
  (b* (((mv ?new-ctrex-relevant ?new-state)
        (fraig-minimize-sat-ctrex-rec id ctrex-relevant
                                      aignet2 ctrex-eval state)))
    (implies (and (<= (num-fanins aignet2)
                      (len ctrex-relevant))
                  (<= (nfix id) (fanin-count aignet2)))
             (equal (len new-ctrex-relevant)
                    (len ctrex-relevant)))))

Theorem: w-state-of-fraig-minimize-sat-ctrex-rec

(defthm w-state-of-fraig-minimize-sat-ctrex-rec
  (b* (((mv ?new-ctrex-relevant ?new-state)
        (fraig-minimize-sat-ctrex-rec id ctrex-relevant
                                      aignet2 ctrex-eval state)))
    (equal (w new-state) (w state))))

Theorem: fraig-minimize-sat-ctrex-rec-of-nfix-id

(defthm fraig-minimize-sat-ctrex-rec-of-nfix-id
  (equal (fraig-minimize-sat-ctrex-rec
              (nfix id)
              ctrex-relevant aignet2 ctrex-eval state)
         (fraig-minimize-sat-ctrex-rec id ctrex-relevant
                                       aignet2 ctrex-eval state)))

Theorem: fraig-minimize-sat-ctrex-rec-nat-equiv-congruence-on-id

(defthm fraig-minimize-sat-ctrex-rec-nat-equiv-congruence-on-id
 (implies
    (nat-equiv id id-equiv)
    (equal (fraig-minimize-sat-ctrex-rec
                id
                ctrex-relevant aignet2 ctrex-eval state)
           (fraig-minimize-sat-ctrex-rec id-equiv ctrex-relevant
                                         aignet2 ctrex-eval state)))
 :rule-classes :congruence)