Home
last modified time | relevance | path

Searched refs:HeapAssertInfo (Results 1 – 2 of 2) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.h264 class HeapAssertInfo {
266 HeapAssertInfo( context::Context* c );
267 ~HeapAssertInfo(){} in ~HeapAssertInfo()
271 std::map< Node, HeapAssertInfo * > d_eqc_info;
272 HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
303 void validatePto( HeapAssertInfo * ei, Node ei_n );
304 void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
H A Dtheory_sep.cpp62 …for( std::map< Node, HeapAssertInfo * >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end();… in ~TheorySep()
501 HeapAssertInfo * ei = getOrMakeEqcInfo( r, true ); in check()
838 TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context* c ) : d_pto(c), d_has_neg_pto(c,false)… in HeapAssertInfo() function in CVC4::theory::sep::TheorySep::HeapAssertInfo
842 TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) { in getOrMakeEqcInfo()
843 std::map< Node, HeapAssertInfo* >::iterator e_i = d_eqc_info.find( n ); in getOrMakeEqcInfo()
846 HeapAssertInfo* ei = new HeapAssertInfo( getSatContext() ); in getOrMakeEqcInfo()
1583 HeapAssertInfo * e2 = getOrMakeEqcInfo( t2, false ); in eqNotifyPostMerge()
1585 HeapAssertInfo * e1 = getOrMakeEqcInfo( t1, true ); in eqNotifyPostMerge()
1600 void TheorySep::validatePto( HeapAssertInfo * ei, Node ei_n ) { in validatePto()
1621 void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ) { in addPto()