Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dtheory_uf_strong_solver.h69 class DiseqList {
71 DiseqList( context::Context* c ) in DiseqList() function
73 ~DiseqList(){} in ~DiseqList()
120 DiseqList* get(unsigned i) { return d_disequalities[i]; } in get()
123 DiseqList d_internal;
124 DiseqList d_external;
126 DiseqList* d_disequalities[2];
H A Dtheory_uf_strong_solver.cpp42 typedef RegionNodeInfo::DiseqList DiseqList; typedef
75 DiseqList* del = rni->get(t); in takeNode()
76 for(DiseqList::iterator it = del->begin(); it != del->end(); ++it ){ in takeNode()
112 RegionNodeInfo::DiseqList* del = rni->get(t); in combine()
113 for( RegionNodeInfo::DiseqList::iterator it2 = del->begin(), in combine()
136 DiseqList* del = d_nodes[b]->get(t); in setEqual()
208 RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->get(type); in isDisequal()
386 DiseqList* del = rni->get(0); in getNumExternalDisequalities()
405 DiseqList* del = rni->get(i); in debugPrint()
794 DiseqList* del = d_regions[ni]->getRegionInfo(n)->get(0); in getNumDisequalitiesToRegion()
[all …]