我想创建一个expr从给定SMTLIB2文件对象。 我可以看到一个Z3_parse_smtlib_string在C实例函数。 有没有，在一个包装expr类？
Answer 1:
Z3的C ++ API没有明确规定这个功能的EXPR类的一部分。 然而，C ++ API可以沿着C API，即，该函数被用于Z3_parse_smtlib_string （或... _file ）可用于实现这一目标。 请注意，这个函数返回一个Z3_ast ，必须转换为expr对象要回C ++的“世界”。
一个简单的例子：
#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;
由于Z3_parse_smtlib2_*函数不执行错误检查，也不例外会在错误被抛出。 这可以通过调用来实现context::check_error()
文章来源: How to read smtlib2 strings using Z3 C++ api?
