Update doccumentation on how to compile Boolector

[pmassolino]

I followed the instructions on how to compile and set up SymbiYosys and the provers from https://symbiyosys.readthedocs.io and I had some problems on getting Boolector prover to work. I run make tests with SymbiYosys and then I got this message:

SBY 10:44:27 [cover] engine_0_0: starting process "cd cover ; btorsim -c --vcd engine_0/trace0.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_0/trace0.wit" SBY 10:44:27 [cover] engine_0: [btor>mc] bad state property 1 at bound k = 6 UNSATISFIABLE SBY 10:44:27 [cover] engine_0: [btor>mc] found 1 reachable and 0 unreachable bad state properties at bound k = 6 SBY 10:44:27 [cover] engine_0_0: *** 'btorsim' error: invalid command line option '--vcd' (try '-h') SBY 10:44:27 [cover] engine_0_0: finished (returncode=1)

btorsim does not support command --vcd After some time looking into the git repository, I saw that SymbiYosys requires that a different version of btor2tools to be compiled. After changing Boolector script ./contrib/setup-btor2tools.sh to

!/usr/bin/env bash

set -e -o pipefail

source "$(dirname "$0")/setup-utils.sh"

BTOR2TOOLS_DIR=${DEPS_DIR}/btor2tools

COMMIT_ID="1df768d75adfb13a8f922f5ffdd1d58e80cb1cc2"

COMMIT_ID="bd4c9d3b28498a30638509bb93d4ea730b23569b"

download_github "nakengelhardt/btor2tools" "$COMMIT_ID" "$BTOR2TOOLS_DIR" cd "${BTOR2TOOLS_DIR}"

if is_windows; then component="Btor2Tools" last_patch_date="20190110" test_apply_patch "${component}" "${last_patch_date}" fi

echo $PWD

./configure.sh -fPIC

./configure.sh cd build make all -j${NPROC} cd ..

install_lib build/libbtor2parser.a

install_include src/btor2parser/btor2parser.h btor2parser

I was able to compile btorsim and use with Symbiyosys. It would be nice if such instructions would be on https://symbiyosys.readthedocs.io until the btor2sim tool has support for the command --vcd.

[nakengelhardt]

Technically, neither make test nor the btor engine are documented at all yet!

The engines documentation only lists smtbmc, aiger and abc. For use with smtbmc boolector the fork is not needed and therefore not mentioned, it's only necessary when using the as-yet undocumented btor btormc. (This documentation will be updated once the btorsim changes are upstreamed.)

make test (also not included in the instructions) is a recent addition and meant for our internal CI, it doesn't really have proper skipping mechanics yet for non-installed solvers. For example, it also calls aiger suprove, but superprove doesn't even compile on mac or windows, so it's a guaranteed failure for many users.

I do think it would make sense to leave a note somewhere about things still under development, but I'm not exactly sure where would be a good place to put it... "undocumented features" documentation section? Random text file lying around?

[pmassolino]

I didn't knew the "make test" was still in development, sorry. You could add a small section it in the README.md in "features that are still in development".