Make the cardinality of the alphabet of strings configurable (#7298)

This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.

25 files changed, 502 insertions, 56 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index d46e5055e..c32c3adbb 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -184,6 +184,15 @@ name   = "Strings Theory"
   help       = "perform eager context-dependent evaluation for applications of string kinds"
 
 [[option]]
+  name       = "stringsAlphaCard"
+  category   = "regular"
+  long       = "strings-alpha-card=N"
+  type       = "uint64_t"
+  default    = "196608"
+  maximum    = "196608"
+  help       = "the assumed cardinality of the alphabet of characters for strings, which is a prefix of the interval of unicode code points in the SMT-LIB standard"
+  
+[[option]]
   name       = "stringsDeqExt"
   category   = "regular"
   long       = "strings-deq-ext"
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index dafd13d98..f63747ebd 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -21,6 +21,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "options/strings_options.h"
 #include "printer/printer.h"
 #include "proof/conv_proof_generator.h"
 #include "smt/dump_manager.h"
@@ -41,8 +42,8 @@ Env::Env(NodeManager* nm, const Options* opts)
       d_nodeManager(nm),
       d_proofNodeManager(nullptr),
       d_rewriter(new theory::Rewriter()),
-      d_evalRew(new theory::Evaluator(d_rewriter.get())),
-      d_eval(new theory::Evaluator(nullptr)),
+      d_evalRew(nullptr),
+      d_eval(nullptr),
       d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())),
       d_dumpManager(new DumpManager(d_userContext.get())),
       d_logic(),
@@ -55,6 +56,11 @@ Env::Env(NodeManager* nm, const Options* opts)
   {
     d_options.copyValues(*opts);
   }
+  // make the evaluators, which depend on the alphabet of strings
+  d_evalRew.reset(new theory::Evaluator(d_rewriter.get(),
+                                        d_options.strings.stringsAlphaCard));
+  d_eval.reset(
+      new theory::Evaluator(nullptr, d_options.strings.stringsAlphaCard));
   d_statisticsRegistry->registerTimer("global::totalTime").start();
   d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options);
 }
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 75c878065..2d6c3de55 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -127,8 +127,8 @@ Node EvalResult::toNode() const
   }
 }
 
