Make skolem definition manager robust to function skolems (#7327)

This led to a model soundness issue in a development branch that reorganizes theory preprocessing.

This ensures that skolem definition manager looks for skolems that appear in operators.

This is important for inputs like:
(declare-fun h (Int) Int)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= h (ite A f g)))
(assert (= (h 0) ...)))

diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
index 5b51d730c798fd199905a834a5bf9af15d25214a..36849424e0ab26284a57d030d73be92f7a6cf304 100644 (file)
--- a/src/prop/skolem_def_manager.cpp
+++ b/src/prop/skolem_def_manager.cpp
@@ -121,20 +121,33 @@ bool SkolemDefManager::hasSkolems(TNode n) const
       }
       else
       {
+        if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+        {
+          visit.push_back(cur.getOperator());
+        }
         visit.insert(visit.end(), cur.begin(), cur.end());
       }
     }
     else
     {
       visit.pop_back();
-      bool hasSkolem = false;
-      for (TNode i : cur)
+      bool hasSkolem;
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED
+          && cur.getOperator().getAttribute(HasSkolemAttr()))
       {
-        Assert(i.getAttribute(HasSkolemComputedAttr()));
-        if (i.getAttribute(HasSkolemAttr()))
+        hasSkolem = true;
+      }
+      else
+      {
+        hasSkolem = false;
+        for (TNode i : cur)
         {
-          hasSkolem = true;
-          break;
+          Assert(i.getAttribute(HasSkolemComputedAttr()));
+          if (i.getAttribute(HasSkolemAttr()))
+          {
+            hasSkolem = true;
+            break;
+          }
         }
       }
       cur.setAttribute(HasSkolemAttr(), hasSkolem);
@@ -172,11 +185,13 @@ void SkolemDefManager::getSkolems(TNode n,
         {
           skolems.insert(cur);
         }
+        continue;
       }
-      else
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
-        visit.insert(visit.end(), cur.begin(), cur.end());
+        visit.push_back(cur.getOperator());
       }
+      visit.insert(visit.end(), cur.begin(), cur.end());
     }
   } while (!visit.empty());
 }