Fix model construction for higher order involving irrelevant function terms (#7526)

This fixes a bug in HO model construction where we were communicating information about irrelevant function terms to the model, leading to incorrect models.

diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index fd7cd467e6bceee1a4a31add1edca26774d134d0..e23262746b38b56c21b6192bc730ecb23c397ebd 100644 (file)
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -200,7 +200,11 @@ Node HoExtension::getApplyUfForHoApply(Node node)
 
 unsigned HoExtension::checkExtensionality(TheoryModel* m)
 {
-  eq::EqualityEngine* ee = d_state.getEqualityEngine();
+  // if we are in collect model info, we require looking at the model's
+  // equality engine, so that we only consider "relevant" (see
+  // Theory::computeRelevantTerms) function terms.
+  eq::EqualityEngine* ee =
+      m != nullptr ? m->getEqualityEngine() : d_state.getEqualityEngine();
   NodeManager* nm = NodeManager::currentNM();
   unsigned num_lemmas = 0;
   bool isCollectModel = (m != nullptr);
@@ -247,8 +251,13 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
       for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++)
       {
         // if these equivalence classes are not explicitly disequal, do
-        // extensionality to ensure distinctness
-        if (!ee->areDisequal(itf->second[j], itf->second[k], false))
+        // extensionality to ensure distinctness. Notice that we always use
+        // the (local) equality engine for this check via the state, since the
+        // model's equality engine does not store any disequalities. This is
+        // an optimization to introduce fewer equalities during model
+        // construction, since we know such disequalities have already been
+        // witness via assertions.
+        if (!d_state.areDisequal(itf->second[j], itf->second[k]))
         {
           Node deq =
               Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
@@ -450,6 +459,11 @@ bool HoExtension::collectModelInfoHo(TheoryModel* m,
       return false;
     }
   }
+  // We apply an explicit extensionality technique for asserting
+  // disequalities to the model to ensure that function values are distinct
+  // in the curried HO_APPLY version of model construction. This is a
+  // non-standard alternative to using a type enumerator over function
+  // values to assign unique values.
   int addedLemmas = checkExtensionality(m);
   return addedLemmas == 0;
 }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8b8a6a926d28f2df84969cc927ac1a077b7a6fc5..c6dcfa967a003bb5c689a4b788de55700f829216 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -661,6 +661,7 @@ set(regress_0_tests
   regress0/ho/match-middle.smt2
   regress0/ho/modulo-func-equality.smt2
   regress0/ho/qgu-fuzz-ho-1-dd.smt2
+  regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
   regress0/ho/shadowing-defs.smt2
   regress0/ho/simple-matching-partial.smt2
   regress0/ho/simple-matching.smt2

diff --git a/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 b/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
new file mode 100644 (file)
index 0000000..7dc3188
--- /dev/null
+++ b/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
@@ -0,0 +1,10 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-const x6 Bool)
+(declare-const x Int)
+(declare-const b (-> Int Int Int))
+(declare-const c (-> Int Int))
+(assert (> (b 1 0) 0))
+(assert (= (c 0) (b 0 1)))
+(assert(= c (ite x6 (b 1) (b (+ 1 x)))))
+(check-sat)