z3 api C++を使用してsmt2コマンドを解析する方法は？

Question

私はsmt2コマンドを解析するためにz3 apiにapi_parsersを使いたいと思っています。その結果、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にリンクする必要があります。 そうでない場合は、パーサへの呼び出しが正しく行われます。