C++ 프로그램에서 z3 API 사용에 대한 도움이 필요합니다.

Question

C++ 프로그램에서 z3 API를 사용하고 싶습니다. 내가 포함 할 헤더 파일을 궁금 방법 Z3 기능 등

내가 Z3의 소스 코드와이 파일을 실행하기 위해 오는 example.cpp 파일을보고이 포함 된 프로그램을 실행하기 위해, 나는에 make examples을 실행했다 내부적으로 명령 내가 어떤 프로그램을 만들 경우 지금

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

을 실행 디렉토리를 구축, 나는 다음과 같이 컴파일해야합니까 내 프로그램을 컴파일 할 때마다 (LIB 파일과 ../src/api와 링크를 포함)?

전 z3을 사용한 적이 없습니다. 어떤 도움이라도 대단히 감사합니다. :)

Answer 1

질문에있는 명령 줄은 Z3 예제 응용 프로그램 중 하나에서 사용됩니다. 이 명령 행은 build 디렉토리에서 실행됩니다. 빌드 디렉토리에는 Z3 컴파일 된 라이브러리 인 libz3.so이 들어 있습니다. 이 명령은 응용 프로그램을 컴파일하고 단일 명령으로 연결하기 때문에 복잡해 보일 수 있습니다. 지시문 -I<path-name>은 지정된 디렉토리에 포함 파일을 찾기 위해 g ++에 지시합니다. 마지막으로 Z3 include 파일과 라이브러리를 시스템에 설치하지 않아도 명령을 실행할 수 있습니다.

시스템에 Z3 포함 파일과 라이브러리를 설치하려면 sudo make install을 실행해야합니다. 그런 다음, 우리는 그것을 컴파일하려면

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

를 포함하는 파일 tst.cpp을 만드는 가정, 우리가 사용할 수 있습니다

g++ -c tst.cpp 

링크 및 실행 파일을 생성하기 위해 사용할 수 있습니다

g++ -o tst tst.o -lz3 

마지막으로 실행할 수 있습니다

./tst