diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-04-14 14:50:10 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-14 17:50:10 +0000 |
| commit | b6db4446a28d498af8fb4e629392985dfe2a976c (patch) | |
| tree | b283483ce265b25bfdd8e769f2026dd414510ac3 /src/preprocessing/passes | |
| parent | f74bdbd182d95a8e6395aaaf348ca0e41baa3bf4 (diff) | |
[unsat-cores] Improving new unsat cores (#6356)
This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.
This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 2 | ||||
| -rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 068e47f13..a03ac21a3 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -62,7 +62,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) imap[assertions->size()] = newSkolems[j]; assertions->pushBackTrusted(newAsserts[j]); // new assertions have a dependence on the node (old pf architecture) - if (options::unsatCores() && !options::produceProofs()) + if (options::unsatCores()) { ProofManager::currentPM()->addDependence(newAsserts[j].getProven(), assertion); diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 66837267a..952ced4d5 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -86,7 +86,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap) for( int i=0; i<(int)assertions.size(); i++ ){ Trace("macros-debug") << " process assertion " << assertions[i] << std::endl; if( processAssertion( assertions[i] ) ){ - if (options::unsatCores() && !options::produceProofs() + if (options::unsatCores() && std::find(macro_assertions.begin(), macro_assertions.end(), assertions[i]) @@ -116,7 +116,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap) // is an over-approximation. a more fine-grained unsat core // computation would require caching dependencies for each subterm of // the formula, which is expensive. - if (options::unsatCores() && !options::produceProofs()) + if (options::unsatCores()) { ProofManager::currentPM()->addDependence(curr, assertions[i]); for (unsigned j = 0; j < macro_assertions.size(); j++) |