summaryrefslogtreecommitdiff
path: root/contrib/get-abc
AgeCommit message (Collapse)Author
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
2020-11-02contrib: Remove dependency directories. (#5367)Aina Niemetz
This automatically removes dependency directories for scripts that get external dependencies instead of aborting with an error.
2020-09-04Change the unavailable ABC mercury repository for the ABC solver code base ↵Malte Mues
on GitHub (#4989) Signed-off-by: Malte Mues (mail.mues@gmail.com)
2019-12-06contrib: Setup all dependencies in deps/ directory. (#3534)Mathias Preiner
2019-08-26Make contrib/get-* more robust. (#3198)Mathias Preiner
We use the command which to determine if a command is available on the system. However, which is not installed on all platforms by default (e.g. CentOS). command is a shell builtin that can be used for the same purpose.
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-02-08Check whether Cryptominisat4/ABC was installed via get-* script. (#1565)Mathias Preiner
2018-02-06Use separate shell script for common get-* script parts. (#1567)Mathias Preiner
2017-05-27[Competition] Fix ABC, fix CryptoMiniSat reqAndres Noetzli
This commit fixes two issues that caused the competition configuration to fail on the cluster machines: We used an ancient version of ABC that declared a function (factorial() luckySimple.c) in a source file as inline but not static. This issue was fixed in the following commit: https://bitbucket.org/alanmi/abc/commits/e0aa7af0d73538fb786c4dcc72745578f0068a38 The issue with non-static inline functions in source files is described in the following Stackoverflow post: https://stackoverflow.com/questions/16740515/simple-c-inline-linker-error This commit updates ABC to a much newer version (commit tagged as abc20160717), which fixes the issue. One of the modifications previously performed by contrib/get-abc does not need to be necessary anymore. CryptoMiniSat was always linked against m4ri, even though it was not getting compiled with it (-DNOM4RI="ON" in contrib/get-cryptominisat4). This commit removes the part of config/cryptominisat.m4 that explicitly sets the libraries linked to and instead uses the result of CVC4_TRY_CRYPTOMINISAT_WITH (which seems to work even though there is comment indicating otherwise). Further, it adds -pthread to the libraries required by CryptoMiniSat because it is required by the version of CryptoMiniSat that we use (a newer version supports disabling that behavior, so it might be a good idea to update). Previously, this would lead to linker errors. Tested with the following configuration: ./configure competition --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3 --enable-static-binary --enable-gpl --with-cln --with-glpk --with-glpk-dir=`pwd`/glpk-cut-log --with-abc --with-abc-dir=`pwd`/abc/alanmi-abc-53f39c11b58d --disable-thread-support --without-readline --disable-shared --with-cryptominisat --with-cryptominisat-dir=`pwd`/cryptominisat4
2014-06-25Don't allow libabc to load extensions at runtime.Morgan Deters
2014-06-19Minor fixes to get-abc script and configure stuff.Morgan Deters
2014-06-11Some clean-up, post bv-merge.Morgan Deters
Add abc to build id and fix static building. Add abc to --show-config output and Configuration class API. Add ability to select abc source path. Fix arch_flags for abc.
2014-06-04Update commit # for get-abc script, anticipating Liana's merge.Morgan Deters
2014-03-12Draft contrib/get-abc script for bitvectors libabc support.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback