Fix care graph computation for higher-order (#7474)

Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph.

Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758.

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 1e240a254a4dc0fd54222dbe5f3604e68acdd591..5e9cb0a1d3a92bc62e0f4780067ea9133ec0814f 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -511,9 +511,8 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
   return EQUALITY_FALSE_IN_MODEL;
 }
 
-bool TheoryUF::areCareDisequal(TNode x, TNode y){
-  Assert(d_equalityEngine->hasTerm(x));
-  Assert(d_equalityEngine->hasTerm(y));
+bool TheoryUF::areCareDisequal(TNode x, TNode y)
+{
   if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
       && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
   {
@@ -534,11 +533,14 @@ void TheoryUF::addCarePairs(const TNodeTrie* t1,
                             unsigned arity,
                             unsigned depth)
 {
+  // Note we use d_state instead of d_equalityEngine in this method in several
+  // places to be robust to cases where the tries have terms that do not
+  // exist in the equality engine, which can be the case if higher order.
   if( depth==arity ){
     if( t2!=NULL ){
       Node f1 = t1->getData();
       Node f2 = t2->getData();
-      if (!d_equalityEngine->areEqual(f1, f2))
+      if (!d_state.areEqual(f1, f2))
       {
         Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
@@ -546,11 +548,9 @@ void TheoryUF::addCarePairs(const TNodeTrie* t1,
         {
           TNode x = f1[k];
           TNode y = f2[k];
-          Assert(d_equalityEngine->hasTerm(x));
-          Assert(d_equalityEngine->hasTerm(y));
-          Assert(!d_equalityEngine->areDisequal(x, y, false));
+          Assert(!d_state.areDisequal(x, y));
           Assert(!areCareDisequal(x, y));
-          if (!d_equalityEngine->areEqual(x, y))
+          if (!d_state.areEqual(x, y))
           {
             if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
                 && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
@@ -586,7 +586,7 @@ void TheoryUF::addCarePairs(const TNodeTrie* t1,
         std::map<TNode, TNodeTrie>::const_iterator it2 = it;
         ++it2;
         for( ; it2 != t1->d_data.end(); ++it2 ){
-          if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
+          if (!d_state.areDisequal(it->first, it2->first))
           {
             if( !areCareDisequal(it->first, it2->first) ){
               addCarePairs( &it->second, &it2->second, arity, depth+1 );
@@ -600,7 +600,7 @@ void TheoryUF::addCarePairs(const TNodeTrie* t1,
       {
         for (const std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
         {
-          if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
+          if (!d_state.areDisequal(tt1.first, tt2.first))
           {
             if (!areCareDisequal(tt1.first, tt2.first))
             {
@@ -618,11 +618,14 @@ void TheoryUF::computeCareGraph() {
   {
     return;
   }
+  NodeManager* nm = NodeManager::currentNM();
   // Use term indexing. We build separate indices for APPLY_UF and HO_APPLY.
   // We maintain indices per operator for the former, and indices per
   // function type for the latter.
   Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..."
                        << std::endl;
+  // temporary keep set for higher-order indexing below
+  std::vector<Node> keep;
   std::map<Node, TNodeTrie> index;
   std::map<TypeNode, TNodeTrie> hoIndex;
   std::map<Node, size_t> arity;
@@ -645,6 +648,25 @@ void TheoryUF::computeCareGraph() {
         Node op = app.getOperator();
         index[op].addTerm(app, reps);
         arity[op] = reps.size();
+        if (logicInfo().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
+          // sub-chains to the HO index if the operator of this term occurs
+          // in a higher-order context in the equality engine.  In other words,
+          // for (f a b c), this will add the terms:
+          // (HO_APPLY f a), (HO_APPLY (HO_APPLY f a) b),
+          // (HO_APPLY (HO_APPLY (HO_APPLY f a) b) c) to the higher-order
+          // term index for consideration when computing care pairs.
+          Node curr = op;
+          for (const Node& c : app)
+          {
+            Node happ = nm->mkNode(kind::HO_APPLY, curr, c);
+            hoIndex[curr.getType()].addTerm(happ, {curr, c});
+            curr = happ;
+            keep.push_back(happ);
+          }
+        }
       }
       else
       {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 52fb41d46b259d0b031c51826143a0060ca9ce56..197c221966db9e49de16eb1354dae923989b2446 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -651,12 +651,16 @@ set(regress_0_tests
   regress0/ho/issue4990-care-graph.smt2
   regress0/ho/issue5233-part1-usort-owner.smt2
   regress0/ho/issue5371.smt2
+  regress0/ho/issue5741-1-cg-model.smt2
+  regress0/ho/issue5741-3-cg-model.smt2
+  regress0/ho/issue5744-cg-model.smt2
   regress0/ho/issue6526.smt2
   regress0/ho/issue6536.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
   regress0/ho/match-middle.smt2
   regress0/ho/modulo-func-equality.smt2
+  regress0/ho/qgu-fuzz-ho-1-dd.smt2
   regress0/ho/shadowing-defs.smt2
   regress0/ho/simple-matching-partial.smt2
   regress0/ho/simple-matching.smt2
@@ -1714,6 +1718,9 @@ set(regress_1_tests
   regress1/ho/issue4065-no-rep.smt2
   regress1/ho/issue4092-sinf.smt2
   regress1/ho/issue4134-sinf.smt2
+  regress1/ho/issue4758.smt2
+  regress1/ho/issue5078-small.smt2
+  regress1/ho/issue5201-1.smt2
   regress1/ho/issue5741-3.smt2
   regress1/ho/NUM638^1.smt2
   regress1/ho/NUM925^1.p

diff --git a/test/regress/regress0/ho/issue5741-1-cg-model.smt2 b/test/regress/regress0/ho/issue5741-1-cg-model.smt2
new file mode 100644 (file)
index 0000000..8989acd
--- /dev/null
+++ b/test/regress/regress0/ho/issue5741-1-cg-model.smt2
@@ -0,0 +1,18 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun a ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(declare-fun c () (_ BitVec 1))
+(declare-fun d () (_ BitVec 32))
+(declare-fun e () (_ BitVec 32))
+(declare-fun f () (_ BitVec 32))
+(declare-fun g ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
+(declare-fun h () (_ BitVec 32))
+(declare-fun i () (_ BitVec 32))
+(declare-fun j () (_ BitVec 1))
+(declare-fun k () (_ BitVec 32))
+(assert (= b (a d e)))
+(assert (= f (g h i)))
+(assert (distinct j (ite (= i k) (_ bv1 1) (_ bv0 1))))
+(assert (= (ite (= i b) (_ bv1 1) (_ bv0 1)) j (ite (= c (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
+(check-sat)

diff --git a/test/regress/regress0/ho/issue5741-3-cg-model.smt2 b/test/regress/regress0/ho/issue5741-3-cg-model.smt2
new file mode 100644 (file)
index 0000000..abc4b76
--- /dev/null
+++ b/test/regress/regress0/ho/issue5741-3-cg-model.smt2
@@ -0,0 +1,5 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun p ((_ BitVec 17) (_ BitVec 16)) Bool)
+(assert (p (_ bv0 17) ((_ sign_extend 15) (ite (p (_ bv0 17) (_ bv0 16)) (_ bv1 1) (_ bv0 1)))))
+(check-sat)

diff --git a/test/regress/regress0/ho/issue5744-cg-model.smt2 b/test/regress/regress0/ho/issue5744-cg-model.smt2
new file mode 100644 (file)
index 0000000..5650351
--- /dev/null
+++ b/test/regress/regress0/ho/issue5744-cg-model.smt2
@@ -0,0 +1,7 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun r4 () Real)
+(declare-fun ufrb5 (Real Real Real Real Real) Bool)
+(assert (ufrb5 0.0 0.0 0.0 0.0 0))
+(assert (ufrb5 (+ r4 r4) 0.0 1 0.0 0.0))
+(check-sat)

diff --git a/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2 b/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2
new file mode 100644 (file)
index 0000000..840db92
--- /dev/null
+++ b/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2
@@ -0,0 +1,6 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-const b (-> Int Int Int))
+(declare-const c (-> Int Int))
+(assert (and (= c (b 1)) (= c (b 0)) (> (b 1 0) 0) (> 0 (b 0 1)) (= 0 (c (b 0 0)))))
+(check-sat)

diff --git a/test/regress/regress1/ho/issue4758.smt2 b/test/regress/regress1/ho/issue4758.smt2
new file mode 100644 (file)
index 0000000..dab284c
--- /dev/null
+++ b/test/regress/regress1/ho/issue4758.smt2
@@ -0,0 +1,6 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b (Real Real) Real)
+(assert (> (b a 0) (b (- a) 1)))
+(check-sat)

diff --git a/test/regress/regress1/ho/issue5078-small.smt2 b/test/regress/regress1/ho/issue5078-small.smt2
new file mode 100644 (file)
index 0000000..2107743
--- /dev/null
+++ b/test/regress/regress1/ho/issue5078-small.smt2
@@ -0,0 +1,8 @@
+(set-logic HO_QF_UFLIA)
+(set-info :status sat)
+(declare-fun a (Int Int) Int)
+(declare-fun d () Int)
+(declare-fun e () Int)
+(assert (= (a d 0) (a 0 1)))
+(assert (= d (mod e 3)))
+(check-sat)

diff --git a/test/regress/regress1/ho/issue5201-1.smt2 b/test/regress/regress1/ho/issue5201-1.smt2
new file mode 100644 (file)
index 0000000..9f6e058
--- /dev/null
+++ b/test/regress/regress1/ho/issue5201-1.smt2
@@ -0,0 +1,20 @@
+(set-logic HO_QF_UFLIA)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b (Int Int) Int)
+(declare-fun c (Int Int) Int)
+(declare-fun d () Int)
+(declare-fun e () Int)
+(declare-fun f () Int)
+(declare-fun g () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun k () Int)
+(assert (= d (b j d) a))
+(assert (= e (c e i)))
+(assert (= (b k f) a))
+(assert (= d (+ g 4)))
+(assert (= j (* g 5)))
+(assert (= e (+ g 5)))
+(assert (= k 0))
+(check-sat)