• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
        • Aig-constructors
        • Aig-vars
        • Aig-sat
        • Bddify
        • Aig-substitution
        • Aig-other
          • Best-aig
          • Aig2c
            • Aig2c-config-p
              • Aig2c-config
                • Make-aig2c-config
                • Change-aig2c-config
                • Make-honsed-aig2c-config
                • Honsed-aig2c-config
                • Aig2c-boolean-sanity-check-p
                • Aig2c-config->type
                • Aig2c-config->prefix
                • Aig2c-config->op-not
                • Aig2c-config->op-and
              • Aig2c-compile
              • Aig2c-maketemps
              • Aig2c-main
              • Aig2c-prologue
              • Aig2c-maketemps-list
              • Aig2c-epilogue
              • Aig2c-main-list
            • Expr-to-aig
            • Aiger-write
            • Aig-random-sim
            • Aiger-read
            • Aig-print
            • Aig-cases
          • Aig-semantics
          • Aig-and-count
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Aig2c-config-p

    Aig2c-config

    Raw constructor for aig2c-config-p structures.

    Syntax:

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

    This is the lowest-level constructor for aig2c-config-p structures. It simply conses together a structure with the specified fields.

    Note: It's generally better to use macros like make-aig2c-config or change-aig2c-config instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

    The aig2c-config-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-aig2c-config instead.

    Definition

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

    Function: aig2c-config

    (defun 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))))
     (cons :aig2c-config
           (cons (cons 'prefix prefix)
                 (cons (cons 'type type)
                       (cons (cons 'op-and op-and)
                             (cons (cons 'op-not op-not) nil))))))