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/sygus_inference.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/sygus_inference.cpp')
-rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
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) |