| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Further, print definitions added with add_definitions(...).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
TODO: cvc4autoconfig.h
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.
This is in preparation for working on solving equations and further inferences in this style.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.
|
|
|
|
|
|
|
|
|
|
(#2478)
|
|
equal (#2444)
This fixes #2429.
This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment.
We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.
Regardless, the strings model construction should be robust to handle this case, which this PR does.
|
|
Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:
- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.
This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously. Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).
[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117
|
|
With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.
|
|
|
|
|
|
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
|
|
This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).
It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.
|
