Home
last modified time | relevance | path

Searched refs:d_eqc_info (Results 1 – 12 of 12) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/sets/
H A Dtheory_sets_rels.h89 bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); } in hasEqcInfo()
129 std::map< Node, EqcInfo* > d_eqc_info; variable
H A Dtheory_sets_rels.cpp1229 for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); in ~TheorySetsRels()
1647 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo()
1648 if( eqc_i == d_eqc_info.end() ){ in getOrMakeEqcInfo()
1651 if( eqc_i!=d_eqc_info.end() ){ in getOrMakeEqcInfo()
1655 d_eqc_info[n] = ei; in getOrMakeEqcInfo()
H A Dtheory_sets_private.h106 std::map< Node, EqcInfo* > d_eqc_info; variable
H A Dtheory_sets_private.cpp77 for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) { in ~TheorySetsPrivate()
202 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo()
203 if( eqc_i==d_eqc_info.end() ){ in getOrMakeEqcInfo()
207 d_eqc_info[n] = ei; in getOrMakeEqcInfo()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dconjecture_generator.cpp106 for (std::map<Node, EqcInfo*>::iterator i = d_eqc_info.begin(), in ~ConjectureGenerator()
107 iend = d_eqc_info.end(); in ~ConjectureGenerator()
126 std::map< Node, EqcInfo* >::iterator it1 = d_eqc_info.find( t1 ); in eqNotifyPreMerge()
127 if( it1!=d_eqc_info.end() && !it1->second->d_rep.get().isNull() ){ in eqNotifyPreMerge()
130 std::map< Node, EqcInfo* >::iterator it2 = d_eqc_info.find( t2 ); in eqNotifyPreMerge()
131 if( it2!=d_eqc_info.end() && !it2->second->d_rep.get().isNull() ){ in eqNotifyPreMerge()
142 if( it1==d_eqc_info.end() ){ in eqNotifyPreMerge()
167 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo()
168 if( eqc_i!=d_eqc_info.end() ){ in getOrMakeEqcInfo()
172 d_eqc_info[n] = ei; in getOrMakeEqcInfo()
H A Dconjecture_generator.h299 std::map< Node, EqcInfo* > d_eqc_info; variable
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Dtheory_datatypes.cpp80 for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); in ~TheoryDatatypes()
99 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo()
101 if( eqc_i != d_eqc_info.end() ){ in getOrMakeEqcInfo()
105 d_eqc_info[n] = ei; in getOrMakeEqcInfo()
119 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); in getOrMakeEqcInfo()
H A Dtheory_datatypes.h156 std::map< Node, EqcInfo* > d_eqc_info; variable
/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.h271 std::map< Node, HeapAssertInfo * > d_eqc_info; variable
H A Dtheory_sep.cpp62 …for( std::map< Node, HeapAssertInfo * >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end();… in ~TheorySep()
843 std::map< Node, HeapAssertInfo* >::iterator e_i = d_eqc_info.find( n ); in getOrMakeEqcInfo()
844 if( e_i==d_eqc_info.end() ){ in getOrMakeEqcInfo()
847 d_eqc_info[n] = ei; in getOrMakeEqcInfo()
/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dtheory_strings.h417 std::map< Node, EqcInfo* > d_eqc_info; variable
H A Dtheory_strings.cpp171 for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){ in ~TheoryStrings()
1089 std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc ); in getOrMakeEqcInfo()
1090 if( eqc_i==d_eqc_info.end() ){ in getOrMakeEqcInfo()
1093 d_eqc_info[eqc] = ei; in getOrMakeEqcInfo()