summaryrefslogtreecommitdiff
path: root/src/base
AgeCommit message (Collapse)Author
2021-08-15Correct copyright print for GLPK (#7015)Andrew V. Jones
In `master`, starting `cvc5` interactively will give you: ``` glpk-cut-log - a modified version of GPLK, the GNU Linear Programming Kit See http://github.com/timothy-king/glpk-cut-log for copyrightinformation ``` Notice: there's a double-space after the dash following the library name, and there's no space between "copyrightinformation". This commit corrects this print such that it gives: ``` glpk-cut-log - a modified version of GPLK, the GNU Linear Programming Kit See http://github.com/timothy-king/glpk-cut-log for copyright information ``` Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
2021-07-14Add missing space for check macro error messages. (#6875)Mathias Preiner
2021-07-12Use default visibility for `cvc5::Exception` (#6856)Andres Noetzli
Currently, `cvc5::Exception` does not have default visibility, which can cause cvc5 to terminate when trying to catch it in `main.cpp`. Presumably, this is because the necessary typeinfo is missing [0]. Due to this issue, production builds for M1 on macOS crashed when parser exceptions were thrown. The commit changes the visibility of the exception. [0] https://gcc.gnu.org/wiki/Visibility, "Problems with C++ exceptions (please read!)"
2021-07-03Add output tags -o, --output. (#6826)Mathias Preiner
Output tags are similar to debug/trace tags, but are always enabled (except for muzzled builds) to provide useful information for users. Available output tags can be queried via -o help/--output help and are specified in the base options module via enum values. Co-authored-by: Gereon Kremer <nafur42@gmail.com>
2021-06-21Make CaDiCaL a required dependency. (#6761)Mathias Preiner
Since the new BV solver is enabled by default and uses CaDiCaL (and optionally CryptoMiniSat) we make CaDiCaL a required dependency.
2021-06-16Make symfpu a required dependency. (#6749)Aina Niemetz
2021-06-09Update CVC4 URLs/macros (#6666)Andres Noetzli
2021-04-21Add explicit dependencies for base lib (#6410)Gereon Kremer
This PR adds missing cmake dependencies for the base library. This makes sure that Debug_tags.h and Trace_tags.h are already present when we start compiling.
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/.
2021-04-16cmake: Build object libraries for base and context. (#6374)Mathias Preiner
cmake complains that the static base and context libraries are not exported as install targets. Since we do not want to install these libraries we'll build object libraries instead.
2021-04-15Build support library from base and context. (#6368)Mathias Preiner
This PR creates a support library from the utilities in base and context, which will be required in the parser as soon as we move the symbol table/manager to the parser. Note: I decided to always build static libraries from base and context (and optionally enable -fPIC for shared builds) since I'm not sure if we want to have these libraries installed separately. Right now these are considered as cvc5 internal utilities that can be used in all cvc5 libraries, but not outside.
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
This renames everything but GitHub links and build system related macros. Switching the build system to cvc5 will be the last step in the renaming process.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-01Add utility classes for new statistics (#6178)Gereon Kremer
This PR introduces two new sets of classes used for the new statistics setup. The first set are the statistic values that hold the actual data and will live in the new statistics registry itself. The second set are proxy objects: they only hold a pointer to the value classes and implement all the modifiers. The code is not used yet, but replaces the code in the stats_* files in a subsequent PR.
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-23Removing unused build options and deprecated proof compile flag (#6195)Haniel Barbosa
2021-03-16cmake: Generate cvc4_export.h and set visibility to hidden. (#6139)Mathias Preiner
The build system (cmake) will automatically generate an export header cvc4_export.h, which makes sure that the correct export features are defined depending on the compiler and target platform. The macro CVC4_EXPORT replaces CVC4_PUBLIC and its usage is reduced by 2/3. Co-authored-by: Gereon Kremer <nafur42@gmail.com>
2021-03-10Use Assert instead of assert. (#6095)Mathias Preiner
This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
2021-03-02Remove non-ASCII characters from source files. (#6039)Mathias Preiner
Make collect_tags.py more robust for non-ASCII characters.
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
2021-03-01Refactor collection of debug and trace tags (#5996)Gereon Kremer
We have a mechanism to collect all debug and trace tags used throughout the code base to allow checking for valid tags. This mechanism relies on a collection of more or less readable shell scripts. #5921 hinted to a problem with the current setup, as it passes all source files via command line. This PR refactors this setup so that the scripts collect the files internally, and only the base directory is passed on the command line. As I was touching this code anyway, I ported everything to python and combined it into a single script, in the hope to make it more maintainable. Fixes #5921.
2020-12-02Rename macro Message to CVC4Message. (#5576)Aina Niemetz
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-08-04Add documentation and build instructions for recompilation (LGPL). (#4844)Mathias Preiner
2020-07-17Replace options listener infrastructure (#4764)Andrew Reynolds
This replaces the old options listener infrastructure with the OptionsManager introduced in cb8d041. It eliminates a "beforeSearchListener", which was a custom way of some options throwing a modal exception if they were set after initialization. Now all options are consistent: no option can be set after initialization. It also moves managed ostream objects to the OptionsManager. @mpreiner The next step will be to remove the "notifies" field from the Options build system and then proceed with cleaning src/options/.
2020-07-17Support for using 'libedit' over 'readline' #4571 (#4579)Andrew V. Jones
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
2020-07-17Integration of libpoly (#4679)Gereon Kremer
This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration. Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities.
2020-07-10Always Update Git information when rebuilding (#4696)Andres Noetzli
Commit 61734b41b7b96e7e7cbf46021a357d840d64b42e changed the way some of our source files are generated. However, the change meant that once `git_versioninfo.cpp` was generated, it was never updated again: The custom command for `git_versioninfo.cpp` has no dependencies, so CMake does not rebuild it unless the output file is missing [0]. This commit reverts the change to our `gen-gitinfo` target and adds `git_versioninfo.cpp` to `BYPRODUCTS` for the target to indicate that the file may have changed. I am not sure if there is a better solution because we actually have to run `GitInfo.cmake` to see if there have been any changes in the Git information. Introducing a dependency on all source files is not sufficient because other files or just the branch name may change. Note: The original solution only updates the timestamp of `git_versioninfo.cpp` if its contents actually change (`GitInfo.cmake` uses `configure_file()` to generate `git_versioninfo.cpp`, which only updates the timestamp when the contents changed [1]), so we don't do any unnecessary work. [0] https://cmake.org/cmake/help/latest/command/add_custom_command.html [1] https://cmake.org/cmake/help/latest/command/configure_file.html Signed-off-by: Andrew V. Jones <andrew.jones@vector.com> Co-authored-by: Andrew V. Jones <andrew.jones@vector.com>
2020-07-02Remove SWIG bindings (#4683)Andres Noetzli
This commit removes support for SWIG bindings for the legacy API. The bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da and we are not planning on using SWIG for the Java API for the new API.
2020-06-16Update copyright headers.Aina Niemetz
2020-06-09Language bindings: Enable catching of exceptions (#2813)Andres Noetzli
Fixes #2810. SWIG relies on throw specifiers to determine which exceptions a method can throw. The wrappers generated by SWIG catch those C++ exceptions and turn them into exceptions for the target language. However, we have removed throw specifiers because they have been deprecated in C++11, so SWIG did not know about any of our exceptions. This commit fixes the issue using the %catches directive, declaring that all methods may throw a CVC4::Exception or a general exception. Note: This means that users of the language bindings will just receive a general CVC4::Exception instead of more specific exceptions like TypeExceptions. Given that we are planning to have a single exception type for the new CVC4 API, this seemed like a natural choice. Additionally, the commit (significantly) simplifies the mapping of C++ to Java exceptions and fixes an issue with Python exceptions not inheriting from BaseException. Finally, the commit adds API examples for Java and Python, which demonstrate catching exceptions, and adds Python examples as tests in our build system.
2020-06-08Ensure correct CMake dependencies on ↵Andrew V. Jones
Debug_tags.h/Trace_tags.h/git_versioninfo.cpp (#4570) ## Issue When building CVC4, and when there are no source code codes (a so-called "no op" build), it seems that some of CMake targets are still fired: ``` [avj@tempvm build]$ ninja -d explain -d stats ninja explain: output proofs/signatures/all of phony edge with no inputs doesn't exist ninja explain: proofs/signatures/all is dirty ninja explain: output doc/all of phony edge with no inputs doesn't exist ninja explain: doc/all is dirty ninja explain: output src/base/CMakeFiles/gen-gitinfo doesn't exist ninja explain: src/base/CMakeFiles/gen-gitinfo is dirty ninja explain: output src/base/CMakeFiles/gen-tags-debug doesn't exist ninja explain: src/base/Debug_tags.tmp is dirty ninja explain: src/base/CMakeFiles/gen-tags-debug is dirty ninja explain: src/base/Debug_tags.tmp is dirty ninja explain: output src/base/CMakeFiles/gen-tags-trace doesn't exist ninja explain: src/base/CMakeFiles/gen-tags-trace is dirty ninja explain: src/base/Trace_tags.tmp is dirty ninja explain: src/base/Debug_tags is dirty ninja explain: src/base/Debug_tags.h is dirty ninja explain: src/base/Trace_tags.tmp is dirty ninja explain: src/base/Trace_tags is dirty ninja explain: src/base/Trace_tags.h is dirty ninja explain: src/base/CMakeFiles/gen-tags is dirty ninja explain: src/base/Debug_tags.h is dirty ninja explain: src/base/Trace_tags.h is dirty ninja explain: src/base/Debug_tags is dirty ninja explain: src/base/Trace_tags is dirty ninja explain: src/base/gen-tags-debug is dirty ninja explain: src/base/gen-tags-trace is dirty ninja explain: output src/base/all of phony edge with no inputs doesn't exist ninja explain: src/base/all is dirty ninja explain: output src/expr/all of phony edge with no inputs doesn't exist ninja explain: src/expr/all is dirty ninja explain: output src/options/all of phony edge with no inputs doesn't exist ninja explain: src/options/all is dirty ninja explain: output src/theory/all of phony edge with no inputs doesn't exist ninja explain: src/theory/all is dirty ninja explain: output src/util/all of phony edge with no inputs doesn't exist ninja explain: src/util/all is dirty ninja explain: src/all is dirty ninja explain: output test/regress/all of phony edge with no inputs doesn't exist ninja explain: test/regress/all is dirty ninja explain: test/all is dirty [5/6] Generating Trace_tags metric count avg (us) total (ms) .ninja parse 2 7192.5 14.4 canonicalize str 3315 0.2 0.7 canonicalize path 3315 0.2 0.5 lookup node 5325 0.2 1.1 .ninja_log load 1 548.0 0.5 .ninja_deps load 1 3882.0 3.9 node stat 2234 1.4 3.0 StartEdge 12 76.8 0.9 FinishCommand 5 74.6 0.4 path->node hash load 0.77 (2468 entries / 3209 buckets) ``` This is mainly because `gen-tags-debug`, `gen-tags-trace` and `gen-gitinfo` are targets with no (stated) outputs and nothing that generates them. ## Solution This commit cleans-up the CMake inside of `src/base/CMakeLists.txt` such that, on an incremental build with no changes, no targets are fired: ``` [avj@tempvm build]$ ninja -d explain -d stats ninja explain: output proofs/signatures/all of phony edge with no inputs doesn't exist ninja explain: proofs/signatures/all is dirty ninja explain: output doc/all of phony edge with no inputs doesn't exist ninja explain: doc/all is dirty ninja explain: output src/base/all of phony edge with no inputs doesn't exist ninja explain: src/base/all is dirty ninja explain: output src/expr/all of phony edge with no inputs doesn't exist ninja explain: src/expr/all is dirty ninja explain: output src/options/all of phony edge with no inputs doesn't exist ninja explain: src/options/all is dirty ninja explain: output src/theory/all of phony edge with no inputs doesn't exist ninja explain: src/theory/all is dirty ninja explain: output src/util/all of phony edge with no inputs doesn't exist ninja explain: src/util/all is dirty ninja explain: src/all is dirty ninja explain: output test/regress/all of phony edge with no inputs doesn't exist ninja explain: test/regress/all is dirty ninja explain: test/all is dirty ninja: no work to do. metric count avg (us) total (ms) .ninja parse 2 9198.0 18.4 canonicalize str 5314 0.2 1.1 canonicalize path 5314 0.2 0.9 lookup node 7324 0.2 1.6 .ninja_log load 1 635.0 0.6 .ninja_deps load 1 4309.0 4.3 node stat 2240 1.3 3.0 path->node hash load 0.78 (2490 entries / 3209 buckets) ``` The important bit is `ninja: no work to do.` in the output. ### Notes I think the only thing to note is that I have changed the CMake around this comment: ``` # Note: gen-tags-{debug,trace} are targets since we always want to generate # the temporary tag files {Debug,Trace}_tags.tmp in order to check if tags # were added/modified/deleted. ``` I believe that the intention here was to ensure that the tags are **always** generated on a source file change. Given that the CVC4 CMake is passing in the files to be processed (`${source_files_list}`, which is a *string*), we can add a target dependency on this *list* (`${source_files}`) to ensure that `{Debug,Trace}_tags.tmp` always get regenerated on a change. So I believe I have captured the intent of the comment, without requiring the targets to be "unconditional". I have also added a dependency on `${gentmptags_script}`/`${gentags_script}`/`${genheader_script}` in some places because, without this, if you change one of `${gentmptags_script}`/`${gentags_script}`/`${genheader_script}` then the associated targets don't get fired. Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
2020-05-22Add support for SAT solver Kissat. (#4514)Aina Niemetz
2020-05-05Update copyright year and AUTHORS/THANKS files. (#4468)Aina Niemetz
2020-03-31Remove replay and use-theory options and idl (#4186)Andrew Reynolds
Towards disentangling Options / NodeManager / SmtEngine. This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work. The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it. The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging. It also removes the solver in src/theory/idl, which cannot be enabled after this commit.
2020-02-02Renaming '--bsd' to '--no-gpl' (#3609)Andrew V. Jones
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
2019-11-29improving parsing error messages related to HOL (#3510)Haniel Barbosa
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
This commit enables compiler warnings for implicit fallthroughs in switch statements that are not explicitly marked as such. The commit introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate that a fallthrough is intentional. The commit fixes existing warnings and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't be triggered easily because we rewrite `abs` to an `ite` while expanding definitions). To have the new macro also available in the parser, the commit changes `src/base/check.h` to be visible to the parser (it includes `cvc4_private_library.h` now instead of `cvc4_private.h`).
2019-11-16Add support for ThreadSanitizer instrumentation (#3467)Andres Noetzli
This commit adds support for compiling CVC4 with ThreadSanitizer instrumentation. This is useful for debugging issues when CVC4 is used in a multi-threaded context (e.g. #3292).
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-11Add support for UBSan instrumentation (#3382)Andres Noetzli
This commit adds support for compiling CVC4 with UBSan instrumentation. The commit also adds a dummy version of `AigBitblaster`. Previously, when CVC4 was built without ABC, `AigBitblaster` was not fully defined (the class was declared but the implementation was not being compiled). This lead to missing RTTI information when compiling with UBSan instrumentation.
2019-09-11Fix not to output all warnings (#2778)Ken Matsui
Fix syntax error when --language-bindings is java Replace __attribute__((__unused__)) with CVC4_UNUSED macro Signed-off-by: matken11235 <26405363+matken11235@users.noreply.github.com>
2019-09-04 Fixes related to destructing null (#3231)Andrew Reynolds
2019-08-08Fix issues with Ninja build system and add configure option. (#3166)Mathias Preiner
Adds option --ninja to configure.sh.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback