diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-12 03:45:29 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-12 10:45:29 +0100 |
| commit | d47a8708171f1cf488fe9ce05f56f2566db53093 (patch) | |
| tree | d9c1e5b69d5acb3d44483c42750aa4de4b01082c /src/preprocessing | |
| parent | dd89a91a12afb86ae34497f2e8b2ebe95ec377a5 (diff) | |
Simplify and fix decision engine's handling of skolem definitions (#5888)
This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver.
With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to.
This also simplifies related interfaces within decision engine.
We should test this PR with --decision=justification on SMT-LIB.
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/assertion_pipeline.h | 2 | ||||
| -rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 2 | ||||
| -rw-r--r-- | src/preprocessing/passes/theory_preprocess.cpp | 2 |
3 files changed, 4 insertions, 2 deletions
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index fcfce0e87..9d65329b0 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -30,6 +30,8 @@ namespace CVC4 { namespace preprocessing { +using IteSkolemMap = std::unordered_map<size_t, Node>; + /** * Assertion Pipeline stores a list of assertions modified by preprocessing * passes. It is assumed that all assertions after d_realAssertionsEnd were diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index c8b713894..0a35e32eb 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -54,7 +54,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) Assert(newSkolems.size() == newAsserts.size()); for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) { - imap[newSkolems[j]] = assertions->size(); + imap[assertions->size()] = newSkolems[j]; assertions->pushBackTrusted(newAsserts[j]); // new assertions have a dependence on the node (old pf architecture) if (options::unsatCores() && !options::proofNew()) diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 50831f585..22ae14762 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -51,7 +51,7 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( Assert(newSkolems.size() == newAsserts.size()); for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) { - imap[newSkolems[j]] = assertions->size(); + imap[assertions->size()] = newSkolems[j]; assertions->pushBackTrusted(newAsserts[j]); // new assertions have a dependence on the node (old pf architecture) if (options::unsatCores()) |