• 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

Aig2c-config-p

Configuration object that governs how we translate an AIG into C/C++.

(aig2c-config-p x) is a std::defaggregate of the following fields.

  • prefix — The naming prefix to use for generating temporary variable names. Typically you just want this to be something that won't clash with other names in the rest of your C program. By default we use "_temp".
        Invariant (stringp prefix).
  • type — The C/C++ data type to use for each temporary variable. By default we use "const uint32_t", which might be appropriate for 32-bit wide simulations. For single-bit simulations, you could use, e.g., "const bool" here, but WARNING if you use bool or const bool you need to also change the operators from & and ~ to && and !, respectively. See aig2c for more information.
        Invariant (stringp type).
  • op-and — The C/C++ operator to use to AND expressions of this type. Typically this should be & for integers or && for booleans.
        Invariant (stringp op-and).
  • op-not — The C/C++ operator used to NOT expressions of this type. Typically this should be ~ for integers or ! for booleans.
        Invariant (stringp op-not).

Source link: aig2c-config-p

The default configuration generates code for carry out 32-bit wide AIG simulations on uint32_ts. Changing to, e.g., 8-bit or 64-bit wide simulations is trivial.

But the C++ bool type is special. If you want to use it, you need to make sure to use && and ! instead of & and ~. Consider for instance this C++ program:

int main() {
  bool b = true;
  cout << "B is " << (bool)b << endl;    // Prints 'B is 1'
  b = ~b;
  cout << "~B is " << (bool)b << endl;   // Prints '~B is 1' (!!!)
  return 0;
}

We try to at least do a rudimentary check for incorrect uses of bool, but it's not any sort of foolproof thing.

Subtopics

Aig2c-config
Raw constructor for aig2c-config-p structures.
Make-aig2c-config
Constructor macro for aig2c-config-p structures.
Change-aig2c-config
A copying macro that lets you create new aig2c-config-p structures, based on existing structures.
Make-honsed-aig2c-config
Constructor macro for honsed aig2c-config-p structures.
Honsed-aig2c-config
Raw constructor for honsed aig2c-config-p structures.
Aig2c-boolean-sanity-check-p
Aig2c-config->type
Access the type field of a aig2c-config-p structure.
Aig2c-config->prefix
Access the prefix field of a aig2c-config-p structure.
Aig2c-config->op-not
Access the op-not field of a aig2c-config-p structure.
Aig2c-config->op-and
Access the op-and field of a aig2c-config-p structure.