| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-25 | Bump library version to 1.7-prerelease. | Aina Niemetz | |
| 2018-06-25 | Cutting release 1.6. | Aina Niemetz | |
| 2018-06-20 | Fix warnings and enable -Wnon-virtual-dtor warning (#2079) | Andres Noetzli | |
| This commit fixes warnings for an unused variable, comparison of two different types and add virtual destructors to classes that were previously missing them. It also enables the -Wnon-virtual-dtor warning which warns about any class definition with virtual methods that does not have a virtual destructor (except if the destructor is protected). This flag is supported by both clang and GCC and not enabled by default. | |||
| 2018-06-20 | Check unsat cores in regressions also without LFSC (#1955) | Andres Noetzli | |
| When moving the LFSC checker out of the CVC4 repository in commit dfa69ff98a14fcc0f2387e59a0c9994ef440e7d0, we disabled checking unsat cores when CVC4 was compiled without LFSC due to the complexity of the regression script. This commit changes the new(-ish) Python regression script to check unsat cores even when CVC4 was compiled without LFSC. This is done by having two separate flags, --with-lfsc and --enable-proof, for the regression script that mirror the configuration flags. The regression script performs unsat cores and proofs checks based on those flags. Additionally, this commit changes the regression script to check proofs and unsat cores in two independent runs. Testing them in a single run masked issues #1953 and #1954. | |||
| 2018-06-20 | Resolve CVC4_USE_SYMFPU in headers at config-time (#2077) | Andres Noetzli | |
| As described in issue #2013, we had `#ifdef CVC4_USE_SYMFPU` conditions in floatingpoint.h, which was problematic when installing the header files because the definition of `CVC4_USE_SYMFPU` was a compile-flag and simply including the header files in another project would be missing that definition. This commit moves floatingpoint.h to a template file floatingpoint.h.in and substitutes the value of `CVC4_USE_SYMFPU` at configure-time when generating floatingpoint.h (this is the same solution that integer.h and rational.h use). I have tested the fix with the examples provided in #2013 and they work. | |||
| 2018-05-21 | Add SymFPU licensing information. (#1952) | Mathias Preiner | |
| 2018-05-14 | Add contrib/get-symfpu for downloading symfpu. (#1905) | Mathias Preiner | |
| 2018-04-05 | Python regression script (#1662) | Andres Noetzli | |
| Until now, we have been using a bash script for the running the regressions. That script had several issues, e.g. it was creating many temprorary files and it was calling itself recursively, making it difficult to maintain. This commit replaces the script with a Python script. The Python script uses the TAP protocol, which allows us to display the results of multiple tests per file (e.g. with --check-models and without) separately and with more details. It also outputs whenever it starts running a test, which allows finding "stuck" regression tests on Travis. As recommended in the automake documentation [0], the commit copies the TAP driver to enable TAP support for the test driver. Note: the commit also changes some of the regressions slightly because we were using "%" for the test directives in SMT files which does not correspond to the comment character ";". Using the comment character simplifies the handling and makes it easier for users to reproduce a failure (they can simply run CVC4 on the regression file). [0] https://www.gnu.org/software/automake/manual/html_node/Use-TAP-with-the-Automake-test-harness.html | |||
| 2018-04-02 | Remove references to nyu (#1721) | Clark Barrett | |
| 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-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
| Adds missing override keywords. | |||
| 2018-02-08 | Replace CMM flag with debug CMM flag, fix leak in debug CMM (#1586) | Andres Noetzli | |
| Previously, we had -DCVC4_CONTEXT_MEMORY_MANAGER that needed to be added as a compile flag to use the context memory manager (which we want by default). This makes compiling with other build systems cumbersome because you have to know about the flag. This commit replaces the -DCVC4_CONTEXT_MEMORY_MANAGER flag with a -DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER flag that does the opposite (in absence of the flag, we use the context memory manager). Additionally, the commit fixes a memory leak in the debug context memory manager (the destructor did not clean up the allocations). | |||
| 2017-11-30 | Add debugging tools for ContextMemoryManager (#1407) | Andres Noetzli | |
| This commit adds two configuration options that help debugging memory issues with allocations in the ContextMemoryManager: --enable/disable-valgrind: This flag enables/disables Valgrind instrumentation of the ContextMemoryManager. Enabled by default for debug builds if the Valgrind headers are available. --enable/disable-context-memory-manager: This flag enables/disables the use of the ContextMemoryManager. If the flag is disableda dummy ContextMemoryManager is used that does single allocations instead of chunks. The flag is enabled by default. | |||
| 2017-10-27 | Modify LDFLAGS to support shared libraries for Win (#1280) | Andres Noetzli | |
| * Use uintptr_t for pointer casts in Swig files CVC4's Swig interface files were casting pointers to longs in multiple instances. The problem with that is that on certain platforms *cough* Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit executable (they use the LLP64 data model). This made the compilation of language bindings fail with MinGW. This commit changes the types to uintptr_t defined in Swig's stdint.i. * Modify LDFLAGS to support shared libraries for Win This commit adds "-no-undefined" to the LDFLAGS of CVC4's library, which is required for building DLLs (shared libraries on Windows). It also adds "--export-all-symbols" to the linker flags of the parser to ensure that there are no unresolved symbols when linking against it (see comment in the Makefile.am for details). * Fix for non-Windows builds * add no-undefined to libcvc4compatjni | |||
| 2017-10-03 | Add Cryptominisat and LFSC to --show-config output. (#1194) | Mathias Preiner | |
| Also removed obsolete CUDD related code. | |||
| 2017-09-05 | Fix link in configure.ac. | Mathias Preiner | |
| 2017-08-30 | Use thread_local instead of compiler extensions (#210) | Andres Noetzli | |
| C++11 introduced the thread_local keyword, so we don't need to use non-standard extensions or our custom pthread extension anymore. The behavior was previously introduced as a workaround in commit 753a072c542c1c254d7c6adbf10e091ba585ede5. This commit introduces the macro CVC4_THREAD_LOCAL that can be used to declare variables as thread local. For Swig, this macro is defined to be empty. | |||
| 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-08-09 | Fix help message for disable-unit-testing in configure.ac (don't -> do not) | Aina Niemetz | |
| Previous help message broke syntax highlighting in vim. | |||
| 2017-08-02 | Disable debug symbols for production builds. | Mathias Preiner | |
| 2017-07-26 | -Og for non-opt build, parallel pcvc4 check (#206) | Andres Noetzli | |
| -Og enables optimizations that do not interfere with debugging. This is the new default for debug builds if the compiler supports the flag. This commit also enables parallel checking for the portfolio build on Travis. | |||
| 2017-07-26 | Use TEST_CPPFLAGS/TEST_CXXFLAGS to add path to CxxTest headers in ↵ | Mathias Preiner | |
| configure.ac. (#200) CxxTest headers were included in test/unit/Makefile.am as -I@CXXTEST@. However, in configure.ac if CXXTEST was not set by the user, it was initially set to `dirname "$CXXTESTGEN"` while determining the path to the header files. If CXXTESTGEN pointed to /usr/bin and if the headers were found in /usr/include, CXXTEST was not reset, which led to CXXTEST being replaced by /usr/bin in test/unit/Makefile.am. As a consequence, the locale binary in /usr/bin got included instead of the locale header file. | |||
| 2017-07-20 | Moving from the gnu extensions for hash maps to the c++11 hash maps | Tim King | |
| * Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes. | |||
| 2017-07-17 | Use is_sorted, merge, copy from std (#199) | Andres Noetzli | |
| Previously, we were checking whether we should use is_sorted from std or __gnu_cxx. With C++11, std::is_sorted is guaranteed to exist. This commit changes arith/normal_form.{h,cpp} to always use std::is_sorted and also removes the custom implementations for merge and copy by using the std implementations instead. | |||
| 2017-07-13 | autoconf: make -std=gnu++11 mandatory | Aina Niemetz | |
| 2017-07-10 | Prerelease versioning for master. | Mathias Preiner | |
| 2017-07-10 | Cutting release 1.5. | Mathias Preiner | |
| 2017-06-21 | Check for sigaltstack in configure (#172) | Clément Pit-Claudel | |
| 2017-05-12 | Conditional coverage build | makaimann | |
| 2017-04-21 | Add check for C++ exceptions to config script | Andres Notzli | |
| Bug 687 was caused by the configuration not properly supporting C++ exceptions. To avoid such an incidence in the future, this commit adds a simple check to `configure.ac` (when not cross compiling). | |||
| 2017-03-08 | Fix MinGW-w64 build | Andres Notzli | |
| This commit fixes configure.ac to try to get clock_gettime() from pthread. Without it, clock_gettime() is detected as missing at configuration time for MinGW-w64 but exists at compile time, which causes conflicts. Additionally, this commit updates the helper script for Windows to use MinGW-w64 by default instead of MinGW. | |||
| 2016-12-01 | Fix build on macOS Sierra | Andres Notzli | |
| Before this fix, the build died with `ar: no archive members specified when linking the empty libreplacements.la.` because macOS Sierra does not require the replacements anymore. With this fix, `ffs.c` and `strtok_r.c` are always getting compiled (even when they are empty) to prevent the error. Also removed the unused `CVC4_NEEDS_REPLACEMENT_FUNCTIONS` from `configure.ac` and added an `#ifndef HAVE_FFS` to `ffs.c` for consistency with `strtok_r.c`. | |||
| 2016-05-24 | Merged cryptominisat from experimental branch. | Liana Hadarean | |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King | |
| What to Know As a User: A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems. The Problem: The build order of CVC4 used to be [roughly] specified as: options < expr < util < libcvc4 < parsers < main Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable. The Solution: To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen: 1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file. 2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options. 3. All of the old options_handlers.h files have been refactored. 4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary. 5. I am removing the libstatistics library. The constraints that the CVC4 build system will eventually satisfy are: - The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files. - The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases. - The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.) - One library per Makefile.am. - No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.) The build order of CVC4 can now be [roughly] specified as base < options < util < expr < smt_util < libcvc4 < parsers < main The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean. More details about the directories: base/ The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere. options/ The options/ directory is self contained. - It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h . - There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options. - Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done. - The */options_handlers.h files have been removed. - The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp. - All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h . util/ The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean. expr/ The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/. - An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h. - Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h. - The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/. - Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes. - Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources. - This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC. smt_util/ The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel. What is up next: - A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed. - The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up. | |||
| 2015-10-26 | This commit fixes a bug related to a public header depending on a compiler ↵ | Tim King | |
| flag. This resulted in user code seeing a different size for the SmtEngine class than what was compiled in the library. Proofs are enabled by default again. See http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=688 for more information. | |||
| 2015-10-24 | Revert "Default builds are now proof enabled." | Kshitij Bansal | |
| This reverts commit 4fd18dee3156a6dd1903b95662034d6e996ff88b. | |||
| 2015-10-23 | Changes configure.ac so that the single recurisve invocation runs with a ↵ | Tim King | |
| relative path. This lets the @srcdir@ variable in configuration be a relative path. | |||
| 2015-10-11 | Default builds are now proof enabled. | Liana Hadarean | |
| 2015-10-09 | Temporary reverting commit 477e72b (proofs as default build) until we fix ↵ | Liana Hadarean | |
| nightly builds. | |||
| 2015-10-07 | Default builds are now proof enabled. | Liana Hadarean | |
| 2015-02-12 | Changing CXXFLAGS for custom cln installation in configure.ac. | Tim King | |
| Making sure the CVC4 flags do not get overwritten after being set. | |||
| 2015-01-19 | Adding an additional search path to configure.ac for cxxtestgen to reflect ↵ | Tim King | |
| the cxxtest git repository. | |||
| 2014-08-12 | To avoid confusion, permit --enable-staticbinary as an alias for ↵ | Morgan Deters | |
| --enable-static-binary. | |||
| 2014-07-13 | Versioning for master. | Morgan Deters | |
| 2014-07-13 | New versioning for development version. | Morgan Deters | |
| 2014-07-13 | Cutting release 1.4.1.4 | Morgan Deters | |
| 2014-06-26 | Minor language bindings fixes. | Morgan Deters | |
| 2014-06-25 | Stack-size portfolio fix. If using Boost 1.50, --thread-stack=MB is now ↵ | Morgan Deters | |
| supported. | |||
| 2014-06-21 | Adjust library dependencies to be more correct (fixes lintian warnings). | Morgan Deters | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
path: root/configure.ac
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback