		Search-engine friendly clone of the ACL2 documentation.

Reference

Gl-interp

Symbolically interpret a term using GL, with inputs generated by parametrization.

Usage:

(gl-interp term bindings :hyp hyp)

The above form runs a symbolic interpretation of term on the symbolic input assignment produced by parametrizing bindings using hyp. The symbolic execution run by this form is similar to that run by

(def-gl-thm <name> :hyp hyp :concl term :g-bindings bindings).

bindings should be a binding list of the same kind as taken by def-gl-thm, that is, a list of elements (var val) such that var is a variable free in term, and val is a shape specifier; see shape-specs.

Similar to def-gl-thm, term and hyp should be the (unquoted) terms of interest, whereas bindings should be something that evaluates to the binding list (the quotation of that binding list, for example.)

In more detail: First, the input bindings are converted to an assignment of symbolic inputs to variables. The hyp term is symbolically interpreted using this variable assignment, yielding a predicate. The symbolic input assignment is parametrized using this predicate to produce a new such assignment whose coverage is restricted to the subset satisfying the hyp. The term is then symbolically interpreted using this assignment, and the result is returned.

This macro expands to a function call taking state and the bvar-db and bvar-db1 live stobjs. It returns:

(mv error-message hyp-bfr param-al result bvar-db bvar-db1 state)

The symbolic interpreter used by gl-interp is the latest interpreter defined using def-gl-clause-processor (as recorded in the gl::latest-greatest-gl-clause-proc table).