Repository for sumbissions of Amaya to SMT-COMP.
I don't know Docker, so it's likely some things are done in a stupid way. Please correct if you find a better way. Many things
$ docker run registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:latest
...
$ docker container run --name benchexec -it registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user
cd /home
apt install git cmake gcc make python3 python3-pip libgmp-dev libhwloc-dev pkg-config
git clone 'https://github.com/trolando/sylvan.git'
cd sylvan
git checkout v1.5.0
sed -i 's/-Werror//g' CMakeLists.txt # Temporarily disable treating warnings as errors; allows building with newer GCC
mkdir build
cd build
cmake -DBUILD_SHARED_LIBS=ON ..
make
make test
sudo make install
git clone https://github.com/MichalHe/amaya-mtbdd.git
cd amaya-mtbdd
make shared-lib
AMAYA_MTBDD_DIR="$(pwd)"
git clone 'https://github.com/MichalHe/amaya.git'
cd amaya
pip install -r requirements.txt
cp $AMAYA_MTBDD_DIR/build/amaya-mtbdd.so ./amaya
./run-amaya.py --fast -O all get-sat <formula.smt2>
The --fast
option enables the C++
backend and turns on eager minimization.
The -O all
option enables all formula optimizations, and also allows the solver
to use the derivative construction (dubbed internally as "lazy" backend).
Python dependencies cannot be installed system-wide, and, therefore, one has to
set up a virtual environment, and install the dependencies there. Sylvan is also
installed system-wide. Therefore, the libsylvan.so object needs to be present in
the submitted archive, and LD_LIBRARY_PATH
must be set accordingly when Amaya.