From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 26 Nov 2020 03:00:13 +0000 (-0600)
Subject: Fix missed case of theory preprocessing (#5531)
X-Git-Tag: cvc5-1.0.0~2549
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0c352ec04846353d630073e78e5b2fea92133c2;p=cvc5.git

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.
---

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;