| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-22 | cmake: Add support for cross-compiling for Windows. | Mathias Preiner | |
| 2018-09-22 | cmake: Various CMakeLists.txt fixes/cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
| 2018-09-17 | Follow 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-04 | Remove CVC3 compatibility layer (#2418) | Andres Noetzli | |
| 2018-08-15 | Add contrib/get-gmp script. (#2292) | Mathias Preiner | |
| 2018-08-01 | Remove outdated references to TLS (#2245) | Andres Noetzli | |
| 2018-07-25 | Use CryptoMiniSat 5.6.3. (#2205) | Mathias Preiner | |
| 2018-06-26 | sygusComp2018: add scripts. (#2103) | Andrew Reynolds | |
| 2018-06-26 | Add casc j9 tfn script (#2100) | Andrew Reynolds | |
| 2018-06-25 | Do not use git blame -C in get-authors (too many false positives). | Aina Niemetz | |
| 2018-06-25 | Fix update-copyright script for files without a header. | Aina Niemetz | |
| 2018-06-25 | Added Makai and Yoni to get-authors script. | Aina Niemetz | |
| 2018-06-08 | Disable 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-30 | Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018) | Mathias Preiner | |
| 2018-05-30 | Draft run script for strings smt comp 2018. (#2016) | Andrew Reynolds | |
| 2018-05-27 | Fix no-cbqi-innermost option name in run script (#1994) | Andres Noetzli | |
| 2018-05-26 | Update SymFPU. (#1992) | Mathias Preiner | |
| 2018-05-25 | Add QF_BV configuration for SMTCOMP'18. (#1981) | Mathias Preiner | |
| 2018-05-14 | Add contrib/get-symfpu for downloading symfpu. (#1905) | Mathias Preiner | |
| 2018-05-03 | Option to interleave tangent plane inferences (#1833) | Andrew Reynolds | |
| 2018-04-23 | Draft smt comp 2018 for quantifiers and non-linear (#1808) | Andrew Reynolds | |
| 2018-04-20 | Draft of casc j9 scripts (#1800) | Andrew Reynolds | |
| 2018-04-08 | Warn about trailing spaces in src/Makefile.am (#1759) | Andres Noetzli | |
| 2018-04-07 | Fixed get-authors. | Aina Niemetz | |
| 2018-04-02 | Remove references to nyu (#1721) | Clark Barrett | |
| 2018-03-21 | Ignore whitespaces and moved code for contrib/get-authors. | Mathias Preiner | |
| 2018-03-21 | Refactor 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-20 | Add support for CaDiCaL as eager BV SAT solver. (#1675) | Mathias Preiner | |
| 2018-03-13 | Use Cryptominisat version 5.0.2 (instead of 4.2.0). (#1664) | Mathias Preiner | |
| 2018-03-08 | Cleanup 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-08 | Fixed message in get-antlr script. | Aina Niemetz | |
| 2018-03-05 | Fix boost url in contrib/get-win-dependencies. | Mathias Preiner | |
| This fixes the broken windows nightly builds. | |||
| 2018-02-13 | Skip header for determining top contributors list. (#1603) | Aina Niemetz | |
| 2018-02-08 | Check whether Cryptominisat4/ABC was installed via get-* script. (#1565) | Mathias Preiner | |
| 2018-02-06 | Use separate shell script for common get-* script parts. (#1567) | Mathias Preiner | |
| 2018-02-06 | Updated year in update-copyright script. | Aina Niemetz | |
| 2018-01-08 | Fix broken GMP URL in get-win-dependencies script (#1493) | Andres Noetzli | |
| 2017-11-28 | Add Cryptominisat script and patches to source file distribution. | Mathias Preiner | |
| This enables building CVC4 from a source release with Cryptominisat support. | |||
| 2017-11-01 | Add option to build shared Windows dependencies (#1282) | Andres Noetzli | |
| This commit adds an option to the contrib/get-win-dependencies script (-s) to build shared library versions of ANTLR and GMP, which enables building the shared versions of the CVC4 libraries needed for language bindings. | |||
| 2017-10-03 | Add initial version of the SMTCOMP2018 run scripts (#1185) | Andres Noetzli | |
| This commit is a preparation step for removing the --thread-stack option (and, ultimately, the dependency on Boost). It just copies the 2017 version of the scripts and changes the --fs-inst flag to --fs-interleave, following the renaming in commit 7766f0ba088ad6d6c58ea9678477b255c9e52fee. | |||
| 2017-08-25 | Move LFSC checker out of the CVC repository. (#222) | Aina Niemetz | |
| LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution anymore. As a consequence, we + Add --with-lfsc and --with-lfsc-directory as configure options. In the case where CVC4 has not been built with integrated LFSC, all code that interacts with LFSC is disabled. + Disable proof checking if CVC4_USE_LFSC is not defined. Configuring the build with --check-proofs but without --with-lfsc results in an error. + Do not call LFSC's cleanup function (but we should in the future). LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt. Disabled call to lfscc_cleanup until the problem in lfscc is fixed. + Disable building with LFSC for the distcheck travis build since it is not part of the distribution anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker before calling make check on the temp build (the build of the unpacked distribution tar ball). | |||
| 2017-07-11 | Remove trailing slashes from directories if specified via command line. | Mathias Preiner | |
| 2017-07-10 | Disable tarball signing for now. | Mathias Preiner | |
| 2017-07-07 | Update copyright headers. | Mathias Preiner | |
| 2017-07-07 | Update files that are part of the CVC4 license, exclude minisat files. | Mathias Preiner | |
| 2017-07-07 | Use consistent author names for the copyright headers. | Mathias Preiner | |
| 2017-07-07 | Escape left brace in regex in update-copyright script. | Mathias Preiner | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback