From 47eb5ed2c6b68d25ebe9e2bd70bdae89c63d50c4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 12 Mar 2022 17:21:02 -0600 Subject: [PATCH] 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. --- src/theory/inference_id.cpp | 1 + src/theory/inference_id.h | 2 + src/theory/sets/cardinality_extension.cpp | 73 +++++++++++-------- test/regress/CMakeLists.txt | 1 + .../sets/proj-issue486-sets-split-eq.smt2 | 5 ++ 5 files changed, 52 insertions(+), 30 deletions(-) create mode 100644 test/regress/regress0/sets/proj-issue486-sets-split-eq.smt2 diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 20d758b21..bca36e196 100644 --- 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 f5699540c..ddfbdb665 100644 --- 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 941a1305a..7871569d7 100644 --- 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 31c056503..6b73f506e 100644 --- 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 index 000000000..252433318 --- /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))))))) -- 2.30.2