如何使用z3 api C++解析smt2命令？

Question

我想用中的api_parsers解析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

我該如何實現我的目標？我的代碼是否適合這個？

Answer 1

這看起來像標準鏈接錯誤。您需要鏈接到z3lib/libz3。 您對解析器的調用是正確的。