How to run Z3 in Java from SMT-Lib standard?

问题:

Up to now, I can run Z3 to get solution of equations in cmd on Window:

z3 -smt2 path_smt_lib_file

But how I can run Z3 with SMT-Lib standard input in Java. Thank in advance.

回答1:

You should be able to find all you need in JavaExample.java in the folder examples/java.

Check out the API. In particular, if you want to read an SMT2 file, see Context.parseSMTLIB2File().