Move cardinality inference scheme to base solver in strings (#3792)

[cvc5.git] / src / theory / strings / theory_strings_rewriter.cpp

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index e9a4ebfd1f02458c6f13e7129f8882509723b199..339d11dd2715332e28a4b6a8f417b07d34dce5a4 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -230,17 +230,6 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
   return Node::null();
 }
 
-unsigned TheoryStringsRewriter::getAlphabetCardinality()
-{
-  if (options::stdPrintASCII())
-  {
-    Assert(128 <= String::num_codes());
-    return 128;
-  }
-  Assert(256 <= String::num_codes());
-  return 256;
-}
-
 Node TheoryStringsRewriter::rewriteEquality(Node node)
 {
   Assert(node.getKind() == kind::EQUAL);