Fix issue in datatypes care graph computation involving subtyping (#8125)

The datatypes care graph was incorrectly computed for constructors taking `Real` arguments, due to subtyping.

This fixes the term index to cache on the *return* type for constructors, not the argument types.  Caching based on argument types was incorrect even for non-parametric datatypes with arguments that have subtyping.

Fixes https://github.com/cvc5/cvc5/issues/8124.

This also does minor cleanup and additions done while debugging the issue.

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 9a55d8377cebb2dbe2e6e7655186f2cd3be3b6b2..542dfc906aa98c005eec27016f22cfbc95190654 100644 (file)
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -136,23 +136,37 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const
 
 void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const
 {
-  out << "Model()";
+  out << "Model(" << std::endl;
+  this->Printer::toStream(out, m);
+  out << ")" << std::endl;
 }
 
 void AstPrinter::toStreamModelSort(std::ostream& out,
                                    TypeNode tn,
                                    const std::vector<Node>& elements) const
 {
-  // shouldn't be called; only the non-Command* version above should be
-  Unreachable();
+  out << "(" << tn << "(";
+  bool firstTime = true;
+  for (const Node& elem : elements)
+  {
+    if (firstTime)
+    {
+      firstTime = false;
+    }
+    else
+    {
+      out << " ";
+    }
+    out << elem;
+  }
+  out << "))" << std::endl;
 }
 
 void AstPrinter::toStreamModelTerm(std::ostream& out,
                                    const Node& n,
                                    const Node& value) const
 {
-  // shouldn't be called; only the non-Command* version above should be
-  Unreachable();
+  out << "(" << n << " " << value << ")" << std::endl;
 }
 
 void AstPrinter::toStreamCmdEmpty(std::ostream& out,

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index a689be7c5c50b7cb0b4cea34734892732be71a74..8854db8772d91b533161e0a984e5d75194b2a3b5 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1057,79 +1057,93 @@ void TheoryDatatypes::addCarePairs(TNodeTrie* t1,
                                    unsigned depth,
                                    unsigned& n_pairs)
 {
+  Trace("dt-cg") << "Process at depth " << depth << "/" << arity << std::endl;
   if( depth==arity ){
-    if( t2!=NULL ){
-      Node f1 = t1->getData();
-      Node f2 = t2->getData();
-      if( !areEqual( f1, f2 ) ){
-        Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
-        vector< pair<TNode, TNode> > currentPairs;
-        for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
-          TNode x = f1[k];
-          TNode y = f2[k];
-          Assert(d_equalityEngine->hasTerm(x));
-          Assert(d_equalityEngine->hasTerm(y));
-          Assert(!areDisequal(x, y));
-          Assert(!areCareDisequal(x, y));
-          if (!d_equalityEngine->areEqual(x, y))
+    Assert(t2 != nullptr);
+    Node f1 = t1->getData();
+    Node f2 = t2->getData();
+    if (!areEqual(f1, f2))
+    {
+      Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
+      std::vector<std::pair<TNode, TNode> > currentPairs;
+      for (size_t k = 0, nchild = f1.getNumChildren(); k < nchild; ++k)
+      {
+        TNode x = f1[k];
+        TNode y = f2[k];
+        Assert(d_equalityEngine->hasTerm(x));
+        Assert(d_equalityEngine->hasTerm(y));
+        Assert(!areDisequal(x, y));
+        Assert(!areCareDisequal(x, y));
+        if (!d_equalityEngine->areEqual(x, y))
+        {
+          Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y
+                         << std::endl;
+          if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES)
+              && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES))
           {
-            Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
-            if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES)
-                && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES))
-            {
-              TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
-                  x, THEORY_DATATYPES);
-              TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
-                  y, THEORY_DATATYPES);
-              currentPairs.push_back(make_pair(x_shared, y_shared));
-            }
+            TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
+                x, THEORY_DATATYPES);
+            TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
+                y, THEORY_DATATYPES);
+            currentPairs.push_back(make_pair(x_shared, y_shared));
           }
         }
-        for (unsigned c = 0; c < currentPairs.size(); ++ c) {
-          Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
-          addCarePair(currentPairs[c].first, currentPairs[c].second);
-          n_pairs++;
-        }
+      }
+      for (std::pair<TNode, TNode>& p : currentPairs)
+      {
+        Trace("dt-cg-pair")
+            << "Pair : " << p.first << " " << p.second << std::endl;
+        addCarePair(p.first, p.second);
+        n_pairs++;
       }
     }
