diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-22 01:05:43 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-21 23:05:43 -0800 |
commit | 9b20af281db3e77a25540305dfb73cbe56519f75 (patch) | |
tree | 2122c9f51c7d536621a3e3d32da66216d3cde1e8 /src/theory/strings/theory_strings.h | |
parent | a626d85e490256a5d872fec49910cdb43e85c16d (diff) |
Move cardinality inference scheme to base solver in strings (#3792)
Moves handling of cardinality to the base solver, refactors how cardinality is accessed.
No intended behavior change in this commit.
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 |