		Search-engine friendly clone of the ACL2 documentation.

Vector-simulation

Random-sim

Exhaustively simulate an AIG with one output node to determine if it is satisfiable

Signature
(random-sim num-sims invals aignet state) → (mv ctrexp invals new-state)
Arguments: num-sims — Guard (natp num-sims).; invals — counterexample written here.

Given a combinational AIG with 37 or fewer inputs and no registers, this uses aignet-vecsim to run through all combinations of inputs to check the satisfiability of the 0th output of the AIG. This function returns NIL if that output is unsatisfiable (always 0), and otherwise returns a natural number giving the satisfying assignment for the PIs; i.e. (logbitp n result) gives the assignment for input n.

Definitions and Theorems

Function: random-sim

(defun random-sim (num-sims invals aignet state)
  (declare (xargs :stobjs (invals aignet state)))
  (declare (xargs :guard (natp num-sims)))
  (declare (xargs :guard (<= 1 (num-outs aignet))))
  (let ((__function__ 'random-sim))
    (declare (ignorable __function__))
    (b* (((local-stobjs s32v)
          (mv ctrexp invals s32v state))
         (s32v (s32v-resize-cols 1 s32v))
         (s32v (s32v-resize-rows (num-fanins aignet)
                                 s32v)))
      (random-sim-aux num-sims invals s32v aignet state))))

Theorem: w-state-of-random-sim

(defthm w-state-of-random-sim
  (b* (((mv ?ctrexp ?invals ?new-state)
        (random-sim num-sims invals aignet state)))
    (equal (w new-state) (w state))))

Theorem: random-sim-of-nfix-num-sims

(defthm random-sim-of-nfix-num-sims
  (equal (random-sim (nfix num-sims)
                     invals aignet state)
         (random-sim num-sims invals aignet state)))

Theorem: random-sim-nat-equiv-congruence-on-num-sims

(defthm random-sim-nat-equiv-congruence-on-num-sims
  (implies (nat-equiv num-sims num-sims-equiv)
           (equal (random-sim num-sims invals aignet state)
                  (random-sim num-sims-equiv invals aignet state)))
  :rule-classes :congruence)