0

I want to use api_parsers in z3 api to parse smt2 commands and then I want to see the contents of resulted vectors(like sorts, variables, params , ...).

but I don't how? I write a piece of code like below:

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

and run it in ubuntu( I have installed z3 in ubuntu earlier)and then I received errors like this after running command: g++ -o parser_api z3_api_parser_tst.cpp

Error

how can I acheive my goal? is my code appropriate for this?

Community
  • 1
  • 1
Mary
  • 55
  • 1
  • 8
  • Possible duplicate of: https://stackoverflow.com/questions/12573816/what-is-an-undefined-reference-unresolved-external-symbol-error-and-how-do-i-fix – Galik Apr 10 '16 at 11:47

1 Answers1

1

This looks like standard linking errors. You need to link with z3lib/libz3. Your call to the parser is otherwise right.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15