| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-12-06 | contrib: Setup all dependencies in deps/ directory. (#3534) | Mathias Preiner | |
| 2019-11-14 | Use Shebang in cxxtestgen when appropriate (#3458) | Alex Ozdemir | |
| CxxTest's generator has one of three names, depending on the CxxTest version: * `cxxtestgen.py`, a python program * `cxxtestgen`, some kind of program with a shebang * `cxxtestgen.pl`, a perl program We were mistakenly assuming that the `cxxtestgen` form was always a python program. Now, if we find that form on the system, we assume that it is has a shebang, and is executable. | |||
| 2019-10-08 | cmake: Fix include of CVC4JavaTargets.cmake. (#3373) | Mathias Preiner | |
| Only include Java targets if Java bindings are enabled. | |||
| 2019-09-25 | Use separate CMake project for CVC4 examples. (#3196) | Mathias Preiner | |
| 2019-09-06 | Remove portfolio (#3236) | Andrew Reynolds | |
| 2019-08-30 | Undo unintential change to FindCxxTest (#3240) | Andrew Reynolds | |
| 2019-08-29 | Infer conflicts based on regular expression inclusion (#3234) | Andres Noetzli | |
| We have a conflict if we have `str.in.re(x, R1)` and `~str.in.re(x, R2)` and `R2` includes `R1` because there is no possible value for `x` that satisfies both memberships. This commit adds code to detect regular expression inclusion for a small fragment of regular expressions: string literals with single char (`re.allchar`) and multichar wildcards (`re.*(re.allchar)`). Signed-off-by: Andres Noetzli <anoetzli@amazon.com> | |||
| 2019-08-14 | cmake: Export CVC4 library interface. (#3179) | Mathias Preiner | |
| 2019-08-02 | Update CaDiCaL to version 1.0.3. (#3137) | Mathias Preiner | |
| * Removes incremental API check (#3011) * Fixes toSatValueLit to use the new semantics of CaDiCaL's val() Fixes #3011 | |||
| 2019-05-17 | Support for incremental bit-blasting with CaDiCaL (#3006) | Andres Noetzli | |
| This commit adds support for eager bit-blasting with CaDiCaL on incremental benchmarks. Since not all CaDiCaL versions support incremental solving, the commit adds a CMake check that checks whether `CaDiCaL::Solver::assume()` exists. Note: The check uses `check_cxx_source_compiles`, which is not very elegant but I could not find a better solution (e.g. `check_cxx_symbol_exists()` does not seem to support methods in classes and `check_struct_has_member()` only seems to support data members). | |||
| 2019-04-15 | Check for rt library in configuration -- support for glibc<2.17 (#2854) | makaimann | |
| This is a minor fix for systems with glibc version < 2.17. In that case, we need to link with `-lrt` according to the clock_gettime man page. | |||
| 2019-01-11 | Fixed linking against drat2er, and use drat2er (#2785) | Alex Ozdemir | |
| * Fixed linking against drat2er/drat-trim We have machinery for linking against drat2er. However, this machinery didn't quite work because libdrat2er.a contains an (undefined) reference to `run_drat_trim` from libdrat-trim.a. Thus, when linking against libdrat2er.a, we also need to link against libdrat-trim.a. I made this change, and then tested it by actually calling a function from the drat2er library (CheckAndConvertToLRAT) which relies on `run_drat_trim`. Since this invocation compiles, we know that the linking is working properly now. * Combined the two libs, per Mathias * drat2er configured gaurds | |||
| 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-10-22 | Only 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-20 | Remove antlr_undefines.h. (#2664) | Mathias Preiner | |
| Is not required anymore since we don't use autotools anymore. | |||
| 2018-09-27 | cmake: Add CxxTest finder module to allow custom paths. (#2542) | Mathias Preiner | |
| 2018-09-26 | cmake: Only print dumping warning if not disabled by user. (#2543) | Mathias Preiner | |
| 2018-09-24 | cmake: Fix and simplify git version info. (#2516) | Aina Niemetz | |
| 2018-09-22 | cmake: Build fully static binaries with option --static. | Mathias Preiner | |
| 2018-09-22 | cmake: Add more documentation, some fixes and cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: Move PACKAGE_NAME to ConfigureCVC4, more cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: Add support for cross-compiling for Windows. | Mathias Preiner | |
| 2018-09-22 | cmake: Do not allow dumping with portfolio build. | Aina Niemetz | |
| 2018-09-22 | cmake: FindANTLR: Check if antlr3FileStreamNew is available. | Mathias Preiner | |
| 2018-09-22 | cmake: Add some more documentation, cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: Move helper functions to cmake/Helpers.cmake. | Mathias Preiner | |
| 2018-09-22 | cmake: Refactor and clean up build profile printing. | Aina Niemetz | |
| 2018-09-22 | cmake: Add module finder for Valgrind. | Mathias Preiner | |
| 2018-09-22 | cmake: Various CMakeLists.txt fixes/cleanup. | Mathias Preiner | |
| 2018-09-22 | cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake. | Mathias Preiner | |
| 2018-09-22 | cmake: Add options for specifying install directories for dependencies. | Mathias Preiner | |
| 2018-09-22 | cmake: Add module finder for GLPK-cut-log. | Mathias Preiner | |
| 2018-09-22 | cmake: Add module finder for ABC. | Mathias Preiner | |
| 2018-09-22 | cmake: Compile Java tests and add to ctest if Java bindings are enabled. | Mathias Preiner | |
| 2018-09-22 | cmake: Various portfolio/default option fixes. | Mathias Preiner | |
| 2018-09-22 | cmake: Enable shared by default. | Mathias Preiner | |
| Further, force shared builds in case of unit tests. | |||
| 2018-09-22 | cmake: Add support for CxxTest. | Aina Niemetz | |
| 2018-09-22 | cmake: Filter through and disable unused HAVE_* variables from autotools. | Aina Niemetz | |
| 2018-09-22 | cmake: Added support for coverage and profiling. | Aina Niemetz | |
| 2018-09-22 | cmake: Added 3-valued option handling (to enable detection of user-set options). | Aina Niemetz | |
| 2018-09-22 | cmake: Add module finder for readline. | Mathias Preiner | |
| 2018-09-22 | cmake: Added licensing options and warnings/errors. | Aina Niemetz | |
| 2018-09-22 | cmake: Add build configurations. | Aina Niemetz | |
| 2018-09-22 | cmake: Add module finder for LFSC. | Mathias Preiner | |
| 2018-09-22 | cmake: Add module finder for CaDiCaL. | Mathias Preiner | |
| 2018-09-22 | cmake: Add module finder for CryptoMiniSat. | Mathias Preiner | |
| 2018-09-22 | cmake: Add module finder for SymFPU. | Mathias Preiner | |
| 2018-09-22 | cmake: Add module finder for CLN. | Mathias Preiner | |
| 2018-09-22 | cmake: Antlr parser generation done. | Mathias Preiner | |
| 2018-09-22 | cmake: .cpp generation done, .h generation not yet complete | Aina Niemetz | |
 |
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