Symbolically interpret a term using GL, with inputs generated by parametrization.
(gl-interp term bindings :hyp hyp)
The above form runs a symbolic interpretation of
(def-gl-thm <name> :hyp hyp :concl term :g-bindings bindings).
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