diff options
| author | PaulMeng <pmtruth@hotmail.com> | 2016-06-25 18:25:59 -0400 |
|---|---|---|
| committer | PaulMeng <pmtruth@hotmail.com> | 2016-06-25 18:25:59 -0400 |
| commit | 3b34ffd99881072d6139e4f7652f12e31d4b5d2c (patch) | |
| tree | af383adb6fd29b7da408e8ac18ccd5e76212ab12 /src/theory | |
| parent | be76c2bab92d75de742abb5367fc38c8605cd61d (diff) | |
debug statement
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index e339740a3..386e9f563 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -43,6 +43,8 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator int TheorySetsRels::EqcInfo::counter = 0; + + // do a test void TheorySetsRels::check(Theory::Effort level) { Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver *******************************\n" << std::endl; if(Theory::fullEffort(level)) { @@ -1553,20 +1555,24 @@ int TheorySetsRels::EqcInfo::counter = 0; Trace("rels-std") << "[sets-rels] Merge TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; EqcInfo* t1_ei = getOrMakeEqcInfo(t1); EqcInfo* t2_ei = getOrMakeEqcInfo(t2); - + Trace("rels-std") << "[sets-rels] 0 debugging merging TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; if(t1_ei != NULL && t2_ei != NULL) { + Trace("rels-std") << "[sets-rels] 1 debugging merging TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; 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()) { + Trace("rels-std") << "[sets-rels] 2 debugging merging TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; NodeSet::const_iterator mem_it = t2_ei->d_mem.begin(); while(mem_it != t2_ei->d_mem.end()) { addTCMemAndSendInfer(t1_ei, MEMBER(*mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*mem_it)).second); mem_it++; } + Trace("rels-std") << "[sets-rels] 3 debugging merging TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; } else if(!t2_ei->d_tc.get().isNull()) { + Trace("rels-std") << "[sets-rels] 4 debugging merging TC eqcs t1 = " << t1 << " and t2 = " << t2 << std::endl; t1_ei->d_tc.set(t2_ei->d_tc); NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin(); while(t1_mem_it != t1_ei->d_mem.end()) { |