Forked repository of the AE-VAL Skolemizer, enhanced with support for nondeterministic synthesis. To build from source, use the installation guide below. Otherwise, you can download a pre-built binary from the releases page.
Compiles with gcc-5 (on Linux) and clang-700 (on Mac). Assumes preinstalled Gmp and Boost (libboost-system1.55-dev) packages.
cd aeval ; mkdir build ; cd buildcmake ../maketo build dependencies (Z3 and LLVM)maketo build AE-VAL
The binary of AE-VAL can be found in build/tools/aeval/.
Each benchmark is split into two files (for the universal and the existential parts of the formula). AE-VAL either returns Valid (with a skolem) or Invalid. Collection of the formulas can be found at bench/tasks/ and the expected skolems at bench/skolems/.
For example, if AE-VAL is run with the following input:
./build/tools/aeval/aeval bench/tasks/fast_1_e8_747_extend_s_part.smt2 bench/tasks/fast_1_e8_747_extend_t_part.smt2
Then, the output is Valid and the synthesized skolem should be close enough to the formula in bench/skolems/fast_1_e8_747_extend_skolem.smt2.
For a synthesized skolem that enables nondeterministic behavior, use option --nondet.