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

Question

我想expr从给定的 SMTLIB2 文件创建一个对象。我可以Z3_parse_smtlib_string在 C 示例中看到一个函数。课堂上是否有包装器expr？

Answer 1

Z3 C++ API 没有明确提供此功能作为 expr 类的一部分。但是，C++ API 可以与 C API 一起使用，即函数Z3_parse_smtlib_string（或 ... _file）可以用来实现这一点。请注意，此函数返回 a 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()。