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, first set up a SAT solver; the default for
FGL is glucose. To use a different SAT solver, see fgl-solving.
;; include FGL
(include-book "centaur/fgl/top" :dir :system)
;; start an external shell from which the SAT solver can be called
(value-triple (acl2::tshell-ensure))
;; 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)))
In addition to a standalone SAT solver program (monolithic solver), for
certain FGL features you may also want an incremental solver implementing the
IPASIR interface; see ipasir::ipasir for an overview and
(see ipasir::building-an-ipasir-solver-library) for how to build one. Then
you'll need to set the environment variable IPASIR_SHARED_LIBRARY and
include the book centaur/ipasir/ipasir-backend in order to allow its
use.
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-counterexamples
- Generating counterexamples from SAT checks in FGL
- Fgl-interpreter-overview
- Outline of the way the FGL interpreter works.
- 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
- Fgl-array-support
- Support for fast array lookups in FGL
- Advanced-equivalence-checking-with-fgl
- Some tools for equivalence checking with FGL.
- Fgl-fty-support
- Utilities for supporting fty types in fgl.
- Fgl-internals
- Topics describing implementation-level details.
