Z3 often gives back models defined in terms of a bunch of intermediate functions. For example, it's common to see the following (pardon my improper syntax):
(define-const myArray (Array Bool Int) (_ as-array f))
(define-fun f (x Bool) Int (f!10 (k!26 x)))
... And so on.
I'd like to be able to get a result back that I can take in my program (calling Z3 using library bindings) and both print the results, and parse them into a function I can actually run. This is much easier if I can get my model functions as single, straight line programs that I can run, instead of as multiple functions defined in terms of each other.
Is this possible? I'm dealing only with finite domain functions, if that helps.
We will be updating the model construction in a future release to compress away intermediate functions when possible. There are, however, cases where this can cause an exponential overhead because the same auxiliary function can be reused in several contexts. For those models, it doesn't make sense to expand the auxiliary functions. So users are still going to be forced to deal with such functions if they want to post-process the models.