z3 api C++ kullanarak smt2 komutlarını nasıl ayrıştırılır?

Question

z3 api numaralı smt2 komutlarını ayrıştırmak için kullanmak istiyorum ve daha sonra vectors (sıralar, değişkenler, params, ... gibi) sonuçlarının içeriğini görmek istiyorum.

ama nasıl yapmıyorum? (Daha önce ubuntu Z3 yüklemiş) ve daha sonra ben çalışan komutundan sonra böyle hatalar alınan

#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; 

ve ubuntu içinde çalıştırmak: g++ -o parser_api z3_api_parser_tst.cpp

aşağıda gibi bir kod parçası yazmak

Hedefime nasıl ulaşabilirim? benim kodum buna uygun mu?

Answer 1

Bu, standart bağlantı hataları gibi görünüyor. Z3lib/libz3 ile bağlantı kurmanız gerekiyor. Ayrıştırıcıya yapılan çağrınız başka türlü doğru değil.