From: Andrew Reynolds Date: Mon, 1 Nov 2021 14:44:13 +0000 (-0500) Subject: Fix upwards closure for relations (#7515) X-Git-Tag: cvc5-1.0.0~920 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3bcc47a3c03f7bb1c3d00f0978296232b7e0aaf5;p=cvc5.git Fix upwards closure for relations (#7515) This PR fixes an issue where we did compute upwards closure (for join, product, etc.) on equivalence classes whose membership cache had already been initialized (perhaps recursively from the computation of upwards/downwards closures on other terms). It also generalizes the fix from #7511. Instead of doing explicit splitting, we mark shared terms and let theory combination (when necessary) do splitting. This is required to fix a more general version of the benchmark from the previous PR, where instead now a term c+1 is used in a position that is relevant to a join. It disables a regression that times out after these fixes, and does further cleanup. --- diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 20c1f0cbd..594834226 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -342,8 +342,6 @@ 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 1bc32d913..cebf02c9d 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -492,7 +492,6 @@ 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 a4028d8fb..57a70f80a 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -125,44 +125,61 @@ void TheorySetsRels::check(Theory::Effort level) TERM_IT t_it = d_terms_cache.begin(); while( t_it != d_terms_cache.end() ) { - if( d_rReps_memberReps_cache.find(t_it->first) == d_rReps_memberReps_cache.end() ) { - Trace("rels-debug") << "[sets-rels] A term does not have membership constraints: " << t_it->first << std::endl; - KIND_TERM_IT k_t_it = t_it->second.begin(); - - while( k_t_it != t_it->second.end() ) { - if( k_t_it->first == kind::JOIN || k_t_it->first == kind::PRODUCT ) { - std::vector::iterator term_it = k_t_it->second.begin(); - while(term_it != k_t_it->second.end()) { - computeMembersForBinOpRel( *term_it ); - ++term_it; - } - } else if( k_t_it->first == kind::TRANSPOSE ) { - std::vector::iterator term_it = k_t_it->second.begin(); - while( term_it != k_t_it->second.end() ) { - computeMembersForUnaryOpRel( *term_it ); - ++term_it; - } - } else if ( k_t_it->first == kind::TCLOSURE ) { - std::vector::iterator term_it = k_t_it->second.begin(); - while( term_it != k_t_it->second.end() ) { - buildTCGraphForRel( *term_it ); - ++term_it; - } - } else if( k_t_it->first == kind::JOIN_IMAGE ) { - std::vector::iterator term_it = k_t_it->second.begin(); - while( term_it != k_t_it->second.end() ) { - computeMembersForJoinImageTerm( *term_it ); - ++term_it; - } - } else if( k_t_it->first == kind::IDEN ) { - std::vector::iterator term_it = k_t_it->second.begin(); - while( term_it != k_t_it->second.end() ) { - computeMembersForIdenTerm( *term_it ); - ++term_it; - } + // check the terms in this equivalence class for e.g. upwards closure + // (computeMembersForBinOpRel / computeMembersForUnaryOpRel). This is + // done regardless of whether we have initialized + // d_rReps_memberReps_cache for this equivalence class. + Trace("rels-debug") + << "[sets-rels] Check equivalence class: " + << t_it->first << std::endl; + KIND_TERM_IT k_t_it = t_it->second.begin(); + + while (k_t_it != t_it->second.end()) + { + Trace("rels-debug") << "[sets-rels] Check " << k_t_it->second.size() + << " terms of kind " << k_t_it->first << std::endl; + std::vector::iterator term_it = k_t_it->second.begin(); + if (k_t_it->first == kind::JOIN || k_t_it->first == kind::PRODUCT) + { + while (term_it != k_t_it->second.end()) + { + computeMembersForBinOpRel(*term_it); + ++term_it; + } + } + else if (k_t_it->first == kind::TRANSPOSE) + { + while (term_it != k_t_it->second.end()) + { + computeMembersForUnaryOpRel(*term_it); + ++term_it; + } + } + else if (k_t_it->first == kind::TCLOSURE) + { + while (term_it != k_t_it->second.end()) + { + buildTCGraphForRel(*term_it); + ++term_it; } - ++k_t_it; } + else if (k_t_it->first == kind::JOIN_IMAGE) + { + while (term_it != k_t_it->second.end()) + { + computeMembersForJoinImageTerm(*term_it); + ++term_it; + } + } + else if (k_t_it->first == kind::IDEN) + { + while (term_it != k_t_it->second.end()) + { + computeMembersForIdenTerm(*term_it); + ++term_it; + } + } + ++k_t_it; } ++t_it; } @@ -229,24 +246,7 @@ void TheorySetsRels::check(Theory::Effort level) if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN || eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE || eqc_node.getKind() == kind::JOIN_IMAGE || eqc_node.getKind() == kind::IDEN ) { - std::vector terms; - std::map< kind::Kind_t, std::vector > rel_terms; - TERM_IT terms_it = d_terms_cache.find(eqc_rep); - - if( terms_it == d_terms_cache.end() ) { - terms.push_back(eqc_node); - rel_terms[eqc_node.getKind()] = terms; - d_terms_cache[eqc_rep] = rel_terms; - } else { - KIND_TERM_IT kind_term_it = terms_it->second.find(eqc_node.getKind()); - - if( kind_term_it == terms_it->second.end() ) { - terms.push_back(eqc_node); - d_terms_cache[eqc_rep][eqc_node.getKind()] = terms; - } else { - kind_term_it->second.push_back(eqc_node); - } - } + d_terms_cache[eqc_rep][eqc_node.getKind()].push_back(eqc_node); } // need to add all tuple elements as shared terms } @@ -657,10 +657,11 @@ void TheorySetsRels::check(Theory::Effort level) Node rel_rep = getRepresentative( tc_rel[0] ); Node tc_rel_rep = getRepresentative( tc_rel ); - std::vector< Node > members = d_rReps_memberReps_cache[rel_rep]; - std::vector< Node > exps = d_rReps_memberReps_exp_cache[rel_rep]; + const std::vector& members = d_rReps_memberReps_cache[rel_rep]; + const std::vector& exps = d_rReps_memberReps_exp_cache[rel_rep]; - for( unsigned int i = 0; i < members.size(); i++ ) { + for (size_t i = 0, msize = members.size(); i < msize; i++) + { Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 )); Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 )); Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep ); @@ -988,10 +989,6 @@ void TheorySetsRels::check(Theory::Effort level) default: break; } - if(d_rReps_memberReps_cache.find(getRepresentative(rel[0])) == d_rReps_memberReps_cache.end() || - d_rReps_memberReps_cache.find(getRepresentative(rel[1])) == d_rReps_memberReps_cache.end()) { - return; - } composeMembersForRels(rel); } @@ -1020,16 +1017,19 @@ void TheorySetsRels::check(Theory::Effort level) } NodeManager* nm = NodeManager::currentNM(); - std::vector members = d_rReps_memberReps_cache[rel0_rep]; - std::vector exps = d_rReps_memberReps_exp_cache[rel0_rep]; + const std::vector& members = d_rReps_memberReps_cache[rel0_rep]; + const std::vector& exps = d_rReps_memberReps_exp_cache[rel0_rep]; Assert(members.size() == exps.size()); - for(unsigned int i = 0; i < members.size(); i++) { - Node reason = exps[i]; - if( rel.getKind() == kind::TRANSPOSE) { + if (rel.getKind() == kind::TRANSPOSE) + { + for (size_t i = 0, msize = members.size(); i < msize; i++) + { + Node reason = exps[i]; if( rel[0] != exps[i][1] ) { - reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, rel[0], exps[i][1])); + reason = nm->mkNode( + kind::AND, reason, nm->mkNode(kind::EQUAL, rel[0], exps[i][1])); } sendInfer(nm->mkNode(MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel), InferenceId::SETS_RELS_TRANSPOSE_REV, @@ -1043,9 +1043,9 @@ void TheorySetsRels::check(Theory::Effort level) * 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) + * if b = c, we infer (a, d) in (join r1 r2) + * else, we mark b and c as shared terms; their equality will be split in + * theory combination if necessary. * * For PRODUCT, we infer (a, b, c, d) in (product r1 r2). */ @@ -1079,6 +1079,11 @@ void TheorySetsRels::check(Theory::Effort level) 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); + // Since we require notification r1_rmost and r2_lmost are equal, + // they must be shared terms of theory of sets. Hence, we make the + // following calls to makeSharedTerm to ensure this is the case. + makeSharedTerm(r1_rmost, r1_rmost.getType()); + makeSharedTerm(r2_lmost, r2_lmost.getType()); Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost << " of type " << r1_rmost.getType() << std::endl; @@ -1086,19 +1091,12 @@ void TheorySetsRels::check(Theory::Effort level) << " 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) { + Trace("rels-debug") << "...equal" << std::endl; reasons.push_back(nm->mkNode(kind::EQUAL, r1_rmost, r2_lmost)); } } @@ -1178,15 +1176,25 @@ void TheorySetsRels::check(Theory::Effort level) return true; } else if( hasTerm( a ) && hasTerm( b ) ){ return d_state.areEqual(a, b); - } else if(a.getType().isTuple()) { - bool equal = true; - for(unsigned int i = 0; i < a.getType().getTupleLength(); i++) { - equal = equal && areEqual(RelsUtils::nthElementOfTuple(a, i), RelsUtils::nthElementOfTuple(b, i)); + } + TypeNode atn = a.getType(); + if (atn.isTuple()) + { + size_t tlen = atn.getTupleLength(); + for (size_t i = 0; i < tlen; i++) + { + if (!areEqual(RelsUtils::nthElementOfTuple(a, i), + RelsUtils::nthElementOfTuple(b, i))) + { + return false; + } } - return equal; - } else if(!a.getType().isBoolean()){ + return true; + } + else if (!atn.isBoolean()) + { // TODO(project##230): Find a safe type for the singleton operator - makeSharedTerm(a, a.getType()); + makeSharedTerm(a, atn); makeSharedTerm(b, b.getType()); } return false; diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 560f47482..a12a28fff 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -113,7 +113,7 @@ class TheorySetsRels : protected EnvObj std::map< Node, std::vector< Node > > d_rReps_memberReps_exp_cache; /** Mapping between a relation representative and its equivalent relations involving relational operators */ - std::map< Node, std::map > > d_terms_cache; + std::map > > d_terms_cache; /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ std::map > > d_rRep_tcGraph; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5d1ff9b49..f64768965 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1037,7 +1037,6 @@ set(regress_0_tests regress0/rels/rel_tc_2_1.cvc.smt2 regress0/rels/rel_tc_3_1.cvc.smt2 regress0/rels/rel_tc_3.cvc.smt2 - regress0/rels/rel_tc_7.cvc.smt2 regress0/rels/rel_tc_8.cvc.smt2 regress0/rels/rel_tp_3_1.cvc.smt2 regress0/rels/rel_tp_join_0.cvc.smt2 @@ -2075,6 +2074,8 @@ set(regress_1_tests regress1/rels/joinImg_2_1.cvc.smt2 regress1/rels/prod-mod-eq.cvc.smt2 regress1/rels/prod-mod-eq2.cvc.smt2 + regress1/rels/qgu-fuzz-relations-2.smt2 + regress1/rels/qgu-fuzz-relations-3-upwards.smt2 regress1/rels/rel_complex_3.cvc.smt2 regress1/rels/rel_complex_4.cvc.smt2 regress1/rels/rel_complex_5.cvc.smt2 @@ -2775,6 +2776,8 @@ set(regression_disabled_tests regress0/auflia/fuzz01.smtv1.smt2 ### regress0/bv/test00.smtv1.smt2 + # timeout after fixing upwards closure for relations + regress0/rels/rel_tc_7.cvc.smt2 # timeout after changes to equality rewriting policy in strings regress0/strings/quad-028-2-2-unsat.smt2 # FIXME #1649 diff --git a/test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 b/test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 new file mode 100644 index 000000000..185c06502 --- /dev/null +++ b/test/regress/regress1/rels/qgu-fuzz-relations-2.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 (= a (singleton (tuple (+ c 1) 1))) (= (tclosure b) (join a a)))) +(check-sat) diff --git a/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 b/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 new file mode 100644 index 000000000..1cb91e94c --- /dev/null +++ b/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun b () (Set (Tuple Int Int))) +(assert +(= (join b (tclosure (join b b))) (as emptyset (Set (Tuple Int Int)))) +) +(assert +(distinct b (as emptyset (Set (Tuple Int Int)))) +) +(assert (= (join b b) (as emptyset (Set (Tuple Int Int))))) +(check-sat)