Fgl-rewrite-rules
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
:rule-classes :rewrite. FGL uses a different set of rules than the ones
that are enabled for use in ACL2, because not all good ACL2 rewrite rules are
good FGL rewrite rules, and
vice versa. A particularly important difference is that syntaxp and
bind-free forms receive FGL symbolic
objects as their inputs, rather than ACL2 terms. FGL rewrite rules also
allow special constructs bind-var, binder, and syntax-bind
which allow free variables to be bound as with bind-free, but in the RHS
of the rewrite rule rather than in the hyps. They additionally support a form
abort-rewrite which causes the application of the rule to be aborted
when encountered in the RHS, similarly to if a hypothesis was not relieved.
Creating and Removing FGL Rewrite Rules
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::add-fgl-branch-merge my-rule) and they can be created using:
(fgl::def-fgl-branch-merge my-rule
body
...)
A suitable branch merge rule has a left-hand side of the form (if test
then else) where then is a function call. Generally, test and
else should be free variables, but this isn't a hard and fast rule.
Binding Free Variables
There are several ways in which variables not present in the LHS of the rule
can become bound:
- Bind-free hypotheses: similar to ACL2's bind-free, but sees existing
variables' values as FGL objects and must bind new variables to FGL
objects (see fgl-object), rather than ACL2 terms.
- Binder functions: see bind-var, binder, and syntax-bind. Binder functions can also determine the values to be assigned to
the free variables using rewriting; see binder-rules.
- Equivalence-based binding hypotheses: a hypothesis of the form (equiv
free-var form) where equiv is a known equivalence relation and free-var is a
variable not bound in the current rewriting context. This will result in FGL
rewriting form under equivalence relation equiv and binding the
result to free-var.
- Match-assums hypotheses: A hypothesis of the form (fgl::match-assums
hyp) will look for an assumption in the current path condition that matches
the form of hyp and binds any free variables in hyp accordingly. In
more detail, for each Boolean variable in the interpreter's Boolean variable
database whose associated object's leading function symbol is the same as that
of hyp, we check whether that object unifies with hyp under the
existing variable bindings, and if so whether that variable is currently
assumed in the path condition. If so, we add the unifying subsitution to the
current variable bindings.
Advanced Features
Two additional features support a new style of programming rewrite rules.
Bind-var and syntax-bind allow functionality similar to bind-free,
but available within the right-hand side of a rewrite rule. Abort-rewrite
allows the rewrite operation to be cancelled partway through interpreting the
right-hand side.
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 (integer-length-bound n-width n))
((unless n-width)
(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 n is not a :g-concrete object.
Then we proceed by interpreting the RHS. We bind x to the result of
rewriting (int x) (where int is an alias for ifix and rebind
n to the result of rewriting (nfix (int n)), and then we encounter
our first syntax-bind form. The syntax-bind form has the free variable
n-concrete, which is here to logically represent the result we get from
evaluating the syntax-bind form. A syntax-bind form is logically equivalent to
its first argument, so when we prove logtail-to-logtail-helper correct we
prove it with the free variable n-concrete in place of the syntax-bind.
That means we are logically justified in returning anything we want from the
syntax-bind form -- since n-concrete is a free variable not previously bound,
the rule is applicable for any value of n-concrete. In this case we evaluate
(fgl-object-case n :g-concrete). (Note: syntax-bind is a macro that
uses the primitive forms bind-var and syntax-interp to implement
this behavior; see their documentation for more general usage.) This will
produce a Boolean value, which is a concrete FGL object representing itself. If
true, then n is concrete and we will produce the result of again rewriting
(logtail n x) -- note that we haven't created a loop here because the
syntaxp hyp required that the original n was not concrete. Otherwise, we
proceed with the next form.
The next form appears to bind (integer-length-bound n-width n) to
n-width, which may appear mysterious since n-width is used in its own
binding. This is because integer-length-bound is a
binder-function
intended to bind its first argument (which must be a free variable) to some
value determined by the rest of its arguments. So here n-width is a free
variable that will be bound to some value determined by examining n; the
definition of integer-length-bound guarantees that that value is either a
bound on the integer-length of n or is NIL. In fact, the value to be bound
is derived in this case by a meta rule integer-length-bound-binder. In
other cases it could be determined by a rewrite rule; see binder-rules.
We then require that n-width is nonnil, meaning we have found a good
bound for the integer-length of n. If not, we have an abort-rewrite
form which causes the current rewrite rule attempt to end, ignoring the form
inside the abort-rewrite. (In this case the form (logtail n x) inside the
abort-rewrite was selected to make it easy to prove
logtail-to-logtail-helper correct.) Otherwise, we go on with our
rewrite.
Last, we finish this rewrite: the point of this rule was to replace a call
of logtail with a logtail-helper form which can be opened iteratively
to create the symbolic value needed.
Examining the Interpreter State
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/top, the rewrite rule
show-counterexample-rw rewrites the constant-nil function
(show-counterexample msg) such that a syntax-bind form fetches the latest
incremental SAT counterexample and prints it.
Subtopics
- Binder-functions
- Functions that describe constraints on bindings for free variables.
- Fgl-syntactic-checker-binders
- Functions for checking syntactic properties of objects, and inferring
the logical properties that they imply
- Binder
- Form that can bind a free variable to the result of some (possibly
nondeterministic) computation.
- Fancy-ev
- Term evaluator used by FGL for syntaxp, bind-free, and syntax-bind interpretation.
- Binder-rules
- Determining free variable bindings using rewriting
- 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.
- 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.
- Collect-cmr-rewrites-for-formula-name
- Fgl-time
- FGL alternative to time$ that does not get elided by rewrite rule storage.
- Fgl-prog2
- In the FGL interpreter, run the first form for side effects and
return the result from the second form.
- 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
