A prover framework that supports bit-blasting.

FGL is the successor to

- 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

;; 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

To learn more about FGL, here are some places to get started:

- fgl-object
- fgl-getting-bits-from-objects
- fgl-rewrite-rules
- fgl-debugging
- fgl-handling-if-then-elses
- fgl-interpreter-overview
- fgl-primitive-and-meta-rules
- fgl-sat-check
- fgl-solving
- fgl-counterexamples

- 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.