Z3 Java API. Reading SMTLib2 and exending it

Question

I am trying to read a common SMTLib2 file by the Java API of Z3 using the following method:

BoolExpr parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)

The issue is that it seems that it only reads the assertions and ignores the rest. So one cannot add a new assertion based on a sort that is defined in the file. The sort is unknown and the addition of the assertion fails.

Is there any way to do this that I miss?

If not, it seems that I should directly generate SMTLib2 format instead of using the API.

Thanks for your consideration.

Answer 1

That's correct, this function returns one expression that is the conjunction of all assertions in the file, ignoring (almost) all other file content. There is no function for reading SMT2 commands as that is usually done outside of Z3.

That said, parseSMTLIB2String takes the parameter sorts, which can be populated by sorts later referred to in the SMT2 file. This can be used such that the SMT2 file and the rest of your infrastructure refer to the same sorts.