From 8f9f8a79a55a7c478f8d26894f4d2e7023c5a39c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Apr 2021 15:45:39 -0500
Subject: [PATCH] Set incomplete if not applying ho extensionality (#6281)

If the user manually disables ho-extensionality via expert option --no-uf-ho-ext, we should answer "unknown" instead of "sat" when applicable.

Fixes #4318.
---
 src/theory/uf/ho_extension.cpp | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index ebbc75e00..ee3753e92 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -202,12 +202,14 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
                  << isCollectModel << "..." << std::endl;
   std::map<TypeNode, std::vector<Node> > func_eqcs;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
+  bool hasFunctions = false;
   while (!eqcs_i.isFinished())
   {
     Node eqc = (*eqcs_i);
     TypeNode tn = eqc.getType();
     if (tn.isFunction())
     {
+      hasFunctions = true;
       // if during collect model, must have an infinite type
       // if not during collect model, must have a finite type
       if (tn.isInterpretedFinite() != isCollectModel)
@@ -219,6 +221,16 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
     }
     ++eqcs_i;
   }
+  if (!options::ufHoExt())
+  {
+    // we are not applying extensionality, thus we are incomplete if functions
+    // are present
+    if (hasFunctions)
+    {
+      d_im.setIncomplete();
+    }
+    return 0;
+  }
 
   for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin();
        itf != func_eqcs.end();
@@ -403,17 +415,14 @@ unsigned HoExtension::check()
     }
   } while (num_facts > 0);
 
-  if (options::ufHoExt())
-  {
-    unsigned num_lemmas = 0;
+  unsigned num_lemmas = 0;
 
-    num_lemmas = checkExtensionality();
-    if (num_lemmas > 0)
-    {
-      Trace("uf-ho") << "...extensionality returned " << num_lemmas
-                     << " lemmas." << std::endl;
-      return num_lemmas;
-    }
+  num_lemmas = checkExtensionality();
+  if (num_lemmas > 0)
+  {
+    Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas."
+                   << std::endl;
+    return num_lemmas;
   }
 
   Trace("uf-ho") << "...finished check higher order." << std::endl;
-- 
2.30.2