question(C/C++ API examples): string to expression conversion on traversing AST

[matu3ba]

Maybe I misinterpret the C and C++ API, but I could not find a way to add functions to be later filled with simple expressions, ie when traversing an AST via Visitor pattern for renaming etc according to stongest postcondition (+LBE).

Say we have (and (< x y) (< x z)).

1. When we traverse and see and. How can we generate a symbolic function land r for the lefthand and righthand side of and?
2. How can we assign expressions or functions to those symbolic functions land r?
3. What is the reason not to offer expression generation from strings? Is the arity and semantic not well enough defined?

My understanding how to parse expressions from strings looks roughly like the following:

1. define necessary sorts (sorted domains that express variable valuations)

    context c;
    sort_vector sorts(c);
    func_decl_vector decls(c);
    std::map<std::string, sort> varmap;
    varmap.emplace("b", c.bool_sort());

2. define possible expressions types as function with variable domains

decls.push_back(c.function("a", 0, 0, varmap["b"]));

3. parse the string in SMTlib2 format

    expr_vector a = c.parse_string("(assert a)", sorts, decls);

Does this mean that

1. I can not use visitor pattern, because I must traverse bottom-up (to build all basic expressions for later usage),
2. I must always provide the variables upfront, because z3 cant figure variable types via lookup on its own?

Any example how to efficiently traverse a simple AST would be appreciated. From what I understand, I must reverse the AST to apply visitor on an according bottom-up representation or keep explicitly track or dump everything into a string and rename it.

related answer

[matu3ba]

After tinkering around, I think collecting everything and dumping a string is easier. Would be great, if documentation would be more explicit about how to do dynamic stuff.

I dont understand the design decision to require Lisp-like strings and then not offer an according AST-API.

[NikolajBjorner]

I have not fully understood the questions and comments in the post yet so find it somewhat difficult to answer.
It seems there are different expectations.

SMTLIB2 is a standard format for exchanging benchmarks. Z3 supports this format and exposes parsers for benchmarks in this format.
The basic structure of and SMTLIB2 benchmark is a sequence of commands. Each command has an effect on a solver state.
We therefore expose SMTLIB2 parsers for solver objects.

Expression parsing can be built in an indirect way using these commands, but it isn't first class.
I have heard before that users somehow want to create expression strings and parse them into objects, but the need to serialize in and out of strings to build expressions programmatically seems to quickly fade with experience of using the programmatic API.
The programmatic API lets you build and traverse expressions, program your visitor patterns etc. The primitives are creating expressions, and decomposing expressions. Since tree traversal is such a common use case, there is also a little sample suggesting how you can traverse expressions:

from __future__ import print_function
from z3 import *

def visitor(e, seen):
    if e in seen:
        return
    seen[e] = True
    yield e
    if is_app(e):
        for ch in e.children():
            for e in visitor(ch, seen):
                yield e
        return
    if is_quantifier(e):
        for e in visitor(e.body(), seen):
            yield e
        return

x, y = Ints('x y')
fml = x + x + y > 2 
seen = {}
for e in visitor(fml, seen):
    if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED:
        print("Variable", e)
    else:
        print(e)

The main message of the example is that there are functions to test the kind of the expression and to get immediate sub-expressions.
And noteworthy, sub-expressions may be shared so you should better perform a DAG traversal because tree traversals leads to re-examining shared structures.