How to efficiently obtain the uninterpreted elements of an expression

[TodAmon]

I'm using the python API. One can obtain a string representation for an expression very quickly. However, obtaining the uninterpreted elements of an expression is horribly inefficient the way I am doing it. Here is an example:

(Pdb) f = z3.Int('x') + z3.Int('y') + z3.If(z3.Int('a') < 5, 0, 1)
(Pdb) all_uninterpreted_set(f)
{ x, a, y}

Where all_uninterpreted_set uses 'children' to walk the ast:

def all_uninterpreted_helper(f, accumulation_set):
    if f.decl().kind() == z3.Z3_OP_UNINTERPRETED:
        accumulation_set.add(f)
    else:
        for child in f.children():
            all_uninterpreted_helper(child,accumulation_set)

def all_uninterpreted_set(f):
    results = set()
    all_uninterpreted_helper(f, results)
    return results

This works just fine on small things... but on large expressions it quickly grinds to a complete halt... does the Python API support ways to obtain metrics or contents of an expression? Is this easy to accomplish using C ? Thanks for any assistance. I'm thinking I've missed a better way of doing this.

[NikolajBjorner]

• it is much faster to use the z3.Z3_xyz functions directly.
  • look at z3.py for the functions you use and see what they call.
• for expressions with shared sub-terms you want a hash-table to avoid traversing the same sub-expressions multiple times.
• instead of using f.children() use f.num_args() and f.arg(i) to bypass time spent creating a vector.