Differences between FGL and ACL2 rewrite rules

FGL rewrite rules are essentially just ACL2 rewrite rules. More
specifically, they are derived from formulas that have basically the same form
as ACL2 rewrite rules; they need not be stored with

An FGL rewrite rule is an ACL2 rewrite rule. You can register an existing ACL2 theorem for use as an FGL rewrite rule using:

(fgl::add-fgl-rewrite my-rule)

And you can disable that rule for use by FGL using:

(fgl::remove-fgl-rewrite my-rule)

To create a new rewrite rule and enable it for FGL, you may use:

(fgl::def-fgl-rewrite my-rule body :hints ...)

This just expands to:

(defthmd my-rule ...) (fgl::add-fgl-rewrite my-rule)

FGL also supports rewrite rules that are triggered not on the leading
function symbol of the LHS, but on the leading function symbol of an
if-then-else branch. These rules can be added using

(fgl::def-fgl-branch-merge my-rule body ...)

A suitable branch merge rule has a left-hand side of the form

FGL rewrite rules support ACL2's syntaxp and bind-free hypothesis forms. However, it generally won't work to use the same rewrite rule in both the ACL2 and FGL rewriters if it has syntaxp or bind-free hypotheses, because in FGL the variables in the syntaxp/bind-free forms will be bound to symbolic objects, whereas in ACL2 they will be bound to terms. Therefore to use syntaxp, bind-free, and bind-var (discussed below), one needs to be familiar with FGL symbolic objects -- see fgl-object.

Two additional features support a new style of programming rewrite rules.

Here is an example that uses both syntax-bind and abort-rewrite, from "bitops.lisp":

(def-fgl-rewrite logtail-to-logtail-helper (implies (syntaxp (not (fgl-object-case n :g-concrete))) (equal (logtail n x) (b* ((x (int x)) (n (nfix (int n))) ((when (syntax-bind n-concrete (fgl-object-case n :g-concrete))) (logtail n x)) (n-width (syntax-bind n-width (fgl-object-case n :g-integer (max 0 (1- (len n.bits))) :otherwise nil))) ((unless (and n-width (check-unsigned-byte-p n-width n))) (abort-rewrite (logtail n x))) (n-rev (int-revapp n-width n 0))) (logtail-helper n-rev n-width x)))))

When attempting to apply this rewrite rule, the FGL rewriter starts in much the same way as the ACL2 rewriter. As a precondition for attempting to apply this rule, the term we are rewriting must be a call of logtail, and that call must unify with the LHS of this rule -- in this case any call of logtail will do so.

Next, we relieve the hyps. This rule only has one hyp, which is a
syntaxp call; we check that

Then we proceed by interpreting the RHS. We bind

This next syntax-bind form (note it must use a different free variable than
the other form!) returns either some natural number value or else NIL. Again,
either way it is a concrete object representing itself. We bind this to

Note we needed to know

FGL's implementation of syntaxp, bind-free, and syntax-bind interpret the
syntactic term using a custom evaluator, fancy-ev, that can be
instrumented to call functions that examine the ACL2 state and the FGL
interpreter state, and even make limited modifications to them. See the
documentation for fancy-ev for how to use it, and see fgl-interpreter-state for documentation of the contents of the interpreter state. One
main use of this is to examine counterexamples produced from incremental SAT
calls. By default, after loading

- Fgl-syntactic-checker-binders
- Functions for checking syntactic properties of objects, and inferring the logical properties that they imply
- Fancy-ev
- Term evaluator used by FGL for syntaxp, bind-free, and syntax-bind interpretation.
- Binder
- Form that can bind a free variable to the result of some (possibly nondeterministic) computation.
- Def-fgl-program
- Define a function that is logically just NIL but has special extralogical behavior in FGL.
- Bind-var
- Form that can bind a free variable to the result of an arbitrary computation.
- Add-fgl-brewrites
- Enable some binder rewrite rules for use in FGL
- Def-fgl-rewrite
- Define a rewrite rule for FGL to use on term-level objects
- Narrow-equiv
- FGL testbench function to interpret a term under a narrower (stricter) equivalence context.
- Def-fgl-branch-merge
- Define a rule for FGL to use in merging IF branches
- Add-fgl-rewrites
- Enable some rewrite rules for use in FGL
- Fgl-interp-obj
- FGL testbench function to interpret a term that is the result of evaluating some form.
- Fgl-prog2
- In the FGL interpreter, run the first form for side effects and return the result from the second form.
- Collect-cmr-rewrites-for-formula-name
- Syntax-bind
- Form that can bind a free variable to a value computed from examining the syntax of other bound variables in the RHS of an FGL rewrite rule.
- Fgl-time
- FGL alternative to time$ that does not get elided by rewrite rule storage.
- Assume
- FGL testbench function to assume some condition while interpreting a term.
- Add-fgl-binder-meta
- Register a metafunction for use in rewriting binder invocations of a trigger function in FGL.
- Add-fgl-primitive
- Register a primitive function for use in rewriting calls of a trigger function in FGL.
- Add-fgl-meta
- Register a metafunction for use in rewriting calls of a trigger function in FGL.
- Add-fgl-branch-merges
- Enable some rewrite rules's use for branch merging in FGL.
- Cmr::rewritelist->lhses
- Remove-fgl-brewrites
- Disable some binder rewrite rules' use in FGL.
- Remove-fgl-branch-merges
- Disable some rewrite rules' use for branch merging in FGL.
- Lhses->branch-function-syms
- Enable-execution
- Enable the use of concrete execution of a function in FGL rewriting.
- Abort-rewrite
- Form that aborts the application of an FGL rewrite rule when encountered while processing the RHS of the rule.
- Syntax-interp
- Interpret a form on the syntactic representations of variables.
- Remove-fgl-rewrites
- Disable some rewrite rules' use in FGL.
- Lhses->leading-function-syms
- Remove-fgl-primitive
- Deregister a primitive function for use in FGL.
- Remove-fgl-binder-meta
- Deregister a binder metafunction for use in FGL.
- If!
- Function implementing IF that under FGL interpretation makes a
:g-ite object instead of doing the usual merging process. - Disable-execution
- Disable the use of concrete execution of a function in FGL rewriting.
- Remove-fgl-meta
- Deregister a metafunction for use in FGL.
- Fgl-time-fn
- Disable-definition
- Disable the use of the given formula in FGL rewriting.
- Def-fgl-brewrite
- Define a binder rewrite rule for FGL to use on term-level objects