diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-25 21:00:13 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-25 19:00:13 -0800 |
commit | d0c352ec04846353d630073e78e5b2fea92133c2 (patch) | |
tree | 41255824f4f72f0eccbc7dbb2402cb46b5b9e54a | |
parent | 084518db641e0648164bbe4461cd98b10e937dc0 (diff) |
Fix missed case of theory preprocessing (#5531)
This fixes a rare case of theory preprocessing where rewriting a quantified formula would introduce a term that would not be preprocessed. This led to solution unsoundness on a branch where the relationship between expand definitions and preprocessing is modified.
This is required for updating to the new policy for expand definitions.
-rw-r--r-- | src/theory/theory_preprocessor.cpp | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 3b68a33ca..f5e5fa505 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -350,30 +350,32 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term) { return (*find).second; } - unsigned nc = term.getNumChildren(); - if (nc == 0) + if (term.getNumChildren() == 0) { return preprocessWithProof(term); } Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; - - Node newTerm = term; + // We must rewrite before preprocessing, because some terms when rewritten + // may introduce new terms that are not top-level and require preprocessing. + // An example of this is (forall ((x Int)) (and (tail L) (P x))) which + // rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L) + // must be preprocessed as a child here. + Node newTerm = rewriteWithProof(term); // do not rewrite inside quantifiers - if (!term.isClosure()) + if (newTerm.getNumChildren() > 0 && !newTerm.isClosure()) { - NodeBuilder<> newNode(term.getKind()); - if (term.getMetaKind() == kind::metakind::PARAMETERIZED) + NodeBuilder<> newNode(newTerm.getKind()); + if (newTerm.getMetaKind() == kind::metakind::PARAMETERIZED) { - newNode << term.getOperator(); + newNode << newTerm.getOperator(); } - unsigned i; - for (i = 0; i < nc; ++i) + for (const Node& nt : newTerm) { - newNode << ppTheoryRewrite(term[i]); + newNode << ppTheoryRewrite(nt); } newTerm = Node(newNode); + newTerm = rewriteWithProof(newTerm); } - newTerm = rewriteWithProof(newTerm); newTerm = preprocessWithProof(newTerm); d_ppCache[term] = newTerm; Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl; |