		Search-engine friendly clone of the ACL2 documentation.

Aig2c

Aig2c-compile

Compile an alist of AIGs into a C code fragment.

Signature
(aig2c-compile aig-alist input-names &key (config '*aig2c-default-config*)) → (mv err c-code)
Arguments: aig-alist — Name → AIG Alist. The names here must be strings and should refer to proper lvalues in your C code, i.e., they might be variables, or fields in a structure that you want to initialize. For the C code to work, these names must be compatible with the datatype you want to use.
Guard (string-listp (alist-keys aig-alist)).; input-names — AIG Variable → Name Alist. This should bind every AIG variable to a string that will be used as its initial value in the C code. Each name should be a C code fragment that evaluates without side effects.
Guard (string-listp (alist-vals input-names)).; config — Controls names, types, and operators to use in the C code being generated.
Guard (aig2c-config-p config).
Returns: err — NIL on success, or an error msg on failure, suitable for printing with ~@.; c-code — C code fragment that implements this AIG, on success, or the empty string on failure.
Type (stringp c-code).

Definitions and Theorems

Function: aig2c-compile-fn

(defun aig2c-compile-fn (aig-alist input-names config)
 (declare (xargs :guard (and (string-listp (alist-keys aig-alist))
                             (string-listp (alist-vals input-names))
                             (aig2c-config-p config))))
 (let ((__function__ 'aig2c-compile))
   (declare (ignorable __function__))
   (b*
    ((output-c-names (alist-keys aig-alist))
     (output-aigs (alist-vals aig-alist))
     (input-vars (alist-keys input-names))
     (input-c-names (alist-vals input-names))
     (all-aig-vars (aig-vars-1pass output-aigs))
     ((unless (uniquep input-vars))
      (mv (msg "Error: multiple bindings for input variables ~x0"
               (duplicated-members input-vars))
          ""))
     ((unless (set::subset all-aig-vars
                           (set::mergesort input-vars)))
      (mv (msg "Some AIG variables do not have C input names: ~x0"
               (set::difference all-aig-vars
                                (set::mergesort input-vars)))
          ""))
     (- (or (set::subset (set::mergesort input-vars)
                         all-aig-vars)
            (cw "Note: Some inputs are never used: ~x0.~%"
                (set::difference (set::mergesort input-vars)
                                 all-aig-vars))))
     (all-c-names (append input-c-names output-c-names))
     (db (vl::vl-starting-namedb all-c-names))
     ((mv tempmap db)
      (aig2c-maketemps-list output-aigs config 'aig2c-tempmap
                            db))
     (- (vl::vl-free-namedb db))
     (input-names (if (hons-get nil tempmap)
                      (cons (cons nil "0") input-names)
                    input-names))
     (input-names
          (if (hons-get t tempmap)
              (cons (cons t
                          (str::cat (aig2c-config->op-not config)
                                    "((" (aig2c-config->type config)
                                    ")0)"))
                    input-names)
            input-names))
     (code nil)
     (code (aig2c-prologue input-names tempmap config code))
     ((mv code seen)
      (aig2c-main-list output-aigs 'aig2c-seen
                       tempmap config code))
     (- (fast-alist-free seen))
     (code (aig2c-epilogue aig-alist tempmap code))
     (- (fast-alist-free tempmap)))
    (mv nil (str::rchars-to-string code)))))

Theorem: stringp-of-aig2c-compile.c-code

(defthm stringp-of-aig2c-compile.c-code
  (b* (((mv ?err ?c-code)
        (aig2c-compile-fn aig-alist input-names config)))
    (stringp c-code))
  :rule-classes :type-prescription)