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:

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

- 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-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-solving
- Proving SAT instances in FGL
- 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.