Fix model unsoundness for relation join (#7511)

This fixes a model unsoundness issue in the theory solver for relations.

1 files changed, 48 insertions, 23 deletions

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index f6ea88b75..a4028d8fb 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -1039,9 +1039,15 @@ void TheorySetsRels::check(Theory::Effort level)
   }
 
   /*
-   * Explicitly compose the join or product relations of r1 and r2
-   * e.g. If (a, b) in X and (b, c) in Y, (a, c) in (X JOIN Y)
+   * Explicitly compose the join or product relations of r1 and r2. For example,
+   * consider the case that (a, b) in r1, (c, d) in r2.
    *
+   * For JOIN, we have three cases:
+   *   b = c, we infer (a, d) in (join r1 r2)
+   *   b != c, do nothing
+   *   else, if neither holds, we add the splitting lemma (b=c or b!=c)
+   *
+   * For PRODUCT, we infer (a, b, c, d) in (product r1 r2).
    */
   void TheorySetsRels::composeMembersForRels( Node rel ) {
     Trace("rels-debug") << "[Theory::Rels] Start composing members for relation = " << rel << std::endl;
@@ -1058,26 +1064,48 @@ void TheorySetsRels::check(Theory::Effort level)
 
     std::vector<Node> r1_rep_exps = d_rReps_memberReps_exp_cache[r1_rep];
     std::vector<Node> r2_rep_exps = d_rReps_memberReps_exp_cache[r2_rep];
-    unsigned int r1_tuple_len = r1.getType().getSetElementType().getTupleLength();
-    unsigned int r2_tuple_len = r2.getType().getSetElementType().getTupleLength();
+    size_t r1_tuple_len = r1.getType().getSetElementType().getTupleLength();
+    size_t r2_tuple_len = r2.getType().getSetElementType().getTupleLength();
 
+    Kind rk = rel.getKind();
+    TypeNode tn = rel.getType().getSetElementType();
     for( unsigned int i = 0; i < r1_rep_exps.size(); i++ ) {
       for( unsigned int j = 0; j < r2_rep_exps.size(); j++ ) {
         std::vector<Node> tuple_elements;
-        TypeNode tn = rel.getType().getSetElementType();
-        Node r1_rmost = RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], r1_tuple_len-1 );
-        Node r2_lmost = RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 );
         tuple_elements.push_back(tn.getDType()[0].getConstructor());
+        std::vector<Node> reasons;
+        if (rk == kind::JOIN)
+        {
+          Node r1_rmost =
+              RelsUtils::nthElementOfTuple(r1_rep_exps[i][0], r1_tuple_len - 1);
+          Node r2_lmost = RelsUtils::nthElementOfTuple(r2_rep_exps[j][0], 0);
+
+          Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost
+                              << " of type " << r1_rmost.getType() << std::endl;
+          Trace("rels-debug") << "[Theory::Rels] r2_lmost: " << r2_lmost
+                              << " of type " << r2_lmost.getType() << std::endl;
+          if (!areEqual(r1_rmost, r2_lmost))
+          {
+            if (!d_state.areDisequal(r1_rmost, r2_lmost))
+            {
+              // If we have (a,b) in R1, (c,d) in R2, and we are considering
+              // join(R1, R2) must split on b=c if they are neither equal nor
+              // disequal.
+              Node eq = r1_rmost.eqNode(r2_lmost);
+              Node lem = nm->mkNode(kind::OR, eq, eq.negate());
+              d_im.addPendingLemma(lem, InferenceId::SETS_RELS_JOIN_ELEM_SPLIT);
+            }
+            continue;
+          }
+          else if (r1_rmost != r2_lmost)
+          {
+            reasons.push_back(nm->mkNode(kind::EQUAL, r1_rmost, r2_lmost));
+          }
+        }
 
-        Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost
-                            << " of type " << r1_rmost.getType() << std::endl;
-        Trace("rels-debug") << "[Theory::Rels] r2_lmost: " << r2_lmost
-                            << " of type " << r2_lmost.getType() << std::endl;
-
-        if (rel.getKind() == kind::PRODUCT
-            || (rel.getKind() == kind::JOIN && areEqual(r1_rmost, r2_lmost)))
+        if (rk == kind::PRODUCT || rk == kind::JOIN)
         {
-          bool isProduct = rel.getKind() == kind::PRODUCT;
+          bool isProduct = rk == kind::PRODUCT;
           unsigned int k = 0;
           unsigned int l = 1;
 
@@ -1092,25 +1120,22 @@ void TheorySetsRels::check(Theory::Effort level)
             tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], l ) );
           }
 
-          Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
-          Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, composed_tuple, rel);
-          std::vector<Node> reasons;
+          Node composed_tuple =
+              nm->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
+          Node fact = nm->mkNode(kind::MEMBER, composed_tuple, rel);
           reasons.push_back( r1_rep_exps[i] );
           reasons.push_back( r2_rep_exps[j] );
 
           if( r1 != r1_rep_exps[i][1] ) {
-            reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1, r1_rep_exps[i][1]) );
+            reasons.push_back(nm->mkNode(kind::EQUAL, r1, r1_rep_exps[i][1]));
           }
           if( r2 != r2_rep_exps[j][1] ) {
-            reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1]) );
+            reasons.push_back(nm->mkNode(kind::EQUAL, r2, r2_rep_exps[j][1]));
           }
           if( isProduct ) {
             sendInfer(
                 fact, InferenceId::SETS_RELS_PRODUCE_COMPOSE, nm->mkNode(kind::AND, reasons));
           } else {
-            if( r1_rmost != r2_lmost ) {
-              reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1_rmost, r2_lmost) );
-            }
             sendInfer(
                 fact, InferenceId::SETS_RELS_JOIN_COMPOSE, nm->mkNode(kind::AND, reasons));
           }