Home
last modified time | relevance | path

Searched refs:d_cardinality (Results 1 – 3 of 3) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dtype_enumerator.h36 unsigned d_cardinality; variable
49 d_cardinality = TheoryStringsRewriter::getAlphabetCardinality();
60 if (d_data[i] + 1 < d_cardinality)
88 unsigned d_cardinality;
97 StringEnumeratorLength(unsigned length, unsigned card = 256) : d_cardinality(card) { in d_cardinality() function
108 if( d_data[i] + 1 < d_cardinality ) {
/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dtheory_uf_strong_solver.cpp472 d_cardinality(c, 1), in SortModel()
687 if( d_reps<=(unsigned)d_cardinality ){ in check()
703 if( d_regions[i]->check( level, d_cardinality, clique ) ){ in check()
713 if( !applyTotality( d_cardinality ) ){ in check()
846 if( !prevHasCard || c<d_cardinality ){ in assertCardinality()
847 d_cardinality = c; in assertCardinality()
887 Assert( d_cardinality>0 ); in checkRegion()
1047 Assert( d_cardinality>0 ); in addCliqueLemma()
1048 while( clique.size()>size_t(d_cardinality+1) ){ in addCliqueLemma()
1060 eqs.push_back(d_cardinality_literal[d_cardinality].notNode()); in addCliqueLemma()
[all …]
H A Dtheory_uf_strong_solver.h266 context::CDO< int > d_cardinality; variable
320 int getCardinality() { return d_cardinality; } in getCardinality()