• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
    • Gl
      • Term-level-reasoning
      • Glmc
      • Other-resources
      • Optimization
        • Term-level-reasoning
        • Def-gl-param-thm
        • Case-splitting
        • Modes
          • Gl-mode-implementation
          • Gl-simplify-satlink-mode
          • Gl-satlink-mode
          • Gl-bdd-mode
          • Gl-aig-bddify-mode
          • Gl-fraig-satlink-mode
        • 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

• Modes
• Reference

Gl-fraig-satlink-mode

GL: Use AIGs as the Boolean function representation and satlink after aignet fraiging to solve queries.