summaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2019-04-03get-authors: Add GitHub user ayveejay -> Andrew V. Jones.Aina Niemetz
2019-03-26update-copyright: Update to 2019.Aina Niemetz
2019-03-26get-authors: Exclude empty lines.Mathias Preiner
2019-03-25get-authors: Exclude common source code patterns. (#2900)Mathias Preiner
Exclude lines that #include header files and define namespaces. Since we use git blame -C -M to determine the current top contributors, git tries to match all #include and namespace definitions to an original author, which is not accurate since these lines are usually not copied over from other files.
2019-03-25update-copyright: Fix matching of excluded paths.Aina Niemetz
2019-03-25get-authors: Readd option -C to git blame command.Aina Niemetz
2018-12-17 Configured for linking against drat2er (#2754)Alex Ozdemir
drat2er is a C/C++ project which includes support for * Checking DRAT proofs * Converting DRAT proofs to LRAT proofs * Converting DRAT proofs to ER proofs It does the first 2 by using drat-trim under the hood. I've modified our CMake configuration to allow drat2er to be linked into CVC4, and I added a contrib script.
2018-11-22Use https for antlr3.org downloads (#2701)Tom Smeding
This commit changes the two www,antlr3.org URL's in contrib/get-antlr-3.4 to use https instead of http, which is more secure.
2018-10-22Only build CryptoMiniSat library, no binary (#2657)Andres Noetzli
This commit changes the contrib/get-cryptominisat script to only build the CryptoMiniSat library instead of both the library and the binary. The advantage of this is that we can compile a static version of the CryptoMiniSat library without having a static version of glibc or libstdc++ (this is fine as long as we do a shared library build of CVC4). This is an issue on Fedora (tested on version 25) where the contrib/get-cryptominisat script was failing when building the CryptoMiniSat binary due to the static version of these libraries not being available. Since we just want to build the library, the commit also changes the script to not install CryptoMiniSat anymore and updates the CMake find script to accomodate the new folder structure. Side note: the folder structure generated after this commit is a bit more uniform with, e.g. the CaDiCaL script: The source files are directly in the cryptominisat5 folder, not in a subfolder.
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-09-22cmake: Add support for cross-compiling for Windows.Mathias Preiner
2018-09-22cmake: Various CMakeLists.txt fixes/cleanup.Mathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-17Follow redirects with cURL in contrib/get* scripts (#2471)Andres Noetzli
On systems without `wget`, we use `curl` to download dependencies. However, we were not using the `-L` (follow redirects) option, which is necessary to download certain dependencies, e.g. CryptoMiniSat.
2018-09-04Remove CVC3 compatibility layer (#2418)Andres Noetzli
2018-08-15Add contrib/get-gmp script. (#2292)Mathias Preiner
2018-08-01Remove outdated references to TLS (#2245)Andres Noetzli
2018-07-25Use CryptoMiniSat 5.6.3. (#2205)Mathias Preiner
2018-06-26sygusComp2018: add scripts. (#2103)Andrew Reynolds
2018-06-26Add casc j9 tfn script (#2100)Andrew Reynolds
2018-06-25Do not use git blame -C in get-authors (too many false positives).Aina Niemetz
2018-06-25Fix update-copyright script for files without a header.Aina Niemetz
2018-06-25Added Makai and Yoni to get-authors script.Aina Niemetz
2018-06-08Disable BV-abstraction in the competition script. (#2061)Mathias Preiner
2018-06-04[SMT-COMP] Add new logics to run-scripts (#2022)Andres Noetzli
2018-05-30[SMT-COMP] Print non-(un)sat output to stderr (#2019)Andres Noetzli
In the SMT-COMP runscript, we are currently discarding output on stdout that is not "sat" or "unsat" when using `trywith` (this is not the case with `finishwith`). Due to this, our tests might miss cases where CVC4 fails and prints an error on stdout when using `trywith`. This commit changes the script to print output other than "sat" or "unsat" to stderr.
2018-05-30Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)Mathias Preiner
2018-05-30Draft run script for strings smt comp 2018. (#2016)Andrew Reynolds
2018-05-27Fix no-cbqi-innermost option name in run script (#1994)Andres Noetzli
2018-05-26Update SymFPU. (#1992)Mathias Preiner
2018-05-25Add QF_BV configuration for SMTCOMP'18. (#1981)Mathias Preiner
2018-05-14Add contrib/get-symfpu for downloading symfpu. (#1905)Mathias Preiner
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-04-23Draft smt comp 2018 for quantifiers and non-linear (#1808)Andrew Reynolds
2018-04-20Draft of casc j9 scripts (#1800)Andrew Reynolds
2018-04-08Warn about trailing spaces in src/Makefile.am (#1759)Andres Noetzli
2018-04-07Fixed get-authors.Aina Niemetz
2018-04-02Remove references to nyu (#1721)Clark Barrett
2018-03-21Ignore whitespaces and moved code for contrib/get-authors.Mathias Preiner
2018-03-21Refactor mkoptions (#1631)Mathias Preiner
This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation. The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick. This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.
2018-03-20Add support for CaDiCaL as eager BV SAT solver. (#1675)Mathias Preiner
2018-03-13Use Cryptominisat version 5.0.2 (instead of 4.2.0). (#1664)Mathias Preiner
2018-03-08Cleanup Cryptominisat SAT wrapper. (#1652)Mathias Preiner
Cryptominisat has name conflicts with the other Minisat implementations since the Minisat implementations export var_Undef, l_True, ... as macro whereas Cryptominisat uses static const. In order to avoid these conflicts we forward declare CMSat::SATSolver and include the cryptominisat header only in cryptominisat.cpp. Further, the helper functions are moved into an anonymous namespace in the .cpp file and functions that were not used are removed.
2018-03-08Fixed message in get-antlr script.Aina Niemetz
2018-03-05Fix boost url in contrib/get-win-dependencies.Mathias Preiner
This fixes the broken windows nightly builds.
2018-02-13Skip header for determining top contributors list. (#1603)Aina Niemetz
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
2018-02-06Updated year in update-copyright script.Aina Niemetz
2018-01-08Fix broken GMP URL in get-win-dependencies script (#1493)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback