Can I read a SMT2 file into a solver through the z3 c++ interface?

Question

I've got a problem where the z3 code embedded in a larger system isn't finding a solution to a certain set of constraints (added through the C++ interface) despite some fairly long timeouts. When I dump the constraints to a file (using the to_smt2() method on the solver, just before the call to check()), and run the file through the standalone z3 executable, it solves the system in about 4 seconds (returning sat). For what it's worth, the file is 476,587 lines long, so a fairly big set of constraints.

Is there a way I can read that file back into the embedded solver using the C++ interface, replacing the existing constraints, to see if the embedded version can solve starting from the exact same starting point as the standalone solver? (Essentially, how could I create a corresponding from_smt2(stream) method on the solver class?)

They should be the same set of constraints as now, of course, but maybe there's some ordering effect going on when they are read from the file, or maybe there are some subtle differences in the solver introduced when we embedded it, or something that didn't get written out with to_smt2(). So I'd like to try reading the file back, if I can, to narrow down the possible sources of the difference. Suggestions on what to look for while debugging the long-running version would also be helpful.

Further note: it looks like another user is having similar issues here. Unlike that user, my problem uses all bit-vectors, and the only unknown result is the one from the embedded code. Is there a way to invoke the (get-info :reason-unknown) from the C++ interface, as suggested there, to find out why the embedded version is having a problem?

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2017-01-27T02:35:16

You can use the method "solver::reason_unknown()" to retrieve explanations for search failure. There are methods for parsing files and strings into a single expression. In case of a set of assertions, the expression is a conjunction. It is perhaps a good idea to add such a method directly to the solver class for convenience. It would be:

    void from_smt2_string(char const* smt2benchmark) {
        expr fml = ctx().parse_string(smt2benchmark);
        add(fml);
    }

So if you were to write it outside of the solver class you need to:

      expr fml = solver.ctx().parse_string(smt2benchmark);
      solver.add(fml);

Can I read a SMT2 file into a solver through the z3 c++ interface?

1 Answers