Is a PythonAPI for z3str3 available?

[swag2198]

[This is less of an issue and more of a beginner trying to use z3str3 for a problem.]
I am trying to solve a set of string constraints over one or more string variables, like this one having 2 string variables x and y:

len(x) <= 3
x[0:1] == "a"
y[2:4] is uppercase regex

Ideally, I would like to know if there is any solution to the set of constraints (sat/unsat) and if there are any, any random satisfying assignment to x and y would suffice. For example here, x = "ab" and "y=avSWac" is a satisfying assignment to the variables. Preferably, I wish to do this in python but C++ is also fine.

I realize these constraints are handled by z3str3 as expressed in the input language description here. But I am new to z3 and z3str3 and I am not able to find any python API handling string variables and constraints. My questions are:

• Does there exist a python API handling string-related things like the numerical/real one?
• Where can I find an end-to-end example solving a string problem (say my example above) in Python or C++?

I am really lost in this repository and cannot find a starting point to use the code or the examples. Any help will be really appreciated.

Thank you.

[NikolajBjorner]

The String API functions start here:

z3/src/api/python/z3/z3.py

Line 10556 in da154b2

#########################################

You will find doc strings, such as

z3/src/api/python/z3/z3.py

Line 10782 in da154b2

def PrefixOf(a, b):

There are two backend solvers for strings in z3. The default is set to seq, the z3str3 is also available if you set the option smt.string.solver=z3str3 (from python it is "set_param("smt.string.solver","z3str3")). Note that z3str3 is currently cannot be characterized as supported.

[swag2198]

Thank you for the pointer in the code. I am sorry but could you kindly elaborate on Note that z3str3 is currently cannot be characterized as supported.?
And another clarification, for my example problem, I assume the default solver seq is able to solve it, right?

[NikolajBjorner]

GitHub issues have not been fixed and there is no support for a long time.