From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 9 Nov 2021 21:40:36 +0000 (-0600)
Subject: Only eliminate lambdas in higher-order elimination if ho-elim is enabled (#7603)
X-Git-Tag: cvc5-1.0.0~844
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d071aa5cfd697cab7177cd3b520a87aaf0049dd;p=cvc5.git

Only eliminate lambdas in higher-order elimination if ho-elim is enabled (#7603)

Required for lazy lambdas in HO.

Also properly guards the case when the preprocessing pass is a no-op.
---

diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index d3372a28e..e122b33d6 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -305,67 +305,76 @@ Node HoElim::eliminateHo(Node n)
 PreprocessingPassResult HoElim::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
+  // this preprocessing pass is only applicable if we are eliminating
+  // higher-order, or are adding the store axiom
+  if (!options().quantifiers.hoElim && !options().quantifiers.hoElimStoreAx)
+  {
+    return PreprocessingPassResult::NO_CONFLICT;
+  }
   // step [1]: apply lambda lifting to eliminate all lambdas
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> axioms;
-  std::map<Node, Node> newLambda;
-  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  if (options().quantifiers.hoElim)
   {
-    Node prev = (*assertionsToPreprocess)[i];
-    Node res = eliminateLambdaComplete(prev, newLambda);
-    if (res != prev)
+    std::map<Node, Node> newLambda;
+    for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
     {
-      res = rewrite(res);
-      Assert(!expr::hasFreeVar(res));
-      assertionsToPreprocess->replace(i, res);
+      Node prev = (*assertionsToPreprocess)[i];
+      Node res = eliminateLambdaComplete(prev, newLambda);
+      if (res != prev)
+      {
+        res = rewrite(res);
+        Assert(!expr::hasFreeVar(res));
+        assertionsToPreprocess->replace(i, res);
+      }
     }
-  }
-  // do lambda lifting on new lambda definitions
-  // this will do fixed point to eliminate lambdas within lambda lifting axioms.
-  while (!newLambda.empty())
-  {
-    std::map<Node, Node> lproc = newLambda;
-    newLambda.clear();
-    for (const std::pair<const Node, Node>& l : lproc)
+    // do lambda lifting on new lambda definitions
+    // this will do fixed point to eliminate lambdas within lambda lifting axioms.
+    while (!newLambda.empty())
     {
-      Node lambda = l.second;
-      std::vector<Node> vars;
-      std::vector<Node> nvars;
-      for (const Node& v : lambda[0])
+      std::map<Node, Node> lproc = newLambda;
+      newLambda.clear();
+      for (const std::pair<const Node, Node>& l : lproc)
       {
-        Node bv = nm->mkBoundVar(v.getType());
-        vars.push_back(v);
-        nvars.push_back(bv);
-      }
+        Node lambda = l.second;
+        std::vector<Node> vars;
+        std::vector<Node> nvars;
+        for (const Node& v : lambda[0])
+        {
+          Node bv = nm->mkBoundVar(v.getType());
+          vars.push_back(v);
+          nvars.push_back(bv);
+        }
 
-      Node bd = lambda[1].substitute(
-          vars.begin(), vars.end(), nvars.begin(), nvars.end());
-      Node bvl = nm->mkNode(BOUND_VAR_LIST, nvars);
+        Node bd = lambda[1].substitute(
+            vars.begin(), vars.end(), nvars.begin(), nvars.end());
+        Node bvl = nm->mkNode(BOUND_VAR_LIST, nvars);
 
-      nvars.insert(nvars.begin(), l.first);
-      Node curr = nm->mkNode(APPLY_UF, nvars);
+        nvars.insert(nvars.begin(), l.first);
+        Node curr = nm->mkNode(APPLY_UF, nvars);
 
-      Node llfax = nm->mkNode(FORALL, bvl, curr.eqNode(bd));
-      Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax
-                          << " for " << lambda << std::endl;
-      Assert(!expr::hasFreeVar(llfax));
-      Node llfaxe = eliminateLambdaComplete(llfax, newLambda);
-      Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for "
-                          << lambda << std::endl;
-      axioms.push_back(llfaxe);
+        Node llfax = nm->mkNode(FORALL, bvl, curr.eqNode(bd));
+        Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax
+                            << " for " << lambda << std::endl;
+        Assert(!expr::hasFreeVar(llfax));
+        Node llfaxe = eliminateLambdaComplete(llfax, newLambda);
+        Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for "
+                            << lambda << std::endl;
+        axioms.push_back(llfaxe);
+      }
     }
-  }
 
-  d_visited.clear();
-  // add lambda lifting axioms as a conjunction to the first assertion
-  if (!axioms.empty())
-  {
-    Node conj = nm->mkAnd(axioms);
-    conj = rewrite(conj);
-    Assert(!expr::hasFreeVar(conj));
-    assertionsToPreprocess->conjoin(0, conj);
+    d_visited.clear();
+    // add lambda lifting axioms as a conjunction to the first assertion
+    if (!axioms.empty())
+    {
+      Node conj = nm->mkAnd(axioms);
+      conj = rewrite(conj);
+      Assert(!expr::hasFreeVar(conj));
+      assertionsToPreprocess->conjoin(0, conj);
+    }
+    axioms.clear();
   }
-  axioms.clear();
 
   // step [2]: eliminate all higher-order constraints
   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 23ef3936c..b08b2f6f5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1725,7 +1725,6 @@ set(regress_1_tests
   regress1/fmf/sort-inf-int.smt2
   regress1/fmf/with-ind-104-core.smt2
   regress1/gensys_brn001.smt2
-  regress1/ho/bug_freevar_PHI004^4-delta.smt2
   regress1/ho/bug_freeVar_BDD_General_data_270.p
   regress1/ho/bound_var_bug.p
   regress1/ho/fta0328.lfho.p
@@ -2804,6 +2803,8 @@ set(regression_disabled_tests
   ###
   regress1/bug472.smt2
   regress1/datatypes/non-simple-rec-set.smt2
+  # disabled temporarily until lazy lambda handling is merged
+  regress1/ho/bug_freevar_PHI004^4-delta.smt2
   # results in an assertion failure (see issue #1650).
   regress1/ho/hoa0102.smt2
   # after disallowing solving for terms with quantifiers