| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
This implements solution number 2 for issue #2613.
|
|
|
|
|
|
|
|
|
|
|
|
This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.
|
|
This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.
As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.
This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.
[0] https://llvm.org/docs/WritingAnLLVMPass.html
|
|
|
|
|
|
|
|
|
|
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 adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
|
|
|
|
|
|
propagator. (#2421)
|
|
|
|
|
|
|
|
|
|
|
|
Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`,
and added the necessary methods for inheritance from PreprocessingPass.
No need to add a test - regress0 fails when adding Assert(false) when assertions had changed.
|
|
|
|
|
|
(#2234)
|
|
|
|
|
|
|
|
|
|
(#2321)
|
|
|
|
|
|
|
|
This corrects a bug that was introduced in #2266 (the hack removed there was necessary).
This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus.
This also enables total semantics for BV div-by-zero for sygus.
|
|
|
|
|
|
|
|
This commit refactors the IteRemoval pass to follow the new format.
In addition to moving the code, this entails the following changes:
- The timer for the ITE removal is now called differently (the default
timer of PreprocessingPass is used) and measures just the
preprocessing pass without applySubstitutions(). It also measures the
time used by both invocations of the ITE removal pass.
- Debug output will be slightly different because we now just rely on
the default functionality of PreprocessingPass.
- d_iteRemover is now passed into the PreprocessingPassContext.
- AssertionPipeline now owns the d_iteSkolemMap, which makes it
accessible by preprocessing passes. The idea behind this is that the
preprocessing passes collect information in AssertionPipeline and
d_iteSkolemMap fits that pattern.
|
|
|
|
|
|
|
|
Since we are using C++11, we can replace the triple and quad classes
with std::tuple.
|
|
|
|
When dumping a `get-unsat-assumptions` command, CVC4 was instead dumping
two `get-unsat-cores` commands. This commit splits
`SmtEngine::getUnsatCores()` into a part that does the dumping and an
internal part that actually gets the unsat core without dumping.
`SmtEngine::getUnsatAssumptions()` now calls the internal version to
avoid the redundant dumping of a `get-unsat-cores` command and changes
the command that gets dumped in `SmtEngine::getUnsatAssumptions()`.
|
