wie smt2 Befehle mit z3 API C++ zu parsen?

Question

Ich möchte api_parsers in z3 api verwenden, um smt2 Befehle zu analysieren, und dann möchte ich den Inhalt der resultierenden vectors (wie Sortierungen, Variablen, Parameter, ...) sehen.

aber ich weiß nicht wie? Ich schreibe ein Stück Code wie unten:

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

und führen Sie es in ubuntu (I z3 in ubuntu früher installiert haben) und dann erhielt ich Fehler wie dies nach dem Ausführen-Befehl: g++ -o parser_api z3_api_parser_tst.cpp

Wie kann ich mein Ziel erreichen? ist mein Code dafür geeignet?

Answer 1

Dies sieht wie Standardverknüpfungsfehler aus. Sie müssen mit z3lib/libz3 verlinken. Ihr Aufruf an den Parser ist sonst richtig.