From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 10 Feb 2021 00:21:56 +0000 (-0600)
Subject: Do not traverse quantifiers in term formula removal (#5859)
X-Git-Tag: cvc5-1.0.0~2295
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dcc1a5ff44ed83bdc1e2abcac3aebb299a376b08;p=cvc5.git

Do not traverse quantifiers in term formula removal (#5859)

Our current policy for term formula removal leaves quantifier bodies unchanged. This simplifies the code based on this observation.
---

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 0df521c0b..0b9d2d9c9 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -180,6 +180,11 @@ Node RemoveTermFormulas::runInternal(TNode assertion,
         ctx.pop();
         processedChildren.pop_back();
       }
+      else if (node.isClosure())
+      {
+        // currently, we never do any term formula removal in quantifier bodies
+        d_tfCache.insert(curr, node);
+      }
       else
       {
         size_t nchild = node.getNumChildren();
@@ -253,6 +258,7 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
   RtfTermContext::getFlags(curr.second, inQuant, inTerm);
   Debug("ite") << "removeITEs(" << node << ")"
                << " " << inQuant << " " << inTerm << std::endl;
+  Assert(!inQuant);
 
   NodeManager *nodeManager = NodeManager::currentNM();
 
@@ -269,57 +275,54 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
     // not in a quantified formula. This policy should be in sync with
     // the policy for when to apply theory preprocessing to terms, see PR
     // #5497.
-    if (!inQuant)
+    skolem = getSkolemForNode(node);
+    if (skolem.isNull())
     {
-      skolem = getSkolemForNode(node);
-      if (skolem.isNull())
-      {
-        Trace("rtf-proof-debug")
-            << "RemoveTermFormulas::run: make ITE skolem" << std::endl;
-        // Make the skolem to represent the ITE
-        SkolemManager* sm = nodeManager->getSkolemManager();
-        skolem = sm->mkPurifySkolem(
-            node,
-            "termITE",
-            "a variable introduced due to term-level ITE removal");
-        d_skolem_cache.insert(node, skolem);
+      Trace("rtf-proof-debug")
+          << "RemoveTermFormulas::run: make ITE skolem" << std::endl;
+      // Make the skolem to represent the ITE
+      SkolemManager* sm = nodeManager->getSkolemManager();
+      skolem = sm->mkPurifySkolem(
+          node,
+          "termITE",
+          "a variable introduced due to term-level ITE removal");
+      d_skolem_cache.insert(node, skolem);
 
-        // The new assertion
-        newAssertion = nodeManager->mkNode(
-            kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
+      // The new assertion
+      newAssertion = nodeManager->mkNode(
+          kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
 
-        // we justify it internally
-        if (isProofEnabled())
-        {
-          Trace("rtf-proof-debug")
-              << "RemoveTermFormulas::run: justify " << newAssertion
-              << " with ITE axiom" << std::endl;
-          // ---------------------- REMOVE_TERM_FORMULA_AXIOM
-          // (ite node[0]
-          //      (= node node[1])            ------------- MACRO_SR_PRED_INTRO
-          //      (= node node[2]))           node = skolem
-          // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
-          // (ite node[0] (= skolem node[1]) (= skolem node[2]))
-          //
-          // Note that the MACRO_SR_PRED_INTRO step holds due to conversion
-          // of skolem into its witness form, which is node.
-          Node axiom = getAxiomFor(node);
-          d_lp->addStep(axiom, PfRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node});
-          Node eq = node.eqNode(skolem);
-          d_lp->addStep(eq, PfRule::MACRO_SR_PRED_INTRO, {}, {eq});
-          d_lp->addStep(newAssertion,
-                        PfRule::MACRO_SR_PRED_TRANSFORM,
-                        {axiom, eq},
-                        {newAssertion});
-          newAssertionPg = d_lp.get();
-        }
+      // we justify it internally
+      if (isProofEnabled())
+      {
+        Trace("rtf-proof-debug")
+            << "RemoveTermFormulas::run: justify " << newAssertion
+            << " with ITE axiom" << std::endl;
+        // ---------------------- REMOVE_TERM_FORMULA_AXIOM
+        // (ite node[0]
+        //      (= node node[1])            ------------- MACRO_SR_PRED_INTRO
+        //      (= node node[2]))           node = skolem
+        // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
+        // (ite node[0] (= skolem node[1]) (= skolem node[2]))
+        //
+        // Note that the MACRO_SR_PRED_INTRO step holds due to conversion
+        // of skolem into its witness form, which is node.
+        Node axiom = getAxiomFor(node);
+        d_lp->addStep(axiom, PfRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node});
+        Node eq = node.eqNode(skolem);
+        d_lp->addStep(eq, PfRule::MACRO_SR_PRED_INTRO, {}, {eq});
+        d_lp->addStep(newAssertion,
+                      PfRule::MACRO_SR_PRED_TRANSFORM,
+                      {axiom, eq},
+                      {newAssertion});
+        newAssertionPg = d_lp.get();
       }
     }
   }
   else if (node.getKind() == kind::LAMBDA)
   {
     // if a lambda, do lambda-lifting
-    if (!inQuant || !expr::hasFreeVar(node))
+    if (!expr::hasFreeVar(node))
     {
       skolem = getSkolemForNode(node);
       if (skolem.isNull())
@@ -363,7 +366,7 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
     // If a witness choice
     //   For details on this operator, see
     //   http://planetmath.org/hilbertsvarepsilonoperator.
-    if (!inQuant || !expr::hasFreeVar(node))
+    if (!expr::hasFreeVar(node))
     {
       // NOTE: we can replace by t if body is of the form (and (= z t) ...)
       skolem = getSkolemForNode(node);
@@ -411,8 +414,7 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
     }
   }
   else if (node.getKind() != kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean()
-           && inTerm
-           && !inQuant)
+           && inTerm)
   {
     // if a non-variable Boolean term within another term, replace it
     skolem = getSkolemForNode(node);