Fgl
A prover framework that supports bit-blasting.
FGL is the successor to GL. It mainly
consists of a clause processor that calls on a custom rewriter/term interpreter
which features support for efficient representations of Boolean functions.
Compared to GL, FGL offers the following new features:
- Support for representing Boolean functions using the aignet package.
- Support for calling incremental SAT during rewriting/symbolic execution.
- Less functionality included in built-in primitives, but better able to be
programmed using rewrite rules and user-provided extensions.
- Explicit representation of the entire interpreter state,
allowing global simplifications (e.g. combinational-equivalence-preserving
AIGNET transformations).
- The symbolic object representation includes a new primitive kind
representing a fast alist or array.
- Better debugging capabilities, including a tracing facility for the
rewriter and the ability to examine the full interpreter stack at any
point.
FGL is currently missing some important features of GL. In particular, BDD
and hons-AIG modes are not complete. Shape specifiers don't exist yet. Many
of the usual ways of doing things in GL are done differently in FGL.
To get started with FGL in the default configuration:
;; include FGL
(include-book "centaur/fgl/top" :dir :system)
;; attach to an incremental SAT backend library.
;; Note: must have environment variable IPASIR_SHARED_LIBRARY set to the path to
;; an IPASIR-compliant shared library
(include-book "centaur/ipasir/ipasir-backend" :dir :system)
;; test a proof
(fgl::fgl-thm
:hyp (and (unsigned-byte-p 5 x) (unsigned-byte-p 5 y))
:concl (equal (+ x y) (+ y x)))
(fgl::def-fgl-thm my-silly-theorem
:hyp (unsigned-byte-p 3 x)
:concl (not (logbitp 4 x)))
To learn more about FGL, here are some places to get started:
Subtopics
- Fgl-rewrite-rules
- Differences between FGL and ACL2 rewrite rules
- Fgl-function-mode
- Limitations on what the FGL interpreter will do to resolve a call of a given function.
- Fgl-object
- FGL symbolic object type
- Fgl-solving
- Proving SAT instances in FGL
- Fgl-handling-if-then-elses
- Discussion of how if-then-else objects are dealt with in FGL.
- Fgl-getting-bits-from-objects
- How to ensure that FGL can reduce your conjecture to a Boolean formula
- Fgl-primitive-and-meta-rules
- Adding fast-executing primitive routines to FGL.
- Fgl-interpreter-overview
- Outline of the way the FGL interpreter works.
- Fgl-counterexamples
- Generating counterexamples from SAT checks in FGL
- Fgl-correctness-of-binding-free-variables
- Discussion of the logical justification for the bind-var feature.
- Fgl-debugging
- Tools for debugging FGL failures
- Fgl-testbenches
- Advanced extralogical programming of FGL.
- Def-fgl-boolean-constraint
- Define a rule that recognizes constraints among FGL generated Boolean variables
- Fgl-stack
- Representation of the FGL interpreter stack.
- Fgl-rewrite-tracing
- How to trace the FGL rewriter
- Def-fgl-param-thm
- Prove a theorem using FGL with case-splitting.
- Def-fgl-thm
- Prove a theorem using FGL
- Fgl-fast-alist-support
- Support for hash-based fast alists in FGL
- Advanced-equivalence-checking-with-fgl
- Some tools for equivalence checking with FGL.
- Fgl-array-support
- Support for fast array lookups in FGL
- Fgl-internals
- Topics describing implementation-level details.
