如何使用 Z3 C++ api 读取 smtlib2 字符串？

Question

我想从给定的 SMTLIB2 文件创建一个 expr 对象。我可以在 C 示例中看到 Z3_parse_smtlib_string 函数。 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() 来实现。