unsat cores from APIs

Question

I know parseSMTLIB2File Java API ignores certain commands in an SMT2 file. However, is there a way around it? I am generating smt2 files and use parseSMTLIB2File and solver.check() to parse and solve the constraints.

Now, I would like to use the unsat cores from the solver for some computation. I know I probably can do it using std in and out (here). However, this will be very inefficient for running the algorithms. Further, it is also not ideal to change the entire code base to switch every constraint generation through Z3 Java APIs.

Since the native C++ interface handles options and (tracked) assertions well. Hence, is there any way around it? How can I do this programmatically and efficiently?

Do other C++/C/Python parseSMTLIB2File APIs perform the same thing as Java's or they may read in additional things.

Answer 1

is there a way around it?

No. parseSMTLIB2File is not a complete interface to the solver, and it's not intended to be. The only options are to switch to the full API interface, or to the full text interface by emitting .smt2 files and passing those to Z3. The latter can be done via pipes instead of actual files, and many users are happy with the performance of that.