diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 19:47:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-02 19:47:52 -0500 |
commit | 5f3d21a7402538af837eaf943b5252b1db90080b (patch) | |
tree | 0f8a791a8b9fcd03545f720df1110516ada7689e /src/preprocessing/passes/quantifiers_preprocess.cpp | |
parent | 4e6eb0a191ec78cbebd842f9c732ef9bd76bd724 (diff) |
(proof-new) Support proofs of quantifier instantiation (#5001)
This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.
Diffstat (limited to 'src/preprocessing/passes/quantifiers_preprocess.cpp')
-rw-r--r-- | src/preprocessing/passes/quantifiers_preprocess.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index 3052e9629..cda7ad67a 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -39,9 +39,10 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal( for (size_t i = 0; i < size; ++i) { Node prev = (*assertionsToPreprocess)[i]; - Node next = quantifiers::QuantifiersRewriter::preprocess(prev); - if (next != prev) + TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(prev); + if (!trn.isNull()) { + Node next = trn.getNode(); assertionsToPreprocess->replace(i, Rewriter::rewrite(next)); Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-preprocess") |