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;
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() ) {
// 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++;
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();
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();
}
/*
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);
}
}
}
} 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);
}
}
// 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 );
}
}
}
}
++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;
- }
-
/*
*
*
* -----------------------------------------------------------
* 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 );
+ }
}
}
* ----------------------------------
* 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)
* -------------------------------------------------------------
* (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 );
}
/*
* -----------------------------------------------
* [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");
}
}
}
* 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 ) {
}
}
- 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);
}
}
- 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);
*/
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++) {
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);
}
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;
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;
}
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();
}
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);
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++;
}
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++;
}
}
+ 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;
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() ) {
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();
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++) {
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) {
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);
- }
}
}
}
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))) );
}
}
}
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 ){
projects / cvc5.git / commitdiff