| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This sets up the preprocessing pass context in preparation for proof production.
This PR makes the top level substitutions map into a TrustSubstitutionMap, the data structure that applies substitutions in a way that tracks proofs.
This PR also makes the "apply subst" preprocessing pass proof producing.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.
The changes that were required for this PR include:
The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.
|
|
|
|
|
|
Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.
|
|
This is in preparation of fixing the issue we currently have with
reset-assertions. This also removes a competition hack for QF_LRA.
|
|
This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.
|
|
This is in preparation of fixing the issue we currently have with reset-assertions.
This also removes a competition hack for QF_LRA.
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
When we do solving in incremental mode, we store substitutions at a
special index in our list of assertions. Previously, we used a
context-dependent variable for that. However, this is not needed since
the list of assertions just consists of the assertions currently being
processed, which are independent of the assertions seen so far. This
commit changes the index to be an ordinary integer and moves it to the
AssertionPipeline. Additionally, it abstracts access to the index in
preparation for splitting AssertionPipeline into three vectors (see
issue #2473).
|
|
Fixes 2887.
|
|
|
|
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 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.
|
|
|
|
|
|
|
|
This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.
|
|
This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).
|
