如何使用 Z3 C++ api 读取 smtlib2 字符串? [英] How to read smtlib2 strings using Z3 C++ api?

问题描述

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

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?

推荐答案

Z3 C++ API 没有明确提供此功能作为 expr 类的一部分.但是，C++ API 可以与 C API 一起使用，即可以使用函数 Z3_parse_smtlib_string(或 ..._file)来实现这一点.请注意，此函数返回一个 Z3_ast，必须将其转换为 expr 对象才能返回 C++世界".

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".

一个简单的例子:

#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() 来实现.

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().

这篇关于如何使用 Z3 C++ api 读取 smtlib2 字符串?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！