CODEWITHSUNDEEP
compilationg++z3theorem-proving
user2347029
user2347029

Reputation: 21

Need help in using z3 API in a c++ program

I want to use z3 API in my C++ program. I am wondering which header files to include and how to run a program which contains z3 functions etc.

I saw the example.cpp file which comes with z3 source code and in order to run this file, I had to run make examples in the build directory which internally executed the command

g++ -o cpp_example  -I../src/api -I../src/api/c++ 
    ../examples/c++/example.cpp libz3.so -lpthread -fopenmp -lrt

Now if I create any program, do I need to compile it like this (include ../src/api and link with lib files) every time I need to compile my program?

Please help me, I have never used z3 before. Any help is greatly appreciated. :)

Upvotes: 1

Views: 2807

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The command-line in your question is used in one of the Z3 example applications. This command line is executed in the build directory. The build directory contains the Z3 compiled library: libz3.so. The command may seem complicated because it is compiling and linking the application with a single command. The directive -I<path-name> instructs g++ to look for include files in the given directory. Finally, the command can be executed even if we do not install the Z3 include files and library in the system.

To install the Z3 include files and library in our system, we should execute sudo make install. Then, assume we create a file tst.cpp containing

#include<iostream>
#include<z3++.h>
using namespace z3;

int main() {
    context c;
    expr x = c.int_const("x");
    std::cout << x + 1 << "\n";
    return 0;
}

To compile it, we can just use:

g++ -c tst.cpp

To link and generate the executable, we can use:

g++ -o tst tst.o -lz3

Finally, we can execute it

./tst

Upvotes: 6

Related Questions