Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.cpp226 Assert( d_loc_to_data_type.find( it->first )!=d_loc_to_data_type.end() ); in postProcessModel()
228 TypeNode data_type = d_loc_to_data_type[it->first]; in postProcessModel()
277 TypeEnumerator te_range( d_loc_to_data_type[it->first] ); in postProcessModel()
761 TypeNode data_type = d_loc_to_data_type[it->first]; in check()
884 d_loc_to_data_type[d_type_ref] = d_type_data; in ppNotifyAssertions()
1031 if( itt==d_loc_to_data_type.end() ){ in registerRefDataTypes()
1032 if( !d_loc_to_data_type.empty() ){ in registerRefDataTypes()
1033 TypeNode te1 = d_loc_to_data_type.begin()->first; in registerRefDataTypes()
1044 d_loc_to_data_type[tn1] = tn2; in registerRefDataTypes()
1055 d_loc_to_data_type[tn1] = tn2; in registerRefDataTypes()
[all …]
H A Dtheory_sep.h233 std::map< TypeNode, TypeNode > d_loc_to_data_type; variable