| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The `normalize*` methods in `ceg_bv_instantiator_utils.{h,cpp}` each modify a
map that marks terms in which `pv` occurs. The map was mapping `TNode`s to
`bool`s. The problem was that the keys in the map could be new terms that
needed to be kept alive for the map to remain valid. When compiling CVC4 with
Clang under macOS, `theory_quantifiers_bv_instantiator_white` and
`theory_quantifiers_bv_inverter_white` were failing because the reference count
of keys in the map reached zero. Generally, the critical keys are contained in
the result of the functions and kept alive by the `visited` stack in
`rewriteAssertionForSolvePv()`. The unit test
`theory_quantifiers_bv_instantiator_white` did not keep the results alive,
resulting in reference counts reaching zero. However, the failure of
`theory_quantifiers_bv_inverter_white` shows that the issue is not limited to
the unit tests of the `normalize*` methods. To avoid this issue, this commit
changes the map to use `Node` keys instead (so the map itself keeps the keys
alive).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Towards fix for non-linear models
* Format
* Fix
* More
* Improve
* Format
* More
|
|
|
|
|
|
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.
|
|
|
|
PR #3388 didn't disable the regression correctly (due to using `REQUIRE`
instead of `REQUIRES`). This commit fixes the issue.
|
|
This commit disables a regression test that was failing for the
competition build due to not emitting the expected error message.
|
|
|
|
|
|
|
|
|
|
Fixes #1399.
|
|
|
|
TS_UTILS_EXPECT_ABORT can be used if an expression in a unit test is
expected to abort() instead of throwing an exception. This can happen if
CVC4_CHECK or CVC4_DCHECK fail.
|
|
CVC4 was printing success when `--force-logic` was used because
internally, `--force-logic` generates a `SetBenchmarkLogicCommand`. This
caused issues with the SMT-COMP trace executor. This commit fixes the
behavior by muting the command if it was not issued by the user.
The issue was likely introduced with #3062.
|
|
Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
|
|
This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar.
It also fixes an issue where skolem variables were not being treated as functions-to-synthesize.
Fixes #3250 and fixes #3356.
|
|
|
|
|
|
|
|
The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.
|
|
+ use explicit types in NodeValue
+ add unit test for Term::isParameterized()
Co-Authored-By: makaimann <makaim@stanford.edu>
|
|
|
|
This fixes a corner case of the str-to-int reduction for the case where the argument is the empty string.
This fixes #3357.
|
|
This commit makes CVC4 complain if the user asked for proofs for an unsupported logic (in this contest, ALL is considered unsupported).
Changes in the regression script are introduced as well, in order to only request proofs for regressions in supported logics.
|
