• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
      • Term-level-reasoning
      • Glmc
      • Other-resources
      • Optimization
        • Term-level-reasoning
        • Def-gl-param-thm
        • Case-splitting
        • Modes
        • Memory-management
        • Preferred-definitions
        • Custom-symbolic-counterparts
        • Redundant-recursion
        • Alternate-definitions
        • Gl-param-thm
      • Reference
      • Debugging
      • Basic-tutorial
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Removable-runes
    • Fgl
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • 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
  • Math
  • Testing-utilities

• Optimization

Custom-symbolic-counterparts

The advanced GL user can write custom symbolic counterparts to get better performance.

This is somewhat involved. Generally, such a function operates by cases on what kinds of symbolic objects it has been given. Most of these cases are easy; for instance, the symbolic counterpart for consp just returns nil when given a :g-boolean or :g-integer. But in other cases the operation can require combining the Boolean expressions making up the arguments in some way, e.g., the symbolic counterpart for binary-* implements a simple binary multiplier.

Once the counterpart has been defined, it must be proven sound with respect to the semantics of ACL2 and the symbolic object format. This is an ordinary ACL2 proof effort that requires some understanding of GL's implementation.

An example of a more sophisticated symbolic counterpart is an aig to ubdd conversion algorithm. This function serves as a symbolic counterpart for AIG evaluation. This algorithm and its correctness proof can be found in the book centaur/aig/g-aig-eval.