Obtaining the computed patterns for quantifiers from the API

[Philipp15b]

Hello all,

Is it possible to obtain the automatically computed patterns for quantifiers from the C API? I am creating formulas via the API and would like to be able to print the computed quantifier patterns to the user of my tool for debugging.
As far as I can tell, there are only APIs to create quantifiers with explicitly added patterns, not retrieve those which Z3 infers.

Thanks for the help!

[NikolajBjorner]

There isn't a self-contained way to get these patterns.
They get compiled within the solvers. You can retrieve assertions after a solver has run for a little while (set max-conflicts to bound time in search).

from z3 import *
s = SimpleSolver()
f = Function('f', IntSort(), IntSort(), IntSort())
g = Function('g', IntSort(), IntSort(), IntSort())
x, y = Ints('x y')
s.add(ForAll([x,y], f(x,y) == g(x,y)))
set_option(verbose=10)
s.set("smt.max_conflicts", 0)
print(s.check())
for f in s.assertions():
    print(f)
    for i in range(f.num_patterns()):
        print(f.pattern(i))