mirror of
https://github.com/Z3Prover/z3
synced 2025-08-22 11:07:51 +00:00
31 lines
897 B
Text
31 lines
897 B
Text
TPTP front-end and utilities as a sample using the C++ bindings.
|
|
To build the example execute
|
|
make examples
|
|
in the build directory.
|
|
|
|
This command will create the executable tptp.
|
|
On Windows, you can just execute it.
|
|
On macOS and Linux, you must install z3 first using
|
|
sudo make install
|
|
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS)
|
|
with the build directory. You need that to be able to
|
|
find the Z3 shared library.
|
|
|
|
The sample illustrates using Z3 from the TPTP language.
|
|
The TPTP language is documented on http://tptp.org
|
|
It also exposes utilities for converting between SMT-LIB
|
|
and TPTP format.
|
|
|
|
|
|
Custom build with CMAKE:
|
|
|
|
Build instructions:
|
|
|
|
1. cd z3
|
|
2. mkdir release
|
|
3. cd release
|
|
4. cmake3 -DZ3_BUILD_LIBZ3_SHARED=FALSE -DCMAKE_BUILD_TYPE=RelWithDebInfo -G "Unix Makefiles" ../
|
|
5. make
|
|
6. make z3_tptp5
|
|
7. cp examples/tptp_build_dir/z3_tptp5 ../../bin/z3_tptp
|
|
|