diff options
| author | Paul Meng <baolmeng@gmail.com> | 2016-11-14 20:09:07 -0600 |
|---|---|---|
| committer | Paul Meng <baolmeng@gmail.com> | 2016-11-14 20:09:07 -0600 |
| commit | 1d6d68a6381e0d1fe4bdb2296bc2774a5b2f5294 (patch) | |
| tree | 8ed4ce7b2bbf970047141a1debffcce489095ff2 /src/theory/sets | |
| parent | dd7341edeab50ee0f19965874ab6c55942a0ef37 (diff) | |
relational solver code refactor and bug fixes
Diffstat (limited to 'src/theory/sets')
| -rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 1470 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rels.h | 65 |
2 files changed, 658 insertions, 877 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 6fb7412da..97e67a423 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -27,7 +27,7 @@ namespace sets { typedef std::map< Node, std::vector< Node > >::iterator MEM_IT; typedef std::map< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_IT; -typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_PAIR_IT; +typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT; typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > > >::iterator TC_IT; @@ -39,31 +39,32 @@ int TheorySetsRels::EqcInfo::counter = 0; collectRelsInfo(); check(); doPendingLemmas(); - Assert(d_lemma_cache.empty()); - Assert(d_pending_facts.empty()); + Assert( d_lemmas_out.empty() ); + Assert( d_pending_facts.empty() ); } else { doPendingMerge(); - doPendingLemmas(); } Trace("rels") << "\n[sets-rels] ******************************* Done with the relational solver *******************************\n" << std::endl; } void TheorySetsRels::check() { - MEM_IT m_it = d_membership_constraints_cache.begin(); + MEM_IT m_it = d_rReps_memberReps_cache.begin(); - while(m_it != d_membership_constraints_cache.end()) { + while(m_it != d_rReps_memberReps_cache.end()) { Node rel_rep = m_it->first; for(unsigned int i = 0; i < m_it->second.size(); i++) { - Node exp = d_membership_exp_cache[rel_rep][i]; + Node mem = d_rReps_memberReps_cache[rel_rep][i]; + Node exp = d_rReps_memberReps_exp_cache[rel_rep][i]; std::map<kind::Kind_t, std::vector<Node> > kind_terms = d_terms_cache[rel_rep]; if( kind_terms.find(kind::TRANSPOSE) != kind_terms.end() ) { std::vector<Node> 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 - for(unsigned int j = 0; j < tp_terms.size(); j++) { - applyTransposeRule( exp, tp_terms[j] ); + if( tp_terms.size() > 0 ) { + applyTransposeRule( tp_terms ); + applyTransposeRule( tp_terms[0], rel_rep, exp ); } } if( kind_terms.find(kind::JOIN) != kind_terms.end() ) { @@ -71,33 +72,21 @@ int TheorySetsRels::EqcInfo::counter = 0; // 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( exp, join_terms[j] ); + for( unsigned int j = 0; j < join_terms.size(); j++ ) { + applyJoinRule( join_terms[j], rel_rep, exp ); } } if( kind_terms.find(kind::PRODUCT) != kind_terms.end() ) { std::vector<Node> product_terms = kind_terms[kind::PRODUCT]; - for(unsigned int j = 0; j < product_terms.size(); j++) { - applyProductRule( exp, product_terms[j] ); + for( unsigned int j = 0; j < product_terms.size(); j++ ) { + applyProductRule( product_terms[j], rel_rep, exp ); } } if( kind_terms.find(kind::TCLOSURE) != kind_terms.end() ) { std::vector<Node> tc_terms = kind_terms[kind::TCLOSURE]; - for(unsigned int j = 0; j < tc_terms.size(); j++) { - applyTCRule( exp, tc_terms[j] ); - } - } - - MEM_IT tp_it = d_arg_rep_tp_terms.find( rel_rep ); - - if( tp_it != d_arg_rep_tp_terms.end() ) { - std::vector< Node >::iterator tp_ts_it = tp_it->second.begin(); - - while( tp_ts_it != tp_it->second.end() ) { - applyTransposeRule( exp, *tp_ts_it, (*tp_ts_it)[0] == rel_rep?Node::null():explain(NodeManager::currentNM()->mkNode(kind::EQUAL,(*tp_ts_it)[0], rel_rep)), true ); - ++tp_ts_it; + for( unsigned int j = 0; j < tc_terms.size(); j++ ) { + applyTCRule( mem, tc_terms[j], rel_rep, exp ); } - ++tp_it; } } m_it++; @@ -105,7 +94,7 @@ int TheorySetsRels::EqcInfo::counter = 0; TERM_IT t_it = d_terms_cache.begin(); while( t_it != d_terms_cache.end() ) { - if( d_membership_constraints_cache.find(t_it->first) == d_membership_constraints_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(); @@ -113,26 +102,29 @@ int TheorySetsRels::EqcInfo::counter = 0; if( k_t_it->first == kind::JOIN || k_t_it->first == kind::PRODUCT ) { std::vector<Node>::iterator term_it = k_t_it->second.begin(); while(term_it != k_t_it->second.end()) { - computeMembersForRelofMultArities(*term_it); + computeMembersForBinOpRel( *term_it ); term_it++; } - } else if ( k_t_it->first == kind::TRANSPOSE ) { + } else if( k_t_it->first == kind::TRANSPOSE ) { std::vector<Node>::iterator term_it = k_t_it->second.begin(); while( term_it != k_t_it->second.end() ) { - computeMembersForUnaryRel(*term_it); + computeMembersForUnaryOpRel( *term_it ); term_it++; } } else if ( k_t_it->first == kind::TCLOSURE ) { - Trace("rels-debug") << "[sets-rels] ********** A TCLOSURE term does not have membership constraints: " << t_it->first << std::endl; - d_tc_rep_term[t_it->first] = k_t_it->second[0]; + std::vector<Node>::iterator term_it = k_t_it->second.begin(); + while( term_it != k_t_it->second.end() ) { + buildTCGraphForRel( *term_it ); + term_it++; + } + } k_t_it++; } } t_it++; } - - finalizeTCInference(); + doTCInference(); } /* @@ -146,31 +138,36 @@ int TheorySetsRels::EqcInfo::counter = 0; Node eqc_rep = (*eqcs_i); eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc_rep, d_eqEngine ); - Trace("rels-ee") << "[sets-rels-ee] term representative: " << eqc_rep << std::endl; + Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << std::endl; while( !eqc_i.isFinished() ){ Node eqc_node = (*eqc_i); Trace("rels-ee") << " term : " << eqc_node << std::endl; - if(getRepresentative(eqc_rep) == getRepresentative(d_trueNode) || - getRepresentative(eqc_rep) == getRepresentative(d_falseNode)) { + if( getRepresentative(eqc_rep) == getRepresentative(d_trueNode) || + getRepresentative(eqc_rep) == getRepresentative(d_falseNode) ) { // collect membership info - if(eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple()) { - Node tup_rep = getRepresentative(eqc_node[0]); - Node rel_rep = getRepresentative(eqc_node[1]); + if( eqc_node.getKind() == kind::MEMBER && eqc_node[1].getType().getSetElementType().isTuple() ) { + Node tup_rep = getRepresentative( eqc_node[0] ); + Node rel_rep = getRepresentative( eqc_node[1] ); - if(eqc_node[0].isVar()){ - reduceTupleVar(eqc_node); + if( eqc_node[0].isVar() ){ + reduceTupleVar( eqc_node ); } - if( safelyAddToMap(d_membership_constraints_cache, rel_rep, tup_rep) ) { - bool is_true_eq = areEqual(eqc_rep, d_trueNode); - Node reason = is_true_eq ? eqc_node : eqc_node.negate(); - addToMap(d_membership_exp_cache, rel_rep, reason); - if( is_true_eq ) { - // add tup_rep to membership database - // and store mapping between tuple and tuple's elements representatives - addToMembershipDB(rel_rep, tup_rep, reason); + + bool is_true_eq = areEqual( eqc_rep, d_trueNode ); + Node reason = is_true_eq ? eqc_node : eqc_node.negate(); + + if( is_true_eq ) { + if( safelyAddToMap(d_rReps_memberReps_cache, rel_rep, tup_rep) ) { + addToMap(d_rReps_memberReps_exp_cache, rel_rep, reason); + 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); } } } @@ -178,22 +175,9 @@ int TheorySetsRels::EqcInfo::counter = 0; } 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 ) { - std::vector<Node> terms; - std::map<kind::Kind_t, std::vector<Node> > rel_terms; - TERM_IT terms_it = d_terms_cache.find(eqc_rep); - - if( eqc_node.getKind() == kind::TRANSPOSE ) { - Node eqc_node0_rep = getRepresentative( eqc_node[0] ); - MEM_IT mem_it = d_arg_rep_tp_terms.find( eqc_node0_rep ); - - if( mem_it != d_arg_rep_tp_terms.end() ) { - mem_it->second.push_back( eqc_node ); - } else { - std::vector< Node > tp_terms; - tp_terms.push_back( eqc_node ); - d_arg_rep_tp_terms[eqc_node0_rep] = tp_terms; - } - } + std::vector<Node> terms; + std::map< kind::Kind_t, std::vector<Node> > rel_terms; + TERM_IT terms_it = d_terms_cache.find(eqc_rep); if( terms_it == d_terms_cache.end() ) { terms.push_back(eqc_node); @@ -211,11 +195,12 @@ int TheorySetsRels::EqcInfo::counter = 0; } } // need to add all tuple elements as shared terms - } else if(eqc_node.getType().isTuple() && !eqc_node.isConst() && !eqc_node.isVar()) { - for(unsigned int i = 0; i < eqc_node.getType().getTupleLength(); i++) { - Node element = RelsUtils::nthElementOfTuple(eqc_node, i); - if(!element.isConst()) { - makeSharedTerm(element); + } else if( eqc_node.getType().isTuple() && !eqc_node.isConst() && !eqc_node.isVar() ) { + for( unsigned int i = 0; i < eqc_node.getType().getTupleLength(); i++ ) { + Node element = RelsUtils::nthElementOfTuple( eqc_node, i ); + + if( !element.isConst() ) { + makeSharedTerm( element ); } } } @@ -223,72 +208,13 @@ int TheorySetsRels::EqcInfo::counter = 0; } ++eqcs_i; } - Trace("rels-debug") << "[sets-rels] Done with collecting relational terms!" << std::endl; + Trace("rels-debug") << "[Theory::Rels] Done with collecting relational terms!" << std::endl; } /* * Construct transitive closure graph for tc_rep based on the members of tc_r_rep */ - std::map< Node, std::hash_set< Node, NodeHashFunction > > TheorySetsRels::constructTCGraph(Node tc_r_rep, Node tc_rep, Node tc_term) { - Trace("rels-tc") << "[sets-rels] Construct TC graph for transitive closure relation " << tc_rep << std::endl; - - std::map< Node, std::hash_set< Node, NodeHashFunction > > tc_graph; - std::map< Node, std::hash_set< Node, NodeHashFunction > > tc_r_graph; - MEM_IT mem_it = d_membership_db.find(tc_r_rep); - - if(mem_it != d_membership_db.end()) { - for(std::vector<Node>::iterator pair_it = mem_it->second.begin(); - pair_it != mem_it->second.end(); pair_it++) { - Node fst_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 0)); - Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 1)); - TC_PAIR_IT pair_set_it = tc_graph.find(fst_rep); - TC_PAIR_IT r_pair_set_it = tc_r_graph.find(fst_rep); - - Trace("rels-tc") << "[sets-rels] **** Member of r = (" << fst_rep << ", " << snd_rep << ")" << std::endl; - - if( pair_set_it != tc_graph.end() ) { - pair_set_it->second.insert(snd_rep); - r_pair_set_it->second.insert(snd_rep); - } else { - std::hash_set< Node, NodeHashFunction > snd_set; - snd_set.insert(snd_rep); - tc_r_graph[fst_rep] = snd_set; - tc_graph[fst_rep] = snd_set; - } - } - } - - Node reason = getReason(tc_rep, tc_term, tc_r_rep, tc_term[0]); - - if(!reason.isNull()) { - d_membership_tc_exp_cache[tc_rep] = reason; - } - d_tc_r_graph[tc_rep] = tc_r_graph; - - TC_PAIR_IT tc_mem_it = d_tc_membership_db.find(tc_term); - - if( tc_mem_it != d_tc_membership_db.end() ) { - for(std::hash_set<Node, NodeHashFunction>::iterator pair_it = tc_mem_it->second.begin(); - pair_it != tc_mem_it->second.end(); pair_it++) { - Node fst_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 0)); - Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 1)); - TC_PAIR_IT pair_set_it = tc_graph.find(fst_rep); - Trace("rels-tc") << "[sets-rels] **** Member of TC(r) = (" << fst_rep << ", " << snd_rep << ")" << std::endl; - - if( pair_set_it != tc_graph.end() ) { - pair_set_it->second.insert(snd_rep); - } else { - std::hash_set< Node, NodeHashFunction > snd_set; - snd_set.insert(snd_rep); - tc_graph[fst_rep] = snd_set; - } - } - } - - return tc_graph; - } - /* * * @@ -302,33 +228,218 @@ int TheorySetsRels::EqcInfo::counter = 0; * ----------------------------------------------------------- * x <= TCLOSURE(x) && (x JOIN x) <= TCLOSURE(x) .... * - * TC(x) = TC(y) => x = y ? - * */ + void TheorySetsRels::applyTCRule( Node mem_rep, Node tc_rel, Node tc_rel_rep, Node exp ) { + Trace("rels-debug") << "[Theory::Rels] *********** Applying TCLOSURE rule on a tc term = " << tc_rel + << ", its representative = " << tc_rel_rep + << " with member rep = " << mem_rep << " and explanation = " << exp << std::endl; + MEM_IT mem_it = d_rReps_memberReps_cache.find( tc_rel[0] ); + + if( mem_it != d_rReps_memberReps_cache.end() && d_rel_nodes.find( tc_rel ) == d_rel_nodes.end() + && d_rRep_tcGraph.find( getRepresentative( tc_rel[0] ) ) == d_rRep_tcGraph.end() ) { + buildTCGraphForRel( tc_rel ); + d_rel_nodes.insert( tc_rel ); + } + + // mem_rep is a member of tc_rel[0] or mem_rep can be infered by TC_Graph of tc_rel[0], thus skip + if( isTCReachable( mem_rep, tc_rel) ) { + Trace("rels-debug") << "[Theory::Rels] mem_rep is a member of tc_rel[0] = " << tc_rel[0] + << " or can be infered by TC_Graph of tc_rel[0]! " << std::endl; + return; + } + // add mem_rep to d_tcrRep_tcGraph + TC_IT tc_it = d_tcr_tcGraph.find( tc_rel ); + Node mem_rep_fst = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 0 ) ); + Node mem_rep_snd = getRepresentative( RelsUtils::nthElementOfTuple( mem_rep, 1 ) ); + Node mem_rep_tup = RelsUtils::constructPair( tc_rel, mem_rep_fst, mem_rep_snd ); + + if( tc_it != d_tcr_tcGraph.end() ) { + std::map< Node, std::map< Node, Node > >::iterator tc_exp_it = d_tcr_tcGraph_exps.find( tc_rel ); + + TC_GRAPH_IT tc_graph_it = (tc_it->second).find( mem_rep_fst ); + Assert( tc_exp_it != d_tcr_tcGraph_exps.end() ); + std::map< Node, Node >::iterator exp_map_it = (tc_exp_it->second).find( mem_rep_tup ); + + if( exp_map_it == (tc_exp_it->second).end() ) { + (tc_exp_it->second)[mem_rep_tup] = exp; + } - void TheorySetsRels::applyTCRule(Node exp, Node tc_term) { - Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSITIVE CLOSURE rule on " - << tc_term << " with explanation " << exp << std::endl; + if( tc_graph_it != (tc_it->second).end() ) { + (tc_graph_it->second).insert( mem_rep_snd ); + } else { + std::hash_set< Node, NodeHashFunction > sets; + sets.insert( mem_rep_snd ); + (tc_it->second)[mem_rep_fst] = sets; + } + } else { + std::map< Node, Node > exp_map; + std::hash_set< Node, NodeHashFunction > sets; + std::map< Node, std::hash_set<Node, NodeHashFunction> > element_map; + sets.insert( mem_rep_snd ); + element_map[mem_rep_fst] = sets; + d_tcr_tcGraph[tc_rel] = element_map; + exp_map[mem_rep_tup] = exp; + d_tcr_tcGraph_exps[tc_rel] = exp_map; + } + + Node fst_element = RelsUtils::nthElementOfTuple( exp[0], 0 ); + Node snd_element = RelsUtils::nthElementOfTuple( exp[0], 1 ); + Node sk_1 = NodeManager::currentNM()->mkSkolem("stc", fst_element.getType()); + Node sk_2 = NodeManager::currentNM()->mkSkolem("stc", snd_element.getType()); + Node mem_of_r = NodeManager::currentNM()->mkNode(kind::MEMBER, exp[0], tc_rel[0]); + Node sk_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sk_1, sk_2); + Node reason = exp; + + if( tc_rel != exp[1] ) { + reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel, exp[1])); + } + + Node conclusion = NodeManager::currentNM()->mkNode(kind::OR, mem_of_r, + (NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, fst_element, sk_1), tc_rel[0]), + (NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_2, snd_element), tc_rel[0]), + (NodeManager::currentNM()->mkNode(kind::OR, sk_eq, NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::constructPair(tc_rel, sk_1, sk_2), tc_rel)))))))); + + Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, conclusion ); + std::vector< Node > require_phase; + require_phase.push_back(Rewriter::rewrite(mem_of_r)); + require_phase.push_back(Rewriter::rewrite(sk_eq)); + d_tc_lemmas_last[tc_lemma] = require_phase; + } - Node tc_rep = getRepresentative(tc_term); - bool polarity = exp.getKind() != kind::NOT; + bool TheorySetsRels::isTCReachable( Node mem_rep, Node tc_rel ) { + MEM_IT mem_it = d_rReps_memberReps_cache.find( getRepresentative( tc_rel[0] ) ); - if( d_rel_nodes.find(tc_rep) == d_rel_nodes.end() ) { - d_tc_rep_term[tc_rep] = tc_term; - d_rel_nodes.insert(tc_rep); + if( mem_it != d_rReps_memberReps_cache.end() && std::find( (mem_it->second).begin(), (mem_it->second).end(), mem_rep) != (mem_it->second).end() ) { + return true; + } + + TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) ); + if( tc_it != d_rRep_tcGraph.end() ) { + bool isReachable = false; + std::hash_set<Node, NodeHashFunction> seen; + isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ), + getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable ); + return isReachable; + } + return false; + } + + void TheorySetsRels::isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, + std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { + if(hasSeen.find(start) == hasSeen.end()) { + hasSeen.insert(start); } - if(polarity) { - TC_PAIR_IT mem_it = d_tc_membership_db.find(tc_term); - if( mem_it == d_tc_membership_db.end() ) { - std::hash_set<Node, NodeHashFunction> members; - members.insert(exp[0]); - d_tc_membership_db[tc_term] = members; + TC_GRAPH_IT pair_set_it = tc_graph.find(start); + + if(pair_set_it != tc_graph.end()) { + if(pair_set_it->second.find(dest) != pair_set_it->second.end()) { + isReachable = true; + return; } else { - mem_it->second.insert(exp[0]); + std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); + + while( set_it != pair_set_it->second.end() ) { + // need to check if *set_it has been looked already + if( hasSeen.find(*set_it) == hasSeen.end() ) { + isTCReachable( *set_it, dest, hasSeen, tc_graph, isReachable ); + } + set_it++; + } + } + } + } + + void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) { + std::map< Node, Node > rel_tc_graph_exps; + std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph; + + 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]; + + for( unsigned int i = 0; i < members.size(); 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 ); + std::map< Node, std::hash_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); + + if( rel_tc_graph_it == rel_tc_graph.end() ) { + std::hash_set< Node, NodeHashFunction > snd_elements; + snd_elements.insert( snd_element_rep ); + rel_tc_graph[fst_element_rep] = snd_elements; + rel_tc_graph_exps[tuple_rep] = exps[i]; + } else if( (rel_tc_graph_it->second).find( snd_element_rep ) == (rel_tc_graph_it->second).end() ) { + (rel_tc_graph_it->second).insert( snd_element_rep ); + rel_tc_graph_exps[tuple_rep] = exps[i]; + } + } + + if( members.size() > 0 ) { + d_rRep_tcGraph[rel_rep] = rel_tc_graph; + d_tcr_tcGraph_exps[tc_rel] = rel_tc_graph_exps; + d_tcr_tcGraph[tc_rel] = rel_tc_graph; + } + } + + void TheorySetsRels::doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { + Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl; + for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) { + for( std::hash_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin(); + snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) { + std::vector< Node > reasons; + std::hash_set<Node, NodeHashFunction> seen; + Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) ); + Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() ); + Node exp = rel_tc_graph_exps.find( tuple )->second; + + reasons.push_back( exp ); + seen.insert( tc_graph_it->first ); + doTCInference( tc_rel, reasons, rel_tc_graph, rel_tc_graph_exps, tc_graph_it->first, *snd_elements_it, seen); + } + } + Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl; + } + + void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, + std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ) { + Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) ); + std::vector< Node > all_reasons( reasons ); + + for( unsigned int i = 0 ; i < reasons.size()-1; i++ ) { + Node fst_element_end = RelsUtils::nthElementOfTuple( reasons[i][0], 1 ); + Node snd_element_begin = RelsUtils::nthElementOfTuple( reasons[i+1][0], 0 ); + if( fst_element_end != snd_element_begin ) { + all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, fst_element_end, snd_element_begin) ); } + if( tc_rel != reasons[i][1] && tc_rel[0] != reasons[i][1] ) { + all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel[0], reasons[i][1]) ); + } + } + if( tc_rel != reasons.back()[1] && tc_rel[0] != reasons.back()[1] ) { + all_reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, tc_rel[0], reasons.back()[1]) ); + } + if( all_reasons.size() > 1) { + sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tc_mem, tc_rel), NodeManager::currentNM()->mkNode(kind::AND, all_reasons), "TCLOSURE-Forward"); } else { - Trace("rels-tc") << "TC non-member = " << exp << std::endl; + sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tc_mem, tc_rel), all_reasons.front(), "TCLOSURE-Forward"); + } + + // check if cur_node has been traversed or not + if( seen.find( cur_node_rep ) != seen.end() ) { + return; + } + seen.insert( cur_node_rep ); + TC_GRAPH_IT cur_set = tc_graph.find( cur_node_rep ); + 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 ); + 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 ); + } } } @@ -336,74 +447,54 @@ int TheorySetsRels::EqcInfo::counter = 0; * ---------------------------------- * a IS_IN X && b IS_IN Y * - * product-compose rule: (a, b) IS_IN X (c, d) IS_IN Y NOT (r, s, t, u) IS_IN (X PRODUCT Y) - * ---------------------------------------------------------------------- - * (a, b, c, d) IS_IN (X PRODUCT Y) + * product-compose rule: (a, b) IS_IN X (c, d) IS_IN Y + * --------------------------------- + * (a, b, c, d) IS_IN (X PRODUCT Y) */ - void TheorySetsRels::applyProductRule(Node exp, Node product_term) { - Trace("rels-debug") << "\n[sets-rels] *********** Applying PRODUCT rule " << std::endl; - if(d_rel_nodes.find(product_term) == d_rel_nodes.end()) { - computeMembersForRelofMultArities(product_term); - d_rel_nodes.insert(product_term); + void TheorySetsRels::applyProductRule( Node pt_rel, Node pt_rel_rep, Node exp ) { + Trace("rels-debug") << "\n[Theory::Rels] *********** Applying PRODUCT rule on producted term = " << pt_rel + << ", its representative = " << pt_rel_rep + << " with explanation = " << exp << std::endl; + + if(d_rel_nodes.find( pt_rel ) == d_rel_nodes.end()) { + Trace("rels-debug") << "\n[Theory::Rels] Apply PRODUCT-COMPOSE rule on term: " << pt_rel + << " with explanation: " << exp << std::endl; + + computeMembersForBinOpRel( pt_rel ); + d_rel_nodes.insert( pt_rel ); } - bool polarity = exp.getKind() != kind::NOT; - Node atom = polarity ? exp : exp[0]; - Node r1_rep = getRepresentative(product_term[0]); - Node r2_rep = getRepresentative(product_term[1]); - Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT-SPLIT rule on term: " << product_term - << " with explanation: " << exp << std::endl; + Node mem = exp[0]; std::vector<Node> r1_element; std::vector<Node> r2_element; - NodeManager *nm = NodeManager::currentNM(); - Datatype dt = r1_rep.getType().getSetElementType().getDatatype(); - unsigned int i = 0; - unsigned int s1_len = r1_rep.getType().getSetElementType().getTupleLength(); - unsigned int tup_len = product_term.getType().getSetElementType().getTupleLength(); + Datatype dt = pt_rel[0].getType().getSetElementType().getDatatype(); + unsigned int s1_len = pt_rel[0].getType().getSetElementType().getTupleLength(); + unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength(); r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); + + unsigned int i = 0; for(; i < s1_len; ++i) { - r1_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i)); + r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); } - - dt = r2_rep.getType().getSetElementType().getDatatype(); + dt = pt_rel[1].getType().getSetElementType().getDatatype(); r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); for(; i < tup_len; ++i) { - r2_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i)); + r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); } + Node reason = exp; + Node mem1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_element); + Node mem2 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_element); + Node fact_1 = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, pt_rel[0]); + Node fact_2 = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, pt_rel[1]); - Node fact_1; - Node fact_2; - Node reason_1 = exp; - Node reason_2 = exp; - Node t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element); - Node t1_rep = getRepresentative(t1); - Node t2 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element); - Node t2_rep = getRepresentative(t2); - - fact_1 = NodeManager::currentNM()->mkNode(kind::MEMBER, t1, r1_rep ); - fact_2 = NodeManager::currentNM()->mkNode(kind::MEMBER, t2, r2_rep ); - if(r1_rep != product_term[0]) { - reason_1 = NodeManager::currentNM()->mkNode(kind::AND,reason_1, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r1_rep, product_term[0]))); - } - if(t1 != t1_rep) { - reason_1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND,reason_1, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t1_rep)))); - } - if(r2_rep != product_term[1]) { - reason_2 = NodeManager::currentNM()->mkNode(kind::AND,reason_2, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r2_rep, product_term[1]))); - } - if(t2 != t2_rep) { - reason_2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND,reason_2, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t2, t2_rep)))); - } - if(polarity) { - sendInfer(fact_1, reason_1, "product-split"); - sendInfer(fact_2, reason_2, "product-split"); - } else { - sendInfer(fact_1.negate(), reason_1, "product-split"); - sendInfer(fact_2.negate(), reason_2, "product-split"); + if( pt_rel != exp[1] ) { + reason = NodeManager::currentNM()->mkNode(kind::AND, exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL, pt_rel, exp[1]))); } + sendInfer( fact_1, reason, "product-split" ); + sendInfer( fact_2, reason, "product-split" ); } /* join-split rule: (a, b) IS_IN (X JOIN Y) @@ -415,86 +506,66 @@ int TheorySetsRels::EqcInfo::counter = 0; * ------------------------------------------------------------- * (a, c) IS_IN (X JOIN Y) */ - void TheorySetsRels::applyJoinRule(Node exp, Node join_term) { - Trace("rels-debug") << "\n[sets-rels] *********** Applying JOIN rule " << std::endl; - if(d_rel_nodes.find(join_term) == d_rel_nodes.end()) { - Trace("rels-debug") << "\n[sets-rels] Apply JOIN-COMPOSE rule on term: " << join_term + void TheorySetsRels::applyJoinRule( Node join_rel, Node join_rel_rep, Node exp ) { + Trace("rels-debug") << "\n[Theory::Rels] *********** Applying JOIN rule on joined term = " << join_rel + << ", its representative = " << join_rel_rep + << " with explanation = " << exp << std::endl; + if(d_rel_nodes.find( join_rel ) == d_rel_nodes.end()) { + Trace("rels-debug") << "\n[Theory::Rels] Apply JOIN-COMPOSE rule on term: " << join_rel << " with explanation: " << exp << std::endl; - computeMembersForRelofMultArities(join_term); - d_rel_nodes.insert(join_term); + computeMembersForBinOpRel( join_rel ); + d_rel_nodes.insert( join_rel ); } - bool polarity = exp.getKind() != kind::NOT; - Node atom = polarity ? exp : exp[0]; - Node r1_rep = getRepresentative(join_term[0]); - Node r2_rep = getRepresentative(join_term[1]); + Node mem = exp[0]; + std::vector<Node> r1_element; + std::vector<Node> r2_element; + Node r1_rep = getRepresentative(join_rel[0]); + Node r2_rep = getRepresentative(join_rel[1]); + TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0]; + Node shared_x = NodeManager::currentNM()->mkSkolem("srj_", shared_type); + Datatype dt = join_rel[0].getType().getSetElementType().getDatatype(); + unsigned int s1_len = join_rel[0].getType().getSetElementType().getTupleLength(); + unsigned int tup_len = join_rel.getType().getSetElementType().getTupleLength(); - if(polarity) { - Trace("rels-debug") << "\n[sets-rels] Apply JOIN-SPLIT rule on term: " << join_term - << " with explanation: " << exp << std::endl; - - std::vector<Node> r1_element; - std::vector<Node> r2_element; - NodeManager *nm = NodeManager::currentNM(); - TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0]; - Node shared_x = nm->mkSkolem("sde_", shared_type); - Datatype dt = r1_rep.getType().getSetElementType().getDatatype(); - unsigned int i = 0; - unsigned int s1_len = r1_rep.getType().getSetElementType().getTupleLength(); - unsigned int tup_len = join_term.getType().getSetElementType().getTupleLength(); - - r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); - for(; i < s1_len-1; ++i) { - r1_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i)); - } - r1_element.push_back(shared_x); - dt = r2_rep.getType().getSetElementType().getDatatype(); - r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); - r2_element.push_back(shared_x); - for(; i < tup_len; ++i) { - r2_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i)); - } - - Node t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element); - Node t2 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element); - - computeTupleReps(t1); - computeTupleReps(t2); - - std::vector<Node> elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[t1]); - - for(unsigned int j = 0; j < elements.size(); j++) { - std::vector<Node> new_tup; - new_tup.push_back(elements[j]); - new_tup.insert(new_tup.end(), d_tuple_reps[t2].begin()+1, d_tuple_reps[t2].end()); - if(d_membership_trie[r2_rep].existsTerm(new_tup) != Node::null()) { - return; - } - } + unsigned int i = 0; + r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); + for(; i < s1_len-1; ++i) { + r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); + } + r1_element.push_back(shared_x); + dt = join_rel[1].getType().getSetElementType().getDatatype(); + r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); + r2_element.push_back(shared_x); + for(; i < tup_len; ++i) { + r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); + } + Node mem1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_element); + Node mem2 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_element); - Node fact; - Node reason = atom[1] == join_term ? exp : NodeManager::currentNM()->mkNode(kind::AND,exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,atom[1], join_term))); - Node reasons = reason; + computeTupleReps(mem1); + computeTupleReps(mem2); - fact = NodeManager::currentNM()->mkNode(kind::MEMBER,t1, r1_rep); - if(r1_rep != join_term[0]) { - reasons = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r1_rep, join_term[0])))); - } - Trace("rels-debug") << "\n[sets-rels] After applying JOIN-split rule, generate a fact : " << fact - << " with explanation: " << reasons << std::endl; - sendInfer(fact, reasons, "join-split"); - reasons = reason; - fact = NodeManager::currentNM()->mkNode(kind::MEMBER,t2, r2_rep); - if(r2_rep != join_term[1]) { - reasons = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r2_rep, join_term[1])))); + std::vector<Node> elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[mem1]); + for(unsigned int j = 0; j < elements.size(); j++) { + std::vector<Node> new_tup; + new_tup.push_back(elements[j]); + new_tup.insert(new_tup.end(), d_tuple_reps[mem2].begin()+1, d_tuple_reps[mem2].end()); + if(d_membership_trie[r2_rep].existsTerm(new_tup) != Node::null()) { + return; } - Trace("rels-debug") << "[sets-rels] After applying JOIN-split rule, generate a fact : " << fact - << " with explanation: " << reasons << std::endl; - sendInfer(fact, reasons, "join-split"); - makeSharedTerm(shared_x); } + Node reason = exp; + if( join_rel != exp[1] ) { + reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, join_rel, exp[1])); + } + Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem1, join_rel[0]); + sendInfer( fact, reason, "JOIN-Split" ); + fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]); + sendInfer( fact, reason, "JOIN-Split" ); + makeSharedTerm( shared_x ); } /* @@ -511,171 +582,121 @@ int TheorySetsRels::EqcInfo::counter = 0; * ----------------------------------------------- * [NOT] (X = Y) */ - void TheorySetsRels::applyTransposeRule(Node exp, Node tp_term, Node more_reason, bool tp_occur) { - Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSPOSE rule on term " << tp_term << std::endl; - - bool polarity = exp.getKind() != kind::NOT; - Node atom = polarity ? exp : exp[0]; - Node reversedTuple = getRepresentative(RelsUtils::reverseTuple(atom[0])); - - if(tp_occur) { - Trace("rels-debug") << "\n[sets-rels] Apply TRANSPOSE-OCCUR rule on term: " << tp_term - << " with explanation: " << exp << std::endl; - - Node fact = polarity ? NodeManager::currentNM()->mkNode(kind::MEMBER,reversedTuple, tp_term) : NodeManager::currentNM()->mkNode(kind::MEMBER,reversedTuple, tp_term).negate(); - sendInfer(fact, more_reason == Node::null()?exp:NodeManager::currentNM()->mkNode(kind::AND,exp, more_reason), "transpose-occur"); + void TheorySetsRels::applyTransposeRule( std::vector<Node> tp_terms ) { + if( tp_terms.size() < 1) { return; } - - Node tp_t0_rep = getRepresentative(tp_term[0]); - Node reason = atom[1] == tp_term ? exp : Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND,exp, NodeManager::currentNM()->mkNode(kind::EQUAL,atom[1], tp_term))); - Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER,reversedTuple, tp_t0_rep); - - if(!polarity) { - fact = fact.negate(); + for( unsigned int i = 1; i < tp_terms.size(); i++ ) { + Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE-Equal rule on transposed term = " << tp_terms[0] << " and " << tp_terms[i] << std::endl; + sendInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, tp_terms[0][0], tp_terms[i][0]), NodeManager::currentNM()->mkNode(kind::EQUAL, tp_terms[0], tp_terms[i]), "TRANSPOSE-Equal"); } - sendInfer(fact, reason, "transpose-rule"); } + void TheorySetsRels::applyTransposeRule( Node tp_rel, Node tp_rel_rep, Node exp ) { + Trace("rels-debug") << "\n[Theory::Rels] *********** Applying TRANSPOSE rule on transposed term = " << tp_rel + << ", its representative = " << tp_rel_rep + << " with explanation = " << exp << std::endl; - void TheorySetsRels::finalizeTCInference() { - Trace("rels-tc") << "[sets-rels] ****** Finalizing transitive closure inferences!" << std::endl; - std::map<Node, Node>::iterator map_it = d_tc_rep_term.begin(); - - while( map_it != d_tc_rep_term.end() ) { - Trace("rels-tc") << "[sets-rels] Start building the TC graph for " << map_it->first << std::endl; + if(d_rel_nodes.find( tp_rel ) == d_rel_nodes.end()) { + Trace("rels-debug") << "\n[Theory::Rels] Apply TRANSPOSE-Compose rule on term: " << tp_rel + << " with explanation: " << exp << std::endl; - std::map< Node, std::hash_set<Node, NodeHashFunction> > d_tc_graph = constructTCGraph(getRepresentative(map_it->second[0]), map_it->first, map_it->second); - inferTC(map_it->first, d_tc_graph); - map_it++; + computeMembersForUnaryOpRel( tp_rel ); + d_rel_nodes.insert( tp_rel ); } - } - void TheorySetsRels::inferTC(Node tc_rep, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph) { - Trace("rels-tc") << "[sets-rels] Infer TC lemma from tc_graph of " << tc_rep << std::endl; + Node reason = exp; + Node reversed_mem = RelsUtils::reverseTuple( exp[0] ); - for(TC_PAIR_IT pair_set_it = tc_graph.begin(); pair_set_it != tc_graph.end(); pair_set_it++) { - for(std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); - set_it != pair_set_it->second.end(); set_it++) { - std::hash_set<Node, NodeHashFunction> elements; - Node pair = constructPair(tc_rep, pair_set_it->first, *set_it); - Node exp = findMemExp(tc_rep, pair); + if( tp_rel != exp[1] ) { + reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, tp_rel, exp[1])); + } + sendInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, reversed_mem, tp_rel[0]), reason, "TRANSPOSE-Reverse" ); + } - if(d_membership_tc_exp_cache.find(tc_rep) != d_membership_tc_exp_cache.end()) { - exp = NodeManager::currentNM()->mkNode(kind::AND,d_membership_tc_exp_cache[tc_rep], exp); - } - Assert(!exp.isNull()); - elements.insert(pair_set_it->first); - inferTC( exp, tc_rep, tc_graph, pair_set_it->first, *set_it, elements ); - } + void TheorySetsRels::doTCInference() { + Trace("rels-debug") << "[Theory::Rels] ****** Finalizing transitive closure inferences!" << std::endl; + TC_IT tc_graph_it = d_tcr_tcGraph.begin(); + while( tc_graph_it != d_tcr_tcGraph.end() ) { + Assert ( d_tcr_tcGraph_exps.find(tc_graph_it->first) != d_tcr_tcGraph_exps.end() ); + doTCInference( tc_graph_it->second, d_tcr_tcGraph_exps.find(tc_graph_it->first)->second, tc_graph_it->first ); + tc_graph_it++; } + Trace("rels-debug") << "[Theory::Rels] ****** Done with finalizing transitive closure inferences!" << std::endl; } - void TheorySetsRels::inferTC( Node exp, Node tc_rep, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, - Node start_node, Node cur_node, std::hash_set< Node, NodeHashFunction >& traversed ) { - Node pair = constructPair(tc_rep, start_node, cur_node); - MEM_IT mem_it = d_membership_db.find(tc_rep); - if(mem_it != d_membership_db.end()) { - if(std::find(mem_it->second.begin(), mem_it->second.end(), pair) == mem_it->second.end()) { - Trace("rels-tc") << "[sets-rels] Infered a TC lemma = " << NodeManager::currentNM()->mkNode(kind::MEMBER,pair, tc_rep) << " by Transitivity" - << " with explanation = " << Rewriter::rewrite(exp) << std::endl; - sendLemma( NodeManager::currentNM()->mkNode(kind::MEMBER,pair, tc_rep), Rewriter::rewrite(exp), "Transitivity" ); + // Bottom-up fashion to compute relations with more than 1 arity + void TheorySetsRels::computeMembersForBinOpRel(Node rel) { + Trace("rels-debug") << "\n[Theory::Rels] computeMembersForBinOpRel for relation " << rel << std::endl; + + switch(rel[0].getKind()) { + case kind::TRANSPOSE: + case kind::TCLOSURE: { + computeMembersForUnaryOpRel(rel[0]); + break; } - } else { - Trace("rels-tc") << "[sets-rels] Infered a TC lemma = " << NodeManager::currentNM()->mkNode(kind::MEMBER,pair, tc_rep) << " by Transitivity" - << " with explanation = " << Rewriter::rewrite(exp) << std::endl; - sendLemma( NodeManager::currentNM()->mkNode(kind::MEMBER,pair, tc_rep), Rewriter::rewrite(exp), "Transitivity" ); - } - // check if cur_node has been traversed or not - if(traversed.find(cur_node) != traversed.end()) { - return; + case kind::JOIN: + case kind::PRODUCT: { + computeMembersForBinOpRel(rel[0]); + break; + } + default: + break; } - traversed.insert(cur_node); - - Node reason = exp; - TC_PAIR_IT cur_set = tc_graph.find(cur_node); - - 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_rep, cur_node, *set_it ); - Assert(!reason.isNull()); - inferTC( NodeManager::currentNM()->mkNode(kind::AND, findMemExp(tc_rep, new_pair), reason ), tc_rep, tc_graph, start_node, *set_it, traversed ); + switch(rel[1].getKind()) { + case kind::TRANSPOSE: { + computeMembersForUnaryOpRel(rel[1]); + break; } + case kind::JOIN: + case kind::PRODUCT: { + computeMembersForBinOpRel(rel[1]); + break; + } + default: + break; } - } - - // Bottom-up fashion to compute relations with more than 1 arity - void TheorySetsRels::computeMembersForRelofMultArities(Node n) { - Trace("rels-debug") << "\n[sets-rels] computeJoinOrProductRelations for relation " << n << std::endl; - switch(n[0].getKind()) { - case kind::TRANSPOSE: - case kind::TCLOSURE: - computeMembersForUnaryRel(n[0]); - break; - case kind::JOIN: - case kind::PRODUCT: - computeMembersForRelofMultArities(n[0]); - break; - default: - break; - } - - switch(n[1].getKind()) { - case kind::TRANSPOSE: - computeMembersForUnaryRel(n[1]); - break; - case kind::JOIN: - case kind::PRODUCT: - computeMembersForRelofMultArities(n[1]); - break; - default: - break; - } - - if(d_membership_db.find(getRepresentative(n[0])) == d_membership_db.end() || - d_membership_db.find(getRepresentative(n[1])) == d_membership_db.end()) - return; - composeTupleMemForRel(n); + 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); } // Bottom-up fashion to compute unary relation - void TheorySetsRels::computeMembersForUnaryRel(Node n) { - switch(n[0].getKind()) { - case kind::TRANSPOSE: - case kind::TCLOSURE: - computeMembersForUnaryRel(n[0]); - break; - case kind::JOIN: - case kind::PRODUCT: - computeMembersForRelofMultArities(n[0]); - break; - default: - break; - } - - if(d_membership_db.find(getRepresentative(n[0])) == d_membership_db.end()) + void TheorySetsRels::computeMembersForUnaryOpRel(Node rel) { + Trace("rels-debug") << "\n[Theory::Rels] computeMembersForUnaryOpRel for relation " << rel << std::endl; + + switch(rel[0].getKind()) { + case kind::TRANSPOSE: + case kind::TCLOSURE: + computeMembersForUnaryOpRel(rel[0]); + break; + case kind::JOIN: + case kind::PRODUCT: + computeMembersForBinOpRel(rel[0]); + break; + default: + break; + } + + Node rel0_rep = getRepresentative(rel[0]); + if(d_rReps_memberReps_cache.find( rel0_rep ) == d_rReps_memberReps_cache.end()) return; - Node n_rep = getRepresentative(n); - Node n0_rep = getRepresentative(n[0]); - std::vector<Node> tuples = d_membership_db[n0_rep]; - std::vector<Node> exps = d_membership_exp_db[n0_rep]; - Assert(tuples.size() == exps.size()); - for(unsigned int i = 0; i < tuples.size(); i++) { - Node reason = exps[i][1] == n0_rep ? exps[i] : NodeManager::currentNM()->mkNode(kind::AND,exps[i], NodeManager::currentNM()->mkNode(kind::EQUAL,exps[i][1], n0_rep)); - if( n.getKind() == kind::TRANSPOSE) { - Node rev_tup = getRepresentative(RelsUtils::reverseTuple(tuples[i])); - Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER,rev_tup, n_rep); - - if(holds(fact)) { - Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds! Skip..." << std::endl; - } else { - sendInfer(fact, Rewriter::rewrite(reason), "transpose-rule"); - } - } else if( n.getKind() == kind::TCLOSURE ) { + std::vector<Node> members = d_rReps_memberReps_cache[rel0_rep]; + std::vector<Node> 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[0] != exps[i][1] ) { + reason = NodeManager::currentNM()->mkNode(kind::AND, reason, NodeManager::currentNM()->mkNode(kind::EQUAL, rel[0], exps[i][1])); + } + sendInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(exps[i][0]), rel), reason, "TRANSPOSE-reverse"); } } } @@ -685,258 +706,166 @@ int TheorySetsRels::EqcInfo::counter = 0; * e.g. If (a, b) in X and (b, c) in Y, (a, c) in (X JOIN Y) * */ - void TheorySetsRels::composeTupleMemForRel( Node n ) { - Node r1 = n[0]; - Node r2 = n[1]; - Node r1_rep = getRepresentative(r1); - Node r2_rep = getRepresentative(r2); - NodeManager* nm = NodeManager::currentNM(); - - Trace("rels-debug") << "[sets-rels] start composing tuples in relations " - << r1 << " and " << r2 << std::endl; - - if(d_membership_db.find(r1_rep) == d_membership_db.end() || - d_membership_db.find(r2_rep) == d_membership_db.end()) - return; - - std::vector<Node> new_tups; - std::vector<Node> new_exps; - std::vector<Node> r1_elements = d_membership_db[r1_rep]; - std::vector<Node> r2_elements = d_membership_db[r2_rep]; - std::vector<Node> r1_exps = d_membership_exp_db[r1_rep]; - std::vector<Node> r2_exps = d_membership_exp_db[r2_rep]; - - Node n_rep = getRepresentative(n); - unsigned int t1_len = r1_elements.front().getType().getTupleLength(); - unsigned int t2_len = r2_elements.front().getType().getTupleLength(); - - for(unsigned int i = 0; i < r1_elements.size(); i++) { - for(unsigned int j = 0; j < r2_elements.size(); j++) { - std::vector<Node> composed_tuple; - TypeNode tn = n.getType().getSetElementType(); - Node r1_rmost = RelsUtils::nthElementOfTuple(r1_elements[i], t1_len-1); - Node r2_lmost = RelsUtils::nthElementOfTuple(r2_elements[j], 0); - composed_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); - - if((areEqual(r1_rmost, r2_lmost) && n.getKind() == kind::JOIN) || - n.getKind() == kind::PRODUCT) { - bool isProduct = n.getKind() == kind::PRODUCT; + void TheorySetsRels::composeMembersForRels( Node rel ) { + Trace("rels-debug") << "[Theory::Rels] Start composing members for relation = " << rel << std::endl; + Node r1 = rel[0]; + Node r2 = rel[1]; + Node r1_rep = getRepresentative( r1 ); + Node r2_rep = getRepresentative( r2 ); + + if(d_rReps_memberReps_cache.find( r1_rep ) == d_rReps_memberReps_cache.end() || + d_rReps_memberReps_cache.find( r2_rep ) == d_rReps_memberReps_cache.end() ) { + return; + } + + std::vector<Node> r1_rep_exps = d_rReps_memberReps_exp_cache[r1_rep]; + std::vector<Node> 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(); + + for( unsigned int i = 0; i < r1_rep_exps.size(); i++ ) { + for( unsigned int j = 0; j < r2_rep_exps.size(); j++ ) { + std::vector<Node> 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( Node::fromExpr(tn.getDatatype()[0].getConstructor()) ); + + if( (areEqual(r1_rmost, r2_lmost) && rel.getKind() == kind::JOIN) || + rel.getKind() == kind::PRODUCT ) { + bool isProduct = rel.getKind() == kind::PRODUCT; unsigned int k = 0; unsigned int l = 1; - for(; k < t1_len - 1; ++k) { - composed_tuple.push_back(RelsUtils::nthElementOfTuple(r1_elements[i], k)); + for( ; k < r1_tuple_len - 1; ++k ) { + tuple_elements.push_back( RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) ); } if(isProduct) { - composed_tuple.push_back(RelsUtils::nthElementOfTuple(r1_elements[i], k)); - composed_tuple.push_back(RelsUtils::nthElementOfTuple(r2_elements[j], 0)); + tuple_elements.push_back( RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], k ) ); + tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 ) ); } - for(; l < t2_len; ++l) { - composed_tuple.push_back(RelsUtils::nthElementOfTuple(r2_elements[j], l)); + for( ; l < r2_tuple_len; ++l ) { + tuple_elements.push_back( RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], l ) ); } - Node composed_tuple_rep = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, composed_tuple)); - Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER,composed_tuple_rep, n_rep); - if(holds(fact)) { - Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds! Skip..." << std::endl; - } else { - std::vector<Node> reasons; - reasons.push_back(explain(r1_exps[i])); - reasons.push_back(explain(r2_exps[j])); - if(n != n_rep) { - reasons.push_back(explain(NodeManager::currentNM()->mkNode(kind::EQUAL, n_rep, n))); - } - if(r1_exps[i].getKind() == kind::MEMBER && r1_exps[i][0] != r1_elements[i]) { - reasons.push_back(explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r1_elements[i], r1_exps[i][0]))); - } - if(r2_exps[j].getKind() == kind::MEMBER && r2_exps[j][0] != r2_elements[j]) { - reasons.push_back(explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r2_elements[j], r2_exps[j][0]))); - } - if(r1_exps[i].getKind() == kind::MEMBER && r1_exps[i][1] != r1_rep) { - reasons.push_back(explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r1_exps[i][1], r1_rep))); - } - if(r2_exps[j].getKind() == kind::MEMBER && r2_exps[j][1] != r2_rep) { - reasons.push_back(explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r2_exps[j][1], r2_rep))); - } - - if(!isProduct) { - if(r1_rmost != r2_lmost) { - reasons.push_back(explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r1_rmost, r2_lmost))); - } - } - if(r1 != r1_rep) { - reasons.push_back(explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r1, r1_rep))); - } - if(r2 != r2_rep) { - reasons.push_back(explain(NodeManager::currentNM()->mkNode(kind::EQUAL,r2, r2_rep))); - } + Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); + Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, composed_tuple, rel); + std::vector<Node> reasons; + reasons.push_back( r1_rep_exps[i] ); + reasons.push_back( r2_rep_exps[j] ); - Node reason = Rewriter::rewrite(nm->mkNode(kind::AND, reasons)); - if(isProduct) { - sendInfer( fact, reason, "product-compose" ); - } else { - sendInfer( fact, reason, "join-compose" ); + if( r1 != r1_rep_exps[i][1] ) { + reasons.push_back( NodeManager::currentNM()->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]) ); + } + if( isProduct ) { + sendInfer( fact, NodeManager::currentNM()->mkNode(kind::AND, reasons), "PRODUCT-Compose" ); + } else { + if( r1_rmost != r2_lmost ) { + reasons.push_back( NodeManager::currentNM()->mkNode(kind::EQUAL, r1_rmost, r2_lmost) ); } - - Trace("rels-debug") << "[sets-rels] Compose tuples: " << r1_elements[i] - << " and " << r2_elements[j] - << "\n Produce a new fact: " << fact - << "\n Reason: " << reason<< std::endl; + sendInfer( fact, NodeManager::currentNM()->mkNode(kind::AND, reasons), "JOIN-Compose" ); } } } } - Trace("rels-debug") << "[sets-rels] Done with composing tuples !" << std::endl; + } void TheorySetsRels::doPendingLemmas() { + Trace("rels-debug") << "[Theory::Rels] **************** Start doPendingLemmas !" << std::endl; if( !(*d_conflict) ){ - if ( (!d_lemma_cache.empty() || !d_pending_facts.empty()) ) { - for( unsigned i=0; i < d_lemma_cache.size(); i++ ){ - Assert(d_lemma_cache[i].getKind() == kind::IMPLIES); - if(holds( d_lemma_cache[i][1] )) { - Trace("rels-lemma") << "[sets-rels-lemma-skip] Skip an already held lemma: " - << d_lemma_cache[i]<< std::endl; + if ( (!d_lemmas_out.empty() || !d_pending_facts.empty()) ) { + for( unsigned i=0; i < d_lemmas_out.size(); i++ ){ + Assert(d_lemmas_out[i].getKind() == kind::IMPLIES); + if(holds( d_lemmas_out[i][1] )) { + Trace("rels-lemma-skip") << "[sets-rels-lemma-skip] Skip an already held lemma: " + << d_lemmas_out[i]<< std::endl; continue; } + d_sets_theory.d_out->lemma( d_lemmas_out[i] ); Trace("rels-lemma") << "[sets-rels-lemma] Send out a lemma : " - << d_lemma_cache[i] << std::endl; - d_sets_theory.d_out->lemma( d_lemma_cache[i] ); + << d_lemmas_out[i] << std::endl; } - for( std::map<Node, Node>::iterator child_it = d_pending_facts.begin(); - child_it != d_pending_facts.end(); child_it++ ) { - if(holds(child_it->first)) { - Trace("rels-lemma") << "[sets-rels-fact-lemma-skip] Skip an already held fact,: " - << child_it->first << std::endl; + for( std::map<Node, Node>::iterator pending_it = d_pending_facts.begin(); + pending_it != d_pending_facts.end(); pending_it++ ) { + if( holds( pending_it->first ) ) { + Trace("rels-lemma-skip") << "[sets-rels-fact-lemma-skip] Skip an already held fact,: " + << pending_it->first << std::endl; continue; } - Trace("rels-lemma") << "[sets-rels-fact-lemma] Send out a fact as lemma : " - << child_it->first << " with reason " << child_it->second << std::endl; - d_sets_theory.d_out->lemma(NodeManager::currentNM()->mkNode(kind::IMPLIES, child_it->second, child_it->first)); + Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, pending_it->second, pending_it->first); + if( d_lemmas_produced.find( lemma ) == d_lemmas_produced.end() ) { + d_sets_theory.d_out->lemma(NodeManager::currentNM()->mkNode(kind::IMPLIES, pending_it->second, pending_it->first)); + Trace("rels-lemma") << "[sets-rels-fact-lemma] Send out a fact as lemma : " + << pending_it->first << " with reason " << pending_it->second << std::endl; + d_lemmas_produced.insert( lemma ); + } } } - doTCLemmas(); } - - d_arg_rep_tp_terms.clear(); - d_tc_membership_db.clear(); - d_rel_nodes.clear(); - d_pending_facts.clear(); - d_membership_constraints_cache.clear(); - d_tc_r_graph.clear(); - d_membership_tc_exp_cache.clear(); - d_membership_exp_cache.clear(); - d_membership_db.clear(); - d_membership_exp_db.clear(); + doTCLemmas(); + Trace("rels-debug") << "[Theory::Rels] **************** Done with doPendingLemmas !" << std::endl; + d_tuple_reps.clear(); +// d_id_node.clear(); +// d_node_id.clear(); + d_tuple_reps.clear(); + d_rReps_memberReps_exp_cache.clear(); d_terms_cache.clear(); - d_lemma_cache.clear(); + d_lemmas_out.clear(); d_membership_trie.clear(); - d_tuple_reps.clear(); - d_id_node.clear(); - d_node_id.clear(); - d_tc_rep_term.clear(); + d_rel_nodes.clear(); + d_pending_facts.clear(); + d_rReps_memberReps_cache.clear(); + d_rRep_tcGraph.clear(); + d_tcr_tcGraph_exps.clear(); + d_tcr_tcGraph.clear(); + d_tc_lemmas_last.clear(); } void TheorySetsRels::doTCLemmas() { - Trace("rels-debug") << "[sets-rels] Start processing TC lemmas .......... " << std::endl; - std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator mem_it = d_tc_membership_db.begin(); - - while(mem_it != d_tc_membership_db.end()) { - Node tc_rep = getRepresentative(mem_it->first); - Node tc_r_rep = getRepresentative(mem_it->first[0]); - std::hash_set< Node, NodeHashFunction >::iterator set_it = mem_it->second.begin(); - - while(set_it != mem_it->second.end()) { - std::hash_set<Node, NodeHashFunction> hasSeen; - bool isReachable = false; - Node fst = RelsUtils::nthElementOfTuple(*set_it, 0); - Node snd = RelsUtils::nthElementOfTuple(*set_it, 1); - Node fst_rep = getRepresentative(fst); - Node snd_rep = getRepresentative(snd); - TC_IT tc_graph_it = d_tc_r_graph.find(tc_rep); - - // the tc_graph of TC(r) is built based on the members of r and TC(r)???????? - isTCReachable(fst_rep, snd_rep, hasSeen, tc_graph_it->second, isReachable); - Trace("rels-tc") << "tuple = " << *set_it << " with rep = (" << fst_rep << ", " << snd_rep << ") " - << " isReachable? = " << isReachable << std::endl; - if((tc_graph_it != d_tc_r_graph.end() && !isReachable) || - (tc_graph_it == d_tc_r_graph.end())) { - Node reason = explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*set_it, mem_it->first)); - Node sk_1 = NodeManager::currentNM()->mkSkolem("sde", fst_rep.getType()); - Node sk_2 = NodeManager::currentNM()->mkSkolem("sde", snd_rep.getType()); - Node mem_of_r = NodeManager::currentNM()->mkNode(kind::MEMBER,RelsUtils::constructPair(tc_r_rep, fst_rep, snd_rep), tc_r_rep); - Node sk_eq = NodeManager::currentNM()->mkNode(kind::EQUAL,sk_1, sk_2); - - if(fst_rep != fst) { - reason = NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,fst_rep, fst))); - } - if(snd_rep != snd) { - reason = NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,snd_rep, snd))); - } - if(tc_r_rep != mem_it->first[0]) { - reason = NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_r_rep, mem_it->first[0]))); - } - if(tc_rep != mem_it->first) { - reason = NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_rep, mem_it->first))); + Trace("rels-debug") << "[Theory::Rels] **************** Start doTCLemmas !" << std::endl; + std::map< Node, std::vector< Node > >::iterator tc_lemma_it = d_tc_lemmas_last.begin(); + while( tc_lemma_it != d_tc_lemmas_last.end() ) { + if( !holds( tc_lemma_it->first[1] ) ) { + if( d_lemmas_produced.find( tc_lemma_it->first ) == d_lemmas_produced.end() ) { + d_sets_theory.d_out->lemma( tc_lemma_it->first ); + d_lemmas_produced.insert( tc_lemma_it->first ); + + for( unsigned int i = 0; i < (tc_lemma_it->second).size(); i++ ) { + if( (tc_lemma_it->second)[i] == d_falseNode ) { + d_sets_theory.d_out->requirePhase((tc_lemma_it->second)[i], true); + } } - - Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, - NodeManager::currentNM()->mkNode(kind::OR,mem_of_r, - (NodeManager::currentNM()->mkNode(kind::AND,NodeManager::currentNM()->mkNode(kind::MEMBER,RelsUtils::constructPair(tc_r_rep, fst_rep, sk_1), tc_r_rep), - (NodeManager::currentNM()->mkNode(kind::AND,NodeManager::currentNM()->mkNode(kind::MEMBER,RelsUtils::constructPair(tc_r_rep, sk_2, snd_rep), tc_r_rep), - (NodeManager::currentNM()->mkNode(kind::OR,sk_eq, NodeManager::currentNM()->mkNode(kind::MEMBER,RelsUtils::constructPair(tc_rep, sk_1, sk_2), tc_rep))))))))); - Trace("rels-lemma") << "[sets-rels-lemma] Send out a TC lemma : " - << tc_lemma << std::endl; - d_sets_theory.d_out->lemma(tc_lemma); - d_sets_theory.d_out->requirePhase(Rewriter::rewrite(mem_of_r), true); - d_sets_theory.d_out->requirePhase(Rewriter::rewrite(sk_eq), true); + Trace("rels-lemma") << "[Theory::Rels] **** Send out a TC lemma = " << tc_lemma_it->first << " by " << "TCLOSURE-Forward"<< std::endl; } - set_it++; } - mem_it++; + ++tc_lemma_it; } + Trace("rels-debug") << "[Theory::Rels] **************** Done with doTCLemmas !" << std::endl; } - void TheorySetsRels::isTCReachable(Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable) { - if(hasSeen.find(start) == hasSeen.end()) { - hasSeen.insert(start); - } - - TC_PAIR_IT pair_set_it = tc_graph.find(start); - - if(pair_set_it != tc_graph.end()) { - if(pair_set_it->second.find(dest) != pair_set_it->second.end()) { - isReachable = true; - return; - } else { - std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); - - while(set_it != pair_set_it->second.end()) { - // need to check if *set_it has been looked already - if(hasSeen.find(*set_it) == hasSeen.end()) { - isTCReachable(*set_it, dest, hasSeen, tc_graph, isReachable); - } - set_it++; - } + void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) { + if( !holds( conc ) ) { + Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); + if( d_lemmas_produced.find( lemma ) == d_lemmas_produced.end() ) { + d_lemmas_out.push_back( lemma ); + d_lemmas_produced.insert( lemma ); + Trace("rels-send-lemma") << "[Theory::Rels] **** Generate a lemma conclusion = " << conc << " with reason = " << ant << " by " << c << std::endl; } } } - void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) { - Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); - d_lemma_cache.push_back(lemma); - d_lemma.insert(lemma); - } - void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) { - d_pending_facts[fact] = exp; - d_infer.push_back( fact ); - d_infer_exp.push_back( exp ); - } - - void TheorySetsRels::assertMembership( Node fact, Node reason, bool polarity ) { - d_eqEngine->assertPredicate( fact, polarity, reason ); + if( !holds( fact ) ) { + d_pending_facts[fact] = exp; + } else { + Trace("rels-send-infer") << "[Theory::Rels] **** Generate an infered fact fact = " + << fact << " with reason = " << exp << " by "<< c + << ", but it holds already, thus skip it!" << std::endl; + } } Node TheorySetsRels::getRepresentative( Node t ) { @@ -1005,92 +934,6 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - inline Node TheorySetsRels::getReason(Node tc_rep, Node tc_term, Node tc_r_rep, Node tc_r) { - if(tc_term != tc_rep) { - Node reason = explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_term, tc_rep)); - if(tc_term[0] != tc_r_rep) { - return NodeManager::currentNM()->mkNode(kind::AND,reason, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_term[0], tc_r_rep))); - } - } - return Node::null(); - } - - // tuple might be a member of tc_rep; or it might be a member of rels or tc_terms such that - // tc_terms are transitive closure of rels and are modulo equal to tc_rep - Node TheorySetsRels::findMemExp(Node tc_rep, Node pair) { - Trace("rels-exp") << "TheorySetsRels::findMemExp ( tc_rep = " << tc_rep << ", pair = " << pair << ")" << std::endl; - Node fst = RelsUtils::nthElementOfTuple(pair, 0); - Node snd = RelsUtils::nthElementOfTuple(pair, 1); - std::vector<Node> tc_terms = d_terms_cache.find(tc_rep)->second[kind::TCLOSURE]; - - Assert(tc_terms.size() > 0); - for(unsigned int i = 0; i < tc_terms.size(); i++) { - Node tc_term = tc_terms[i]; - Node tc_r_rep = getRepresentative(tc_term[0]); - - Trace("rels-exp") << "TheorySetsRels::findMemExp ( r_rep = " << tc_r_rep << ", pair = " << pair << ")" << std::endl; - std::map< Node, std::vector< Node > >::iterator tc_r_mems = d_membership_db.find(tc_r_rep); - if(tc_r_mems != d_membership_db.end()) { - for(unsigned int i = 0; i < tc_r_mems->second.size(); i++) { - Node fst_mem = RelsUtils::nthElementOfTuple(tc_r_mems->second[i], 0); - Node snd_mem = RelsUtils::nthElementOfTuple(tc_r_mems->second[i], 1); - - if(areEqual(fst_mem, fst) && areEqual(snd_mem, snd)) { - Node exp = NodeManager::currentNM()->mkNode(kind::MEMBER,tc_r_mems->second[i], tc_r_mems->first); - - if(tc_r_rep != tc_term[0]) { - exp = explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_r_rep, tc_term[0])); - } - if(tc_rep != tc_term) { - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_rep, tc_term))); - } - if(tc_r_mems->second[i] != pair) { - if(fst_mem != fst) { - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,fst_mem, fst))); - } - if(snd_mem != snd) { - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,snd_mem, snd))); - } - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, NodeManager::currentNM()->mkNode(kind::EQUAL,tc_r_mems->second[i], pair)); - } - return Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND,exp, explain(d_membership_exp_db[tc_r_rep][i]))); - } - } - } - - Node tc_term_rep = getRepresentative(tc_terms[i]); - std::map< Node, std::vector< Node > >::iterator tc_t_mems = d_membership_db.find(tc_term_rep); - - if(tc_t_mems != d_membership_db.end()) { - for(unsigned int j = 0; j < tc_t_mems->second.size(); j++) { - Node fst_mem = RelsUtils::nthElementOfTuple(tc_t_mems->second[j], 0); - Node snd_mem = RelsUtils::nthElementOfTuple(tc_t_mems->second[j], 1); - - if(areEqual(fst_mem, fst) && areEqual(snd_mem, snd)) { - Node exp = NodeManager::currentNM()->mkNode(kind::MEMBER,tc_t_mems->second[j], tc_t_mems->first); - if(tc_rep != tc_terms[i]) { - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_rep, tc_terms[i]))); - } - if(tc_term_rep != tc_terms[i]) { - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,tc_term_rep, tc_terms[i]))); - } - if(tc_t_mems->second[j] != pair) { - if(fst_mem != fst) { - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,fst_mem, fst))); - } - if(snd_mem != snd) { - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,snd_mem, snd))); - } - exp = NodeManager::currentNM()->mkNode(kind::AND,exp, NodeManager::currentNM()->mkNode(kind::EQUAL,tc_t_mems->second[j], pair)); - } - return Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND,exp, explain(d_membership_exp_db[tc_term_rep][j]))); - } - } - } - } - return Node::null(); - } - void TheorySetsRels::addSharedTerm( TNode n ) { Trace("rels-debug") << "[sets-rels] Add a shared term: " << n << std::endl; d_sets_theory.addSharedTerm(n); @@ -1124,13 +967,6 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - inline void TheorySetsRels::addToMembershipDB(Node rel, Node member, Node reasons) { - addToMap(d_membership_db, rel, member); - addToMap(d_membership_exp_db, rel, reasons); - computeTupleReps(member); - d_membership_trie[rel].addTerm(member, d_tuple_reps[member]); - } - 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); @@ -1142,7 +978,7 @@ int TheorySetsRels::EqcInfo::counter = 0; */ void TheorySetsRels::reduceTupleVar(Node n) { if(d_symbolic_tuples.find(n) == d_symbolic_tuples.end()) { - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one " << " node = " << n << std::endl; + Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl; std::vector<Node> tuple_elements; tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor())); for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) { @@ -1170,9 +1006,7 @@ int TheorySetsRels::EqcInfo::counter = 0; d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)), d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)), d_pending_merge(c), - d_infer(c), - d_infer_exp(c), - d_lemma(u), + d_lemmas_produced(u), d_shared_terms(u) { d_eqEngine->addFunctionKind(kind::PRODUCT); @@ -1276,19 +1110,9 @@ int TheorySetsRels::EqcInfo::counter = 0; } TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) : - d_mem(c), d_not_mem(c), d_mem_exp(c), d_in(c), d_out(c), + d_mem(c), d_mem_exp(c), d_in(c), d_out(c), d_tp(c), d_pt(c), d_join(c), d_tc(c) {} - void TheorySetsRels::eqNotifyNewClass( Node n ) { - Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl; - if(isRel(n) && (n.getKind() == kind::TRANSPOSE || - n.getKind() == kind::PRODUCT || - n.getKind() == kind::JOIN || - n.getKind() == kind::TCLOSURE)) { - getOrMakeEqcInfo( n, true ); - } - } - // Create an integer id for tuple element int TheorySetsRels::getOrMakeElementRepId(EqcInfo* ei, Node e_rep) { Trace("rels-std") << "[sets-rels] getOrMakeElementRepId:" << " e_rep = " << e_rep << std::endl; @@ -1384,12 +1208,21 @@ int TheorySetsRels::EqcInfo::counter = 0; return (*ei->d_mem_exp.find(pair)).second; } NodeMap::iterator mem_exp_it = ei->d_mem_exp.begin(); + while(mem_exp_it != ei->d_mem_exp.end()) { Node tuple = (*mem_exp_it).first; Node fst_e = RelsUtils::nthElementOfTuple(tuple, 0); Node snd_e = RelsUtils::nthElementOfTuple(tuple, 1); + Node reason = (*mem_exp_it).second; + if(areEqual(fst, fst_e) && areEqual(snd, snd_e)) { - return NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,snd, snd_e)), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,fst, fst_e)), (*mem_exp_it).second)); + if( fst != fst_e) { + reason = NodeManager::currentNM()->mkNode(kind::AND, reason, explain( NodeManager::currentNM()->mkNode(kind::EQUAL, fst, fst_e)) ); + } + if( snd != snd_e) { + reason = NodeManager::currentNM()->mkNode(kind::AND, reason, explain( NodeManager::currentNM()->mkNode(kind::EQUAL, snd, snd_e)) ); + } + return reason; } ++mem_exp_it; } @@ -1403,13 +1236,21 @@ int TheorySetsRels::EqcInfo::counter = 0; Node tuple = (*rel_mem_exp_it).first; Node fst_e = RelsUtils::nthElementOfTuple(tuple, 0); Node snd_e = RelsUtils::nthElementOfTuple(tuple, 1); + if(areEqual(fst, fst_e) && areEqual(snd, snd_e)) { - return NodeManager::currentNM()->mkNode(kind::AND,exp, NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,snd, snd_e)), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,fst, fst_e)), (*rel_mem_exp_it).second))); + if( fst != fst_e) { + exp = NodeManager::currentNM()->mkNode(kind::AND, exp, explain( NodeManager::currentNM()->mkNode(kind::EQUAL, fst, fst_e)) ); + } + if( snd != snd_e) { + exp = NodeManager::currentNM()->mkNode(kind::AND, exp, explain( NodeManager::currentNM()->mkNode(kind::EQUAL, snd, snd_e)) ); + } + return NodeManager::currentNM()->mkNode(kind::AND, exp, (*rel_mem_exp_it).second); } ++rel_mem_exp_it; } } } + Trace("rels-tc") << "End explainTCMem ############ pair = " << pair << std::endl; return Node::null(); } @@ -1418,10 +1259,9 @@ int TheorySetsRels::EqcInfo::counter = 0; Node exp = explainTCMem(tc_ei, mem_rep, fst_rep, snd_rep); Assert(!exp.isNull()); - Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER,mem_rep, tc_ei->d_tc.get())); - d_pending_merge.push_back(tc_lemma); - d_lemma.insert(tc_lemma); + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, mem_rep, tc_ei->d_tc.get()), exp, "TC-Infer"); std::hash_set<int>::iterator in_reachable_it = in_reachable.begin(); + while(in_reachable_it != in_reachable.end()) { Node in_node = d_id_node[*in_reachable_it]; Node in_pair = RelsUtils::constructPair(tc_ei->d_tc.get(), in_node, fst_rep); @@ -1431,10 +1271,7 @@ int TheorySetsRels::EqcInfo::counter = 0; tc_ei->d_mem_exp[new_pair] = reason; tc_ei->d_mem.insert(new_pair); - Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, NodeManager::currentNM()->mkNode(kind::MEMBER,new_pair, tc_ei->d_tc.get())); - - d_pending_merge.push_back(tc_lemma); - d_lemma.insert(tc_lemma); + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, new_pair, tc_ei->d_tc.get()), reason, "TC-Infer"); in_reachable_it++; } @@ -1457,9 +1294,7 @@ int TheorySetsRels::EqcInfo::counter = 0; reason = NodeManager::currentNM()->mkNode(kind::AND,reason, in_pair_exp); tc_ei->d_mem_exp[new_pair] = reason; tc_ei->d_mem.insert(new_pair); - Node tc_lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, reason, NodeManager::currentNM()->mkNode(kind::MEMBER,new_pair, tc_ei->d_tc.get())); - d_pending_merge.push_back(tc_lemma); - d_lemma.insert(tc_lemma); + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, new_pair, tc_ei->d_tc.get()), reason, "TC-Infer"); in_reachable_it++; } out_reachable_it++; @@ -1484,6 +1319,16 @@ int TheorySetsRels::EqcInfo::counter = 0; } } + void TheorySetsRels::eqNotifyNewClass( Node n ) { + Trace("rels-std") << "[sets-rels] eqNotifyNewClass:" << " t = " << n << std::endl; + if(isRel(n) && (n.getKind() == kind::TRANSPOSE || + n.getKind() == kind::PRODUCT || + n.getKind() == kind::JOIN || + n.getKind() == kind::TCLOSURE)) { + getOrMakeEqcInfo( n, true ); + } + } + // Merge t2 into t1, t1 will be the rep of the new eqc void TheorySetsRels::eqNotifyPostMerge( Node t1, Node t2 ) { Trace("rels-std") << "[sets-rels] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; @@ -1499,8 +1344,6 @@ int TheorySetsRels::EqcInfo::counter = 0; if( polarity ) { ei->d_mem.insert(t2[0]); ei->d_mem_exp[t2[0]] = explain(t2); - } else { - ei->d_not_mem.insert(t2[0]); } // Process a membership constraint that a tuple is a member of transpose of rel if( !ei->d_tp.get().isNull() ) { @@ -1540,12 +1383,6 @@ int TheorySetsRels::EqcInfo::counter = 0; EqcInfo* t2_ei = getOrMakeEqcInfo(t2); if(t1_ei != NULL && t2_ei != NULL) { - NodeSet::const_iterator non_mem_it = t2_ei->d_not_mem.begin(); - - while(non_mem_it != t2_ei->d_not_mem.end()) { - t1_ei->d_not_mem.insert(*non_mem_it); - non_mem_it++; - } if(!t1_ei->d_tc.get().isNull()) { NodeSet::const_iterator mem_it = t2_ei->d_mem.begin(); @@ -1595,11 +1432,6 @@ int TheorySetsRels::EqcInfo::counter = 0; sendInferProduct( true, *itr, t1_ei->d_pt.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1_ei->d_pt.get(), t2)), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t2))) ); } } - for(NodeSet::key_iterator itr = t2_ei->d_not_mem.key_begin(); itr != t2_ei->d_not_mem.key_end(); itr++) { - if(!t1_ei->d_not_mem.contains(*itr)) { - sendInferProduct( false, *itr, t1_ei->d_pt.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1_ei->d_pt.get(), t2)), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t2).negate())) ); - } - } } else if(!t2_ei->d_pt.get().isNull()) { t1_ei->d_pt.set(t2_ei->d_pt); for(NodeSet::key_iterator itr = t1_ei->d_mem.key_begin(); itr != t1_ei->d_mem.key_end(); itr++) { @@ -1607,11 +1439,6 @@ int TheorySetsRels::EqcInfo::counter = 0; sendInferProduct( true, *itr, t2_ei->d_pt.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2_ei->d_pt.get())), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t1))) ); } } - for(NodeSet::key_iterator itr = t1_ei->d_not_mem.key_begin(); itr != t1_ei->d_not_mem.key_end(); itr++) { - if(!t2_ei->d_not_mem.contains(*itr)) { - sendInferProduct( false, *itr, t2_ei->d_pt.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2_ei->d_pt.get())), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t1).negate())) ); - } - } } // t1 was created already and t2 was not } else if(t1_ei != NULL) { @@ -1626,9 +1453,6 @@ int TheorySetsRels::EqcInfo::counter = 0; t1_ei->d_mem.insert(*itr); t1_ei->d_mem_exp.insert(*itr, t2_ei->d_mem_exp[*itr]); } - for(NodeSet::key_iterator itr = t2_ei->d_not_mem.key_begin(); itr != t2_ei->d_not_mem.key_end(); itr++) { - t1_ei->d_not_mem.insert(*itr); - } } } } @@ -1648,25 +1472,15 @@ int TheorySetsRels::EqcInfo::counter = 0; if( !t1_ei->d_tp.get().isNull() ) { for( NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++ ) { if( !t1_ei->d_mem.contains( *itr ) ) { - sendInferTranspose( true, *itr, t1_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1_ei->d_tp.get(), t2)), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t2))) ); + sendInferTranspose( true, *itr, t1_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::AND, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1_ei->d_tp.get(), t2)), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t2))) ); } } - for( NodeSet::key_iterator itr = t2_ei->d_not_mem.key_begin(); itr != t2_ei->d_not_mem.key_end(); itr++ ) { - if(!t1_ei->d_not_mem.contains(*itr)) { - sendInferTranspose( false, *itr, t1_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1_ei->d_tp.get(), t2)), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t2).negate())) ); - } - } - // Apply transpose rule on (non)members of t1 and t2->tp + // Apply transpose rule on members of t1 and t2->tp } else if( !t2_ei->d_tp.get().isNull() ) { t1_ei->d_tp.set( t2_ei->d_tp ); for( NodeSet::key_iterator itr = t1_ei->d_mem.key_begin(); itr != t1_ei->d_mem.key_end(); itr++ ) { if( !t2_ei->d_mem.contains(*itr) ) { - sendInferTranspose( true, *itr, t2_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::AND,explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2_ei->d_tp.get())), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t1))) ); - } - } - for( NodeSet::key_iterator itr = t1_ei->d_not_mem.key_begin(); itr != t1_ei->d_not_mem.key_end(); itr++ ) { - if( !t2_ei->d_not_mem.contains(*itr) ) { - sendInferTranspose( false, *itr, t2_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::AND, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2_ei->d_tp.get())), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t1).negate()) ) ); + sendInferTranspose( true, *itr, t2_ei->d_tp.get(), NodeManager::currentNM()->mkNode(kind::AND, explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2_ei->d_tp.get())), explain(NodeManager::currentNM()->mkNode(kind::MEMBER,*itr, t1))) ); } } } @@ -1683,116 +1497,82 @@ int TheorySetsRels::EqcInfo::counter = 0; t1_ei->d_mem.insert( *itr ); t1_ei->d_mem_exp.insert( *itr, t2_ei->d_mem_exp[*itr] ); } - for( NodeSet::key_iterator itr = t2_ei->d_not_mem.key_begin(); itr != t2_ei->d_not_mem.key_end(); itr++ ) { - t1_ei->d_not_mem.insert( *itr ); - } } } } void TheorySetsRels::doPendingMerge() { for( NodeList::const_iterator itr = d_pending_merge.begin(); itr != d_pending_merge.end(); itr++ ) { - Trace("rels-std") << "[sets-rels-lemma] Process pending merge fact : " - << *itr << std::endl; - d_sets_theory.d_out->lemma( *itr ); + if( !holds(*itr) ) { + if( d_lemmas_produced.find(*itr)==d_lemmas_produced.end() ) { + Trace("rels-lemma") << "[std-sets-rels-lemma] Send out a merge fact as lemma: " + << *itr << std::endl; + d_sets_theory.d_out->lemma( *itr ); + d_lemmas_produced.insert(*itr); + } + } } } void TheorySetsRels::sendInferTranspose( bool polarity, Node t1, Node t2, Node exp, bool reverseOnly ) { Assert( t2.getKind() == kind::TRANSPOSE ); + if( !polarity ) { + return; + } if( polarity && isRel(t1) && isRel(t2) ) { Assert(t1.getKind() == kind::TRANSPOSE); - Node n = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::EQUAL,t1[0], t2[0]) ); - Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying transpose rule: " - << n << std::endl; - d_pending_merge.push_back( n ); - d_lemma.insert( n ); + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::EQUAL, t1[0], t2[0]), exp, "Transpose-Equal"); return; } - Node n1; if( reverseOnly ) { - if( polarity ) { - n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER,RelsUtils::reverseTuple(t1), t2[0]) ); - } else { - n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER,RelsUtils::reverseTuple(t1), t2[0]).negate() ); - } + sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(t1), t2[0]), exp, "Transpose-Rule" ); } else { - Node n2; - if(polarity) { - n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER,t1, t2) ); - n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER,RelsUtils::reverseTuple(t1), t2[0]) ); - } else { - n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER,t1, t2).negate() ); - n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER,RelsUtils::reverseTuple(t1), t2[0]).negate() ); - } - Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying transpose rule: " - << n2 << std::endl; - d_pending_merge.push_back(n2); - d_lemma.insert(n2); + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, t1, t2), exp, "Transpose-Rule"); + sendMergeInfer(NodeManager::currentNM()->mkNode(kind::MEMBER, RelsUtils::reverseTuple(t1), t2[0]), exp, "Transpose-Rule"); } - Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying transpose rule: " - << n1 << std::endl; - d_pending_merge.push_back(n1); - d_lemma.insert(n1); + } + void TheorySetsRels::sendMergeInfer( Node fact, Node reason, const char * c ) { + if( !holds( fact ) ) { + Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, reason, fact); + d_pending_merge.push_back(lemma); + Trace("std-rels") << "[std-rels-lemma] Generate a lemma by applying " << c + << ": " << lemma << std::endl; + } } - void TheorySetsRels::sendInferProduct( bool polarity, Node t1, Node t2, Node exp ) { - Assert( t2.getKind() == kind::PRODUCT ); - if( polarity && isRel(t1) && isRel(t2) ) { - //PRODUCT(x) = PRODUCT(y) => x = y; - Assert( t1.getKind() == kind::PRODUCT ); - Node n = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::EQUAL,t1[0], t2[0]) ); - Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying product rule: " - << n << std::endl; - d_pending_merge.push_back( n ); - d_lemma.insert( n ); + void TheorySetsRels::sendInferProduct( bool polarity, Node member, Node pt_rel, Node exp ) { + Assert( pt_rel.getKind() == kind::PRODUCT ); + + if(!polarity) { return; } std::vector<Node> r1_element; std::vector<Node> r2_element; - Node r1 = t2[0]; - Node r2 = t2[1]; - NodeManager *nm = NodeManager::currentNM(); + Node r1 = pt_rel[0]; + Node r2 = pt_rel[1]; Datatype dt = r1.getType().getSetElementType().getDatatype(); unsigned int i = 0; unsigned int s1_len = r1.getType().getSetElementType().getTupleLength(); - unsigned int tup_len = t2.getType().getSetElementType().getTupleLength(); + unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength(); r1_element.push_back(Node::fromExpr(dt[0].getConstructor())); for( ; i < s1_len; ++i ) { - r1_element.push_back( RelsUtils::nthElementOfTuple( t1, i ) ); + r1_element.push_back( RelsUtils::nthElementOfTuple( member, i ) ); } dt = r2.getType().getSetElementType().getDatatype(); r2_element.push_back( Node::fromExpr( dt[0].getConstructor() ) ); for( ; i < tup_len; ++i ) { - r2_element.push_back( RelsUtils::nthElementOfTuple(t1, i) ); + r2_element.push_back( RelsUtils::nthElementOfTuple(member, i) ); } - Node n1; - Node n2; - Node tuple_1 = getRepresentative( nm->mkNode( kind::APPLY_CONSTRUCTOR, r1_element ) ); - Node tuple_2 = getRepresentative( nm->mkNode( kind::APPLY_CONSTRUCTOR, r2_element ) ); - - if( polarity ) { - n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_1, r1 ) ); - n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_2, r2 ) ); - } else { - n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_1, r1 ).negate() ); - n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_2, r2 ).negate() ); - } - Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying product-split rule: " - << n1 << std::endl; - d_pending_merge.push_back( n1 ); - d_lemma.insert( n1 ); - Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying product-split rule: " - << n2 << std::endl; - d_pending_merge.push_back( n2 ); - d_lemma.insert( n2 ); - + Node tuple_1 = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, r1_element ); + Node tuple_2 = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, r2_element ); + sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_1, r1), exp, "Product-Split" ); + sendMergeInfer( NodeManager::currentNM()->mkNode(kind::MEMBER, tuple_2, r2), exp, "Product-Split" ); } TheorySetsRels::EqcInfo* TheorySetsRels::getOrMakeEqcInfo( Node n, bool doMake ){ diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index e5c0ad10c..b5c839a66 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -80,7 +80,6 @@ private: ~EqcInfo(){} static int counter; NodeSet d_mem; - NodeSet d_not_mem; NodeMap d_mem_exp; NodeListMap d_in; NodeListMap d_out; @@ -126,14 +125,11 @@ private: /** Facts and lemmas to be sent to EE */ std::map< Node, Node > d_pending_facts; - std::map< Node, Node > d_pending_split_facts; - std::vector< Node > d_lemma_cache; + std::vector< Node > d_lemmas_out; NodeList d_pending_merge; /** inferences: maintained to ensure ref count for internally introduced nodes */ - NodeList d_infer; - NodeList d_infer_exp; - NodeSet d_lemma; + NodeSet d_lemmas_produced; NodeSet d_shared_terms; /** Relations that have been applied JOIN, PRODUCT, TC composition rules */ @@ -144,11 +140,14 @@ 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)members representatives */ - std::map< Node, std::vector<Node> > d_membership_constraints_cache; + /** Mapping between relation and its (non)member representatives */ + std::map< Node, std::vector<Node> > d_rReps_memberReps_cache; + std::map< Node, std::vector<Node> > d_rReps_nonMemberReps_cache; - /** Mapping between relation and its (non)members' explanation */ - std::map< Node, std::vector<Node> > d_membership_exp_cache; + + /** Mapping between relation and its (non)member representatives explanation */ + std::map< Node, std::vector<Node> > d_rReps_memberReps_exp_cache; + std::map< Node, std::vector<Node> > d_rReps_nonMemberReps_exp_cache; /** Mapping between relation and its member representatives */ std::map< Node, std::vector<Node> > d_membership_db; @@ -170,9 +169,12 @@ private: /** 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<Node, NodeHashFunction> > > d_tc_r_graph; + std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_rRep_tcGraph; + std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > 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, Node > d_tc_rep_term; std::map< Node, EqcInfo* > d_eqc_info; public: @@ -201,30 +203,31 @@ private: void check(); Node explain(Node); void collectRelsInfo(); - void applyTCRule( Node, Node ); - void applyJoinRule( Node, Node ); - void applyProductRule( Node, Node ); - void composeTupleMemForRel( Node ); - void assertMembership( Node fact, Node reason, bool polarity ); - void applyTransposeRule( Node, Node, Node more_reason = Node::null(), bool tp_occur_rule = false ); - - + void applyTransposeRule( std::vector<Node> tp_terms ); + 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 applyTCRule( Node mem, Node rel, Node rel_rep, Node exp); + void buildTCGraphForRel( Node tc_rel ); + void doTCInference(); + void doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); + void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, + std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ); + + void composeMembersForRels( Node ); + void computeMembersForBinOpRel( Node ); + void computeMembersForUnaryOpRel( Node ); + + bool isTCReachable( Node mem_rep, Node tc_rel ); + void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, + std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); - void computeMembersForRelofMultArities( Node ); - void computeMembersForUnaryRel( Node ); - void finalizeTCInference(); - void inferTC( Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >& ); - void inferTC( Node, Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >&, - Node, Node, std::hash_set< Node, NodeHashFunction >&); - void isTCReachable(Node fst, Node snd, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool&); - std::map< Node, std::hash_set< Node, NodeHashFunction > > constructTCGraph( Node, Node, Node ); - - void doTCLemmas(); void addSharedTerm( TNode n ); void sendInfer( Node fact, Node exp, const char * c ); void sendLemma( Node fact, Node reason, const char * c ); + void sendMergeInfer( Node fact, Node reason, const char * c ); + void doTCLemmas(); // Helper functions bool holds( Node ); @@ -235,7 +238,6 @@ private: void computeTupleReps( Node ); bool areEqual( Node a, Node b ); Node getRepresentative( Node t ); - Node findMemExp(Node r, Node pair); bool insertIntoIdList(IdList&, int); bool exists( std::vector<Node>&, Node ); Node mkAnd( std::vector< TNode >& assumptions ); @@ -244,7 +246,6 @@ private: inline Node constructPair(Node tc_rep, Node a, Node b); void addToMap( std::map< Node, std::vector<Node> >&, Node, Node ); bool safelyAddToMap( std::map< Node, std::vector<Node> >&, Node, Node ); - inline Node getReason(Node tc_rep, Node tc_term, Node tc_r_rep, Node tc_r); bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();} |