Age | Commit message (Collapse) | Author |
|
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>
|
|
Since the new BV solver is enabled by default and uses CaDiCaL
(and optionally CryptoMiniSat) we make CaDiCaL a required dependency.
|
|
|
|
|
|
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.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
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>
|
|
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.
|
|
|
|
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.
|
|
Make collect_tags.py more robust for non-ASCII characters.
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
|
|
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/.
|
|
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
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.
|
|
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>
|
|
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.
|
|
|
|
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.
|
|
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>
|
|
|
|
|
|
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.
|
|
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
|
|
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`).
|
|
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).
|
|
|
|
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.
|
|
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>
|
|
|
|
Adds option --ninja to configure.sh.
|
|
|
|
`let_shadowing.smt2` uses dumping to test our printing infrastructure.
Since some builds do not support dumping, this commit disables that
regression for non-dumping builds. Additionally, it enables an error
message when trying to dump with a muzzled build and corrects the output
of `--show-config` to indicate that muzzled builds cannot dump.
Previously, the dumping output of a muzzled build was just silently
empty.
Most of the changes in `dump.cpp` are due to reformatting.
|
|
Fixes 2887.
|