Java API push and pop for smt2 file

Question

I have generated an smt2 file which is already successfully read (parsed) by Z3 (4.3) via Z3 Java APIs. Now I would like to know that how to make Z3 start to solve formulas in multiple scopes (push and pop). The smt2 file contains a list of push and pop commands.

I know you can use solver.push() and solver.pop() to do that, but the issue here is the scopes are already generated in the file and I am not using Z3 internal APIs to make these formulas and scopes. I just need to feed the entire smt2 file to Z3 and perform multiple solving (only this part I need Z3 APIs). By simply calling solver.check() method seems Z3 just completely ignores all the scopes in the middle of the smt2 file, and only gives me the model for the last (check-sat) command.

So is there a way of calling Z3 APIs (Java) to perform a series of solving for multiple scopes defined in an existing smt2 file ?

Any concrete examples will be very appreciated.

Answer 1

No, there is no way to do that. The parser functions can read the input file, but they ignore all SMT commands, i.e., the output is always only a set of assertions, nothing else.

In your use-case where you're working with files, the recommended procedure would be to pipe the files into Z3, either by directly providing a filename or by piping them into stdin.