		Search-engine friendly clone of the ACL2 documentation.

Vector-simulation

Exhaustive-sim

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

Signature
(exhaustive-sim aignet) → ctrex
Returns: ctrex — Type (acl2::maybe-natp ctrex).

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: exhaustive-sim

(defun exhaustive-sim (aignet)
  (declare (xargs :stobjs (aignet)))
  (declare (xargs :guard (and (<= (num-ins aignet) 37)
                              (<= 1 (num-outs aignet)))))
  (let ((__function__ 'exhaustive-sim))
    (declare (ignorable __function__))
    (b* (((local-stobjs s32v) (mv ctrex s32v))
         (s32v (s32v-resize-cols 1 s32v))
         (s32v (s32v-resize-rows (num-fanins aignet)
                                 s32v)))
      (exhaustive-sim-aux 0
                          (logmask (nfix (- (num-ins aignet) 5)))
                          s32v aignet))))

Theorem: maybe-natp-of-exhaustive-sim

(defthm maybe-natp-of-exhaustive-sim
  (b* ((ctrex (exhaustive-sim aignet)))
    (acl2::maybe-natp ctrex))
  :rule-classes :type-prescription)

Theorem: exhaustive-sim-correct

(defthm exhaustive-sim-correct
  (b* ((?ctrex (exhaustive-sim aignet)))
    (implies (and (equal (output-eval 0 invals regvals aignet)
                         1)
                  (equal (num-regs aignet) 0))
             ctrex)))