Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Gl
Term-level-reasoning
Glmc
Other-resources
Optimization
Reference
Def-gl-thm
Shape-specs
Symbolic-objects
Gl-aside
Def-gl-param-thm
Symbolic-arithmetic
Bfr
Def-gl-boolean-constraint
Gl-mbe
Bvec
Flex-bindings
Auto-bindings
Gl-interp
Gl-set-uninterpreted
Def-gl-clause-processor
Def-glcp-ctrex-rewrite
ACL2::always-equal
Gl-hint
Def-gl-rewrite
Def-gl-branch-merge
Gl-force-check
Gl-concretize
Gl-assert
Gl-param-thm
Gl-simplify-satlink-mode
Gl-satlink-mode
Gl-bdd-mode
Gl-aig-bddify-mode
Gl-fraig-satlink-mode
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-aig-bddify-mode
GL: use AIGs as the Boolean function representation and solve queries by transforming them to BDDs.