Bugfix/ipasir #683
Closed
Bugfix/ipasir #683
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
When building solvers.a while aiming at building CBMC with support for
IPASIR solvers, all projects that need SAT checkers would require to
link against the provided libipasir.a library. To make this library
visible for all subprojects at the same time, but furthermore allow the
user to choose which library to pick, the variable LIBSOLVER was
introduced, which is set to an empty value by default.
To compile while using IPASIR solvers, use for example:
IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a \
CFLAGS="-DSATCHECK_IPSAIR" make -j 7 -C src
Add the necessary source changes to allow CBMC to use IPASIR solvers.
Add necessary steps to set variables for IPASIR Furthermore, allow to select SAT solver from make command line, for example by calling IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a make Not, to compile with a different SAT solver, e.g. GLUCOSE=../../glucose-syrup make it has to be ensured, that the solvers.a library is rebuild, and all components that link against this library are renewed as well. This can be achieved by touching the satcheck.h flie, i.e.: touch src/solvers/sat/satcheck.h
Besides the usual test with Minisat, also compile with glucose, and test whether compilation with IPASIR works. Perform tests and regression testing for the two variants as well. Furthermore, if libzip and zlib and not inizialized properly, any build will fail. Hence, these targets are added as well.
mgudemann
force-pushed
the
bugfix/ipasir
branch
from
a28600c to
5cfc5bb
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
fixing #552 on glucose compilation