-  }else{
-    if( t2==NULL ){
-      if( depth<(arity-1) ){
-        //add care pairs internal to each child
-        for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
-        {
-          addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs);
-        }
+    return;
+  }
+  if (t2 == nullptr)
+  {
+    if (depth + 1 < arity)
+    {
+      // add care pairs internal to each child
+      for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+      {
+        Trace("dt-cg-debug") << "Traverse into arg " << tt.first << " at depth "
+                             << depth << std::endl;
+        addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs);
       }
-      //add care pairs based on each pair of non-disequal arguments
-      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
-           it != t1->d_data.end();
-           ++it)
+    }
+    // add care pairs based on each pair of non-disequal arguments
+    for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+         it != t1->d_data.end();
+         ++it)
+    {
+      std::map<TNode, TNodeTrie>::iterator it2 = it;
+      ++it2;
+      for (; it2 != t1->d_data.end(); ++it2)
       {
-        std::map<TNode, TNodeTrie>::iterator it2 = it;
-        ++it2;
-        for( ; it2 != t1->d_data.end(); ++it2 ){
-          if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
+        if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
+        {
+          if (!areCareDisequal(it->first, it2->first))
           {
-            if( !areCareDisequal(it->first, it2->first) ){
-              addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
-            }
+            addCarePairs(&it->second, &it2->second, arity, depth + 1, n_pairs);
           }
         }
       }
-    }else{
-      //add care pairs based on product of indices, non-disequal arguments
-      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+    }
+    return;
+  }
+  // add care pairs based on product of indices, non-disequal arguments
+  for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+  {
+    for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+    {
+      if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
       {
-        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+        if (!areCareDisequal(tt1.first, tt2.first))
         {
-          if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
-          {
-            if (!areCareDisequal(tt1.first, tt2.first))
-            {
-              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
-            }
-          }
+          Trace("dt-cg-debug")
+              << "Traverse into " << tt1.first << " " << tt2.first
+              << " at depth " << depth << std::endl;
+          addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
         }
       }
     }
@@ -1148,9 +1162,13 @@ void TheoryDatatypes::computeCareGraph(){
     TNode f1 = d_functionTerms[i];
     Assert(d_equalityEngine->hasTerm(f1));
     Trace("dt-cg-debug") << "...build for " << f1 << std::endl;
-    //break into index based on operator, and type of first argument (since some operators are parametric)
+    // Break into index based on operator.
+    // To handle parameteric datatypes, we also indexed based on the overall
+    // type if a constructor, or the type of the argument (e.g. if a selector)
+    // otherwise
     Node op = f1.getOperator();
-    TypeNode tn = f1[0].getType();
+    TypeNode tn =
+        f1.getKind() == APPLY_CONSTRUCTOR ? f1.getType() : f1[0].getType();
     std::vector< TNode > reps;
     bool has_trigger_arg = false;
     for( unsigned j=0; j<f1.getNumChildren(); j++ ){
@@ -1160,6 +1178,8 @@ void TheoryDatatypes::computeCareGraph(){
         has_trigger_arg = true;
       }
     }
+    Trace("dt-cg-debug") << "...has trigger arg = " << has_trigger_arg
+                         << std::endl;
     //only may contribute to care pairs if has at least one trigger argument
     if( has_trigger_arg ){
       index[tn][op].addTerm( f1, reps );
@@ -1174,6 +1194,7 @@ void TheoryDatatypes::computeCareGraph(){
       Trace("dt-cg") << "Process index " << tt.first << ", " << t.first << "..."
                      << std::endl;
       addCarePairs(&t.second, nullptr, arity[t.first], 0, n_pairs);
+      Trace("dt-cg") << "...finish" << std::endl;
     }
   }
   Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c2b2e30c90b520a382d20d5748cd2eb2003bc22b..74c16350390bb7d64c90ab85b8a53200b89dec89 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1736,6 +1736,7 @@ set(regress_1_tests
   regress1/datatypes/dt-param-card4-unsat.smt2
   regress1/datatypes/issue3266-small.smt2
   regress1/datatypes/issue4851-cdt-model.smt2
+  regress1/datatypes/issue8124-real-int-cg.smt2
   regress1/datatypes/issue-variant-dt-zero.smt2
   regress1/datatypes/manos-model.smt2
   regress1/datatypes/non-simple-rec.smt2

diff --git a/test/regress/regress1/datatypes/issue8124-real-int-cg.smt2 b/test/regress/regress1/datatypes/issue8124-real-int-cg.smt2
new file mode 100644 (file)
index 0000000..1ba0f1f
--- /dev/null
+++ b/test/regress/regress1/datatypes/issue8124-real-int-cg.smt2
@@ -0,0 +1,20 @@
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-datatype RR ((rr (first_rr Real) (second_rr Real))))
+(declare-datatype RI ((ri (first_ri Real) (second_ri Int))))
+(declare-datatype IR ((ir (first_ir Int) (second_ir Real))))
+
+(declare-fun x () RR)
+(declare-fun t () (Set RI))
+(declare-fun e () (Set IR))
+(declare-fun V () Real)
+
+(assert 
+(and 
+(distinct x (rr 0.0 0.0))
+(not (set.member (ir (to_int (first_rr x)) (second_rr x)) e))
+(not (set.member (ri (first_rr x) (to_int (second_rr x))) t)))
+)
+
+(check-sat)