Fix ho extensionality in collect model info (#3435)

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 0ca9b151fcb564344599267b9529da5c2fd113fb..6d6f49c7f5664f6473ac47d57633c5dd69bde3fd 100644 (file)
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -50,43 +50,49 @@ Node HoExtension::expandDefinition(Node node)
   return node;
 }
 
-Node HoExtension::getExtensionalityDeq(TNode deq)
+Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached)
 {
   Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
   Assert(deq[0][0].getType().isFunction());
-  std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
-  if (it == d_extensionality_deq.end())
+  if (isCached)
   {
-    TypeNode tn = deq[0][0].getType();
-    std::vector<TypeNode> argTypes = tn.getArgTypes();
-    std::vector<Node> skolems;
-    NodeManager* nm = NodeManager::currentNM();
-    for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+    std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
+    if (it != d_extensionality_deq.end())
     {
-      Node k =
-          nm->mkSkolem("k", argTypes[i], "skolem created for extensionality.");
-      skolems.push_back(k);
+      return it->second;
     }
-    Node t[2];
-    for (unsigned i = 0; i < 2; i++)
+  }
+  TypeNode tn = deq[0][0].getType();
+  std::vector<TypeNode> argTypes = tn.getArgTypes();
+  std::vector<Node> skolems;
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+  {
+    Node k =
+        nm->mkSkolem("k", argTypes[i], "skolem created for extensionality.");
+    skolems.push_back(k);
+  }
+  Node t[2];
+  for (unsigned i = 0; i < 2; i++)
+  {
+    std::vector<Node> children;
+    Node curr = deq[0][i];
+    while (curr.getKind() == HO_APPLY)
     {
-      std::vector<Node> children;
-      Node curr = deq[0][i];
-      while (curr.getKind() == HO_APPLY)
-      {
-        children.push_back(curr[1]);
-        curr = curr[0];
-      }
-      children.push_back(curr);
-      std::reverse(children.begin(), children.end());
-      children.insert(children.end(), skolems.begin(), skolems.end());
-      t[i] = nm->mkNode(APPLY_UF, children);
+      children.push_back(curr[1]);
+      curr = curr[0];
     }
-    Node conc = t[0].eqNode(t[1]).negate();
+    children.push_back(curr);
+    std::reverse(children.begin(), children.end());
+    children.insert(children.end(), skolems.begin(), skolems.end());
+    t[i] = nm->mkNode(APPLY_UF, children);
+  }
+  Node conc = t[0].eqNode(t[1]).negate();
+  if (isCached)
+  {
     d_extensionality_deq[deq] = conc;
-    return conc;
   }
-  return it->second;
+  return conc;
 }
 
 unsigned HoExtension::applyExtensionality(TNode deq)
@@ -228,8 +234,10 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
           // either add to model, or add lemma
           if (isCollectModel)
           {
-            // add extentionality disequality to the model
-            Node edeq = getExtensionalityDeq(deq);
+            // Add extentionality disequality to the model.
+            // It is important that we construct new (unconstrained) variables
+            // k here, so that we do not generate any inconsistencies.
+            Node edeq = getExtensionalityDeq(deq, false);
             Assert(edeq.getKind() == NOT && edeq[0].getKind() == EQUAL);
             // introducing terms, must add required constraints, e.g. to
             // force equalities between APPLY_UF and HO_APPLY terms

diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h
index a38d1803aa99b44ecb647b0aba81dc5961390d2e..47336e085fdf8bd3227e5d36845eb96ee5a39606 100644 (file)
--- a/src/theory/uf/ho_extension.h
+++ b/src/theory/uf/ho_extension.h
@@ -127,8 +127,12 @@ class HoExtension
    *
    * Given disequality deq f != g, this returns the disequality:
    *   (f k) != (g k) for fresh constant(s) k.
+   *
+   * If isCached is true, then this returns the same k for all calls to this
+   * method with the same deq. If it is false, it creates fresh k and does not
+   * cache the result.
    */
-  Node getExtensionalityDeq(TNode deq);
+  Node getExtensionalityDeq(TNode deq, bool isCached = true);
 
   /**
    * Check whether extensionality should be applied for any pair of terms in the