• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Removable-runes
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-interpreter-overview
      • Fgl-counterexamples
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
        • Fgl-support-vars
        • Fgl-gatecount
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
      • Fgl-rewrite-tracing
      • Def-fgl-param-thm
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-array-support
      • Fgl-internals
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Fgl-debugging

Fgl-gatecount

Display how many AIG gates are used in the symbolic representation of an object

Logically, this returns its second argument; its first argument should be a variable symbol. This counts the number of AIG gates that are used in the symbolic representation of the object (second argument) and prints that out as a debugging message.

If you want to do anything else with the gatecount, you can get that count using (gatecount! x) under an unequiv context, or using the binder form (gatecount free-var x) in a rewrite rule.