The :named smtlib annotation has relatively annoying semantics. In particular, it implicitly introduces a global definition. Therefore this PR does a few things:
Add a generic support for implicit definition/declarations that can ben generated during typechecking, and propagate that change. In particular this means that the result of typechecking one "thing"( be it a term/formula/declaration/definition) is actually a list of implicit declarations, a list of implicit definitions, and then the result of typechecking that "thing". Also, typechecking a single statement now results in multiple statements. This PR decides to keep these as a list, instead of exploding them as could be possible with an adequate Pipeline transformation. This is because if we exploded them, then the intermediate typechecking state could be surprising to downstream pipes, since it would contain statements that these pipes have not yet seen.
That support is used by the typechecker to emit the various implicit definition and declarations that were already recorded but not emitted, for instance, all the constants (but not the variables) that are inferred.
A new Hook result for tags is added in the typechecker to allow for tags to arbitrarily change the typechecked term (instead of simply adding/setting some flags/tags in terms)
Lastly, the core theory of smtlib2 is adapted to use the Hook mechanism to properly replace named expression by their symbol, which is required since named expressions can be referred later by their symbol.
The
:namedsmtlib annotation has relatively annoying semantics. In particular, it implicitly introduces a global definition. Therefore this PR does a few things:Pipelinetransformation. This is because if we exploded them, then the intermediate typechecking state could be surprising to downstream pipes, since it would contain statements that these pipes have not yet seen.Hookresult for tags is added in the typechecker to allow for tags to arbitrarily change the typechecked term (instead of simply adding/setting some flags/tags in terms)coretheory of smtlib2 is adapted to use theHookmechanism to properly replace named expression by their symbol, which is required since named expressions can be referred later by their symbol.