Introduce new splitting inference in sets + cardinality (#8290)

Fixes cvc5/cvc5-projects#486.

This introduces a new strategy which splits on whether Venn regions are equal to each other before it splits them into sub-Venn regions.

The issue in the above was caused by a case where the sets solver decided to make 2 Venn regions of the same equivalence class disjoint. By splitting on their equality first, this should introduce the necessary information to discover this is a conflict (via disequality witnessing). It should also be more efficient since we introduce new set terms lazier.

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 20d758b2147a094d0fe2817495691c7a5ac57421..bca36e196edfb9698b677deea8b538c1b9220120 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -332,6 +332,7 @@ const char* toString(InferenceId i)
     case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2";
     case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV";
     case InferenceId::SETS_CARD_SPLIT_EMPTY: return "SETS_CARD_SPLIT_EMPTY";
+    case InferenceId::SETS_CARD_SPLIT_EQ: return "SETS_CARD_SPLIT_EQ";
     case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE";
     case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL";
     case InferenceId::SETS_CARD_GRAPH_EMP: return "SETS_CARD_GRAPH_EMP";

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index f5699540c2b85db273156485d8a052f4c7668f44..ddfbdb665b904262f4148bdcc8522ebcac31e49f 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -481,6 +481,8 @@ enum class InferenceId
   //-------------------- sets cardinality solver
   // split on emptyset
   SETS_CARD_SPLIT_EMPTY,
+  // split on equality between two distinct Venn regions
+  SETS_CARD_SPLIT_EQ,
   // cycle of cardinalities, hence all sets have the same
   SETS_CARD_CYCLE,
   // two sets have the same cardinality

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 941a1305aaad4b84f39fd38d21699c9e8a94db7e..7871569d7999d9bef1a038b5d5b187fc84b99e0b 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -822,39 +822,52 @@ void CardinalityExtension::checkNormalForm(Node eqc,
             bool disjoint = false;
             Trace("sets-nf-debug")
                 << "Try split " << o0 << " against " << o1 << std::endl;
-            // split them
-            for (unsigned e = 0; e < 2; e++)
+            if (!d_state.areDisequal(o0, o1))
             {
-              Node r1 = e == 0 ? o0 : o1;
-              Node r2 = e == 0 ? o1 : o0;
-              // check if their intersection exists modulo equality
-              Node r1r2i = d_state.getBinaryOpTerm(SET_INTER, r1, r2);
-              if (!r1r2i.isNull())
-              {
-                Trace("sets-nf-debug")
-                    << "Split term already exists, but not in cardinality "
-                       "graph : "
-                    << r1r2i << ", should be empty." << std::endl;
-                // their intersection is empty (probably?)
-                // e.g. these are two disjoint venn regions, proceed to next
-                // pair
-                Assert(d_state.areEqual(emp_set, r1r2i));
-                disjoint = true;
-                break;
-              }
+              // Just try to make them equal. This is analogous
+              // to the STRINGS_LEN_SPLIT inference in strings.
+              d_im.split(
+                  o0.eqNode(o1), InferenceId::SETS_CARD_SPLIT_EQ, 1);
+              Assert(d_im.hasSent());
+              return;
             }
-            if (!disjoint)
+            else
             {
-              // simply introduce their intersection
-              Assert(o0 != o1);
-              Node kca = d_treg.getProxy(o0);
-              Node kcb = d_treg.getProxy(o1);
-              Node intro = rewrite(nm->mkNode(SET_INTER, kca, kcb));
-              Trace("sets-nf") << "   Intro split : " << o0 << " against " << o1
-                               << ", term is " << intro << std::endl;
-              intro_sets.push_back(intro);
-              Assert(!d_state.hasTerm(intro));
-              return;
+              // split them by introducing an intersection term, which is
+              // analogous to e.g. STRINGS_SSPLIT_VAR in strings.
+              for (unsigned e = 0; e < 2; e++)
+              {
+                Node r1 = e == 0 ? o0 : o1;
+                Node r2 = e == 0 ? o1 : o0;
+                // check if their intersection exists modulo equality
+                Node r1r2i = d_state.getBinaryOpTerm(SET_INTER, r1, r2);
+                if (!r1r2i.isNull())
+                {
+                  Trace("sets-nf-debug")
+                      << "Split term already exists, but not in cardinality "
+                        "graph : "
+                      << r1r2i << ", should be empty." << std::endl;
+                  // their intersection is empty (probably?)
+                  // e.g. these are two disjoint venn regions, proceed to next
+                  // pair
+                  Assert(d_state.areEqual(emp_set, r1r2i));
+                  disjoint = true;
+                  break;
+                }
+              }
+              if (!disjoint)
+              {
+                // simply introduce their intersection
+                Assert(o0 != o1);
+                Node kca = d_treg.getProxy(o0);
+                Node kcb = d_treg.getProxy(o1);
+                Node intro = rewrite(nm->mkNode(SET_INTER, kca, kcb));
+                Trace("sets-nf") << "   Intro split : " << o0 << " against " << o1
+                                << ", term is " << intro << std::endl;
+                intro_sets.push_back(intro);
+                Assert(!d_state.hasTerm(intro));
+                return;
+              }
             }
           }
         }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 31c056503581fb85a9f5d20794ab1d03979bb313..6b73f506e1185e8cbc9847af5c3b363baa35ec43 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1252,6 +1252,7 @@ set(regress_0_tests
   regress0/sets/nonvar-univ.smt2
   regress0/sets/pre-proc-univ.smt2
   regress0/sets/proj-issue177.smt2
+  regress0/sets/proj-issue486-sets-split-eq.smt2
   regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
   regress0/sets/setel-eq.smt2
   regress0/sets/sets-deq-dd.smt2

diff --git a/test/regress/regress0/sets/proj-issue486-sets-split-eq.smt2 b/test/regress/regress0/sets/proj-issue486-sets-split-eq.smt2
new file mode 100644 (file)
index 0000000..2524333
--- /dev/null
+++ b/test/regress/regress0/sets/proj-issue486-sets-split-eq.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const x Int)
+(declare-const _x Int)
+(check-sat-assuming ((= x (set.card (set.insert _x 1 (set.singleton (* 2 _x)))))))