		Search-engine friendly clone of the ACL2 documentation.

Aig2c-config-p

Honsed-aig2c-config

Raw constructor for honsed aig2c-config-p structures.

Syntax:

(honsed-aig2c-config prefix type op-and op-not)

This is identical to aig2c-config, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by std::defaggregate.

Function: honsed-aig2c-config

(defun honsed-aig2c-config (prefix type op-and op-not)
 (declare
  (xargs
    :guard (and (stringp prefix)
                (stringp type)
                (stringp op-and)
                (stringp op-not)
                (aig2c-boolean-sanity-check-p type op-and op-not))))
 (mbe :logic (aig2c-config prefix type op-and op-not)
      :exec
      (hons :aig2c-config
            (hons (hons 'prefix prefix)
                  (hons (hons 'type type)
                        (hons (hons 'op-and op-and)
                              (hons (hons 'op-not op-not) nil)))))))