From 22ab38c4a3bad18129c740968b36af8c378c4294 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 7 Oct 2021 07:18:08 -0500 Subject: [PATCH] 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. --- src/options/strings_options.toml | 9 + src/smt/env.cpp | 10 +- src/theory/evaluator.cpp | 4 +- src/theory/evaluator.h | 6 +- src/theory/strings/base_solver.cpp | 2 +- src/theory/strings/base_solver.h | 1 + src/theory/strings/extf_solver.cpp | 2 +- src/theory/strings/proof_checker.cpp | 2 +- src/theory/strings/proof_checker.h | 4 +- src/theory/strings/regexp_operation.cpp | 2 +- src/theory/strings/regexp_solver.cpp | 5 +- src/theory/strings/regexp_solver.h | 3 +- src/theory/strings/strings_rewriter.cpp | 7 +- src/theory/strings/strings_rewriter.h | 8 +- src/theory/strings/term_registry.cpp | 20 +- src/theory/strings/term_registry.h | 7 +- src/theory/strings/theory_strings.cpp | 23 +- src/theory/strings/theory_strings.h | 2 - src/theory/strings/theory_strings_utils.cpp | 2 +- src/theory/strings/theory_strings_utils.h | 4 +- src/theory/strings/type_enumerator.cpp | 9 +- src/theory/theory_model_builder.cpp | 5 +- src/theory/type_enumerator.h | 27 +- test/regress/CMakeLists.txt | 1 + .../strings/strings-alpha-card-129.smt2 | 393 ++++++++++++++++++ 25 files changed, 502 insertions(+), 56 deletions(-) create mode 100644 test/regress/regress2/strings/strings-alpha-card-129.smt2 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 @@ -183,6 +183,15 @@ name = "Strings Theory" default = "true" 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" 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(*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& children, const std::vector& 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* statistics) - : SequencesRewriter(r, statistics) + HistogramStat* statistics, + uint32_t alphaCard) + : SequencesRewriter(r, statistics), d_alphaCard(alphaCard) { } @@ -276,7 +277,7 @@ Node StringsRewriter::rewriteStringFromCode(Node n) { Integer i = n[0].getConst().getNumerator(); Node ret; - if (i >= 0 && i < strings::utils::getAlphabetCardinality()) + if (i >= 0 && i < d_alphaCard) { std::vector 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* statistics); + StringsRewriter(Rewriter* r, + HistogramStat* 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 vec = n.getConst().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().getNumerator().toUnsignedInt(); std::unique_ptr 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& 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(type), - d_wenum(0, utils::getAlphabetCardinality()) + d_wenum(0, + tep ? tep->getStringsAlphabetCard() + : utils::getDefaultAlphabetCardinality()) { Assert(type.getKind() == kind::TYPE_CONSTANT && type.getConst() == 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 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 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) -- 2.30.2