-Evaluator::Evaluator(Rewriter* rr)
-    : d_rr(rr), d_alphaCard(strings::utils::getAlphabetCardinality())
+Evaluator::Evaluator(Rewriter* rr, uint32_t alphaCard)
+    : d_rr(rr), d_alphaCard(alphaCard)
 {
 }
 
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index 2e96952b8..e13dcfbca 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -90,7 +90,11 @@ class Rewriter;
 class Evaluator
 {
  public:
-  Evaluator(Rewriter* rr);
+  /**
+   * @param rr (optional) the rewriter to use when a node cannot be evaluated.
+   * @param strAlphaCard The assumed cardinality of the alphabet for strings.
+   */
+  Evaluator(Rewriter* rr, uint32_t strAlphaCard = 196608);
   /**
    * Evaluates node `n` under the substitution described by the variable names
    * `args` and the corresponding values `vals`. This method uses evaluation
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index e5de8ce16..b675d2444 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -35,7 +35,7 @@ BaseSolver::BaseSolver(Env& env, SolverState& s, InferenceManager& im)
     : EnvObj(env), d_state(s), d_im(im), d_congruent(context())
 {
   d_false = NodeManager::currentNM()->mkConst(false);
-  d_cardSize = utils::getAlphabetCardinality();
+  d_cardSize = options().strings.stringsAlphaCard;
 }
 
 BaseSolver::~BaseSolver() {}
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index 27f9ec40d..bf61b93b2 100644
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -27,6 +27,7 @@
 #include "theory/strings/normal_form.h"
 #include "theory/strings/skolem_cache.h"
 #include "theory/strings/solver_state.h"
+#include "theory/strings/term_registry.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 86f4e48fd..4b12d2673 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -175,7 +175,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
     Node s = n[1];
     // positive contains reduces to a equality
     SkolemCache* skc = d_termReg.getSkolemCache();
-    Node eq = d_termReg.eagerReduce(n, skc);
+    Node eq = d_termReg.eagerReduce(n, skc, d_termReg.getAlphabetCardinality());
     Assert(!eq.isNull());
     Assert(eq.getKind() == ITE && eq[0] == n);
     eq = eq[1];
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 3f5edbb8e..b9038e3c8 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -325,7 +325,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     {
       Assert(args.size() == 1);
       SkolemCache skc(nullptr);
-      ret = TermRegistry::eagerReduce(t, &skc);
+      ret = TermRegistry::eagerReduce(t, &skc, d_alphaCard);
     }
     else if (id == PfRule::STRING_LENGTH_POS)
     {
diff --git a/src/theory/strings/proof_checker.h b/src/theory/strings/proof_checker.h
index 56afaed84..8d0a70f8b 100644
--- a/src/theory/strings/proof_checker.h
+++ b/src/theory/strings/proof_checker.h
@@ -30,7 +30,7 @@ namespace strings {
 class StringProofRuleChecker : public ProofRuleChecker
 {
  public:
-  StringProofRuleChecker() {}
+  StringProofRuleChecker(uint32_t alphaCard) : d_alphaCard(alphaCard) {}
   ~StringProofRuleChecker() {}
 
   /** Register all rules owned by this rule checker in pc. */
@@ -41,6 +41,8 @@ class StringProofRuleChecker : public ProofRuleChecker
   Node checkInternal(PfRule id,
                      const std::vector<Node>& children,
                      const std::vector<Node>& args) override;
+  /** cardinality of the alphabet, which impacts certain inferences */
+  uint32_t d_alphaCard;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index a37cb7936..81ac75c84 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -49,7 +49,7 @@ RegExpOpr::RegExpOpr(Env& env, SkolemCache* sc)
 
   d_emptySingleton =
       NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, d_emptyString);
-  d_lastchar = utils::getAlphabetCardinality() - 1;
+  d_lastchar = options().strings.stringsAlphaCard - 1;
 }
 
 RegExpOpr::~RegExpOpr() {}
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 92dee215b..614a5e6e0 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -20,6 +20,7 @@
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
 #include "theory/ext_theory.h"
+#include "theory/strings/term_registry.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/theory_model.h"
 #include "util/statistics_value.h"
