How to read smtlib2 strings using Z3 C++ api?
z3
Solution
The Z3 C++ API does not explicitly provide this functionality as part of the expr class. However, the C++ API can be used alongside the C API, i.e., the function `Z3_parse_smtlib_string` (or ...`_file`) can be used to achieve this. Note that this function returns a `Z3_ast`, which must be converted to an `expr` object to get back to the C++ "world".
A simple example:
#include <z3++.h>
...
context ctx;
Z3_ast a = Z3_parse_smtlib2_file(ctx, "test.smt2", 0, 0, 0, 0, 0, 0);
expr e(ctx, a);
std::cout << "Result = " << e << std::endl;
Since the `Z3_parse_smtlib2_*` functions do not perform error checking, no exception will be thrown upon errors. This can be achieved by calls to `context::check_error()`.
Problem
I want to create an `expr` object from a given SMTLIB2 file. I can see a `Z3_parse_smtlib_string` function in the C examples. Is there a wrapper for that in the `expr` class?