Module LustreFunDefs

SMT-level definitions of the recursive functions applied to quantified variables

A recursive function is compiled by unrolling its definition a number of times in the transition system, with the outputs of every instance tied to a functional symbol f.out.__function_of_inputs, and the recursive calls past the unrollings either left unconstrained or abstracted by the contract of the function (see LustreTransSys). A call applied to quantified variables has no instance to be unrolled: it is compiled to an application of the functional symbol, and the function is then given a definition by this module, as an SMT-LIB define-funs-rec block, so that the solver knows it at every argument the quantifier ranges over. The definition also ties the instances of the function to its body past their unrollings, so no counterexample is spurious for a defined function (see RecUnrolling).

Only a function whose recursive calls past the unrollings are left unconstrained is defined: one with no contract to abstract it with (no guarantee and no mode with an ensure, whether explicit or from a refinement type of an output; assumptions do not count) or declared transparent, or, outside of compositional analyses, any function not declared opaque (see contract_abstracts; LustreUserFunctions only accepts a quantified call to such a function). An opaque function with a contract is always abstracted by it, and a translucent one is in a compositional analysis.

The definition of a function is built from the equations of its body. A call to a function of the same recursive group applies the symbol of the callee under the guard of the termination checks of the call, and yields an arbitrary value (f.out.__undefined_call) otherwise: the definitions are then well-founded whether or not the measure of the function actually decreases, so they always have a model and cannot make the transition system inconsistent. The termination checks themselves remain properties of the transition system. A call to a recursive function of another group applies the functional symbol of the callee, which either has a definition of its own or is uninterpreted; a call to an imported function applies its functional symbol; and a call to any other function applies the symbols of a definition of that function (f.out.__function_definition), in a block of its own. Inlining the body of such a function instead would copy it at every call, and the definition of a function that calls another twice, which calls another twice, and so on, would grow exponentially with the depth of the calls. The symbols are not the functional symbols of the function, which the transition system ties to the instances of the function, where a contract may abstract it.

Every function of a recursive group is defined, or none is. A group is defined only if a function of it is applied to quantified variables, or called by the definitions of such a group, and each of its functions is eligible (not abstracted by its contract, as above) and definable: its body is a total function of its inputs, without assertions, oracles, array-typed variables or calls to nodes, and the same holds for the functions it calls that are neither recursive nor imported. Definitions are only produced for the solvers that support them (Z3 and cvc5) and when no logic is set with --smt_logic; a function that is applied to quantified variables but not defined, for any of these reasons, has its functional symbol left uninterpreted, and LustreTransSys warns about it.