| Age | Commit message (Collapse) | Author |
|---|
|
PR #2764 removed `Solver::mkBitVector(uint32_t)` (returns a bit-vector
of a given size with value zero), which made the build fail when SymFPU
was enabled because solver_black used it for SymFPU-enabled builds. This
commit simply adds a zero default argument to `mkBitVector(uint32_t,
uint64_t)` to allow users to create zero-valued bit-vectors without
explicitly specifying the value again. Additionally, the commit replaces
the use of the `CVC4_USE_SYMFPU` macro by a call to
`Configuration::isBuiltWithSymFPU()`, making sure that we can catch
compile-time errors regardless of configuration. Finally,
`Solver::mkConst(Kind, uint32_t, uint32_t, Term)` now checks whether
CVC4 has been compiled with SymFPU when creating a `CONST_FLOATINGPOINT`
and throws an exception otherwise (solver_black has been updated
correspondingly).
|
|
|
|
|
|
|
|
|
|
This was causing assertion failures when using Sets + Sygus.
|
|
|
|
|
|
|
|
|
|
|
|
* Enable BV proofs when using and eager bitblaster
Specifically:
* Removed assertions that blocked them.
* Made sure that only bitvectors were stored in the BV const let-map
* Prevented true/false from being bit-blasted by the eager bitblaster
Also:
* uncommented "no-check-proofs" from relevant tests
* Option handler logic for BV proofs
BV eager proofs only work when minisat is the sat solver being used by
the BV theory.
Added logic to the --proof hanlder to verify this or throw an option
exception.
* Bugfix for proof options handler
I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.
* Clang-format
|
|
|
|
In certain cases, we can share skolems between similar reductions, e.g.
`(str.replace x y z)` and `(str.replace (str.substr x 0 n) y z)` because the
first occurrence of `y` in `x` has to be the first occurrence
of `y` in `(str.substr x 0 n)` (assuming that `y` appears in both, otherwise the value of
the skolems does not matter). This commit adds a helper function in the
skolem cache that does some of those simplifications.
|
|
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
|
|
Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.
This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.
After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.
|
|
|
|
|
|
initialized (#2708)
|
|
|
|
|
|
|
|
|
|
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
|
|
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
|
|
|
|
|
|
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
|
|
|
|
|
|
|
|
This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.
This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
|
|
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
|
|
|
|
|
|
|
|
|
|
|
|
This commit disables three regressions when using an ASAN build. The
regressions are all leaking memory when invoking the subsolver (see
issue #2649). Debugging the issue will take a while but is not very
critical since this feature is currently only used by CVC4 developers
but it prevents our nightly builds from going through.
|
|
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
|
|
|
|
This implements solution number 2 for issue #2613.
|
|
|
|
|
|
|
|
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
|
|
|
|
|
|
|
|
|
