search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Fixed cmake script + removed a compilation warning. #59

Closed BrunoDutertre closed 4 years ago

BrunoDutertre commented 5 years ago

Script cmake/FindBtor2Tools.cmake didn't take Btor2Tools_ROOT_DIR into account. Something like "./configure.sh --btor2tools-dir <...>" failed because of that.

Fixed a string format in btormbt.c to avoid compilation warnings.

Signed-off-by: Bruno Dutertre bruno@csl.sri.com

mpreiner commented 5 years ago

Thanks Bruno! I didn't forget about the PR, but things were a little crazy lately, I'll have a look asap.

BrunoDutertre commented 4 years ago

Yes, but I think it would still make sense to allow users to install the dependencies by hand in case the contrib/setup-xxx.sh don't work.

Everything worked fine for me on Linux, apart from various compilation warnings (on Ubuntu 16.04, using gcc 5.4). Nothing worked on MacOS.

The contrib/setup-xxx.sh scripts assume thatwget is available, but there's no wget by default on MacOS X. (You can use curl -L instead).

There are other potential problems:

aniemetz commented 4 years ago

Yes, but I think it would still make sense to allow users to install the dependencies by hand in case the contrib/setup-xxx.sh don't work.

We have an idea how to resolve this without changing the current Find*.cmake files. We'll address this asap. @BrunoDutertre can you remove the changes to the FindBtor2Tools.cmake file from this PR and (squash and) sign off your commits? Then we can go ahead and merge the changes in btormbt.c in.

the minisat version downloaded by setup-minisat.sh is flaky. It may fail to compile on Linux depending on the compiler and it always fails on MacOS

That's unfortunately a problem in the MiniSat source code with newer compilers, not a problem of the script or Boolector.

picosat does not compile on MacOS

This is also not a problem of the setup script or Boolector, but the build configuration of PicoSAT. That's also the reason why we currently don't build with MiniSat or PicoSAT on Azure.

cryptominisat depends on various third-party things (e.g., boost) so setup-cms.sh may fail if they are not found.

I enabled building CMS on Azure without boost, and it builds without issues. AFAIK it only needs boost for the binary, and we build the library only. We certainly do not want to pull in dependencies of CMS without the user being aware of it, and fail on purpose in that case. If dependencies are missing, users should resolve this.

aniemetz commented 4 years ago

The contrib/setup-xxx.sh scripts assume thatwget is available, but there's no wget by default on MacOS X. (You can use curl -L instead).

Addressed this on master in https://github.com/Boolector/boolector/commit/1e9fee1ac27e2d8ae3c5ca07d15c41f84f0b1888.

BrunoDutertre commented 4 years ago

I'll fix the pull request. This may take a few days.

Note that there's another occurrence of 'wget' in contrib/setup-utils.sh.

BrunoDutertre commented 4 years ago

Actually, it would just be simpler for you to directly fix the code. The change is very small:

It's in macro BTORMBT_LOG_STATUS in src/btormbt.c: In the format string, replace %" PRId64 " by %zu.

mpreiner commented 4 years ago

Ok will do! Thanks @BrunoDutertre !

mpreiner commented 4 years ago

@BrunoDutertre 1552c2564 adds support for configuring additional dependency locations via option --path <dir1> --path <dir2> .... Let me know if that works for you.