Function synthesis

[LeventErkok]

I'm playing around with how much z3 can find definitions of uninterpreted functions. I do realize this is a huge research area, and I'm not expecting out-of-the-box results that can figure out arbitrary functions. But what can we get out of z3 without much work?

For instance, this seems to go through just fine:

from z3 import *

s = Solver()
I = Function('I', IntSort(), IntSort())
x = Int('x')

s.add (ForAll([x], I(x) == 2*x+3))
print(s.check())
print(s.model())

printing:

[I = [else -> 3 + 2*Var(0)]]

But the slightly more complicated:

s.add (ForAll([x], I(x) == If(x<2, 2*x, x+3)))

makes z3 goes into a (seemingly) infinite loop. (Feels like any use of if-then-else is too much.)

Just wondering perhaps this is the case of a missing heuristic? The above skeleton pretty much defines the function itself, so I wonder why the if-then-else ends up causing trouble.

Again, this is mere curiosity and I'd love to hear if you have any quick rules of thumb on what sort of constructs lead to "good performance" when used this way. (I'd totally understand if the answer is anyone's guess!) Cheers!

[NikolajBjorner]

There is a "macro" finder that detects explicit and implicit definitions.
The default implementation does not find it.

There is an entirely new implementation with the tactic "elim-predicates".
https://microsoft.github.io/z3guide/docs/strategies/summary#tactic-elim-predicates
It works in this case.

from z3 import *

s = Solver()
I = Function('I', IntSort(), IntSort())
x = Int('x')

s.add (ForAll([x], I(x) == If(x<2, 2*x, x+3)))

g = Goal()
g.add(s.assertions())
t = Tactic('elim-predicates')
r = t(g)[0]
print(r)

There are many areas where even the new implementation misses macros.
Good macro finders is one area that may be improved based on benchmarking.

The more general problem of function synthesis is not covered by macros.
In the more general setting there is no explicit definition for functions or predicates, but they have solutions.
The Horn clause setting exemplifies such a setting. This direction is more open ended.