C++20 Arithmetic Expression Library on Z3 Booleans and Bit Vectors
Minimum requirements this project is guaranteed to work with:
- LLVM Clang Compiler (v11.0.0)
- CMake (v3.13.4)
- Z3 Theorem Prover (v4.8.9), available by source through a git submodule
Clone the repository and its submodule:
git clone https://github.com/superbr4in/formulae1.git
cd formulae1
git submodule update --init
Configure and compile the source code:
mkdir build
cd build
cmake .. -D"CMAKE_BUILD_TYPE=Release" -W"no-dev"
make formulae1 -j $(nproc)
Find libformulae1.so
in source/formulae1/
.
Run the tests (requires Catch2):
make formulae1_test
./test/formulae1/formulae1_test
Use a CMakeLists.txt
file to integrate the library into another project:
# Older versions may work as well but are not tested
cmake_minimum_required(VERSION 3.13)
# Choose the directory this repository has been cloned into
add_subdirectory(formulae1)
...
# All header files will become available automatically
target_link_libraries(<some-project> PUBLIC formulae1)
See the official CMake documentation for further explanations and more options.