From: Tim King Date: Wed, 23 Mar 2016 04:09:55 +0000 (-0700) Subject: Garbage collecting the EqcInfo s in TheoryDatatypes::d_eqc_info. X-Git-Tag: cvc5-1.0.0~6049^2~97 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c91733f4b458cb888d915baa309b2ba29488fa10;p=cvc5.git Garbage collecting the EqcInfo s in TheoryDatatypes::d_eqc_info. --- diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 26ca50897..8123fe39c 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -75,6 +75,12 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, } TheoryDatatypes::~TheoryDatatypes() { + for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); + i != iend; ++i){ + EqcInfo* current = (*i).second; + Assert(current != NULL); + delete current; + } } void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -91,7 +97,7 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); EqcInfo* ei; - if( eqc_i!=d_eqc_info.end() ){ + if( eqc_i != d_eqc_info.end() ){ ei = eqc_i->second; }else{ ei = new EqcInfo( getSatContext() ); @@ -901,10 +907,11 @@ void TheoryDatatypes::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ } -TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c ) : -d_inst( c, false ), d_constructor( c, Node::null() ), d_selectors( c, false ){ - -} +TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c ) + : d_inst( c, false ) + , d_constructor( c, Node::null() ) + , d_selectors( c, false ) +{} bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){ return ( eqc && !eqc->d_constructor.get().isNull() ) || !getLabel( n ).isNull(); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 0f110b369..0a038f0ed 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -133,8 +133,8 @@ private: void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons ); void getSelectorsForCons( Node r, std::map< int, bool >& sels ); /** mkExpDefSkolem */ - void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ); - /** skolems for terms */ + void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ); + /** skolems for terms */ NodeMap d_term_sk; Node getTermSkolemFor( Node n ); private: