simple string-based API ?

[pcarbonn]

Regularly, I wish Z3 would expose a string-based API that would allow me to write a Python program like this:

with session():
    send("(declare-const p Bool)")
    send("(assert (and p (not p)))")
    out = send("(check-sat)")
    if out == "sat":
        ....

In other words, I would send SMTLib2 statements, and get a string result.

I would think it is easy to develop such an API on top of the existing SMTLib2 support. It would then be possible to build a REPL for Z3 (e.g., for education). If every SMT solver supported this API, it would be straightforward to build portfolio solvers.

The performance impact of using string should be minimal. Are there any drawbacks I'm missing?

[NikolajBjorner]

Try the following change to z3.py or something similar outside

def send(cmd, ctx=None):
      ctx = _get_ctx(cx)
      return Z3_eval_smtlib2_string(cmd, ctx.ref())