Fixes for theory combination + HO (cvc5#10167)

Fixes two current model soundness issue with HO.

The first involved not applying HO extensionality for functions that had finite return type but infinite function type.
The second involved not considering care pairs over higher-order arguments.

src/theory/inference_id.cpp

@@ -537,6 +537,7 @@ const char* toString(InferenceId i)
     case InferenceId::UF_CARD_SIMPLE_CONFLICT: return "UF_CARD_SIMPLE_CONFLICT";
     case InferenceId::UF_CARD_SPLIT: return "UF_CARD_SPLIT";
 
+    case InferenceId::UF_HO_CG_SPLIT: return "UF_HO_CG_SPLIT";
     case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
     case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
     case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY";

src/theory/inference_id.h

@@ -918,6 +918,8 @@ enum class InferenceId
   UF_CARD_SPLIT,
   //-------------------- end cardinality extension to UF
   //-------------------- HO extension to UF
+  // A care graph split due to HO
+  UF_HO_CG_SPLIT,
   // Encodes an n-ary application as a chain of binary HO_APPLY applications
   //   (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
   UF_HO_APP_ENCODE,

src/theory/quantifiers/fmf/full_model_check.cpp

@@ -362,6 +362,12 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     // nothing to do if no functions
     return true;
   }
+  // if higher-order, we must use the standard assignment method
+  if (logicInfo().isHigherOrder())
+  {
+    TheoryEngineModelBuilder::assignFunctions(m);
+    return true;
+  }
   FirstOrderModelFmc* fm = d_fm.get();
   Trace("fmc") << "---Full Model Check reset() " << std::endl;
   d_quant_models.clear();
@@ -557,6 +563,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     if (!m->hasAssignedFunctionDefinition(it->first))
     {
       Node f_def = getFunctionValue(fm, it->first, "$x");
+      Trace("model-builder-debug") << "...assign via fmc" << std::endl;
       m->assignFunctionDefinition(it->first, f_def);
     }
   }

src/theory/theory_model_builder.cpp

@@ -1317,6 +1317,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
   ss << "_arg_";
   Rewriter* r = condenseFuncValues ? d_env.getRewriter() : nullptr;
   Node val = ufmt.getFunctionValue(ss.str(), r);
+  Trace("model-builder-debug") << "...assign via function" << std::endl;
   m->assignFunctionDefinition(f, val);
   // ufmt.debugPrint( std::cout, m );
 }
@@ -1351,14 +1352,15 @@ void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
       Assert(hn.getKind() == Kind::HO_APPLY);
       Assert(m->areEqual(hn[0], f));
       Node hni = m->getRepresentative(hn[1]);
-      Trace("model-builder-debug2") << "      get rep : " << hn[0]
-                                    << " returned " << hni << std::endl;
+      Trace("model-builder-debug2")
+          << "      get rep : " << hn[1] << " returned " << hni << std::endl;
       Assert(hni.getType() == args[0].getType());
       hni = rewrite(args[0].eqNode(hni));
       Node hnv = m->getRepresentative(hn);
       Trace("model-builder-debug2") << "      get rep val : " << hn
                                     << " returned " << hnv << std::endl;
-      Assert(hnv.isConst());
+      // hnv is expected to be constant but may not be the case if e.g. a non-trivial
+      // lambda is given as argument to this function.
       if (!apply_args.empty())
       {
         // Convert to lambda, which is necessary if hnv is a function array
@@ -1384,6 +1386,7 @@ void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
       Kind::LAMBDA,
       NodeManager::currentNM()->mkNode(Kind::BOUND_VAR_LIST, args),
       curr);
+  Trace("model-builder-debug") << "...assign via ho function" << std::endl;
   m->assignFunctionDefinition(f, val);
 }
 
