From: Andrew Reynolds Date: Wed, 27 Oct 2021 18:02:52 +0000 (-0500) Subject: Fix model unsoundness for relation join (#7511) X-Git-Tag: cvc5-1.0.0~955 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c0ec4ead7a013c2da36c16d9d17471d921ca00e;p=cvc5.git Fix model unsoundness for relation join (#7511) This fixes a model unsoundness issue in the theory solver for relations. --- 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 r1_rep_exps = d_rReps_memberReps_exp_cache[r1_rep]; std::vector 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 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 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 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)