Fix model unsoundness for relation join (#7511)

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

7 files changed, 70 insertions, 27 deletions

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 5439e7549..b50522834 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -341,6 +341,8 @@ const char* toString(InferenceId i)
     case InferenceId::SETS_RELS_JOIN_IMAGE_UP: return "SETS_RELS_JOIN_IMAGE_UP";
     case InferenceId::SETS_RELS_JOIN_SPLIT_1: return "SETS_RELS_JOIN_SPLIT_1";
     case InferenceId::SETS_RELS_JOIN_SPLIT_2: return "SETS_RELS_JOIN_SPLIT_2";
+    case InferenceId::SETS_RELS_JOIN_ELEM_SPLIT:
+      return "SETS_RELS_JOIN_ELEM_SPLIT";
     case InferenceId::SETS_RELS_PRODUCE_COMPOSE:
       return "SETS_RELS_PRODUCE_COMPOSE";
     case InferenceId::SETS_RELS_PRODUCT_SPLIT: return "SETS_RELS_PRODUCT_SPLIT";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index f6a689cf6..3c644e545 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -491,6 +491,7 @@ enum class InferenceId
   SETS_RELS_JOIN_IMAGE_UP,
   SETS_RELS_JOIN_SPLIT_1,
   SETS_RELS_JOIN_SPLIT_2,
+  SETS_RELS_JOIN_ELEM_SPLIT,
   SETS_RELS_PRODUCE_COMPOSE,
   SETS_RELS_PRODUCT_SPLIT,
   SETS_RELS_TCLOSURE_FWD,
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));
           }
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 1a0549a0a..f50e7e0ee 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -452,7 +452,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
   for (; !eqcs_i.isFinished(); ++eqcs_i)
   {
     Node eqc = *eqcs_i;
-
+    Trace("model-builder") << "  Processing EQC " << eqc << std::endl;
     // Information computed for each equivalence class
 
     // The assigned represenative and constant representative
@@ -484,7 +484,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
     for (; !eqc_i.isFinished(); ++eqc_i)
     {
       Node n = *eqc_i;
-      Trace("model-builder") << "  Processing Term: " << n << endl;
+      Trace("model-builder") << "    Processing Term: " << n << endl;
 
       // For each term n in this equivalence class, below we register its
       // assignable subterms, compute whether it is a constant or assigned
@@ -505,7 +505,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
         Assert(constRep.isNull());
         constRep = n;
         Trace("model-builder")
-            << "  ConstRep( " << eqc << " ) = " << constRep << std::endl;
+            << "    ..ConstRep( " << eqc << " ) = " << constRep << std::endl;
         // if we have a constant representative, nothing else matters
         continue;
       }
@@ -522,7 +522,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
         // these cases here.
         rep = itm->second;
         Trace("model-builder")
-            << "  Rep( " << eqc << " ) = " << rep << std::endl;
+            << "    ..Rep( " << eqc << " ) = " << rep << std::endl;
       }
 
       // (3) Finally, process assignable information
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5e64cfcbc..52fb41d46 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -998,6 +998,8 @@ set(regress_0_tests
   regress0/rels/join-eq-u.cvc.smt2
   regress0/rels/joinImg_0.cvc.smt2
   regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
+  regress0/rels/qgu-fuzz-relations-1.smt2
+  regress0/rels/qgu-fuzz-relations-1-dd.smt2
   regress0/rels/rel_1tup_0.cvc.smt2
   regress0/rels/rel_complex_0.cvc.smt2
   regress0/rels/rel_complex_1.cvc.smt2
diff --git a/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2 b/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2
new file mode 100644
index 000000000..52ee0b1c0
--- /dev/null
+++ b/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun d () (Tuple Int Int))
+(assert (= (as emptyset (Set (Tuple Int Int))) (join (singleton (tuple 1 0)) (singleton d))))
+(check-sat)
diff --git a/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2 b/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2
new file mode 100644
index 000000000..b489ce65b
--- /dev/null
+++ b/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Set (Tuple Int Int)))
+(declare-fun b () (Set (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+(assert (and (= b (singleton (tuple 1 0))) (= a (join b (transpose a))) (= a (join b (tclosure a))) (= a (join b (singleton d)))))
+(check-sat)