first experience

[jvpeetz]

Hi Mate,
here is my first experience with bosphorus.
I use the Debian distribution (testing/unstable but actually mainly unstable which has. e.g. gcc 8.2).
First, I compiled BRiAl by myself. That needed also the package libboost-test-dev.
But finally, I used the Debian package libbrial-dev.
Since I do experiments with several versions of CryptoMiniSat, I don't do the make install step there but run cryptominisat5 from the build directory. Therefore, I added the line

include_directories( ${cryptominisat5_DIR}/cmsat5-src )

to the file CMakeLists.txt right behind the block

find_package(cryptominisat5 REQUIRED)
if (cryptominisat4_FOUND)
    message(STATUS "OK, CryptoMiniSat5 found")
endif()

to make cmake find the CMS header files and called cmake with something like this

cmake -Dcryptominisat5_DIR=/home/opt/cryptominisat.git-ff39e02a ..

The build succeded. Your test example also works. I just added the switch -e <path-to-cryptominisat5-version>.
I also tried a small example of mine and learned that bosphorus just accepts variables with x and a number.

I will do further tests for sure. At the moment I'm trying to make the newer SageMath working with CMS since I use it for the generation of some ANF (or I have to recompile version 7.6).

Regards,
Jörg.

[msoos]

Thank you for the feedback! I have already added the libboost-test-dev as suggested, thank you! I will think about explaining the more advanced build setup you used. In the meanwhile, I have built a Docker image, I just need to test it then it will go to the README. I should be able to test and fix on Friday so it will be a lot easier to use then :)

Thanks again for the quick feedback. Please let me know if you see anything that's off in the actual running of the tool! :)

Mate

[msoos]

Hi,

So I had a look -- I agree that we could make CryptoMinSat work from a sub-directory as well, but I would argue that that's advanced usage. Most people have compiling code so I wanted to make it as easy as possible. Compiling and building separately is easier I believe.

So I am closing because although I agree that the way you compiled works, it's on average harder for a user. Further, I have added a working Docker image which should make it a lot easier for most people to use the tool.

Thanks again for the feedback and please let me know if the tool was useful :)

Mate