Reference documentation for using GL.

- Def-gl-thm
- Prove a theorem using GL symbolic simulation.
- Shape-specs
- Simplified symbolic objects useful for coverage proofs in GL.
- Symbolic-objects
- Format of symbolic objects in gl.
- Gl-aside
- A debugging facility that is typically used for printing messages during GL symbolic execution.
- Def-gl-param-thm
- Prove a theorem using GL symbolic simulation with parametrized case-splitting.
- Symbolic-arithmetic
- Internal operations for computing on symbolic bit vectors.
- Bfr
- An abstraction of the
**B**oolean**F**unction**R**epresentation used by GL. - Def-gl-boolean-constraint
- Define a rule that recognizes constraints among GL generated Boolean variables
- Gl-mbe
- Assert that a particular symbolic object is equivalent to a second form, and use the second in place of the first.
- Bvec
- Internal representations of symbolic bit vectors.
- Flex-bindings
- Shape specifiers for
:g-bindings , more flexible than auto-bindings. - Auto-bindings
- Simplified shape specifiers for
:g-bindings . - Gl-interp
- Symbolically interpret a term using GL, with inputs generated by parametrization.
- Gl-set-uninterpreted
- Prevent GL from interpreting a function's definition or concretely executing it.
- Def-gl-clause-processor
- Define a GL clause processor with a given set of built-in symbolic counterparts.
- Def-glcp-ctrex-rewrite
- Define a heuristic for GL to use when generating counterexamples
- ACL2::always-equal
- Alias for equal that has a special meaning in gl-bdd-mode.
- Gl-hint
- Try to prove a goal using GL symbolic simulation.
- Def-gl-rewrite
- Define a rewrite rule for GL to use on term-level objects
- Def-gl-branch-merge
- Define a rule for GL to use in merging IF branches
- Gl-force-check
- When found in an
if test, forces GL to check satisfiability of the test. - Gl-concretize
- During GL symbolic execution, try to reduce a symbolic object to a concrete one.
- Gl-assert
- During GL symbolic execution, check that a condition holds, causing an error if it does not.
- Gl-param-thm
- Prove a theorem using GL symbolic simulation with parametrized case-splitting, without storing the theorem.
- Gl-simplify-satlink-mode
- GL: Use AIGs as the Boolean function representation and satlink after a configurable list of aignet transforms to solve queries.
- Gl-satlink-mode
- GL: Use AIGs as the Boolean function representation and satlink to solve queries.
- Gl-bdd-mode
- Use BDD-based symbolic simulation in GL.
- Gl-aig-bddify-mode
- GL: use AIGs as the Boolean function representation and solve queries by transforming them to BDDs.
- Gl-fraig-satlink-mode
- GL: Use AIGs as the Boolean function representation and satlink after aignet fraiging to solve queries.