Home
last modified time | relevance | path

Searched refs:d_splits (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dtheory_uf_strong_solver.h138 NodeBoolMap d_splits; variable
162 split_iterator begin_splits() { return d_splits.begin(); } in begin_splits()
163 split_iterator end_splits() { return d_splits.end(); } in end_splits()
H A Dtheory_uf_strong_solver.cpp49 , d_splits( c ) in Region()
171 if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){ in setDisequal()
174 d_splits[ eq ] = false; in setDisequal()
199 d_splits[ (*it).first ] = false; in setRep()
340 d_splits[ j_eq_k ] = true; in check()
352 d_splits[ it_eq_j ] = true; in check()
430 if( !d_splits.empty() ){ in debugPrint()
433 for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); in debugPrint()
/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dtheory_strings.h877 IntStat d_splits;
H A Dtheory_strings.cpp4157 ++(d_statistics.d_splits); in sendSplit()
4747 : d_splits("theory::strings::NumOfSplitOnDemands", 0), in Statistics()
4752 smtStatisticsRegistry()->registerStat(&d_splits); in Statistics()
4759 smtStatisticsRegistry()->unregisterStat(&d_splits); in ~Statistics()