How to do mixing of multiple string inputs with C or C++ api?

[davedets]

I've been banging my head agaist this problem for a couple of days; thought I'd see if anyone has a solution.

I'm trying to write a program verification system (for C++), using Z3 to do the theorem-proving. This would have three kinds of Z3 input:

• a fairly large set of Z3 definitions (sorts, functions) in support of the language semantics.
• Programmer written Z3 definitions in support of particular verifications (e.g., a predicate expressing that some slice of an array is sorted).
• Verification conditions created by the verification system.

I would ideally like to do the first two by passing the text representation to Z3. The third would be done via the C++ interface.

My problem is that this just doesn't seem to work. At first I was just looking at the C++ interface, and saw parse_string. I assume this would have side effects on the Z3_context, declaring things. But doing multiple calls to parse_string doesn't work the way I thought it would; things defined in the first string are not defined in the second.

I thought this variant might be relevant:

    expr_vector parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);

but I couldn't figure out a way to do one parse_string and retrieve the sorts and decls.

So I looked Z3_api.h, and got excited by Z3_eval_smtlib2_string, which seemed more like what I was looking for. And, indeed, if I do two calls to this, the first with

(define-fun inc ((i Int)) Int (+ i 1))
and the second with:

            (push)
            (assert (not (forall ((j Int)) (> (inc j) j))))
            (check-sat)
            (pop)

The check-sat yields unsat, as expected.

However, I'm still stuck: I can't figure out how to get the C++ API to recognize the definitions done in the Z3_eval_smtlib2_string calls. If I try to do the second call described above via the C++ interface, as in:

  z3::context c;
  c.set_enable_exceptions(false);
  z3::solver solv(c);

  std::string s1 =
    Z3_eval_smtlib2_string(c, "(define-fun inc ((i Int)) Int (+ i 1))");

  auto x = c.int_const("x");
  auto inc = c.function("inc", c.int_sort(), c.int_sort());
  auto body = inc(x) > x;
  auto pred = z3::forall(x, body);
  solv.add(!pred);
  auto res = solv.check();
  std::cerr << "QQQ: res is "
            << (res == z3::sat ? "sat"
                               : (res == z3::unsat ? "unsat" : "unknown"))
            << "\n";

I get sat as the result!

I assume the problem is that the

auto inc = c.function("inc", c.int_sort(), c.int_sort());

creates a new, undefined function named "inc" instead of looking up the previously-function with that name. To convince myself of this, and that I wasn't going crazy, I substited this version for "body", essentially inlining the definition of "inc":

auto body = (x + c.int_val(1)) > x;
That correctly got unsat.

So, I'm stuck, wondering whether it's possible, in the C or C++ apis, to create a function application that applies a function defined in a previous call to Z3_eval_smtlib2_string. So far I haven't figured anything out.

I'm investigating whether it's possible to do this completely in the C or C++ apis. The C++ api doesn't seem to have a way to give a func_decl a body. The C api does (Z3_add_rec_def) -- but, AFAICT, this forces everything to use the C api, which would be unfortunate. I'll probably try to complete the small experiment with C api, see if that works.

But I'm hoping against hope that someone will point out a misunderstanding I've had, and how this is actually simple :-)...!

[davedets]

I realized after writing this that I ought to be able to use Z3_eval_smtlib2_string, which seems to have the semantics I desire (that a sequence of calls to it with strings s1, ..., sn, is like a single call with the concatenation of the si) to do what I want. Where I would do C/C++ API, calls, just convert what I want to do to a string and call Z3_eval_smtlib2_string. But this doesn't quite work. Because Z3_eval_smtlib2_string takes only a Z3_context as argument, not a Z3_solver. I guess it creates a solver whose lifetime is the duration of the call? In any case, this sequence of calls (where c is a Z3_context):

  std::string s1 =
      Z3_eval_smtlib2_string(c, "(define-fun inc ((i Int)) Int (+ i 1))");
  std::string s2 = Z3_eval_smtlib2_string(
      c, "(push) "
         "(assert (not (forall ((j Int)) (> (inc j) j)))) "
         "(check-sat) "
         "(pop)");

yields the desired "unsat" result, while this one (where s is a solver with c as a context):

  std::string s1 =
      Z3_eval_smtlib2_string(c, "(define-fun inc ((i Int)) Int (+ i 1))");
  s.push();
  std::string s2 = Z3_eval_smtlib2_string(
      c, "(assert (not (forall ((j Int)) (> (inc j) j)))) ");
  std::cerr << "QQQ: s2 = " << s2 << "\n";
  auto res = s.check();
  s.pop();

does not; res is sat. Which is obvious in retrospect, because the Z3_eval_smtlib2_string call didn't mention s.

This is a problem, because I'd really like to be able to query the model of the solver, treating it something like a debugging session. I can't do that with the first form above, the one that works. So I'm back to tearing my hair out...

[NikolajBjorner]