@@ -1473,8 +1476,6 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
   {
     Node f = funcs_to_assign[k];
     Trace("model-builder") << "  Function #" << k << " is " << f << std::endl;
-    // std::map< Node, std::vector< Node > >::iterator itht =
-    // m->d_ho_uf_terms.find( f );
     if (!logicInfo().isHigherOrder())
     {
       Trace("model-builder") << "  Assign function value for " << f

src/theory/uf/ho_extension.cpp

@@ -276,7 +276,9 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
       hasFunctions = true;
       // if during collect model, must have an infinite type
       // if not during collect model, must have a finite type
-      if (d_env.isFiniteType(tn) != isCollectModel)
+      // we consider the cardinality of tn's range type (as opposed to tn)
+      // since the model construction will enumerate values of this type.
+      if (d_env.isFiniteType(tn.getRangeType()) != isCollectModel)
       {
         func_eqcs[tn].push_back(eqc);
         Trace("uf-ho-debug")
@@ -698,6 +700,7 @@ bool HoExtension::collectModelInfoHo(TheoryModel* m,
     Assert(!lam.isNull());
     m->assertEquality(p.second, lam, true);
     m->assertSkeleton(lam);
+    Trace("model-builder-debug") << "Assign via lambda: " << lam << std::endl;
     // assign it as the function definition for all variables in this class
     m->assignFunctionDefinition(p.second, lam);
   }

src/theory/uf/theory_uf.cpp

@@ -595,6 +595,34 @@ void TheoryUF::processCarePairArgs(TNode a, TNode b)
   }
   // otherwise, we add pairs for each of their arguments
   addCarePairArgs(a, b);
+
+  // also split on functions
+  if (logicInfo().isHigherOrder())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    for (size_t k = 0, nchild = a.getNumChildren(); k < nchild; ++k)
+    {
+      TNode x = a[k];
+      TNode y = b[k];
+      if (d_state.areEqual(x, y))
+      {
+        continue;
+      }
+      // Splitting on functions. This is required since conceptually the HO
+      // extension should be considered a separate entity with regards to
+      // theory combination (in particular, with the core UF solver). This is
+      // similar to how we handle sets of sets, where each set type is
+      // considered a separate entity. The types below must be equal to handle
+      // polymorphic operators taking higher-order arguments, e.g. set.map.
+      TypeNode xt = x.getType();
+      if (xt.isFunction() && xt==y.getType())
+      {
+        Node lemma = x.eqNode(y);
+        lemma = nm->mkNode(Kind::OR, lemma, lemma.notNode());
+        d_im.lemma(lemma, InferenceId::UF_HO_CG_SPLIT);
+      }
+    }
+  }
 }
 
 void TheoryUF::computeCareGraph() {
@@ -608,6 +636,7 @@ void TheoryUF::computeCareGraph() {
   // function type for the latter.
   Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..."
                        << std::endl;
+  bool isHigherOrder = logicInfo().isHigherOrder();
   // temporary keep set for higher-order indexing below
   std::vector<Node> keep;
   std::map<Node, TNodeTrie> index;
@@ -620,7 +649,10 @@ void TheoryUF::computeCareGraph() {
     for (const Node& j : app)
     {
       reps.push_back(d_equalityEngine->getRepresentative(j));
-      if (d_equalityEngine->isTriggerTerm(j, THEORY_UF))
+      // if doing higher-order, higher-order arguments must all be considered as
+      // well
+      if (d_equalityEngine->isTriggerTerm(j, THEORY_UF)
+          || (isHigherOrder && j.getType().isFunction()))
       {
         has_trigger_arg = true;
       }
@@ -635,7 +667,7 @@ void TheoryUF::computeCareGraph() {
         Node op = app.getOperator();
         index[op].addTerm(app, reps);
         arity[op] = reps.size();
-        if (logicInfo().isHigherOrder() && d_equalityEngine->hasTerm(op))
+        if (isHigherOrder && d_equalityEngine->hasTerm(op))
         {
           // Since we use a lazy app-completion scheme for equating fully
           // and partially applied versions of terms, we must add all

test/regress/cli/CMakeLists.txt

@@ -769,6 +769,8 @@ set(regress_0_tests
   regress0/ho/cong.smt2
   regress0/ho/datatype-field-ho.smt2
   regress0/ho/dd.shadowing-defs.smt2
+  regress0/ho/dd.syo009.smt2
+  regress0/ho/dd.syo372-finite-ho-ext.smt2
   regress0/ho/declare-fun-variants.smt2
   regress0/ho/def-fun-flatten.smt2
   regress0/ho/ext-finite-unsat.smt2
@@ -809,6 +811,7 @@ set(regress_0_tests
   regress0/ho/simple-conf-lazy-lambda-lift-app.smt2
   regress0/ho/simple-matching-partial.smt2
   regress0/ho/simple-matching.smt2
+  regress0/ho/SYO372.smt2
   regress0/ho/trans.smt2
   regress0/hung10_itesdk_output1.smt2
   regress0/hung13sdk_output1.smt2

test/regress/cli/regress0/ho/SYO372.smt2

@@ -0,0 +1,13 @@
+; COMMAND-LINE: --mbqi
+; EXPECT: unsat
+(set-logic HO_ALL)
+(set-info :status unsat)
+(declare-sort $$unsorted 0)
+(declare-sort tptp.b 0)
+(declare-sort tptp.gtype 0)
+(declare-fun tptp.g (tptp.b) Bool)
+(declare-fun tptp.h ((-> tptp.b Bool)) tptp.gtype)
+(declare-fun tptp.f (tptp.b) Bool)
+(assert (not (=> (forall ((Xx tptp.b)) (= (@ tptp.f Xx) (@ tptp.g Xx))) (= (@ tptp.h tptp.f) (@ tptp.h tptp.g)))))
+(set-info :filename SYO372^5)
+(check-sat-assuming ( true ))

test/regress/cli/regress0/ho/dd.syo009.smt2

@@ -0,0 +1,7 @@
+(set-logic HO_ALL)
+(set-info :status unsat)
+(declare-sort $ 0)
+(declare-fun t ((-> $ $)) Bool)
+(declare-fun p ($) $)
+(assert (and (t p) (not (t (lambda ((X $)) (p X))))))
+(check-sat)

test/regress/cli/regress0/ho/dd.syo372-finite-ho-ext.smt2

@@ -0,0 +1,9 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-sort V 0)
+(declare-fun t (U) Bool)
+(declare-fun p ((-> U Bool)) V)
+(declare-fun tp (U) Bool)
+(assert (not (= (p tp) (p t))))
+(check-sat)