diff options
| -rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 59 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rels.h | 4 |
2 files changed, 32 insertions, 31 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 19f22e0cf..a29394d53 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -192,10 +192,11 @@ int TheorySetsRels::EqcInfo::counter = 0; * Construct transitive closure graph for tc_rep based on the members of tc_r_rep */ - void TheorySetsRels::constructTCGraph(Node tc_r_rep, Node tc_rep, Node tc_term) { + 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()) { @@ -204,19 +205,29 @@ int TheorySetsRels::EqcInfo::counter = 0; 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() ) { @@ -237,12 +248,7 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - 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_graph[tc_rep] = tc_graph; + return tc_graph; } /* @@ -542,8 +548,8 @@ int TheorySetsRels::EqcInfo::counter = 0; while( map_it != d_tc_rep_term.end() ) { Trace("rels-tc") << "[sets-rels] Start building the TC graph for " << map_it->first << std::endl; - constructTCGraph(getRepresentative(map_it->second[0]), map_it->first, map_it->second); - inferTC(map_it->first, d_tc_graph[map_it->first]); + 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++; } } @@ -799,7 +805,7 @@ int TheorySetsRels::EqcInfo::counter = 0; d_rel_nodes.clear(); d_pending_facts.clear(); d_membership_constraints_cache.clear(); - d_tc_graph.clear(); + d_tc_r_graph.clear(); d_membership_tc_exp_cache.clear(); d_membership_exp_cache.clear(); d_membership_db.clear(); @@ -820,14 +826,6 @@ int TheorySetsRels::EqcInfo::counter = 0; while(mem_it != d_tc_membership_db.end()) { Node tc_rep = getRepresentative(mem_it->first); Node tc_r_rep = getRepresentative(mem_it->first[0]); - -// // build the TC graph for tc_rep if it was not created before -// if( d_rel_nodes.find(tc_rep) == d_rel_nodes.end() ) { -// Trace("rels-debug") << "[sets-rels] Start building the TC graph for relation " << mem_it->first << std::endl; -// constructTCGraph(tc_r_rep, tc_rep, mem_it->first); -// d_rel_nodes.insert(tc_rep); -// } - std::hash_set< Node, NodeHashFunction >::iterator set_it = mem_it->second.begin(); while(set_it != mem_it->second.end()) { @@ -836,12 +834,15 @@ int TheorySetsRels::EqcInfo::counter = 0; Node fst = RelsUtils::nthElementOfTuple(*set_it, 0); Node snd = RelsUtils::nthElementOfTuple(*set_it, 1); Node fst_rep = getRepresentative(fst); - Node snd_rep = getRepresentative(RelsUtils::nthElementOfTuple(*set_it, 1)); - TC_IT tc_graph_it = d_tc_graph.find(tc_rep); + 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); - if((tc_graph_it != d_tc_graph.end() && !isReachable) || - (tc_graph_it == d_tc_graph.end())) { +// 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(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()); @@ -866,7 +867,7 @@ int TheorySetsRels::EqcInfo::counter = 0; (AND(MEMBER(RelsUtils::constructPair(tc_r_rep, fst_rep, sk_1), tc_r_rep), (AND(MEMBER(RelsUtils::constructPair(tc_r_rep, sk_2, snd_rep), tc_r_rep), (OR(sk_eq, MEMBER(RelsUtils::constructPair(tc_rep, sk_1, sk_2), tc_rep))))))))); - Trace("rels-tc-lemma") << "[sets-rels-lemma] Send out a TC lemma : " + 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); @@ -1154,11 +1155,11 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - TheorySetsRels::TheorySetsRels(context::Context* c, - context::UserContext* u, - eq::EqualityEngine* eq, - context::CDO<bool>* conflict, - TheorySets& d_set): + TheorySetsRels::TheorySetsRels( context::Context* c, + context::UserContext* u, + eq::EqualityEngine* eq, + context::CDO<bool>* conflict, + TheorySets& d_set ): d_eqEngine(eq), d_conflict(conflict), d_sets_theory(d_set), @@ -1240,7 +1241,7 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - Node TheorySetsRels::explain(Node literal) + Node TheorySetsRels::explain( Node literal ) { Trace("rels-exp") << "[sets-rels] TheorySetsRels::explain(" << literal << ")"<< std::endl; std::vector<TNode> assumptions; diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 36cb61a94..9f47978f5 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -154,7 +154,7 @@ private: std::map< Node, std::hash_set<Node, NodeHashFunction> > d_tc_membership_db; /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ - std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tc_graph; + std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tc_r_graph; /** Mapping between transitive closure TC(r)'s representative and TC(r) */ std::map< Node, Node > d_tc_rep_term; @@ -192,7 +192,7 @@ private: void applyJoinRule( Node, Node ); void applyProductRule( Node, Node ); void applyTCRule( Node, Node ); - void constructTCGraph( Node, Node, Node ); + std::map< Node, std::hash_set< Node, NodeHashFunction > > constructTCGraph( Node, Node, Node ); void computeTuplesInRel( Node ); void computeTpRel( Node ); void finalizeTCInference(); |