From d0c352ec04846353d630073e78e5b2fea92133c2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 21:00:13 -0600 Subject: [PATCH] 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. --- src/theory/theory_preprocessor.cpp | 26 ++++++++++++++------------ 1 file 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; -- 2.30.2