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

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

diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index a564c82e16a136f6fc47befb0038e57a3e5bbc41..a325108e446a0970ea41906c6d48b863121685ce 100644 (file)
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/strings/theory_strings_utils.h"
 
+#include "options/strings_options.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;
@@ -25,6 +26,17 @@ namespace theory {
 namespace strings {
 namespace utils {
 
+uint32_t getAlphabetCardinality()
+{
+  if (options::stdPrintASCII())
+  {
+    Assert(128 <= String::num_codes());
+    return 128;
+  }
+  Assert(256 <= String::num_codes());
+  return 256;
+}
+
 Node mkAnd(const std::vector<Node>& a)
 {
   std::vector<Node> au;