From 7152d6136fc8bd4701d9440ba3eee6bb7bf3a16c Mon Sep 17 00:00:00 2001 From: Paul Meng Date: Thu, 20 Apr 2017 14:04:24 -0500 Subject: [PATCH] Support for relational operators identity and join image --- src/parser/cvc/Cvc.g | 10 +- src/printer/cvc/cvc_printer.cpp | 12 +- src/theory/sets/kinds | 6 + src/theory/sets/theory_sets_rels.cpp | 282 ++++++++++++++++++--- src/theory/sets/theory_sets_rels.h | 46 +--- src/theory/sets/theory_sets_rewriter.cpp | 85 ++++++- src/theory/sets/theory_sets_type_rules.h | 73 +++++- test/regress/regress0/rels/Makefile.am | 12 +- test/regress/regress0/rels/iden_0.cvc | 28 ++ test/regress/regress0/rels/iden_1.cvc | 18 ++ test/regress/regress0/rels/iden_1_1.cvc | 21 ++ test/regress/regress0/rels/joinImg_0.cvc | 33 +++ test/regress/regress0/rels/joinImg_0_1.cvc | 35 +++ test/regress/regress0/rels/joinImg_0_2.cvc | 38 +++ test/regress/regress0/rels/joinImg_1.cvc | 20 ++ test/regress/regress0/rels/joinImg_1_1.cvc | 21 ++ test/regress/regress0/rels/joinImg_2.cvc | 33 +++ test/regress/regress0/rels/joinImg_2_1.cvc | 24 ++ 18 files changed, 718 insertions(+), 79 deletions(-) create mode 100644 test/regress/regress0/rels/iden_0.cvc create mode 100644 test/regress/regress0/rels/iden_1.cvc create mode 100644 test/regress/regress0/rels/iden_1_1.cvc create mode 100644 test/regress/regress0/rels/joinImg_0.cvc create mode 100644 test/regress/regress0/rels/joinImg_0_1.cvc create mode 100644 test/regress/regress0/rels/joinImg_0_2.cvc create mode 100644 test/regress/regress0/rels/joinImg_1.cvc create mode 100644 test/regress/regress0/rels/joinImg_1_1.cvc create mode 100644 test/regress/regress0/rels/joinImg_2.cvc create mode 100644 test/regress/regress0/rels/joinImg_2_1.cvc diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 2dc74afdb..b5bad6a2d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -209,6 +209,8 @@ tokens { TRANSPOSE_TOK = 'TRANSPOSE'; PRODUCT_TOK = 'PRODUCT'; TRANSCLOSURE_TOK = 'TCLOSURE'; + IDEN_TOK = 'IDEN'; + JOIN_IMAGE_TOK = 'JOIN_IMAGE'; // Strings @@ -324,6 +326,8 @@ int getOperatorPrecedence(int type) { case JOIN_TOK: case TRANSPOSE_TOK: case PRODUCT_TOK: + case IDEN_TOK: + case JOIN_IMAGE_TOK: case TRANSCLOSURE_TOK: return 24; case LEQ_TOK: case LT_TOK: @@ -365,6 +369,7 @@ Kind getOperatorKind(int type, bool& negate) { case PRODUCT_TOK: return kind::PRODUCT; case JOIN_TOK: return kind::JOIN; + case JOIN_IMAGE_TOK: return kind::JOIN_IMAGE; // comparisonBinop case EQUAL_TOK: return kind::EQUAL; @@ -1509,6 +1514,7 @@ booleanBinop[unsigned& op] | AND_TOK | JOIN_TOK | PRODUCT_TOK + | JOIN_IMAGE_TOK ; comparison[CVC4::Expr& f] @@ -1706,7 +1712,9 @@ relationTerm[CVC4::Expr& f] const Datatype& dt = t.getDatatype(); args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); - } + } + | IDEN_TOK relationTerm[f] + { f = MK_EXPR(CVC4::kind::IDEN, f); } | postfixTerm[f] ; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 6b42d4e74..4605d1956 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -810,6 +810,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << "TCLOSURE"; opType = PREFIX; break; + case kind::IDEN: + op << "IDEN"; + opType = PREFIX; + break; + case kind::JOIN_IMAGE: + op << "JOIN_IMAGE"; + opType = INFIX; + break; case kind::SINGLETON: out << "{"; toStream(out, n[0], depth, types, false); @@ -818,7 +826,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; case kind::INSERT: { if(bracket) { - out << '('; + out << '('; } out << '{'; size_t i = 0; @@ -830,7 +838,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << "} | "; toStream(out, n[i], depth, types, true); if(bracket) { - out << ')'; + out << ')'; } return; break; diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index cfe7eb632..34fef7d64 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -50,6 +50,8 @@ operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" operator TRANSPOSE 1 "set transpose" operator TCLOSURE 1 "set transitive closure" +operator JOIN_IMAGE 2 "set join image" +operator IDEN 1 "set identity" typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -67,6 +69,8 @@ typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule +typerule JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule +typerule IDEN ::CVC4::theory::sets::RelIdenTypeRule construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -80,5 +84,7 @@ construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule construle TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule +construle JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule +construle IDEN ::CVC4::theory::sets::RelIdenTypeRule endtheory diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 0c5c7a6a2..03e0c64f8 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -58,8 +58,6 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > if( kind_terms.find(kind::TRANSPOSE) != kind_terms.end() ) { std::vector tp_terms = kind_terms[kind::TRANSPOSE]; - // exp is a membership term and tp_terms contains all - // transposed terms that are equal to the right hand side of exp if( tp_terms.size() > 0 ) { applyTransposeRule( tp_terms ); applyTransposeRule( tp_terms[0], rel_rep, exp ); @@ -67,9 +65,6 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } if( kind_terms.find(kind::JOIN) != kind_terms.end() ) { std::vector join_terms = kind_terms[kind::JOIN]; - // exp is a membership term and join_terms contains all - // terms involving "join" operator that are in the same - // equivalence class with the right hand side of exp for( unsigned int j = 0; j < join_terms.size(); j++ ) { applyJoinRule( join_terms[j], rel_rep, exp ); } @@ -86,6 +81,18 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > applyTCRule( mem, tc_terms[j], rel_rep, exp ); } } + if( kind_terms.find(kind::JOIN_IMAGE) != kind_terms.end() ) { + std::vector join_image_terms = kind_terms[kind::JOIN_IMAGE]; + for( unsigned int j = 0; j < join_image_terms.size(); j++ ) { + applyJoinImageRule( mem, join_image_terms[j], exp ); + } + } + if( kind_terms.find(kind::IDEN) != kind_terms.end() ) { + std::vector iden_terms = kind_terms[kind::IDEN]; + for( unsigned int j = 0; j < iden_terms.size(); j++ ) { + applyIdenRule( mem, iden_terms[j], exp ); + } + } } m_it++; } @@ -115,7 +122,18 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > 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++; + } } k_t_it++; } @@ -136,7 +154,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > Node eqc_rep = (*eqcs_i); eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine ); - Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << std::endl; + Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl; while( !eqc_i.isFinished() ){ Node eqc_node = (*eqc_i); @@ -164,16 +182,13 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > computeTupleReps(tup_rep); d_membership_trie[rel_rep].addTerm(tup_rep, d_tuple_reps[tup_rep]); } - } else { - if( safelyAddToMap(d_rReps_nonMemberReps_cache, rel_rep, tup_rep) ) { - addToMap(d_rReps_nonMemberReps_exp_cache, rel_rep, reason); - } } } // collect relational terms info } else if( eqc_rep.getType().isSet() && eqc_rep.getType().getSetElementType().isTuple() ) { 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::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); @@ -210,6 +225,205 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > Trace("rels-debug") << "[Theory::Rels] Done with collecting relational terms!" << std::endl; } + /* JOIN-IMAGE UP : (x, x1) IS_IN R, ..., (x, xn) IS_IN R (R JOIN_IMAGE n) + * ------------------------------------------------------- + * x IS_IN (R JOIN_IMAGE n) || NOT DISTINCT(x1, ... , xn) + * + */ + + void TheorySetsRels::computeMembersForJoinImageTerm( Node join_image_term ) { + Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for JoinImage Term = " << join_image_term << std::endl; + MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( getRepresentative( join_image_term[0] ) ); + + if( rel_mem_it == d_rReps_memberReps_cache.end() ) { + return; + } + + Node join_image_rel = join_image_term[0]; + std::hash_set< Node, NodeHashFunction > hasChecked; + Node join_image_rel_rep = getRepresentative( join_image_rel ); + std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin(); + MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep ); + std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin(); + unsigned int min_card = join_image_term[1].getConst().getNumerator().getUnsignedInt(); + + while( mem_rep_it != (*rel_mem_it).second.end() ) { + Node fst_mem_rep = RelsUtils::nthElementOfTuple( *mem_rep_it, 0 ); + + if( hasChecked.find( fst_mem_rep ) != hasChecked.end() ) { + ++mem_rep_it; + ++mem_rep_exp_it; + continue; + } + hasChecked.insert( fst_mem_rep ); + + Datatype dt = join_image_term.getType().getSetElementType().getDatatype(); + Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER, + NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, + Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ), + join_image_term); + if( holds( new_membership ) ) { + ++mem_rep_it; + ++mem_rep_exp_it; + continue; + } + + std::vector< Node > reasons; + std::vector< Node > existing_members; + std::vector< Node >::iterator mem_rep_exp_it_snd = (*rel_mem_exp_it).second.begin(); + + while( mem_rep_exp_it_snd != (*rel_mem_exp_it).second.end() ) { + Node fst_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 0 ); + + if( areEqual( fst_mem_rep, fst_element_snd_mem ) ) { + bool notExist = true; + std::vector< Node >::iterator existing_mem_it = existing_members.begin(); + Node snd_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 1 ); + + while( existing_mem_it != existing_members.end() ) { + if( areEqual( (*existing_mem_it), snd_element_snd_mem ) ) { + notExist = false; + break; + } + ++existing_mem_it; + } + + if( notExist ) { + existing_members.push_back( snd_element_snd_mem ); + reasons.push_back( *mem_rep_exp_it_snd ); + if( fst_mem_rep != fst_element_snd_mem ) { + reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem_rep, fst_element_snd_mem ) ); + } + if( join_image_rel != (*mem_rep_exp_it_snd)[1] ) { + reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it_snd)[1], join_image_rel )); + } + if( existing_members.size() == min_card ) { + if( min_card >= 2) { + new_membership = NodeManager::currentNM()->mkNode( kind::OR, new_membership, NodeManager::currentNM()->mkNode( kind::NOT, NodeManager::currentNM()->mkNode( kind::DISTINCT, existing_members ) )); + } + Assert(reasons.size() >= 1); + sendInfer( new_membership, reasons.size() > 1 ? NodeManager::currentNM()->mkNode( kind::AND, reasons) : reasons[0], "JOIN-IMAGE UP" ); + break; + } + } + } + ++mem_rep_exp_it_snd; + } + ++mem_rep_it; + ++mem_rep_exp_it; + } + Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for JoinImage Term" << join_image_term << "*********** " << std::endl; + } + + /* JOIN-IMAGE DOWN : (x) IS_IN (R JOIN_IMAGE n) + * ------------------------------------------------------- + * (x, x1) IS_IN R .... (x, xn) IS_IN R DISTINCT(x1, ... , xn) + * + */ + + void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) { + Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term + << " with mem_rep = " << mem_rep << " and exp = " << exp << std::endl; + if( d_rel_nodes.find( join_image_term ) == d_rel_nodes.end() ) { + computeMembersForJoinImageTerm( join_image_term ); + d_rel_nodes.insert( join_image_term ); + } + + Node join_image_rel = join_image_term[0]; + Node join_image_rel_rep = getRepresentative( join_image_rel ); + MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( join_image_rel_rep ); + unsigned int min_card = join_image_term[1].getConst().getNumerator().getUnsignedInt(); + + if( rel_mem_it != d_rReps_memberReps_cache.end() ) { + if( d_membership_trie.find( join_image_rel_rep ) != d_membership_trie.end() ) { + computeTupleReps( mem_rep ); + if( d_membership_trie[join_image_rel_rep].findSuccessors(d_tuple_reps[mem_rep]).size() >= min_card ) { + return; + } + } + } + + Node reason = exp; + Node conclusion = d_trueNode; + std::vector< Node > distinct_skolems; + Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 ); + + if( exp[1] != join_image_term ) { + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) ); + } + for( unsigned int i = 0; i < min_card; i++ ) { + Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] ); + distinct_skolems.push_back( skolem ); + conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) ); + } + if( distinct_skolems.size() >= 2 ) { + conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) ); + } + sendInfer( conclusion, reason, "JOIN-IMAGE DOWN" ); + Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl; + + } + + + /* IDENTITY-DOWN : (x, y) IS_IN IDEN(R) + * ------------------------------------------------------- + * x = y, (x IS_IN R) + * + */ + + void TheorySetsRels::applyIdenRule( Node mem_rep, Node iden_term, Node exp) { + Trace("rels-debug") << "\n[Theory::Rels] *********** applyIdenRule on " << iden_term + << " with mem_rep = " << mem_rep << " and exp = " << exp << std::endl; + if( d_rel_nodes.find( iden_term ) == d_rel_nodes.end() ) { + computeMembersForIdenTerm( iden_term ); + d_rel_nodes.insert( iden_term ); + } + Node reason = exp; + Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 ); + Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 ); + Datatype dt = iden_term[0].getType().getSetElementType().getDatatype(); + Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] ); + + if( exp[1] != iden_term ) { + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) ); + } + sendInfer( NodeManager::currentNM()->mkNode( kind::AND, fact, NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem, snd_mem ) ), reason, "IDENTITY-DOWN" ); + Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyIdenRule on " << iden_term << std::endl; + } + + /* IDEN UP : (x) IS_IN R IDEN(R) IN T + * -------------------------------- + * (x, x) IS_IN IDEN(R) + * + */ + + void TheorySetsRels::computeMembersForIdenTerm( Node iden_term ) { + Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for Iden Term = " << iden_term << std::endl; + Node iden_term_rel = iden_term[0]; + Node iden_term_rel_rep = getRepresentative( iden_term_rel ); + + if( d_rReps_memberReps_cache.find( iden_term_rel_rep ) == d_rReps_memberReps_cache.end() ) { + return; + } + + MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( iden_term_rel_rep ); + std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin(); + + while( mem_rep_exp_it != (*rel_mem_exp_it).second.end() ) { + Node reason = *mem_rep_exp_it; + Node fst_exp_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it)[0], 0 ); + Node new_mem = RelsUtils::constructPair( iden_term, fst_exp_mem, fst_exp_mem ); + + if( (*mem_rep_exp_it)[1] != iden_term_rel ) { + reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it)[1], iden_term_rel ) ); + } + sendInfer( NodeManager::currentNM()->mkNode( kind::MEMBER, new_mem, iden_term ), reason, "IDENTITY-UP" ); + ++mem_rep_exp_it; + } + Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for Iden Term = " << iden_term << std::endl; + } + + /* * Construct transitive closure graph for tc_rep based on the members of tc_r_rep */ @@ -434,7 +648,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > if( cur_set != tc_graph.end() ) { for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); set_it != cur_set->second.end(); set_it++ ) { - Node new_pair = constructPair( tc_rel, cur_node_rep, *set_it ); + Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it ); std::vector< Node > new_reasons( reasons ); new_reasons.push_back( rel_tc_graph_exps.find( new_pair )->second ); doTCInference( tc_rel, new_reasons, tc_graph, rel_tc_graph_exps, start_node_rep, *set_it, seen ); @@ -548,6 +762,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > computeTupleReps(mem2); std::vector elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[mem1]); + for(unsigned int j = 0; j < elements.size(); j++) { std::vector new_tup; new_tup.push_back(elements[j]); @@ -966,11 +1181,6 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } } - inline Node TheorySetsRels::constructPair(Node tc_rep, Node a, Node b) { - Datatype dt = tc_rep.getType().getSetElementType().getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b); - } - /* * Node n[0] is a tuple variable, reduce n[0] to a concrete representation, * which is (e1, ..., en) where e1, ... ,en are concrete elements of tuple n[0]. @@ -1011,6 +1221,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > d_eqEngine->addFunctionKind(kind::JOIN); d_eqEngine->addFunctionKind(kind::TRANSPOSE); d_eqEngine->addFunctionKind(kind::TCLOSURE); + d_eqEngine->addFunctionKind(kind::JOIN_IMAGE); + d_eqEngine->addFunctionKind(kind::IDEN); } TheorySetsRels::~TheorySetsRels() { @@ -1045,6 +1257,27 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } } + std::vector TupleTrie::findSuccessors( std::vector< Node >& reps, int argIndex ) { + std::vector nodes; + std::map< Node, TupleTrie >::iterator it; + + if( argIndex==(int)reps.size() ){ + it = d_data.begin(); + while(it != d_data.end()) { + nodes.push_back(it->first); + it++; + } + return nodes; + }else{ + it = d_data.find( reps[argIndex] ); + if( it==d_data.end() ){ + return nodes; + }else{ + return it->second.findSuccessors( reps, argIndex+1 ); + } + } + } + Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) { if( argIndex==(int)reps.size() ){ if( d_data.empty() ){ @@ -1483,16 +1716,3 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } } } - - - - - - - - - - - - - diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index fed808de4..576430eb1 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -36,6 +36,7 @@ public: std::map< Node, TupleTrie > d_data; public: std::vector findTerms( std::vector< Node >& reps, int argIndex = 0 ); + std::vector findSuccessors( std::vector< Node >& reps, int argIndex = 0 ); Node existsTerm( std::vector< Node >& reps, int argIndex = 0 ); bool addTerm( Node n, std::vector< Node >& reps, int argIndex = 0 ); void debugPrint( const char * c, Node n, unsigned depth = 0 ); @@ -45,12 +46,7 @@ public: class TheorySetsRels { typedef context::CDChunkList< Node > NodeList; - typedef context::CDChunkList< int > IdList; - typedef context::CDHashMap< int, IdList* > IdListMap; typedef context::CDHashSet< Node, NodeHashFunction > NodeSet; - typedef context::CDHashMap< Node, bool, NodeHashFunction > NodeBoolMap; - typedef context::CDHashMap< Node, NodeList*, NodeHashFunction > NodeListMap; - typedef context::CDHashMap< Node, NodeSet*, NodeHashFunction > NodeSetMap; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; public: @@ -71,7 +67,6 @@ private: * d_not_mem tuples that are not members of this equivalence class * d_tp is a node of kind TRANSPOSE (if any) in this equivalence class, * d_pt is a node of kind PRODUCT (if any) in this equivalence class, - * d_join is a node of kind JOIN (if any) in this equivalence class, * d_tc is a node of kind TCLOSURE (if any) in this equivalence class, */ class EqcInfo @@ -101,15 +96,13 @@ private: Node d_falseNode; /** Facts and lemmas to be sent to EE */ - std::map< Node, Node > d_pending_facts; - std::vector< Node > d_lemmas_out; NodeList d_pending_merge; - - /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeSet d_lemmas_produced; NodeSet d_shared_terms; + std::vector< Node > d_lemmas_out; + std::map< Node, Node > d_pending_facts; + - /** Relations that have been applied JOIN, PRODUCT, TC composition rules */ std::hash_set< Node, NodeHashFunction > d_rel_nodes; std::map< Node, std::vector > d_tuple_reps; std::map< Node, TupleTrie > d_membership_trie; @@ -117,41 +110,21 @@ private: /** Symbolic tuple variables that has been reduced to concrete ones */ std::hash_set< Node, NodeHashFunction > d_symbolic_tuples; - /** Mapping between relation and its (non)member representatives */ - std::map< Node, std::vector > d_rReps_memberReps_cache; - std::map< Node, std::vector > d_rReps_nonMemberReps_cache; - - - /** Mapping between relation and its (non)member representatives explanation */ - std::map< Node, std::vector > d_rReps_memberReps_exp_cache; - std::map< Node, std::vector > d_rReps_nonMemberReps_exp_cache; - /** Mapping between relation and its member representatives */ - std::map< Node, std::vector > d_membership_db; + std::map< Node, std::vector< Node > > d_rReps_memberReps_cache; - /** Mapping between relation and its members' explanation */ - std::map< Node, std::vector > d_membership_exp_db; + /** Mapping between relation and its member representatives explanation */ + 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; - /** Mapping between relation and its member representatives */ - std::map< Node, std::vector > d_arg_rep_tp_terms; - - /** Mapping between TC(r) and one explanation when building TC graph*/ - std::map< Node, Node > d_membership_tc_exp_cache; - - /** Mapping between transitive closure relation TC(r) (is not necessary a representative) and members directly asserted members */ - std::map< Node, std::hash_set > d_tc_membership_db; - /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ - std::map< Node, std::map< Node, std::hash_set > > d_tc_r_graph; std::map< Node, std::map< Node, std::hash_set > > d_rRep_tcGraph; std::map< Node, std::map< Node, std::hash_set > > d_tcr_tcGraph; std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps; std::map< Node, std::vector< Node > > d_tc_lemmas_last; - /** Mapping between transitive closure TC(r)'s representative and TC(r) */ std::map< Node, EqcInfo* > d_eqc_info; public: @@ -176,6 +149,8 @@ private: void applyTransposeRule( Node rel, Node rel_rep, Node exp ); void applyProductRule( Node rel, Node rel_rep, Node exp ); void applyJoinRule( Node rel, Node rel_rep, Node exp); + void applyJoinImageRule( Node mem_rep, Node rel_rep, Node exp); + void applyIdenRule( Node mem_rep, Node rel_rep, Node exp); void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp); void buildTCGraphForRel( Node tc_rel ); void doTCInference(); @@ -185,7 +160,9 @@ private: void composeMembersForRels( Node ); void computeMembersForBinOpRel( Node ); + void computeMembersForIdenTerm( Node ); void computeMembersForUnaryOpRel( Node ); + void computeMembersForJoinImageTerm( Node ); bool isTCReachable( Node mem_rep, Node tc_rel ); void isTCReachable( Node start, Node dest, std::hash_set& hasSeen, @@ -206,7 +183,6 @@ private: void computeTupleReps( Node ); bool areEqual( Node a, Node b ); Node getRepresentative( Node t ); - bool insertIntoIdList(IdList&, int); bool exists( std::vector&, Node ); Node mkAnd( std::vector< TNode >& assumptions ); inline void addToMembershipDB( Node, Node, Node ); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 8facf1f48..3590fc62d 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -288,7 +288,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { std::set right = NormalForm::getElementsFromNormalConstant(node[1]); std::set newSet; std::set_union(left.begin(), left.end(), right.begin(), right.end(), - std::inserter(newSet, newSet.begin())); + std::inserter(newSet, newSet.begin())); Node newNode = NormalForm::elementsToSet(newSet, node.getType()); Assert(newNode.isConst()); Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; @@ -381,7 +381,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { std::set::iterator right_it = right.begin(); int right_len = (*right_it).getType().getTupleLength(); while(right_it != right.end()) { - Trace("rels-debug") << "Sets::postRewrite processing left_it = " << *right_it << std::endl; + Trace("rels-debug") << "Sets::postRewrite processing right_it = " << *right_it << std::endl; std::vector right_tuple; for(int j = 0; j < right_len; j++) { right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j)); @@ -468,6 +468,77 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { break; } + case kind::IDEN: { + if(node[0].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + } else if (node[0].isConst()) { + std::set iden_rel_mems; + std::set rel_mems = NormalForm::getElementsFromNormalConstant(node[0]); + std::set::iterator rel_mems_it = rel_mems.begin(); + + while( rel_mems_it != rel_mems.end() ) { + Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0); + iden_rel_mems.insert(RelsUtils::constructPair(node, fst_mem, fst_mem)); + ++rel_mems_it; + } + + Node new_node = NormalForm::elementsToSet(iden_rel_mems, node.getType()); + Assert(new_node.isConst()); + Trace("rels-postrewrite") << "Rels::postRewrite returning " << new_node << std::endl; + return RewriteResponse(REWRITE_DONE, new_node); + + } else { + Trace("rels-postrewrite") << "Rels::postRewrite miss to handle term " << node << std::endl; + } + break; + } + + case kind::JOIN_IMAGE: { + unsigned int min_card = node[1].getConst().getNumerator().getUnsignedInt(); + Trace("rels-postrewrite") << "Rels::postRewrite " << node << " with min_card = " << min_card << std::endl; + + if( min_card == 0) { + return RewriteResponse(REWRITE_DONE, nm->mkNullaryOperator( node.getType(), kind::UNIVERSE_SET )); + } else if(node[0].getKind() == kind::EMPTYSET) { + return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + } else if (node[0].isConst()) { + std::set has_checked; + std::set join_img_mems; + std::set rel_mems = NormalForm::getElementsFromNormalConstant(node[0]); + std::set::iterator rel_mems_it = rel_mems.begin(); + + while( rel_mems_it != rel_mems.end() ) { + Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0); + if( has_checked.find( fst_mem ) != has_checked.end() ) { + ++rel_mems_it; + continue; + } + has_checked.insert( fst_mem ); + std::set existing_mems; + std::set::iterator rel_mems_it_snd = rel_mems.begin(); + while( rel_mems_it_snd != rel_mems.end() ) { + Node fst_mem_snd = RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 0); + if( fst_mem == fst_mem_snd ) { + existing_mems.insert( RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 1) ); + } + ++rel_mems_it_snd; + } + if( existing_mems.size() >= min_card ) { + Datatype dt = node.getType().getSetElementType().getDatatype(); + join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem )); + } + ++rel_mems_it; + } + Node new_node = NormalForm::elementsToSet(join_img_mems, node.getType()); + Assert(new_node.isConst()); + Trace("rels-postrewrite") << "Rels::postRewrite returning " << new_node << std::endl; + return RewriteResponse(REWRITE_DONE, new_node); + } else { + Trace("rels-postrewrite") << "Rels::postRewrite miss to handle term " << node << std::endl; + } + break; + } + default: break; }//switch(node.getKind()) @@ -494,13 +565,13 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { size_t setNodeIndex = node.getNumChildren()-1; for(size_t i = 1; i < setNodeIndex; ++i) { insertedElements = nm->mkNode(kind::UNION, - insertedElements, - nm->mkNode(kind::SINGLETON, node[i])); + insertedElements, + nm->mkNode(kind::SINGLETON, node[i])); } return RewriteResponse(REWRITE_AGAIN, - nm->mkNode(kind::UNION, - insertedElements, - node[setNodeIndex])); + nm->mkNode(kind::UNION, + insertedElements, + node[setNodeIndex])); }//kind::INSERT else if(node.getKind() == kind::SUBSET) { diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 25ca63c28..a3abdf508 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -227,10 +227,10 @@ struct RelBinaryOperatorTypeRule { TypeNode resultType = firstRelType; if(!firstRelType.isSet() || !secondRelType.isSet()) { - throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets"); + throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-sets"); } if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) { - throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)"); + throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-relations (sets of tuples)"); } std::vector newTupleTypes; @@ -306,6 +306,75 @@ struct RelTransClosureTypeRule { } };/* struct RelTransClosureTypeRule */ +struct JoinImageTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::JOIN_IMAGE); + + TypeNode firstRelType = n[0].getType(check); + + if(!firstRelType.isSet()) { + throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations"); + } + if(!firstRelType[0].isTuple()) { + throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations (sets of tuples)"); + } + + std::vector tupleTypes = firstRelType[0].getTupleTypes(); + if(tupleTypes.size() != 2) { + throw TypeCheckingExceptionPrivate(n, " JoinImage operates on a non-binary relation"); + } + TypeNode valType = n[1].getType(check); + if (valType != nodeManager->integerType()) { + throw TypeCheckingExceptionPrivate( + n, " JoinImage cardinality constraint must be integer"); + } + if (n[1].getKind() != kind::CONST_RATIONAL) { + throw TypeCheckingExceptionPrivate( + n, " JoinImage cardinality constraint must be a constant"); + } + CVC4::Rational r(INT_MAX); + if (n[1].getConst() > r) { + throw TypeCheckingExceptionPrivate( + n, " JoinImage Exceeded INT_MAX in cardinality constraint"); + } + if (n[1].getConst().getNumerator().getSignedInt() < 0) { + throw TypeCheckingExceptionPrivate( + n, " JoinImage cardinality constraint must be non-negative"); + } + std::vector newTupleTypes; + newTupleTypes.push_back(tupleTypes[0]); + return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::JOIN_IMAGE); + return false; + } +};/* struct JoinImageTypeRule */ + +struct RelIdenTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::IDEN); + TypeNode setType = n[0].getType(check); + if(check) { + if(!setType.isSet() && !setType.getSetElementType().isTuple()) { + throw TypeCheckingExceptionPrivate(n, " Identity operates on non-relation"); + } + if(setType[0].getTupleTypes().size() != 1) { + throw TypeCheckingExceptionPrivate(n, " Identity operates on non-unary relations"); + } + } + std::vector tupleTypes = setType[0].getTupleTypes(); + tupleTypes.push_back(tupleTypes[0]); + return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + return false; + } +};/* struct RelIdenTypeRule */ struct SetsProperties { inline static Cardinality computeCardinality(TypeNode type) { diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am index bb9c49298..d1c035371 100644 --- a/test/regress/regress0/rels/Makefile.am +++ b/test/regress/regress0/rels/Makefile.am @@ -102,7 +102,17 @@ TESTS = \ set-strat.cvc \ rel_tc_8.cvc \ atom_univ2.cvc \ - rels-sharing-simp.cvc + rels-sharing-simp.cvc \ + iden_0.cvc \ + iden_1_1.cvc \ + iden_1.cvc \ + joinImg_0_1.cvc \ + joinImg_0_2.cvc \ + joinImg_0.cvc \ + joinImg_1_1.cvc \ + joinImg_1.cvc \ + joinImg_2_1.cvc \ + joinImg_2.cvc # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/rels/iden_0.cvc b/test/regress/regress0/rels/iden_0.cvc new file mode 100644 index 000000000..4c2693084 --- /dev/null +++ b/test/regress/regress0/rels/iden_0.cvc @@ -0,0 +1,28 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +id : SET OF IntPair; + +t : SET OF [INT]; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT TUPLE(1) IS_IN t; +ASSERT TUPLE(2) IS_IN t; +ASSERT z IS_IN x; +ASSERT zt IS_IN x; +ASSERT v IS_IN x; +ASSERT a IS_IN x; +ASSERT id = IDEN(t); +ASSERT NOT ((1, 1) IS_IN (id & x)); + +CHECKSAT; diff --git a/test/regress/regress0/rels/iden_1.cvc b/test/regress/regress0/rels/iden_1.cvc new file mode 100644 index 000000000..f73700e88 --- /dev/null +++ b/test/regress/regress0/rels/iden_1.cvc @@ -0,0 +1,18 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom:TYPE; +AtomPair: TYPE = [Atom, Atom]; +x : SET OF AtomPair; +t : SET OF [Atom]; +univ : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +ASSERT univ = UNIVERSE::SET OF [Atom]; +ASSERT (a, b) IS_IN x; +ASSERT (c, d) IS_IN x; +ASSERT NOT(a = b); +ASSERT IDEN(x JOIN univ) = x; +CHECKSAT; diff --git a/test/regress/regress0/rels/iden_1_1.cvc b/test/regress/regress0/rels/iden_1_1.cvc new file mode 100644 index 000000000..d118f15dd --- /dev/null +++ b/test/regress/regress0/rels/iden_1_1.cvc @@ -0,0 +1,21 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +Atom:TYPE; +AtomPair: TYPE = [Atom, Atom]; +x : SET OF AtomPair; +t : SET OF [Atom]; +univ : SET OF [Atom]; +univ2 : SET OF [Atom,Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +ASSERT univ = UNIVERSE::SET OF [Atom]; +ASSERT univ2 = UNIVERSE::SET OF [Atom, Atom]; +ASSERT univ2 = (univ PRODUCT univ); +ASSERT (a, b) IS_IN x; +ASSERT (c, d) IS_IN x; +ASSERT NOT(a = b); +ASSERT IDEN(univ) <= x; +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc new file mode 100644 index 000000000..e36c6a647 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_0.cvc @@ -0,0 +1,33 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +t : SET OF [INT]; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT z IS_IN x; + +ASSERT (7, 5) IS_IN y; + +ASSERT t = (x JOIN_IMAGE 2); + +ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2); + +ASSERT NOT(TUPLE(1) IS_IN (x JOIN_IMAGE 2)); + +ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); + +ASSERT TUPLE(1) IS_IN (x JOIN_IMAGE 1); +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc new file mode 100644 index 000000000..602c4fe3f --- /dev/null +++ b/test/regress/regress0/rels/joinImg_0_1.cvc @@ -0,0 +1,35 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +t : SET OF [INT]; +u : SET OF [INT]; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); +b: INT; + +ASSERT (1, 7) IS_IN x; +ASSERT z IS_IN x; + +ASSERT (7, 5) IS_IN y; + +ASSERT t = (x JOIN_IMAGE 2); + +ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2); + +ASSERT u = (x JOIN_IMAGE 1); + +ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); + +ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1); +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_0_2.cvc b/test/regress/regress0/rels/joinImg_0_2.cvc new file mode 100644 index 000000000..f71069217 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_0_2.cvc @@ -0,0 +1,38 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +t : SET OF [INT]; +u : SET OF [INT]; +univ : SET OF [INT]; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +s : IntPair; +ASSERT s = (1,1); +a : IntPair; +ASSERT a = (1,5); +b: INT; + +ASSERT (1, 7) IS_IN x; +ASSERT z IS_IN x; + +ASSERT (7, 5) IS_IN y; + +ASSERT t = (x JOIN_IMAGE 2); +ASSERT univ = (x JOIN_IMAGE 0); +ASSERT TUPLE(100) IS_IN t; + +ASSERT NOT (TUPLE(3) IS_IN univ); + +ASSERT u = (x JOIN_IMAGE 1); + +ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); + +ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1); +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc new file mode 100644 index 000000000..47e57c1fb --- /dev/null +++ b/test/regress/regress0/rels/joinImg_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +x : SET OF [Atom, Atom]; +y : SET OF [Atom, Atom]; +r : SET OF [Atom, Atom]; + +t : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +e : Atom; + +ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); +ASSERT x = {(b, c), (d, e), (c, e)}; +ASSERT NOT(a = b); + +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc new file mode 100644 index 000000000..a7927f7e2 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_1_1.cvc @@ -0,0 +1,21 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +x : SET OF [Atom, Atom]; +y : SET OF [Atom, Atom]; +r : SET OF [Atom, Atom]; + +t : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +e : Atom; + +ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); +ASSERT t = (x JOIN_IMAGE 2); +ASSERT x = {(b, c), (d, e), (c, e)}; +ASSERT TUPLE(c) IS_IN t; + +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc new file mode 100644 index 000000000..bbf57629b --- /dev/null +++ b/test/regress/regress0/rels/joinImg_2.cvc @@ -0,0 +1,33 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +x : SET OF [Atom, Atom]; +y : SET OF [Atom, Atom]; +r : SET OF [Atom, Atom]; + +t : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +e : Atom; +f : Atom; +g : Atom; + +ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); +ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 3); +%ASSERT y = {(f, g), (b, c), (d, e), (c, e)}; +ASSERT x = {(f, g), (b, c), (d, e), (c, e), (f, b)}; +ASSERT (a, f) IS_IN x; +ASSERT (a, f) IS_IN y; +ASSERT x = y; + + + +ASSERT NOT(a = b); + +ASSERT NOT (TUPLE(d) IS_IN (x JOIN_IMAGE 2)); +ASSERT f = d; + +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc new file mode 100644 index 000000000..b38bfab06 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_2_1.cvc @@ -0,0 +1,24 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +x : SET OF [Atom, Atom]; +y : SET OF [Atom, Atom]; +r : SET OF [Atom, Atom]; + +t : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +e : Atom; +f : Atom; +g : Atom; + +ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); +ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 1); +ASSERT y = {(f, g), (b, c), (d, e), (c, e)}; +ASSERT x = {(f, g), (b, c), (d, e), (c, e)}; +ASSERT (NOT(a = b)) OR (NOT(a = f)); + +CHECKSAT; \ No newline at end of file -- 2.30.2