Simplify and fix care graph for ufHo (#4924)

We now separate APPLY_UF and HO_APPLY. We do not generate care pairs based on comparing APPLY_UF terms with HO_APPLY terms, which led to type errors previously.

Fixes #4990.

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index c8ae3d8442c0fec28b3ea659d281c87fcf1fdb68..0b97d8a5da1f51e774d397b6d162868f6417d246 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -200,20 +200,6 @@ void TheoryUF::check(Effort level) {
   }
 }/* TheoryUF::check() */
 
-Node TheoryUF::getOperatorForApplyTerm( TNode node ) {
-  Assert(node.getKind() == kind::APPLY_UF || node.getKind() == kind::HO_APPLY);
-  if( node.getKind()==kind::APPLY_UF ){
-    return node.getOperator();
-  }else{
-    return d_equalityEngine->getRepresentative(node[0]);
-  }
-}
-
-unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) {
-  Assert(node.getKind() == kind::APPLY_UF || node.getKind() == kind::HO_APPLY);
-  return node.getKind()==kind::APPLY_UF ? 0 : 1;
-}
-
 TrustNode TheoryUF::expandDefinition(Node node)
 {
   Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : "
@@ -543,8 +529,8 @@ bool TheoryUF::areCareDisequal(TNode x, TNode y){
   return false;
 }
 
-void TheoryUF::addCarePairs(TNodeTrie* t1,
-                            TNodeTrie* t2,
+void TheoryUF::addCarePairs(const TNodeTrie* t1,
+                            const TNodeTrie* t2,
                             unsigned arity,
                             unsigned depth)
 {
@@ -556,8 +542,8 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
       {
         Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
-        unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
-        for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) {
+        for (size_t k = 0, nchildren = f1.getNumChildren(); k < nchildren; ++k)
+        {
           TNode x = f1[k];
           TNode y = f2[k];
           Assert(d_equalityEngine->hasTerm(x));
@@ -587,17 +573,17 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
     if( t2==NULL ){
       if( depth<(arity-1) ){
         //add care pairs internal to each child
-        for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+        for (const std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
         {
           addCarePairs(&tt.second, NULL, arity, depth + 1);
         }
       }
       //add care pairs based on each pair of non-disequal arguments
-      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+      for (std::map<TNode, TNodeTrie>::const_iterator it = t1->d_data.begin();
            it != t1->d_data.end();
            ++it)
       {
-        std::map<TNode, TNodeTrie>::iterator it2 = it;
+        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))
@@ -610,9 +596,9 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
       }
     }else{
       //add care pairs based on product of indices, non-disequal arguments
-      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+      for (const std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
       {
-        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+        for (const std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
         {
           if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
           {
@@ -628,40 +614,63 @@ void TheoryUF::addCarePairs(TNodeTrie* t1,
 }
 
 void TheoryUF::computeCareGraph() {
-
-  if (d_sharedTerms.size() > 0) {
-    //use term indexing
-    Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
-    std::map<Node, TNodeTrie> index;
-    std::map< Node, unsigned > arity;
-    unsigned functionTerms = d_functionsTerms.size();
-    for (unsigned i = 0; i < functionTerms; ++ i) {
-      TNode f1 = d_functionsTerms[i];
-      Node op = getOperatorForApplyTerm( f1 );
-      unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
-      std::vector< TNode > reps;
-      bool has_trigger_arg = false;
-      for( unsigned j=arg_start_index; j<f1.getNumChildren(); j++ ){
-        reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
-        if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_UF))
-        {
-          has_trigger_arg = true;
-        }
-      }
-      if( has_trigger_arg ){
-        index[op].addTerm(f1, reps);
-        arity[op] = reps.size();
+  if (d_sharedTerms.empty())
+  {
+    return;
+  }
+  // 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;
+  std::map<Node, TNodeTrie> index;
+  std::map<TypeNode, TNodeTrie> hoIndex;
+  std::map<Node, size_t> arity;
+  for (TNode app : d_functionsTerms)
+  {
+    std::vector<TNode> reps;
+    bool has_trigger_arg = false;
+    for (const Node& j : app)
+    {
+      reps.push_back(d_equalityEngine->getRepresentative(j));
+      if (d_equalityEngine->isTriggerTerm(j, THEORY_UF))
+      {
+        has_trigger_arg = true;
       }
     }
-    //for each index
-    for (std::pair<const Node, TNodeTrie>& tt : index)
+    if (has_trigger_arg)
     {
-      Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index "
-                           << tt.first << "..." << std::endl;
-      addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
+      if (app.getKind() == kind::APPLY_UF)
+      {
+        Node op = app.getOperator();
+        index[op].addTerm(app, reps);
+        arity[op] = reps.size();
+      }
+      else
+      {
+        Assert(app.getKind() == kind::HO_APPLY);
+        // add it to the hoIndex for the function type
+        hoIndex[app[0].getType()].addTerm(app, reps);
+      }
     }
-    Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl;
   }
+  // for each index
+  for (std::pair<const Node, TNodeTrie>& tt : index)
+  {
+    Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index "
+                         << tt.first << "..." << std::endl;
+    Assert(arity.find(tt.first) != arity.end());
+    addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
+  }
+  for (std::pair<const TypeNode, TNodeTrie>& tt : hoIndex)
+  {
+    Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process ho index "
+                         << tt.first << "..." << std::endl;
+    // the arity of HO_APPLY is always two
+    addCarePairs(&tt.second, nullptr, 2, 0);
+  }
+  Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished."
+                       << std::endl;
 }/* TheoryUF::computeCareGraph() */
 
 void TheoryUF::conflict(TNode a, TNode b) {

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 4d0a3126f1759222c4fdf6818018d700b3afd16d..7d17fdb8684bb4d10310718d2b7cabc93cf6ed88 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -150,15 +150,6 @@ private:
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 
- private:
-  /** get the operator for this node (node should be either APPLY_UF or
-   * HO_APPLY)
-   */
-  Node getOperatorForApplyTerm(TNode node);
-  /** get the starting index of the arguments for node (node should be either
-   * APPLY_UF or HO_APPLY) */
-  unsigned getArgumentStartIndexForApplyTerm(TNode node);
-
  public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
@@ -211,8 +202,8 @@ private:
 
  private:
   bool areCareDisequal(TNode x, TNode y);
-  void addCarePairs(TNodeTrie* t1,
-                    TNodeTrie* t2,
+  void addCarePairs(const TNodeTrie* t1,
+                    const TNodeTrie* t2,
                     unsigned arity,
                     unsigned depth);
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e7ca73a75622a7e043fc7c1a413ed03ce33a6b68..99f06e0df32dd94efa93fe31b6f37f03160d19f3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -545,6 +545,7 @@ set(regress_0_tests
   regress0/ho/ho-std-fmf.smt2
   regress0/ho/hoa0008.smt2
   regress0/ho/issue4477.smt2
+  regress0/ho/issue4990-care-graph.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
   regress0/ho/match-middle.smt2

diff --git a/test/regress/regress0/ho/issue4990-care-graph.smt2 b/test/regress/regress0/ho/issue4990-care-graph.smt2
new file mode 100644 (file)
index 0000000..6c44a94
--- /dev/null
+++ b/test/regress/regress0/ho/issue4990-care-graph.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: sat
+(set-logic QF_AUFBVLIA)
+(set-option :uf-ho true)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c (Int) Int)
+(declare-fun d (Int Int) Int)
+(assert (xor (= c (d a)) (= c (d b))))
+(check-sat)