我想在api_parsers中使用z3 api来解析smt2命令，然后我要查看生成的vectors的内容（如排序，变量，参数...）。
但我不怎么？我写了一段如下代码：
#include<iostream>
#include<z3++.h>
#include<z3_api.h>
using namespace z3;
int main() {
context ctx;
//z3_string fname = ;
Z3_ast a = Z3_parse_smtlib2_file(ctx, "smt_z3.smt2", 0, 0, 0, 0, 0, 0);
expr e(ctx, a);
std::cout << "result = " <<e << std::endl;
return 0;
并在ubuntu中运行它（我之前已经在ubuntu中安装了z3），然后在运行以下命令后收到如下错误：
g++ -o parser_api z3_api_parser_tst.cpp我如何实现我的目标？我的代码适合这个吗？
最佳答案
这看起来像是标准链接错误。您需要链接到z3lib / libz3。
否则您对解析器的调用是正确的。
关于c++ - 如何使用z3 api c++解析smt2命令？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/36529258/