Searched refs:d_type_references_all (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.cpp | 520 …ypeNode, std::vector< Node > >::iterator itt = d_type_references_all.begin(); itt != d_type_refere… in check()
570 …if( std::find( d_type_references_all[vtn].begin(), d_type_references_all[vtn].end(), s_atom[0] )!=… in check()
1139 …d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), … in getBaseLabel()
1154 for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){ in getBaseLabel()
1155 … Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, e, d_type_references_all[tn][j] ); in getBaseLabel()
1158 d_type_references_all[tn].push_back( e ); in getBaseLabel()
1163 …d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begi… in getBaseLabel()
1169 d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] ); in getBaseLabel()
1531 Assert( d_type_references_all.find( tn )!=d_type_references_all.end() ); in computeLabelModel()
1532 Assert( !d_type_references_all[tn].empty() ); in computeLabelModel()
[all …]
|
| H A D | theory_sep.h | 252 std::map< TypeNode, std::vector< Node > > d_type_references_all; variable
|