Age | Commit message (Collapse) | Author |
|
|
|
|
|
This comment was slightly out-of-date.
|
|
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`).
|
|
|
|
|
|
* Updates to the unit tests, api, and examples for datatypes
* Format
|
|
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).
|
|
|
|
|
|
|
|
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.
|
|
Fixes #3353. #3062 introduced a flag that tracks whether we have seen a
`(set-logic ...)` command to improve the handling of `--force-logic`.
However, the flag was not set to `false` when `(reset)` was called. This
commit fixes the issue.
|
|
|
|
* Refactor non-linear extension for model-based refinement
* Format
* Minor
* Address
|
|
|
|
|
|
|
|
|
|
|
|
The current code is creating/destroying datatypes unnecessarily.
|
|
Fixes #971.
|
|
This is work towards splitting a "core solver" object from TheoryStrings.
This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects.
It also corrects an issue where we were maintaining two `d_conflict` fields.
|
|
This adds node-level interfaces for a few missing functions that will be necessary to have a Node-level API for datatypes.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit fixes some minor (performance) issues in
`TheoryStrings::checkFlatForms()`: The `inelig` vector was initialized
with copies of the `start` element instead of all the elements before
`start` and the `else` branch of `count == asize` was looping over all
elements from `1` instead of `start + 1`. Additionally, this commit
refactors the code to be a bit more readable.
|
|
|
|
|
|
|
|
|
|
* Split arith util
* Cleaner
* cpp
* Format
* Minor
|
|
* Towards fix for non-linear models
* Format
* Fix
* More
* Improve
* Format
* More
|
|
|
|
This ensures we add lemmas when collect model info fails for the higher order extension of UF. This fixes #3405 (that benchmark now answers unknown).
|
|
|
|
This commit fixes numerous issues involving the combination of SyGuS and regular expressions.
Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior.
|
|
This refactors skolems introduced in the theory of sets. This is analogous to how skolems are treated for the theory of strings.
A key change that this commit enables is to identify "variable" sets based on those that weren't introduced by the SkolemCache (instead of via a check that their kind is `VARIABLE`, which is done currently and is error prone).
|
|
Previously, the metakind header defined macros for the number of bits
reserved for fields in the NodeValue "header" (for the reference count,
the node kind, the number of children and the node id). These macros
were redundant, since the only one using them was the NodeValue itself,
which redefined them (while using them) as constants in the class.
Additionally, MAX_CHILDREN was defined (using these macros) not only
in the metakind header, but redefined in other places.
This commit defines the above values as constexpr members of the
NodeValue class and cleans up redundancy.
|
|
definitions (#3399)
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|