From: Paul Meng Date: Tue, 11 Oct 2016 18:43:28 +0000 (-0500) Subject: - fixed a memory leak issue with context dependent data structure X-Git-Tag: cvc5-1.0.0~6029 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=773e7d27d606b71ff0f78e84efe1deef2653f016;p=cvc5.git - fixed a memory leak issue with context dependent data structure - clean up --- diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 5b75c7810..d8230d31b 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -1188,23 +1188,14 @@ int TheorySetsRels::EqcInfo::counter = 0; Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one " << " node = " << n << std::endl; std::vector tuple_elements; tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor())); - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 0" << std::endl; for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) { - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 1" << std::endl; Node element = RelsUtils::nthElementOfTuple(n[0], i); - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 2" << std::endl; makeSharedTerm(element); - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 3" << std::endl; tuple_elements.push_back(element); - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 4" << std::endl; } - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 5" << std::endl; Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 6" << std::endl; tuple_reduct = MEMBER(tuple_reduct, n[1]); - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 7" << std::endl; Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, tuple_reduct); - Trace("rels-debug") << "Reduce tuple var: " << n[0] << " to concrete one ****** 8" << std::endl; sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); d_symbolic_tuples.insert(n); } @@ -1215,6 +1206,7 @@ int TheorySetsRels::EqcInfo::counter = 0; eq::EqualityEngine* eq, context::CDO* conflict, TheorySets& d_set ): + d_vec_size(c), d_eqEngine(eq), d_conflict(conflict), d_sets_theory(d_set), @@ -1320,8 +1312,8 @@ int TheorySetsRels::EqcInfo::counter = 0; } TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) : - d_mem(c), d_not_mem(c), d_in(c), d_out(c), d_mem_exp(c), - d_id_in(c), d_id_out(c), d_tp(c), d_pt(c), d_join(c),d_tc(c) {} + d_mem(c), d_not_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; @@ -1333,17 +1325,17 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - // Create a integer id for tuple element + // 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; - std::map::iterator nid_it = d_node_id.find(e_rep); + std::map< Node, int >::iterator nid_it = d_node_id.find(e_rep); if( nid_it == d_node_id.end() ) { - if(d_eqEngine->hasTerm(e_rep)) { - // it is possible that e's rep changes at this moment, thus we need to know the eqc of e's previous rep + if( d_eqEngine->hasTerm(e_rep) ) { + // it is possible that e's rep changes at this moment, thus we need to know the previous rep id of eqc of e eq::EqClassIterator rep_eqc_i = eq::EqClassIterator( e_rep, d_eqEngine ); - while(!rep_eqc_i.isFinished()) { - std::map::iterator id_it = d_node_id.find(*rep_eqc_i); + while( !rep_eqc_i.isFinished() ) { + std::map< Node, int >::iterator id_it = d_node_id.find(*rep_eqc_i); if( id_it != d_node_id.end() ) { d_id_node[id_it->second] = e_rep; @@ -1374,11 +1366,9 @@ int TheorySetsRels::EqcInfo::counter = 0; return true; } - void TheorySetsRels::addTCMemAndSendInfer(EqcInfo* tc_ei, Node membership, Node exp, bool fromRel) { + void TheorySetsRels::addTCMemAndSendInfer( EqcInfo* tc_ei, Node membership, Node exp, bool fromRel ) { Trace("rels-std") << "[sets-rels] addTCMemAndSendInfer:" << " membership = " << membership << " from a relation? " << fromRel<< std::endl; - IdList* in_lst; - IdList* out_lst; Node fst = RelsUtils::nthElementOfTuple(membership[0], 0); Node snd = RelsUtils::nthElementOfTuple(membership[0], 1); Node fst_rep = getRepresentative(fst); @@ -1389,28 +1379,18 @@ int TheorySetsRels::EqcInfo::counter = 0; return; } - int fst_rep_id = getOrMakeElementRepId(tc_ei, fst_rep); - int snd_rep_id = getOrMakeElementRepId(tc_ei, snd_rep); - IdListMap::iterator tc_in_mem_it = tc_ei->d_id_in.find(snd_rep_id); - - if(tc_in_mem_it == tc_ei->d_id_in.end()) { - in_lst = new(d_sets_theory.getSatContext()->getCMM()) IdList( true, d_sets_theory.getSatContext(), false, - context::ContextMemoryAllocator(d_sets_theory.getSatContext()->getCMM()) ); - tc_ei->d_id_in.insertDataFromContextMemory(snd_rep_id, in_lst); - Trace("rels-std") << "Create in cache for " << snd_rep << std::endl; - } else { - in_lst = (*tc_in_mem_it).second; - } + int fst_rep_id = getOrMakeElementRepId( tc_ei, fst_rep ); + int snd_rep_id = getOrMakeElementRepId( tc_ei, snd_rep ); std::hash_set in_reachable; std::hash_set out_reachable; - collectInReachableNodes(tc_ei, fst_rep_id, in_reachable); - collectOutReachableNodes(tc_ei, snd_rep_id, out_reachable); + collectReachableNodes(tc_ei->d_id_inIds, fst_rep_id, in_reachable); + collectReachableNodes(tc_ei->d_id_outIds, snd_rep_id, out_reachable); // If fst_rep is inserted into in_lst successfully, // save rep pair's exp and send out TC inference lemmas. // Otherwise, mem's rep is already in the TC and return. - if(insertIntoIdList(*in_lst, fst_rep_id)) { + if( addId(tc_ei->d_id_inIds, snd_rep_id, fst_rep_id) ) { Node reason = exp == Node::null() ? explain(membership) : exp; if(!fromRel && tc_ei->d_tc.get() != membership[1]) { reason = AND(reason, explain(EQUAL(tc_ei->d_tc.get(), membership[1]))); @@ -1429,18 +1409,8 @@ int TheorySetsRels::EqcInfo::counter = 0; // Nothing inserted into the eqc return; } - - IdListMap::iterator tc_out_mem_it = tc_ei->d_id_out.find(fst_rep_id); - if(tc_out_mem_it == tc_ei->d_id_out.end()) { - out_lst = new(d_sets_theory.getSatContext()->getCMM()) IdList( true, d_sets_theory.getSatContext(), false, - context::ContextMemoryAllocator(d_sets_theory.getSatContext()->getCMM()) ); - tc_ei->d_id_out.insertDataFromContextMemory(fst_rep_id, out_lst); - Trace("rels-std") << "Create out arrow cache for " << snd_rep << std::endl; - } else { - out_lst = (*tc_out_mem_it).second; - } - insertIntoIdList(*out_lst, snd_rep_id); Trace("rels-std") << "Add out membership arrow for " << fst_rep << " to : " << snd_rep << std::endl; + addId(tc_ei->d_id_inIds, fst_rep_id, snd_rep_id); sendTCInference(tc_ei, in_reachable, out_reachable, mem_rep, fst_rep, snd_rep, fst_rep_id, snd_rep_id); } @@ -1532,41 +1502,21 @@ int TheorySetsRels::EqcInfo::counter = 0; } } - void TheorySetsRels::collectInReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set& in_reachable, bool firstRound) { - Trace("rels-std") << "**** Start collecting in-reachable nodes for node with id " << start_id << std::endl; - if(in_reachable.find(start_id) != in_reachable.end()) { + void TheorySetsRels::collectReachableNodes(std::map< int, std::vector< int > >& id_map, int start_id, std::hash_set< int >& reachable_set, bool firstRound) { + Trace("rels-std") << "**** Collecting reachable nodes for node with id " << start_id << std::endl; + if(reachable_set.find(start_id) != reachable_set.end()) { return; } if(!firstRound) { - in_reachable.insert(start_id); + reachable_set.insert(start_id); } - IdListMap::const_iterator id_list_map_it = tc_ei->d_id_in.find(start_id); - if(id_list_map_it != tc_ei->d_id_in.end()) { - IdList::const_iterator id_list_it = (*id_list_map_it).second->begin(); - while(id_list_it != (*id_list_map_it).second->end()) { - collectInReachableNodes(tc_ei, *id_list_it, in_reachable, false); - id_list_it++; - } - } - } + std::vector< int > id_list = getIdList(id_map, start_id); + std::vector< int >::iterator id_list_it = id_list.begin(); - void TheorySetsRels::collectOutReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set& out_reachable, bool firstRound) { - Trace("rels-std") << "**** Start collecting out-reachable nodes for node with id " << start_id << std::endl; - if(out_reachable.find(start_id) != out_reachable.end()) { - return; - } - if(!firstRound) { - out_reachable.insert(start_id); - } - IdListMap::const_iterator id_list_map_it = tc_ei->d_id_out.find(start_id); - - if(id_list_map_it != tc_ei->d_id_out.end()) { - IdList::const_iterator id_list_it = (*id_list_map_it).second->begin(); - while(id_list_it != (*id_list_map_it).second->end()) { - collectOutReachableNodes(tc_ei, *id_list_it, out_reachable, false); - id_list_it++; - } + while( id_list_it != id_list.end() ) { + collectReachableNodes( id_map, *id_list_it, reachable_set, false ); + id_list_it++; } } @@ -1575,21 +1525,21 @@ int TheorySetsRels::EqcInfo::counter = 0; Trace("rels-std") << "[sets-rels] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl; // Merge membership constraint with "true" or "false" eqc - if((t1 == d_trueNode || t1 == d_falseNode) && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple()) { + if( (t1 == d_trueNode || t1 == d_falseNode) && t2.getKind() == kind::MEMBER && t2[0].getType().isTuple() ) { Assert(t1 == d_trueNode || t1 == d_falseNode); bool polarity = t1 == d_trueNode; Node t2_1rep = getRepresentative(t2[1]); EqcInfo* ei = getOrMakeEqcInfo( t2_1rep, true ); - if(polarity) { + 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()) { + if( !ei->d_tp.get().isNull() ) { Node exp = polarity ? explain(t2) : explain(t2.negate()); if(ei->d_tp.get() != t2[1]) { exp = AND( explain(EQUAL( ei->d_tp.get(), t2[1]) ), exp ); @@ -1597,33 +1547,20 @@ int TheorySetsRels::EqcInfo::counter = 0; sendInferTranspose( polarity, t2[0], ei->d_tp.get(), exp, true ); } // Process a membership constraint that a tuple is a member of product of rel - if(!ei->d_pt.get().isNull()) { + if( !ei->d_pt.get().isNull() ) { Node exp = polarity ? explain(t2) : explain(t2.negate()); if(ei->d_pt.get() != t2[1]) { exp = AND( explain(EQUAL( ei->d_pt.get(), t2[1]) ), exp ); } - sendInferProduct(polarity, t2[0], ei->d_pt.get(), exp); + sendInferProduct( polarity, t2[0], ei->d_pt.get(), exp ); } // Process a membership constraint that a tuple is a member of transitive closure of rel if( polarity && !ei->d_tc.get().isNull() ) { - addTCMemAndSendInfer(ei, t2, Node::null()); -// Node rel_rep = getRepresentative(ei->d_tc.get()[0]); -// EqcInfo* rel_ei = getOrMakeEqcInfo(rel_rep); -// if(rel_ei != NULL) { -// NodeSet::const_iterator mem = rel_ei->d_mem.begin(); -// while(mem != rel_ei->d_mem.end()) { -// if(!ei->d_mem.contains(*mem)) { -// addTCMemAndSendInfer(ei, MEMBER(*mem, rel_rep), rel_ei->d_mem_exp[*mem], true); -// } -// mem++; -// } -// } + addTCMemAndSendInfer( ei, t2, Node::null() ); } // Merge two relation eqcs - } else if(t1.getType().isSet() && - t2.getType().isSet() && - t1.getType().getSetElementType().isTuple()) { + } else if( t1.getType().isSet() && t2.getType().isSet() && t1.getType().getSetElementType().isTuple() ) { mergeTransposeEqcs(t1, t2); mergeProductEqcs(t1, t2); mergeTCEqcs(t1, t2); @@ -1657,10 +1594,9 @@ int TheorySetsRels::EqcInfo::counter = 0; NodeSet::const_iterator t1_mem_it = t1_ei->d_mem.begin(); while(t1_mem_it != t1_ei->d_mem.end()) { - Node membership = MEMBER(*t1_mem_it, t1_ei->d_tc.get()); NodeMap::const_iterator reason_it = t1_ei->d_mem_exp.find(*t1_mem_it); Assert(reason_it != t1_ei->d_mem_exp.end()); - addTCMemAndSendInfer(t1_ei, membership, (*reason_it).second); + addTCMemAndSendInfer(t1_ei, MEMBER(*t1_mem_it, t1_ei->d_tc.get()), (*reason_it).second); t1_mem_it++; } @@ -1967,6 +1903,35 @@ int TheorySetsRels::EqcInfo::counter = 0; } } + bool TheorySetsRels::addId( std::map< int, std::vector< int > >& id_map, int key, int id ) { + int n_data = d_vec_size[key]; + int len = n_data < id_map[key].size() ? n_data : id_map[key].size(); + + for( int i = 0; i < len; i++ ) { + if( id_map[key][i] == id) { + return false; + } + } + if( n_data < id_map[key].size() ) { + id_map[key][n_data] = id; + } else { + id_map[key].push_back( id ); + } + d_vec_size[key] = n_data+1; + return true; + } + + std::vector< int > TheorySetsRels::getIdList( std::map< int, std::vector< int > >& id_map, int key ) { + std::vector< int > id_list; + int n_data = d_vec_size[key]; + int len = n_data < id_map[key].size() ? n_data : id_map[key].size(); + + for( int i = 0; i < len; i++ ) { + id_list.push_back(id_map[key][i]); + } + return id_list; + } + } } } diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 7877cdde5..83f9bf5d4 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -44,14 +44,14 @@ public: class TheorySetsRels { - typedef context::CDChunkList NodeList; - typedef context::CDChunkList IdList; - typedef context::CDHashMap IdListMap; - typedef context::CDHashSet NodeSet; - typedef context::CDHashMap NodeBoolMap; - typedef context::CDHashMap NodeListMap; - typedef context::CDHashMap NodeSetMap; - typedef context::CDHashMap NodeMap; + typedef context::CDChunkList< Node > NodeList; + typedef context::CDChunkList< int > IdList; + typedef context::CDHashMap< int, IdList* > IdListMap; + typedef context::CDHashSet< Node, NodeHashFunction > NodeSet; + typedef context::CDHashMap< Node, bool, NodeHashFunction > NodeBoolMap; + typedef context::CDHashMap< Node, NodeList*, NodeHashFunction > NodeListMap; + typedef context::CDHashMap< Node, NodeSet*, NodeHashFunction > NodeSetMap; + typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; public: TheorySetsRels(context::Context* c, @@ -81,27 +81,39 @@ private: static int counter; NodeSet d_mem; NodeSet d_not_mem; + NodeMap d_mem_exp; NodeListMap d_in; NodeListMap d_out; - NodeMap d_mem_exp; - IdListMap d_id_in; // mapping from a element rep id to a list of rep ids that pointed by - IdListMap d_id_out; // mapping from a element rep id to a list of rep ids that point to context::CDO< Node > d_tp; context::CDO< Node > d_pt; context::CDO< Node > d_join; context::CDO< Node > d_tc; + /** mapping from an element rep id to a list of rep ids that pointed by */ + /** Context dependent map Int -> IntList */ + std::map< int, std::vector< int > > d_id_inIds; + /** mapping from an element rep id to a list of rep ids that point to */ + /** Context dependent map Int -> IntList */ + std::map< int, std::vector< int > > d_id_outIds; }; private: + /** Context */ + context::CDHashMap< int, int > d_vec_size; + /** Mapping between integer id and tuple element rep */ - std::map d_id_node; + std::map< int, Node > d_id_node; /** Mapping between tuple element rep and integer id*/ - std::map d_node_id; + std::map< Node, int > d_node_id; /** has eqc info */ bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); } + bool addId( std::map< int, std::vector< int > >& id_map, int key, int id ); + std::vector< int > getIdList( std::map< int, std::vector< int > >& id_map, int key ); + + void collectReachableNodes(std::map< int, std::vector< int > >& id_map, int start_id, std::hash_set& reachable_set, bool firstRound=true); + private: eq::EqualityEngine *d_eqEngine; @@ -182,8 +194,6 @@ private: EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); void sendInferTranspose(bool, Node, Node, Node, bool reverseOnly = false); void addTCMemAndSendInfer(EqcInfo* tc_ei, Node mem, Node exp, bool fromRel = false); - void collectInReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set& in_reachable, bool firstRound = true); - void collectOutReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set& out_reachable, bool firstRound = true); void sendTCInference(EqcInfo* tc_ei, std::hash_set in_reachable, std::hash_set out_reachable, Node mem_rep, Node fst_rep, Node snd_rep, int id1, int id2);