diff options
| author | PaulMeng <baolmeng@gmail.com> | 2016-03-01 14:36:36 -0600 |
|---|---|---|
| committer | PaulMeng <baolmeng@gmail.com> | 2016-03-01 14:36:36 -0600 |
| commit | 31ab3e21f285b0b6a3a8de7ab352c0c6276b6695 (patch) | |
| tree | ecdcf72d0661235779e849dd707d1e444c93e018 | |
| parent | 08e68bd440dae2893d58c39875e3f2bf776b0354 (diff) | |
small fixes for eq rep names
| -rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 8 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rels.h | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 384432f04..6ea13aa67 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -41,7 +41,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; void TheorySetsRels::check(Theory::Effort level) { Trace("rels-debug") << "[sets-rels] Start the relational solver..." << std::endl; - collectRelationalInfo(); + collectRelsInfo(); check(); doPendingSplitFacts(); doPendingLemmas(); @@ -97,7 +97,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; * Polulate the relational terms data structure */ - void TheorySetsRels::collectRelationalInfo() { + void TheorySetsRels::collectRelsInfo() { Trace("rels-debug") << "[sets-rels] Start collecting relational terms..." << std::endl; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine ); while( !eqcs_i.isFinished() ){ @@ -447,6 +447,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; std::vector<Node> r2_exps = d_membership_exp_cache[r2_rep]; Node new_rel = n.getKind() == kind::JOIN ? NodeManager::currentNM()->mkNode(kind::JOIN, r1_rep, r2_rep) : NodeManager::currentNM()->mkNode(kind::PRODUCT, r1_rep, r2_rep); + Node new_rel_rep = getRepresentative(new_rel); unsigned int t1_len = 1; unsigned int t2_len = 1; if(r1_elements.front().getType().isTuple()) @@ -489,7 +490,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; fact = composedTuple[0]; } new_tups.push_back(fact); - fact = MEMBER(fact, new_rel); + fact = MEMBER(fact, new_rel_rep); std::vector<Node> reasons; reasons.push_back(r1_exps[i]); reasons.push_back(r2_exps[j]); @@ -518,7 +519,6 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it; } } - Node new_rel_rep = getRepresentative( new_rel ); if(d_membership_cache.find( new_rel_rep ) != d_membership_cache.end()) { std::vector<Node> tups = d_membership_cache[new_rel_rep]; std::vector<Node> exps = d_membership_exp_cache[new_rel_rep]; diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index dbb48ffcd..a63a0c253 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -69,7 +69,7 @@ private: context::CDO<bool> *d_conflict; void check(); - void collectRelationalInfo(); + void collectRelsInfo(); void assertMembership( Node fact, Node reason, bool polarity ); void composeTuplesForRels( Node ); void applyTransposeRule( Node, Node, Node ); |