| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Improves the existing implementation for sygus-active-gen=basic.
|
|
|
|
|
|
|
|
|
|
|
|
Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588
Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
|
|
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
|
|
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.
|
|
Is not required anymore since we don't use autotools anymore.
|
|
|
|
(#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
|
|
const. (#2647)
|
|
|
|
|
|
|
|
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 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.
|
|
|
|
|
|
const. (#2643)
Match: `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`
On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
| CVC4-base | CVC4-concatpullup-or |
BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] |
totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 |
```
|
|
ones (#2596).
|
|
1 (#2596).
|
|
0 (#2596).
|
|
|
|
|
|
|
|
|
|
|
|
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`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
