diff options
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 55852490f..f40af6e67 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -206,7 +206,7 @@ class TheoryStrings : public Theory { Node d_one; Node d_neg_one; /** the cardinality of the alphabet */ - unsigned d_card_size; + uint32_t d_cardSize; /** The notify class */ NotifyClass d_notify; /** Equaltity engine */ @@ -401,13 +401,6 @@ private: * FroCoS 2015. */ void checkMemberships(); - /** check cardinality - * - * This function checks whether a cardinality inference needs to be applied - * to a set of equivalence classes. For details, see Step 5 of the proof - * procedure from Liang et al, CAV 2014. - */ - void checkCardinality(); //-----------------------end inference steps //-----------------------representation of the strategy |