Reference
Reference documentation for using GL.
Subtopics
- 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 Boolean Function
Representation 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.
