diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index dd8524ba0..6d3524544 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -48,7 +48,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_string(c, str); RESET_ERROR_CODE(); - zstring s(str, zstring::ascii); + zstring s(str); app* a = mk_c(c)->sutil().str.mk_string(s); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_ast(a)); @@ -62,7 +62,7 @@ extern "C" { RESET_ERROR_CODE(); unsigned_vector chs; for (unsigned i = 0; i < sz; ++i) chs.push_back(str[i]); - zstring s(sz, chs.c_ptr(), zstring::ascii); + zstring s(sz, chs.c_ptr()); app* a = mk_c(c)->sutil().str.mk_string(s); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_ast(a)); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index c429e34ba..4eed120b5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -473,6 +473,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_RE_LOOP: st = mk_re_loop(f, num_args, args, result); break; + case OP_RE_POWER: + st = mk_re_power(f, args[0], result); + break; case OP_RE_EMPTY_SET: return BR_FAILED; case OP_RE_FULL_SEQ_SET: @@ -558,6 +561,18 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); st = mk_str_lt(args[0], args[1], result); break; + case OP_STRING_FROM_CODE: + SASSERT(num_args == 1); + st = mk_str_from_code(args[0], result); + break; + case OP_STRING_TO_CODE: + SASSERT(num_args == 1); + st = mk_str_to_code(args[0], result); + break; + case OP_STRING_IS_DIGIT: + SASSERT(num_args == 1); + st = mk_str_is_digit(args[0], result); + break; case OP_STRING_CONST: st = BR_FAILED; if (!m_coalesce_chars) { @@ -1493,6 +1508,19 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu return BR_FAILED; } +br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& result) { + return BR_FAILED; +} + +br_status seq_rewriter::mk_seq_replace_re_all(expr* a, expr* b, expr* c, expr_ref& result) { + return BR_FAILED; +} + +br_status seq_rewriter::mk_seq_replace_re(expr* a, expr* b, expr* c, expr_ref& result) { + return BR_FAILED; +} + + br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << "\n";); zstring s1, s2; @@ -1708,6 +1736,54 @@ br_status seq_rewriter::mk_str_lt(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } +br_status seq_rewriter::mk_str_from_code(expr* a, expr_ref& result) { + rational r; + if (m_autil.is_numeral(a, r)) { + if (r.is_neg() || r > m_util.str.max_char_value()) { + result = m_util.str.mk_string(symbol("")); + } + else { + unsigned num = r.get_unsigned(); + zstring s(1, &num); + result = m_util.str.mk_string(s); + } + return BR_DONE; + } + return BR_FAILED; +} + +br_status seq_rewriter::mk_str_to_code(expr* a, expr_ref& result) { + zstring str; + if (m_util.str.is_string(a, str)) { + if (str.length() == 1) + result = m_autil.mk_int(str[0]); + else + result = m_autil.mk_int(-1); + return BR_DONE; + } + return BR_FAILED; +} + +br_status seq_rewriter::mk_str_is_digit(expr* a, expr_ref& result) { + zstring str; + if (m_util.str.is_string(a, str)) { + if (str.length() == 1 && '0' <= str[0] && str[0] <= '9') + result = m().mk_true(); + else + result = m().mk_false(); + return BR_DONE; + } + if (m_util.str.is_empty(a)) { + result = m().mk_false(); + return BR_DONE; + } + // when a has length > 1 -> false + // when a is a unit character -> evaluate + + return BR_FAILED; +} + + br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { rational r; if (m_autil.is_numeral(a, r)) { @@ -2216,6 +2292,13 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* return BR_FAILED; } +br_status seq_rewriter::mk_re_power(func_decl* f, expr* a, expr_ref& result) { + unsigned p = f->get_parameter(0).get_int(); + result = m_util.re.mk_loop(a, p, p); + return BR_REWRITE1; +} + + /* a** = a* (a* + b)* = (a + b)* diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 7c9f3c102..098b2f82d 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -143,6 +143,9 @@ class seq_rewriter { br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result); br_status mk_seq_last_index(expr* a, expr* b, expr_ref& result); br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_replace_re_all(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_replace_re(expr* a, expr* b, expr* c, expr_ref& result); br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result); br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result); br_status mk_str_units(func_decl* f, expr_ref& result); @@ -152,6 +155,9 @@ class seq_rewriter { br_status mk_str_to_regexp(expr* a, expr_ref& result); br_status mk_str_le(expr* a, expr* b, expr_ref& result); br_status mk_str_lt(expr* a, expr* b, expr_ref& result); + br_status mk_str_from_code(expr* a, expr_ref& result); + br_status mk_str_to_code(expr* a, expr_ref& result); + br_status mk_str_is_digit(expr* a, expr_ref& result); br_status mk_re_concat(expr* a, expr* b, expr_ref& result); br_status mk_re_union(expr* a, expr* b, expr_ref& result); br_status mk_re_inter(expr* a, expr* b, expr_ref& result); @@ -160,6 +166,7 @@ class seq_rewriter { br_status mk_re_diff(expr* a, expr* b, expr_ref& result); br_status mk_re_plus(expr* a, expr_ref& result); br_status mk_re_opt(expr* a, expr_ref& result); + br_status mk_re_power(func_decl* f, expr* a, expr_ref& result); br_status mk_re_loop(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result); br_status mk_re_range(expr* lo, expr* hi, expr_ref& result); br_status lift_ite(func_decl* f, unsigned n, expr* const* args, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index c4372c3aa..4ffe77d1a 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -158,10 +158,10 @@ static bool is_escape_char(char const *& s, unsigned& result) { return false; } -zstring::zstring(encoding enc): m_encoding(enc) {} +zstring::zstring() {} -zstring::zstring(char const* s, encoding enc): m_encoding(enc) { - unsigned mask = 0xFF; // TBD for UTF +zstring::zstring(char const* s) { + unsigned mask = 0xFF; // TBD for Unicode while (*s) { unsigned ch; if (is_escape_char(s, ch)) { @@ -176,17 +176,14 @@ zstring::zstring(char const* s, encoding enc): m_encoding(enc) { zstring::zstring(zstring const& other) { m_buffer = other.m_buffer; - m_encoding = other.m_encoding; } -zstring::zstring(unsigned sz, unsigned const* s, encoding enc) { +zstring::zstring(unsigned sz, unsigned const* s) { m_buffer.append(sz, s); - m_encoding = enc; } zstring::zstring(unsigned num_bits, bool const* ch) { - SASSERT(num_bits == 8 || num_bits == 16); - m_encoding = (num_bits == 8)?ascii:unicode; + SASSERT(num_bits == 8); // TBD for unicode unsigned n = 0; for (unsigned i = 0; i < num_bits; ++i) { n |= (((unsigned)ch[i]) << i); @@ -194,20 +191,19 @@ zstring::zstring(unsigned num_bits, bool const* ch) { m_buffer.push_back(n); } -zstring::zstring(unsigned ch, encoding enc) { - m_encoding = enc; - m_buffer.push_back(ch & ((enc == ascii)?0x000000FF:0x0000FFFF)); +zstring::zstring(unsigned ch) { + SASSERT(ch <= 196607); + m_buffer.push_back(ch); } zstring& zstring::operator=(zstring const& other) { - m_encoding = other.m_encoding; m_buffer.reset(); m_buffer.append(other.m_buffer); return *this; } zstring zstring::replace(zstring const& src, zstring const& dst) const { - zstring result(m_encoding); + zstring result; if (length() < src.length()) { return zstring(*this); } @@ -272,7 +268,6 @@ std::string zstring::encode() const { } std::string zstring::as_string() const { - SASSERT(m_encoding == ascii); std::ostringstream strm; char buffer[100]; unsigned offset = 0; @@ -351,7 +346,7 @@ int zstring::last_indexof(zstring const& other) const { } zstring zstring::extract(unsigned offset, unsigned len) const { - zstring result(m_encoding); + zstring result; if (offset + len < offset) return result; int last = std::min(offset+len, length()); for (int i = offset; i < last; ++i) { @@ -361,7 +356,6 @@ zstring zstring::extract(unsigned offset, unsigned len) const { } zstring zstring::operator+(zstring const& other) const { - SASSERT(m_encoding == other.m_encoding); zstring result(*this); result.m_buffer.append(other.m_buffer); return result; @@ -578,6 +572,8 @@ void seq_decl_plugin::init() { sort* boolT = m.mk_bool_sort(); sort* intT = arith_util(m).mk_int(); sort* predA = array_util(m).mk_array_sort(A, boolT); + sort* seqAseqAseqA[3] = { seqA, seqA, seqA }; + sort* seqAreAseqA[3] = { seqA, reA, seqA }; sort* seqAseqA[2] = { seqA, seqA }; sort* seqAreA[2] = { seqA, reA }; sort* reAreA[2] = { reA, reA }; @@ -615,6 +611,7 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA); m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA); m_sigs[OP_RE_LOOP] = alloc(psig, m, "re.loop", 1, 1, &reA, reA); + m_sigs[OP_RE_POWER] = alloc(psig, m, "re.^", 1, 1, &reA, reA); m_sigs[OP_RE_COMPLEMENT] = alloc(psig, m, "re.comp", 1, 1, &reA, reA); m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re.empty", 1, 0, nullptr, reA); m_sigs[OP_RE_FULL_SEQ_SET] = alloc(psig, m, "re.all", 1, 0, nullptr, reA); @@ -622,6 +619,9 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA); m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT); + m_sigs[OP_SEQ_REPLACE_RE_ALL] = alloc(psig, m, "str.replace_re_all", 1, 3, seqAreAseqA, seqA); + m_sigs[OP_SEQ_REPLACE_RE] = alloc(psig, m, "str.replace_re", 1, 3, seqAreAseqA, seqA); + m_sigs[OP_SEQ_REPLACE_ALL] = alloc(psig, m, "str.replace_all", 1, 3, seqAseqAseqA, seqA); m_sigs[OP_STRING_CONST] = nullptr; m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); @@ -629,6 +629,9 @@ void seq_decl_plugin::init() { m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to_int", 0, 1, &strT, intT); m_sigs[OP_STRING_LT] = alloc(psig, m, "str.<", 0, 2, str2T, boolT); m_sigs[OP_STRING_LE] = alloc(psig, m, "str.<=", 0, 2, str2T, boolT); + m_sigs[OP_STRING_IS_DIGIT] = alloc(psig, m, "str.is_digit", 0, 1, &strT, boolT); + m_sigs[OP_STRING_TO_CODE] = alloc(psig, m, "str.to_code", 0, 1, &strT, intT); + m_sigs[OP_STRING_FROM_CODE] = alloc(psig, m, "str.from_code", 0, 1, &intT, strT); m_sigs[_OP_STRING_CONCAT] = alloc(psig, m, "str.++", 1, 2, str2T, strT); m_sigs[_OP_STRING_LENGTH] = alloc(psig, m, "str.len", 0, 1, &strT, intT); m_sigs[_OP_STRING_STRCTN] = alloc(psig, m, "str.contains", 0, 2, str2T, boolT); @@ -752,6 +755,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_STRING_STOI: case OP_STRING_LT: case OP_STRING_LE: + case OP_STRING_IS_DIGIT: + case OP_STRING_TO_CODE: + case OP_STRING_FROM_CODE: match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); @@ -812,6 +818,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, default: m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters"); } + case OP_RE_POWER: + m_has_re = true; + if (num_parameters == 1 && parameters[0].is_int() && arity == 1 && parameters[0].get_int() >= 0) { + rng = domain[0]; + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); + } + m.raise_exception("Incorrect arguments used for re.^. Expected one non-negative integer parameter"); case OP_STRING_CONST: if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) { @@ -823,6 +836,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_RE_UNION: case OP_RE_CONCAT: case OP_RE_INTERSECT: + case OP_RE_DIFF: m_has_re = true; return mk_assoc_fun(k, arity, domain, range, k, k); @@ -1066,11 +1080,13 @@ app* seq_util::str::mk_string(zstring const& s) const { } app* seq_util::str::mk_char(zstring const& s, unsigned idx) const { - return u.bv().mk_numeral(s[idx], s.num_bits()); + // TBD: change to unicode + return u.bv().mk_numeral(s[idx], 8); } app* seq_util::str::mk_char(char ch) const { - zstring s(ch, zstring::ascii); + // TBD: change to unicode + zstring s(ch); return mk_char(s, 0); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 0b2328f3d..81e9009dc 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -17,15 +17,6 @@ Revision History: Updated to string sequences 2015-12-5 -TBD: -- ((_ re.^ n) RegLan RegLan) -- (str.replace_re_all String RegLan String String) -- (str.replace_re String RegLan String String) -- (str.replace_all String String String String) -- (str.is_digit String Bool) would replace smt/seq_skolem is_digit. -- (str.to_code String Int) -- (str.from_code Int String) - --*/ #ifndef SEQ_DECL_PLUGIN_H_ #define SEQ_DECL_PLUGIN_H_ @@ -60,6 +51,9 @@ enum seq_op_kind { OP_SEQ_LAST_INDEX, OP_SEQ_TO_RE, OP_SEQ_IN_RE, + OP_SEQ_REPLACE_RE_ALL, // Seq -> RegEx -> Seq -> Seq + OP_SEQ_REPLACE_RE, // Seq -> RegEx -> Seq -> Seq + OP_SEQ_REPLACE_ALL, // Seq -> Seq -> Seq -> Seq OP_RE_PLUS, OP_RE_STAR, @@ -70,6 +64,7 @@ enum seq_op_kind { OP_RE_DIFF, OP_RE_INTERSECT, OP_RE_LOOP, + OP_RE_POWER, OP_RE_COMPLEMENT, OP_RE_EMPTY_SET, OP_RE_FULL_SEQ_SET, @@ -83,6 +78,9 @@ enum seq_op_kind { OP_STRING_STOI, OP_STRING_LT, OP_STRING_LE, + OP_STRING_IS_DIGIT, + OP_STRING_TO_CODE, + OP_STRING_FROM_CODE, // internal only operators. Converted to SEQ variants. _OP_STRING_STRREPL, _OP_STRING_CONCAT, @@ -103,25 +101,17 @@ enum seq_op_kind { class zstring { -public: - enum encoding { - ascii, - unicode - }; private: buffer m_buffer; - encoding m_encoding; public: - zstring(encoding enc = ascii); - zstring(char const* s, encoding enc = ascii); - zstring(unsigned sz, unsigned const* s, encoding enc = ascii); + zstring(); + zstring(char const* s); + zstring(unsigned sz, unsigned const* s); zstring(zstring const& other); zstring(unsigned num_bits, bool const* ch); - zstring(unsigned ch, encoding enc = ascii); + zstring(unsigned ch); zstring& operator=(zstring const& other); zstring replace(zstring const& src, zstring const& dst) const; - unsigned num_bits() const { return (m_encoding==ascii)?8:16; } - encoding get_encoding() const { return m_encoding; } std::string encode() const; std::string as_string() const; unsigned length() const { return m_buffer.size(); } @@ -267,6 +257,9 @@ public: public: str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {} + unsigned min_char_value() const { return 0; } + unsigned max_char_value() const { return 196607; } + sort* mk_seq(sort* s) const { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, ¶m); } sort* mk_string_sort() const { return m.mk_sort(m_fid, _STRING_SORT, 0, nullptr); } app* mk_empty(sort* s) const { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, nullptr, 0, (expr*const*)nullptr, s)); } @@ -300,6 +293,9 @@ public: app* mk_is_empty(expr* s) const; app* mk_lex_lt(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LT, 2, es); } app* mk_lex_le(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LE, 2, es); } + app* mk_to_code(expr* e) const { return m.mk_app(m_fid, OP_STRING_TO_CODE, 1, &e); } + app* mk_from_code(expr* e) const { return m.mk_app(m_fid, OP_STRING_FROM_CODE, 1, &e); } + app* mk_is_digit(expr* e) const { return m.mk_app(m_fid, OP_STRING_IS_DIGIT, 1, &e); } bool is_nth_i(func_decl const* f) const { return is_decl_of(f, m_fid, OP_SEQ_NTH_I); } @@ -335,6 +331,9 @@ public: bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } bool is_lt(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LT); } bool is_le(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LE); } + bool is_is_digit(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_IS_DIGIT); } + bool is_from_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_CODE); } + bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_FROM_CODE); } bool is_string_term(expr const * n) const { sort * s = get_sort(n); @@ -363,6 +362,9 @@ public: MATCH_BINARY(is_le); MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); + MATCH_UNARY(is_is_digit); + MATCH_UNARY(is_from_code); + MATCH_UNARY(is_to_code); MATCH_BINARY(is_in_re); MATCH_UNARY(is_unit); diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index 76d549f27..cc9241446 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -50,10 +50,11 @@ void monotone::monotonicity_lemma(monic const& m) { Example: 0 >= x >= -2 & 0 <= y <= 3 => x*y >= -6 - + 0 >= x >= -2 & 0 <= y <= 3 => x*x*y <= 12 + */ void monotone::monotonicity_lemma_gt(const monic& m) { - new_lemma lemma(c(), __FUNCTION__); + new_lemma lemma(c(), "monotonicity > "); rational product(1); for (lpvar j : m.vars()) { auto v = c().val(j); @@ -75,7 +76,7 @@ void monotone::monotonicity_lemma_gt(const monic& m) { x <= -2 & y >= 3 => x*y <= -6 */ void monotone::monotonicity_lemma_lt(const monic& m) { - new_lemma lemma(c(), __FUNCTION__); + new_lemma lemma(c(), "monotonicity <"); rational product(1); for (lpvar j : m.vars()) { auto v = c().val(j); diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index decc81438..6930bc9c0 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -289,6 +289,7 @@ void order::generate_ol(const monic& ac, lemma |= ineq(c.var(), val(c.var()).is_neg() ? llc::GE : llc::LE, 0); _().negate_var_relation_strictly(lemma, ac.var(), bc.var()); _().negate_var_relation_strictly(lemma, a.var(), b.var()); + lemma &= ac; lemma &= a; lemma &= bc; diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index 8f24cb528..620653c8c 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -771,6 +771,59 @@ void seq_axioms::add_le_axiom(expr* n) { add_axiom(~lt, le); } +/** + is_digit(e) <=> e = '0' or ... or e = '9' + */ +void seq_axioms::add_is_digit_axiom(expr* n) { + expr* e = nullptr; + VERIFY(seq.str.is_is_digit(n, e)); + literal is_digit = mk_literal(n); + literal_vector digits; + digits.push_back(~is_digit); + for (unsigned i = 0; i < 10; ++i) { + unsigned d = '0' + i; + zstring str(1, &d); + expr_ref s(seq.str.mk_string(str), m); + m_rewrite(s); // if the solver depends on unit normal form + literal digit_i = mk_eq(e, s); + digits.push_back(digit_i); + add_axiom(~digit_i, is_digit); + } + // literals are marked relevant by add_axiom of binary clauses + ctx().mk_th_axiom(th.get_id(), digits); +} + +/** + len(e) = 1 => 0 <= to_code(e) <= max_code + len(e) != 1 => to_code(e) = -1 + */ +void seq_axioms::add_str_to_code_axiom(expr* n) { + expr* e = nullptr; + VERIFY(seq.str.is_to_code(n, e)); + literal len_is1 = mk_eq(mk_len(e), a.mk_int(1)); + add_axiom(~len_is1, mk_ge(n, 0)); + add_axiom(~len_is1, mk_le(n, seq.str.max_char_value())); + add_axiom(len_is1, mk_eq(n, a.mk_int(-1))); +} + +/** + 0 <= e <= max_char => len(from_code(e)) = 1 + 0 <= e <= max_char => to_code(from_code(e)) = e + e < 0 or e > max_char => len(from_code(e)) = "" + */ +void seq_axioms::add_str_from_code_axiom(expr* n) { + expr* e = nullptr; + VERIFY(seq.str.is_from_code(n, e)); + literal ge = mk_ge(e, 0); + literal le = mk_le(e, seq.str.max_char_value()); + literal emp = mk_literal(seq.str.mk_is_empty(n)); + add_axiom(~ge, ~le, mk_eq(mk_len(n), a.mk_int(1))); + add_axiom(~ge, ~le, mk_eq(seq.str.mk_to_code(n), e)); + add_axiom(ge, emp); + add_axiom(le, emp); +} + + /** Unit is injective: diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index 1cf26edc3..65f883564 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -84,6 +84,9 @@ namespace smt { void add_itos_axiom(expr* s, unsigned k); void add_lt_axiom(expr* n); void add_le_axiom(expr* n); + void add_is_digit_axiom(expr* n); + void add_str_to_code_axiom(expr* n); + void add_str_from_code_axiom(expr* n); void add_unit_axiom(expr* n); void add_length_axiom(expr* n); void unroll_not_contains(expr* n);