ILAng requires CMake (3.8 or above) and compilers with CXX11 support. To install dependencies on Debian-based UNIX:
apt-get install bison flex libboost-all-dev z3 libz3-dev
To install dependencies on OSX:
brew install bison flex boost boost-python z3
- The z3 SMT solver (over 4.4.0) is required. Detailed instruction for building latest z3 can be found here.
- The Boost package is required only for building the synthesis engine and the Python API.
To build ILAng with default configuration, create a build directory and execute:
mkdir -p build && cd build
cmake ..
make -j$(nproc)
After the build complete, run unit tests and install the library.
make run_test
sudo make install
- Use
-DILANG_FETCH_DEPS=OFF
to disable config-time updating submodules for in-source dependencies. - Use
-DILANG_BUILD_TEST=OFF
to disalbe building the unit tests. - Use
-DILANG_BUILD_SYNTH=OFF
to disable building the synthesis engine. - Use
-DILANG_INSTALL_DEV=ON
to enable installing working features.
You can use the ilang::ilang
interface target in CMake.
This target populates the appropriate usage requirements for include directories, linked libraries, and compile features.
To use the ILAng library, ilang++.h
is the file to include.
(This does not include working features.)
// cxx source
#include <ilang/ilang++.h>
void foo () {
auto m = ilang::Ila("new_ila_model");
}
To use the ILAng library from a CMake project, you can locate it directly with find_package()
and use the namespaced imported target from the generated package configuration:
# CMakeLists.txt
find_package(ilang REQUIRED)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilang::ilang)
ILAng also supports embedded build, but is not recommended due to its size.
To embed the library directly into an existing CMake project, place the entire source tree in a subdirectory and call add_subdirectory()
in your CMakeLists.txt
file:
# CMakeLists.txt
add_subdirectory(ilang)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilang::ilang)
To allow your project to support either an externally installed or an embedded library, you can use the following pattern:
# Top level CMakeLists.txt
project(MY_PROJ)
...
option(MY_PROJ_USE_EXTERNAL_ILANG "Use an external ILAng library" OFF)
...
add_subdirectory(externals)
...
add_library(my_proj ...)
...
target_link_libraries(my_proj PRIVATE ilang::ilang)
# externals/CMakeLists.txt
...
if(MY_PROJ_USE_EXTERNAL_ILANG)
find_package(ilang REQUIRED)
else()
add_subdirectory(ilang)
endif()
...
externals/ilang
is then a complete copy of this source tree, if enabled.
An docker image with the ILAng platform and all dependencies can be fetched from Docker Hub.
docker pull byhuang/ilang:latest
Once the container is initiated, run
source init.sh
to initialize the environment settings. This docker image also contains the model checker CoSA with the SMT solvers z3 and Boolector.