eval_smtlib2_string creates an internal solver.
It's life-time extends the first call.
So you can call it again, passing a "(check-sat)" and get the result you want.
You can also pass "(push)" and "(pop)".
There is no connection with solver objects you create and eval_smtlib2_string.

[davedets]

Thanks for rersponding!

So you can call it again, passing a "(check-sat)" and get the result you want.

I understand that you can get the sat/unsat/uknown result (by parsing the string returned by eval_smtlib2_string. But in the case of an unsuccessful proof (a "sat" result for asserting the negated predicate), I'd like to be able to access the values of various variables in the satisfying model. I guess I could do that by redoing the proof when it fails, with a "script" that gets the model, and then evals various the variables I care about, parsing the string results. But that is, at the very least, a bit inconvenient.

[davedets]

Do I understand correctly that this means there's no way to make an assertion in one call to eval_smtlib2_string that is necessary for the proof of a negated assertion in a second call to eval_smtlib2_string? This is the fundamental problem I'm wrestling with. I'd like to be able to proof lemmas (prove them, then assert them) that the user writes.

How would you feel about an extension to Z3_context: a method to creat a "current solver" of the context, one that is used, if it exists, in Z3_eval_smtlib2_string calls. (Rather then one created for the lifetime of that call.) I guess this would mean that you'd have to add an extra error check, that Z3_eval_smtlib2_string calls leave the push/pop depth unchanged. The would also be an accessor to yield this solver from the context if it exists.

We'd also add an analog of Z3_eval_smtlib2_string to the C++ API.

With that, I could do what I'm trying to do. I would do the push from the C++ interface, then call evalString on a string with just the assertion. Then I'd do check_set from the C++ api, and query the model as needed for a failed proof. Then pop from the C++ api.

(If you think this would be valuable, I'd be happy to try to do a PR.)

[NikolajBjorner]

The C++ api doesn't seem to have a way to give a func_decl a body.

Missing functionality can be added to the C++ API. Or you can call C API functions directly from C++ (with appropriate reference counting).

[NikolajBjorner]

Do I understand correctly that this means there's no way to make an assertion in one call to eval_smtlib2_string that is necessary for the proof of a negated assertion in a second call to eval_smtlib2_string?

I think I am trying to say the opposite.
For example, this minimal mcp server is stateful.

https://github.com/Z3Prover/z3/blob/master/src/api/mcp/z3mcp.py

[davedets]

Ah, thanks! This cleared up some of my confusion. I'm going to explain my confusion in detail, and the resolution, for future readers of this thread. I thought I still had a problem, but then I finally found the function I should have been looking for in the C++ API.

Confusion and resolution:

I had gotten confused by the fact that add, which one uses to make assertions, is a method of the solver class of the C++ api. And the fact that Z3_solver_assert takes a Z3_solver in the C api. I'd thought that these two kinds of state, the context and the solver, were separate, and that the solver had the assertions.

But apparently they are not separate. First, as one would expect, passing this string:

  std::string kInput = "(declare-const x Int) "
    "(assert (> x 10)) "
    "(assert (< x 8)) "
    "(check-sat)";

to Z3_eval_smtlib2_string correctly yields unsat. I thought that breaking this into two strings:

  std::string kInput1 = "(declare-const x Int) "
                        "(assert (> x 10)) ";

  std::string kInput2 = "(assert (< x 8)) "
                        "(check-sat)";

and making two calls with these strings would yield sat, thinking that the first call would side-effect the context with the decl of x, making the (< x 8) assertion syntactically valid, but that the assertion would be in the internal solver, and lost after the first call.

But no! When I do this, I get unsat for the check-sat, just as with the single-call case (exactly as your comment would indicate.)

To clear up my mental model, previously in this discussion you said:

eval_smtlib2_string creates an internal solver.
It's life-time extends the first call.

Communication is hard; the second sentence isn't 100% correct english, and I decided you meant "extends to the end of the first call." I think now maybe you meant "extends beyond the first call." That is, it when it creates the internal solver, it saves it (in the context I guess?), and uses it for subsequent eval_smtlib2_string calls? Could you confirm or deny?

Remaining problem, and (finally!) solution.

If this is correct, then you've already done half of what I proposed: the "current solver" already exists. The problem is that this solver is private, I guess to Z3_context. I need it to be able to allow the programmer to debug failed proofs, but getting and querying the model.

Finally I realized that in the C++ api z3::solver has the method from_string. This seems to do what I want -- execute arbitrary z3 commands in a solver, saving the resulting state for future such calls, in a way where the the solver is available in the C++, to get a model for failed proofs.

I wish I'd noticed this sooner :-)!

FWIW, I found the description of the corresponding function in the C api, Z3_solver_from_string, a little bit misleading. It says: "load solver assertions from a string." Which I originally read as deliberately separating solver assertions from definitions. But that is not the case.

Thanks very much for taking the time to help me work through this!