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.
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"
#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"
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(),
{
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);
}
}
}
-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)
{
}
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
: 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() {}
#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 {
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];
{
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)
{
class StringProofRuleChecker : public ProofRuleChecker
{
public:
- StringProofRuleChecker() {}
+ StringProofRuleChecker(uint32_t alphaCard) : d_alphaCard(alphaCard) {}
~StringProofRuleChecker() {}
/** Register all rules owned by this rule checker in pc. */
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
d_emptySingleton =
NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, d_emptyString);
- d_lastchar = utils::getAlphabetCardinality() - 1;
+ d_lastchar = options().strings.stringsAlphaCard - 1;
}
RegExpOpr::~RegExpOpr() {}
#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"
RegExpSolver::RegExpSolver(Env& env,
SolverState& s,
InferenceManager& im,
- SkolemCache* skc,
+ TermRegistry& tr,
CoreSolver& cs,
ExtfSolver& es,
SequencesStatistics& stats)
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);
#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 {
RegExpSolver(Env& env,
SolverState& s,
InferenceManager& im,
- SkolemCache* skc,
+ TermRegistry& tr,
CoreSolver& cs,
ExtfSolver& es,
SequencesStatistics& stats);
namespace strings {
StringsRewriter::StringsRewriter(Rewriter* r,
- HistogramStat<Rewrite>* statistics)
- : SequencesRewriter(r, statistics)
+ HistogramStat<Rewrite>* statistics,
+ uint32_t alphaCard)
+ : SequencesRewriter(r, statistics), d_alphaCard(alphaCard)
{
}
{
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));
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;
* Returns the rewritten form of n.
*/
Node rewriteStringIsDigit(Node n);
+
+ private:
+ /** The cardinality of the alphabet */
+ uint32_t d_alphaCard;
};
} // namespace strings
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;
// 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)
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
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
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
*
* @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
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. */
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,
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)
{
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;
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
{
// 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());
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;
/**
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());
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
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
{
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);
#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"
<< 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:
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>
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
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff