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())

[pcarbonn]

Thanks ! It works.

Here is a working example:

from z3 import Z3_eval_smtlib2_string, Context

def send(cmd, ctx):
    return Z3_eval_smtlib2_string(ctx.ref(), cmd)

ctx = Context()
send("(declare-const p Bool)", ctx)
send("(assert (and p (not p)))", ctx)
print(send("(check-sat)", ctx))

[pcarbonn]

On the other hand, if I declare p using the python API in the same context, the send does not work anymore:

from z3 import Z3_eval_smtlib2_string, Context, Const, BoolSort

def send(cmd, ctx):
  return Z3_eval_smtlib2_string(ctx.ref(), cmd)

ctx = Context()
p = Const("p", BoolSort(ctx))
send("(assert (and p (not p)))", ctx)
print(send("(check-sat)", ctx))

Result:

Traceback (most recent call last):
  File "main.py", line 11, in <module>
    send("(assert (and p (not p)))", ctx)
  File "main.py", line 5, in send
    return Z3_eval_smtlib2_string(ctx.ref(), cmd)
  File "/home/runner/smtlib/.pythonlibs/lib/python3.10/site-packages/z3/z3core.py", line 3506, in Z3_eval_smtlib2_string
    _elems.Check(a0)
  File "/home/runner/smtlib/.pythonlibs/lib/python3.10/site-packages/z3/z3core.py", line 1505, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 1 column 14: unknown constant p")\n'

Am I doing something wrong ?