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 | |
| 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')
| -rw-r--r-- | src/preprocessing/passes/quantifiers_preprocess.cpp | 5 | ||||
| -rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 7 |
2 files changed, 9 insertions, 3 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") diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index d44321a35..82515c6a4 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -24,6 +24,7 @@ using namespace std; using namespace CVC4::kind; +using namespace CVC4::theory; namespace CVC4 { namespace preprocessing { @@ -135,7 +136,11 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions, if (pas.getKind() == FORALL) { // preprocess the quantified formula - pas = theory::quantifiers::QuantifiersRewriter::preprocess(pas); + TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(pas); + if (!trn.isNull()) + { + pas = trn.getNode(); + } Trace("sygus-infer-debug") << " ...preprocessed to " << pas << std::endl; } if (pas.getKind() == FORALL) |