Z3 ceiling and the methodology of programatic semantics

[benbrastmckie]

There is a methodological point to make coming from the limitations of Z3 which motivates simplicity in the arity of primitives and the number of nested operators used in constraints. Here is the inline comment about Z3 limitations:

    M: could we save the extensions of all the functions?
        - not that much for small values of N.
        - you could then save all those extensions and when you're evaluating you'd just need to check if a specific set of values is in the extension of the given function. 
        - the problem is how do we know for a generic case what the name of a given function is?
        - maybe it is better to rely on a method that is like the current evaluate one but for functions.
        - as a concrete example take find_compatible_parts in model_definitions rn.
        - to find what bits are compatible with a world, you check if some things are in the extension of other things.
        - with the new implementation, you would simply do z3_model.evaluate(compatible_parts).

    M: I tried this, it didn't work because it actually takes a lot of computational power.
        - it turns out that even for small values of N saving the extensions of function is a lot
        - since there are a couple functions that would take 3 inputs (e.g. is_alternative), which has inputs in R^3, meaning, with e.g. N=7 there are (2^7)^3 = 2 million different input combos.
        - even worse, in that strategy you'd create a constraint for every single combination of bits in the space R^n for n the number of arguments taken by the function.
        - so for N=7 and a 3-place predicate, you'd create a constraint that is itself a conjunction of 2 million constraints—in tests Z3 was taking too long for that (I never saw it terminate).

To develop this methodological point, we need to:
- Figure out the precise size calculations for with a citation to Z3 literature or some official source.
- Measure where things break down computationally given the compute of an average laptop for a case study.
- Develop a section of the paper which makes the methodological point.