@@ -35,7 +36,7 @@ namespace strings {
 RegExpSolver::RegExpSolver(Env& env,
                            SolverState& s,
                            InferenceManager& im,
-                           SkolemCache* skc,
+                           TermRegistry& tr,
                            CoreSolver& cs,
                            ExtfSolver& es,
                            SequencesStatistics& stats)
@@ -48,7 +49,7 @@ RegExpSolver::RegExpSolver(Env& env,
       d_regexp_ucached(userContext()),
       d_regexp_ccached(context()),
       d_processed_memberships(context()),
-      d_regexp_opr(env, skc)
+      d_regexp_opr(env, tr.getSkolemCache())
 {
   d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::String(""));
   d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY);
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index 1d617eb1e..d6c7f517b 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -31,6 +31,7 @@
 #include "theory/strings/sequences_stats.h"
 #include "theory/strings/skolem_cache.h"
 #include "theory/strings/solver_state.h"
+#include "theory/strings/term_registry.h"
 #include "util/string.h"
 
 namespace cvc5 {
@@ -50,7 +51,7 @@ class RegExpSolver : protected EnvObj
   RegExpSolver(Env& env,
                SolverState& s,
                InferenceManager& im,
-               SkolemCache* skc,
+               TermRegistry& tr,
                CoreSolver& cs,
                ExtfSolver& es,
                SequencesStatistics& stats);
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 9204bfab6..46b36986a 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -28,8 +28,9 @@ namespace theory {
 namespace strings {
 
 StringsRewriter::StringsRewriter(Rewriter* r,
-                                 HistogramStat<Rewrite>* statistics)
-    : SequencesRewriter(r, statistics)
+                                 HistogramStat<Rewrite>* statistics,
+                                 uint32_t alphaCard)
+    : SequencesRewriter(r, statistics), d_alphaCard(alphaCard)
 {
 }
 
@@ -276,7 +277,7 @@ Node StringsRewriter::rewriteStringFromCode(Node n)
   {
     Integer i = n[0].getConst<Rational>().getNumerator();
     Node ret;
-    if (i >= 0 && i < strings::utils::getAlphabetCardinality())
+    if (i >= 0 && i < d_alphaCard)
     {
       std::vector<unsigned> svec = {i.toUnsignedInt()};
       ret = nm->mkConst(String(svec));
diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h
index 65c0b67ab..52f1e44d7 100644
--- a/src/theory/strings/strings_rewriter.h
+++ b/src/theory/strings/strings_rewriter.h
@@ -32,7 +32,9 @@ namespace strings {
 class StringsRewriter : public SequencesRewriter
 {
  public:
-  StringsRewriter(Rewriter* r, HistogramStat<Rewrite>* statistics);
+  StringsRewriter(Rewriter* r,
+                  HistogramStat<Rewrite>* statistics,
+                  uint32_t alphaCard = 196608);
 
   RewriteResponse postRewrite(TNode node) override;
 
@@ -99,6 +101,10 @@ class StringsRewriter : public SequencesRewriter
    * Returns the rewritten form of n.
    */
   Node rewriteStringIsDigit(Node n);
+
+ private:
+  /** The cardinality of the alphabet */
+  uint32_t d_alphaCard;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 2fc86a5a5..c459649fb 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -69,14 +69,17 @@ TermRegistry::TermRegistry(Env& env,
   d_zero = nm->mkConst(Rational(0));
   d_one = nm->mkConst(Rational(1));
   d_negOne = NodeManager::currentNM()->mkConst(Rational(-1));
-  d_cardSize = utils::getAlphabetCardinality();
+  Assert(options().strings.stringsAlphaCard <= String::num_codes());
+  d_alphaCard = options().strings.stringsAlphaCard;
 }
 
 TermRegistry::~TermRegistry() {}
 
+uint32_t TermRegistry::getAlphabetCardinality() const { return d_alphaCard; }
+
 void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
 
-Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
+Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
 {
   NodeManager* nm = NodeManager::currentNM();
   Node lemma;
@@ -86,11 +89,10 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
     // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
     Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
     Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
-    Node code_range = nm->mkNode(
-        AND,
-        nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
-        nm->mkNode(
-            LT, t, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
+    Node code_range =
+        nm->mkNode(AND,
+                   nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
+                   nm->mkNode(LT, t, nm->mkConst(Rational(alphaCard))));
     lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
   }
   else if (tk == STRING_INDEXOF || tk == STRING_INDEXOF_RE)
@@ -225,7 +227,7 @@ void TermRegistry::preRegisterTerm(TNode n)
       std::vector<unsigned> vec = n.getConst<String>().getVec();
       for (unsigned u : vec)
       {
-        if (u >= d_cardSize)
+        if (u >= d_alphaCard)
         {
           std::stringstream ss;
           ss << "Characters in string \"" << n
@@ -322,7 +324,7 @@ void TermRegistry::registerTerm(Node n, int effort)
   else if (n.getKind() != STRING_CONTAINS)
   {
     // we don't send out eager reduction lemma for str.contains currently
-    Node eagerRedLemma = eagerReduce(n, &d_skCache);
+    Node eagerRedLemma = eagerReduce(n, &d_skCache, d_alphaCard);
     if (!eagerRedLemma.isNull())
     {
       // if there was an eager reduction, we make the trust node for it
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 4dfe58aab..a80e48744 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -58,6 +58,8 @@ class TermRegistry : protected EnvObj
                SequencesStatistics& statistics,
                ProofNodeManager* pnm);
   ~TermRegistry();
+  /** get the cardinality of the alphabet used, based on the options */
+  uint32_t getAlphabetCardinality() const;
   /** Finish initialize, which sets the inference manager */
   void finishInit(InferenceManager* im);
   /** The eager reduce routine
@@ -69,9 +71,10 @@ class TermRegistry : protected EnvObj
    *
    * @param t The node to reduce,
    * @param sc The Skolem cache to use for new variables,
+   * @param alphaCard The cardinality of the alphabet we are assuming
    * @return The eager reduction for t.
    */
-  static Node eagerReduce(Node t, SkolemCache* sc);
+  static Node eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard);
   /**
    * Returns a lemma indicating that the length of a term t whose type is
    * string-like has positive length. The exact form of this lemma depends
@@ -216,7 +219,7 @@ class TermRegistry : protected EnvObj
   Node d_one;
   Node d_negOne;
   /** the cardinality of the alphabet */
-  uint32_t d_cardSize;
+  uint32_t d_alphaCard;
   /** Reference to the solver state of the theory of strings. */
   SolverState& d_state;
   /** Pointer to the inference manager of the theory of strings. */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 27640341a..88698d9d8 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -60,7 +60,11 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
       d_extTheoryCb(),
       d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm),
       d_extTheory(env, d_extTheoryCb, d_im),
-      d_rewriter(env.getRewriter(), &d_statistics.d_rewrites),
+      d_rewriter(env.getRewriter(),
+                 &d_statistics.d_rewrites,
+                 d_termReg.getAlphabetCardinality()),
+      // the checker depends on the cardinality of the alphabet
+      d_checker(d_termReg.getAlphabetCardinality()),
       d_bsolver(env, d_state, d_im),
       d_csolver(env, d_state, d_im, d_termReg, d_bsolver),
       d_esolver(env,
@@ -72,13 +76,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
                 d_csolver,
                 d_extTheory,
                 d_statistics),
-      d_rsolver(env,
-                d_state,
-                d_im,
-                d_termReg.getSkolemCache(),
-                d_csolver,
-                d_esolver,
-                d_statistics),
+      d_rsolver(
+          env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
       d_regexp_elim(options::regExpElimAgg(), d_pnm, userContext()),
       d_stringsFmf(env, valuation, d_termReg)
 {
@@ -90,8 +89,6 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 
-  d_cardSize = utils::getAlphabetCardinality();
-
   // set up the extended function callback
   d_extTheoryCb.d_esolver = &d_esolver;
 
@@ -438,11 +435,11 @@ bool TheoryStrings::collectModelInfoType(
           lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt();
       std::unique_ptr<SEnumLen> sel;
       Trace("strings-model") << "Cardinality of alphabet is "
-                             << utils::getAlphabetCardinality() << std::endl;
+                             << d_termReg.getAlphabetCardinality() << std::endl;
       if (tn.isString())  // string-only
       {
         sel.reset(new StringEnumLen(
-            currLen, currLen, utils::getAlphabetCardinality()));
+            currLen, currLen, d_termReg.getAlphabetCardinality()));
       }
       else
       {
@@ -1005,7 +1002,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
     //   witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "")
     NodeManager* nm = NodeManager::currentNM();
     Node t = atom[0];
-    Node card = nm->mkConst(Rational(utils::getAlphabetCardinality()));
+    Node card = nm->mkConst(Rational(d_termReg.getAlphabetCardinality()));
     Node cond =
         nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card));
     Node v = nm->mkBoundVar(nm->stringType());
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8f0205b48..f23b2449f 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -245,8 +245,6 @@ class TheoryStrings : public Theory {
   Node d_zero;
   Node d_one;
   Node d_neg_one;
-  /** the cardinality of the alphabet */
-  uint32_t d_cardSize;
   /** The notify class */
   NotifyClass d_notify;
   /**
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index ea35d53a4..9ab65f6ec 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -37,7 +37,7 @@ namespace theory {
 namespace strings {
 namespace utils {
 
-uint32_t getAlphabetCardinality()
+uint32_t getDefaultAlphabetCardinality()
 {
   // 3*16^4 = 196608 values in the SMT-LIB standard for Unicode strings
   Assert(196608 <= String::num_codes());
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 58162ac1b..0cfcd64d0 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -27,8 +27,8 @@ namespace theory {
 namespace strings {
 namespace utils {
 
-/** get the cardinality of the alphabet used, based on the options */
-uint32_t getAlphabetCardinality();
+/** get the default cardinality of the alphabet used */
+uint32_t getDefaultAlphabetCardinality();
 
 /**
  * Make the conjunction of nodes in a. Removes duplicate conjuncts, returns
diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index e17879e4d..833af8c18 100644
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -239,7 +239,10 @@ SEnumLen* SEnumLenSet::getEnumerator(size_t len, TypeNode tn)
   if (tn.isString())  // string-only
   {
     d_sels[key].reset(
-        new StringEnumLen(len, len, utils::getAlphabetCardinality()));
+        new StringEnumLen(len,
+                          len,
+                          d_tep ? d_tep->getStringsAlphabetCard()
+                                : utils::getDefaultAlphabetCardinality()));
   }
   else
   {
@@ -250,7 +253,9 @@ SEnumLen* SEnumLenSet::getEnumerator(size_t len, TypeNode tn)
 
 StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
     : TypeEnumeratorBase<StringEnumerator>(type),
-      d_wenum(0, utils::getAlphabetCardinality())
+      d_wenum(0,
+              tep ? tep->getStringsAlphabetCard()
+                  : utils::getDefaultAlphabetCardinality())
 {
   Assert(type.getKind() == kind::TYPE_CONSTANT
          && type.getConst<TypeConstant>() == STRING_TYPE);
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index ac177a114..33dbe9ffa 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -19,6 +19,7 @@
 #include "expr/uninterpreted_constant.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "smt/env.h"
@@ -396,7 +397,9 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       << std::endl;
 
   // type enumerator properties
-  TypeEnumeratorProperties tep;
+  bool tepFixUSortCard = options().quantifiers.finiteModelFind;
+  uint32_t tepStrAlphaCard = options().strings.stringsAlphaCard;
+  TypeEnumeratorProperties tep(tepFixUSortCard, tepStrAlphaCard);
 
   // In the first step of model building, we do a traversal of the
   // equality engine and record the information in the following:
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 97bf7aaac..2965cf199 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -64,16 +64,29 @@ class TypeEnumeratorInterface {
   const TypeNode d_type;
 }; /* class TypeEnumeratorInterface */
 
-// AJR: This class stores particular information that is relevant to type enumeration.
-//      For finite model finding, we set d_fixed_usort=true,
-//      and store the finite cardinality bounds for each uninterpreted sort encountered in the model.
+/**
+ * This class stores particular information that is relevant to type
+ * enumeration. For finite model finding, we set d_fixed_usort=true, and store
+ * the finite cardinality bounds for each uninterpreted sort encountered in the
+ * model. For strings, we store the cardinality for the alphabet that we are
+ * assuming.
+ */
 class TypeEnumeratorProperties
 {
 public:
-  TypeEnumeratorProperties() : d_fixed_usort_card(false){}
-  Integer getFixedCardinality( TypeNode tn ) { return d_fixed_card[tn]; }
-  bool d_fixed_usort_card;
-  std::map< TypeNode, Integer > d_fixed_card;
+ TypeEnumeratorProperties(bool fixUSortCard, uint32_t strAlphaCard)
+     : d_fixed_usort_card(fixUSortCard), d_stringAlphaCard(strAlphaCard)
+ {
+ }
+ Integer getFixedCardinality(TypeNode tn) { return d_fixed_card[tn]; }
+ bool d_fixed_usort_card;
+ std::map<TypeNode, Integer> d_fixed_card;
+ /** Get the alphabet for strings */
+ uint32_t getStringsAlphabetCard() const { return d_stringAlphaCard; }
+
+private:
+ /** The cardinality of the alphabet */
+ uint32_t d_stringAlphaCard;
 };
 
 template <class T>
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 768fe852f..190903327 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2557,6 +2557,7 @@ set(regress_2_tests
   regress2/strings/replaceall-diffrange.smt2
   regress2/strings/replaceall-len-c.smt2
   regress2/strings/small-1.smt2
+  regress2/strings/strings-alpha-card-129.smt2
   regress2/strings/update-ex3.smt2
   regress2/strings/update-ex4-seq.smt2
   regress2/sygus/MPwL_d1s3.sy
diff --git a/test/regress/regress2/strings/strings-alpha-card-129.smt2 b/test/regress/regress2/strings/strings-alpha-card-129.smt2
new file mode 100644
index 000000000..c0b4ae0a2
--- /dev/null
+++ b/test/regress/regress2/strings/strings-alpha-card-129.smt2
@@ -0,0 +1,393 @@
+; COMMAND-LINE: --strings-alpha-card=128 --simplification=none
+; EXPECT: unsat
+(set-logic QF_SLIA)
+(declare-fun s1 () String)
+(assert (= (str.len s1) 1))
+(declare-fun s2 () String)
+(assert (= (str.len s2) 1))
+(declare-fun s3 () String)
+(assert (= (str.len s3) 1))
+(declare-fun s4 () String)
+(assert (= (str.len s4) 1))
+(declare-fun s5 () String)
+(assert (= (str.len s5) 1))
+(declare-fun s6 () String)
+(assert (= (str.len s6) 1))
+(declare-fun s7 () String)
+(assert (= (str.len s7) 1))
+(declare-fun s8 () String)
+(assert (= (str.len s8) 1))
+(declare-fun s9 () String)
+(assert (= (str.len s9) 1))
+(declare-fun s10 () String)
+(assert (= (str.len s10) 1))
+(declare-fun s11 () String)
+(assert (= (str.len s11) 1))
+(declare-fun s12 () String)
+(assert (= (str.len s12) 1))
+(declare-fun s13 () String)
+(assert (= (str.len s13) 1))
+(declare-fun s14 () String)
+(assert (= (str.len s14) 1))
+(declare-fun s15 () String)
+(assert (= (str.len s15) 1))
+(declare-fun s16 () String)
+(assert (= (str.len s16) 1))
+(declare-fun s17 () String)
+(assert (= (str.len s17) 1))
+(declare-fun s18 () String)
+(assert (= (str.len s18) 1))
+(declare-fun s19 () String)
+(assert (= (str.len s19) 1))
+(declare-fun s20 () String)
+(assert (= (str.len s20) 1))
+(declare-fun s21 () String)
+(assert (= (str.len s21) 1))
+(declare-fun s22 () String)
+(assert (= (str.len s22) 1))
+(declare-fun s23 () String)
+(assert (= (str.len s23) 1))
+(declare-fun s24 () String)
+(assert (= (str.len s24) 1))
+(declare-fun s25 () String)
+(assert (= (str.len s25) 1))
+(declare-fun s26 () String)
+(assert (= (str.len s26) 1))
+(declare-fun s27 () String)
+(assert (= (str.len s27) 1))
+(declare-fun s28 () String)
+(assert (= (str.len s28) 1))
+(declare-fun s29 () String)
+(assert (= (str.len s29) 1))
+(declare-fun s30 () String)
+(assert (= (str.len s30) 1))
+(declare-fun s31 () String)
+(assert (= (str.len s31) 1))
+(declare-fun s32 () String)
+(assert (= (str.len s32) 1))
+(declare-fun s33 () String)
+(assert (= (str.len s33) 1))
+(declare-fun s34 () String)
+(assert (= (str.len s34) 1))
+(declare-fun s35 () String)
+(assert (= (str.len s35) 1))
+(declare-fun s36 () String)
+(assert (= (str.len s36) 1))
+(declare-fun s37 () String)
+(assert (= (str.len s37) 1))
+(declare-fun s38 () String)
+(assert (= (str.len s38) 1))
+(declare-fun s39 () String)
+(assert (= (str.len s39) 1))
+(declare-fun s40 () String)
+(assert (= (str.len s40) 1))
+(declare-fun s41 () String)
+(assert (= (str.len s41) 1))
+(declare-fun s42 () String)
+(assert (= (str.len s42) 1))
+(declare-fun s43 () String)
+(assert (= (str.len s43) 1))
+(declare-fun s44 () String)
+(assert (= (str.len s44) 1))
+(declare-fun s45 () String)
+(assert (= (str.len s45) 1))
+(declare-fun s46 () String)
+(assert (= (str.len s46) 1))
+(declare-fun s47 () String)
+(assert (= (str.len s47) 1))
+(declare-fun s48 () String)
+(assert (= (str.len s48) 1))
+(declare-fun s49 () String)
+(assert (= (str.len s49) 1))
+(declare-fun s50 () String)
+(assert (= (str.len s50) 1))
+(declare-fun s51 () String)
+(assert (= (str.len s51) 1))
+(declare-fun s52 () String)
+(assert (= (str.len s52) 1))
+(declare-fun s53 () String)
+(assert (= (str.len s53) 1))
+(declare-fun s54 () String)
+(assert (= (str.len s54) 1))
+(declare-fun s55 () String)
+(assert (= (str.len s55) 1))
+(declare-fun s56 () String)
+(assert (= (str.len s56) 1))
+(declare-fun s57 () String)
+(assert (= (str.len s57) 1))
+(declare-fun s58 () String)
+(assert (= (str.len s58) 1))
+(declare-fun s59 () String)
+(assert (= (str.len s59) 1))
+(declare-fun s60 () String)
+(assert (= (str.len s60) 1))
+(declare-fun s61 () String)
+(assert (= (str.len s61) 1))
+(declare-fun s62 () String)
+(assert (= (str.len s62) 1))
+(declare-fun s63 () String)
+(assert (= (str.len s63) 1))
+(declare-fun s64 () String)
+(assert (= (str.len s64) 1))
+(declare-fun s65 () String)
+(assert (= (str.len s65) 1))
+(declare-fun s66 () String)
+(assert (= (str.len s66) 1))
+(declare-fun s67 () String)
+(assert (= (str.len s67) 1))
+(declare-fun s68 () String)
+(assert (= (str.len s68) 1))
+(declare-fun s69 () String)
+(assert (= (str.len s69) 1))
+(declare-fun s70 () String)
+(assert (= (str.len s70) 1))
+(declare-fun s71 () String)
+(assert (= (str.len s71) 1))
+(declare-fun s72 () String)
+(assert (= (str.len s72) 1))
+(declare-fun s73 () String)
+(assert (= (str.len s73) 1))
+(declare-fun s74 () String)
+(assert (= (str.len s74) 1))
+(declare-fun s75 () String)
+(assert (= (str.len s75) 1))
+(declare-fun s76 () String)
+(assert (= (str.len s76) 1))
+(declare-fun s77 () String)
+(assert (= (str.len s77) 1))
+(declare-fun s78 () String)
+(assert (= (str.len s78) 1))
+(declare-fun s79 () String)
+(assert (= (str.len s79) 1))
+(declare-fun s80 () String)
+(assert (= (str.len s80) 1))
+(declare-fun s81 () String)
+(assert (= (str.len s81) 1))
+(declare-fun s82 () String)
+(assert (= (str.len s82) 1))
+(declare-fun s83 () String)
+(assert (= (str.len s83) 1))
+(declare-fun s84 () String)
+(assert (= (str.len s84) 1))
+(declare-fun s85 () String)
+(assert (= (str.len s85) 1))
+(declare-fun s86 () String)
+(assert (= (str.len s86) 1))
+(declare-fun s87 () String)
+(assert (= (str.len s87) 1))
+(declare-fun s88 () String)
+(assert (= (str.len s88) 1))
+(declare-fun s89 () String)
+(assert (= (str.len s89) 1))
+(declare-fun s90 () String)
+(assert (= (str.len s90) 1))
+(declare-fun s91 () String)
+(assert (= (str.len s91) 1))
+(declare-fun s92 () String)
+(assert (= (str.len s92) 1))
+(declare-fun s93 () String)
+(assert (= (str.len s93) 1))
+(declare-fun s94 () String)
+(assert (= (str.len s94) 1))
+(declare-fun s95 () String)
+(assert (= (str.len s95) 1))
+(declare-fun s96 () String)
+(assert (= (str.len s96) 1))
+(declare-fun s97 () String)
+(assert (= (str.len s97) 1))
+(declare-fun s98 () String)
+(assert (= (str.len s98) 1))
+(declare-fun s99 () String)
+(assert (= (str.len s99) 1))
+(declare-fun s100 () String)
+(assert (= (str.len s100) 1))
+(declare-fun s101 () String)
+(assert (= (str.len s101) 1))
+(declare-fun s102 () String)
+(assert (= (str.len s102) 1))
+(declare-fun s103 () String)
+(assert (= (str.len s103) 1))
+(declare-fun s104 () String)
+(assert (= (str.len s104) 1))
+(declare-fun s105 () String)
+(assert (= (str.len s105) 1))
+(declare-fun s106 () String)
+(assert (= (str.len s106) 1))
+(declare-fun s107 () String)
+(assert (= (str.len s107) 1))
+(declare-fun s108 () String)
+(assert (= (str.len s108) 1))
+(declare-fun s109 () String)
+(assert (= (str.len s109) 1))
+(declare-fun s110 () String)
+(assert (= (str.len s110) 1))
+(declare-fun s111 () String)
+(assert (= (str.len s111) 1))
+(declare-fun s112 () String)
+(assert (= (str.len s112) 1))
+(declare-fun s113 () String)
+(assert (= (str.len s113) 1))
+(declare-fun s114 () String)
+(assert (= (str.len s114) 1))
+(declare-fun s115 () String)
+(assert (= (str.len s115) 1))
+(declare-fun s116 () String)
+(assert (= (str.len s116) 1))
+(declare-fun s117 () String)
+(assert (= (str.len s117) 1))
+(declare-fun s118 () String)
+(assert (= (str.len s118) 1))
+(declare-fun s119 () String)
+(assert (= (str.len s119) 1))
+(declare-fun s120 () String)
+(assert (= (str.len s120) 1))
+(declare-fun s121 () String)
+(assert (= (str.len s121) 1))
+(declare-fun s122 () String)
+(assert (= (str.len s122) 1))
+(declare-fun s123 () String)
+(assert (= (str.len s123) 1))
+(declare-fun s124 () String)
+(assert (= (str.len s124) 1))
+(declare-fun s125 () String)
+(assert (= (str.len s125) 1))
+(declare-fun s126 () String)
+(assert (= (str.len s126) 1))
+(declare-fun s127 () String)
+(assert (= (str.len s127) 1))
+(declare-fun s128 () String)
+(assert (= (str.len s128) 1))
+(declare-fun s129 () String)
+(assert (= (str.len s129) 1))
+(assert (distinct
+s1
+s2
+s3
+s4
+s5
+s6
+s7
+s8
+s9
+s10
+s11
+s12
+s13
+s14
+s15
+s16
+s17
+s18
+s19
+s20
+s21
+s22
+s23
+s24
+s25
+s26
+s27
+s28
+s29
+s30
+s31
+s32
+s33
+s34
+s35
+s36
+s37
+s38
+s39
+s40
+s41
+s42
+s43
+s44
+s45
+s46
+s47
+s48
+s49
+s50
+s51
+s52
+s53
+s54
+s55
+s56
+s57
+s58
+s59
+s60
+s61
+s62
+s63
+s64
+s65
+s66
+s67
+s68
+s69
+s70
+s71
+s72
+s73
+s74
+s75
+s76
+s77
+s78
+s79
+s80
+s81
+s82
+s83
+s84
+s85
+s86
+s87
+s88
+s89
+s90
+s91
+s92
+s93
+s94
+s95
+s96
+s97
+s98
+s99
+s100
+s101
+s102
+s103
+s104
+s105
+s106
+s107
+s108
+s109
+s110
+s111
+s112
+s113
+s114
+s115
+s116
+s117
+s118
+s119
+s120
+s121
+s122
+s123
+s124
+s125
+s126
+s127
+s128
+s129
+))
+(check-sat)