Version 1.0
make
./out/tym
e.g., ./out/tym -i tests/4.test
The -v flag activates verbose output.
To build with backend solver support (to use Z3)
define TYM_Z3_PATH to point to Z3's installation directory when calling make:
TYM_Z3_PATH=${Z3_PATH} make.
When running the resulting binary, remember to indicate where to find Z3's dynamically-liked library (libz3.dylib on macOS -- or the .so analogue on Linux).
For example, DYLD_LIBRARY_PATH=z3-4.5.0-x64-osx-10.11.6/bin/ ./out/tym -f smt_solve -m fact -i tests/4.test -q "e(X)."
Use -f c_output to translate a Datalog program to C, then use tymc.sh
to compile and link it with Tym, to produce a standalone executable from your
original program. Use the CFLAGS environment variable to instruct tymc on
-L and -I parameters to find Tym's binaries and headers.
LGPL v3 or any later version (see LICENSE).
Nik Sultana