diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index fc075af6e..c147e6c67 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -187,6 +187,9 @@ extern "C" {
MK_BINARY(Z3_mk_seq_prefix, mk_c(c)->get_seq_fid(), OP_SEQ_PREFIX, SKIP);
MK_BINARY(Z3_mk_seq_suffix, mk_c(c)->get_seq_fid(), OP_SEQ_SUFFIX, SKIP);
MK_BINARY(Z3_mk_seq_contains, mk_c(c)->get_seq_fid(), OP_SEQ_CONTAINS, SKIP);
+ MK_BINARY(Z3_mk_str_lt, mk_c(c)->get_seq_fid(), OP_STRING_LT, SKIP);
+ MK_BINARY(Z3_mk_str_le, mk_c(c)->get_seq_fid(), OP_STRING_LE, SKIP);
+
MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP);
MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP);
MK_BINARY(Z3_mk_seq_at, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP);
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index c5222d340..73193fcb8 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2452,6 +2452,28 @@ namespace Microsoft.Z3
return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
}
+ ///
+ /// Check if the string s1 is lexicographically strictly less than s2.
+ ///
+ public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
+ {
+ Debug.Assert(s1 != null);
+ Debug.Assert(s2 != null);
+ CheckContextMatch(s1, s2);
+ return new BoolExpr(this, Native.Z3_mk_str_lt(nCtx, s1.NativeObject, s2.NativeObject));
+ }
+
+ ///
+ /// Check if the string s1 is lexicographically strictly less than s2.
+ ///
+ public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
+ {
+ Debug.Assert(s1 != null);
+ Debug.Assert(s2 != null);
+ CheckContextMatch(s1, s2);
+ return new BoolExpr(this, Native.Z3_mk_str_le(nCtx, s1.NativeObject, s2.NativeObject));
+ }
+
///
/// Retrieve sequence of length one at index.
///
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 2dcf89927..712b9aace 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -9990,6 +9990,18 @@ class SeqRef(ExprRef):
return Z3_get_string(self.ctx_ref(), self.as_ast())
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
+ def __le__(self, other):
+ return SeqRef(Z3_mk_str_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
+
+ def __lt__(self, other):
+ return SeqRef(Z3_mk_str_lt(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
+
+ def __ge__(self, other):
+ return SeqRef(Z3_mk_str_le(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
+
+ def __gt__(self, other):
+ return SeqRef(Z3_mk_str_lt(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
+
def _coerce_seq(s, ctx=None):
if isinstance(s, str):
@@ -10049,6 +10061,13 @@ def String(name, ctx=None):
ctx = _get_ctx(ctx)
return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)
+def Strings(names, ctx=None):
+ """Return string constants"""
+ ctx = _get_ctx(ctx)
+ if isinstance(names, str):
+ names = names.split(" ")
+ return [String(name, ctx) for name in names]
+
def SubString(s, offset, length):
"""Extract substring or subsequence starting at offset"""
return Extract(s, offset, length)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 3a666ec37..642c959cc 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3474,6 +3474,25 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
+
+ /**
+ \brief Check if \c s1 is lexicographically strictly less than \c s2.
+
+ \pre \c s1 and \c s2 are strings
+
+ def_API('Z3_mk_str_lt' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+ */
+ Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s);
+
+ /**
+ \brief Check if \c s1 is equal or lexicographically strictly less than \c s2.
+
+ \pre \c s1 and \c s2 are strings
+
+ def_API('Z3_mk_str_le' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+ */
+ Z3_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s);
+
/**
\brief Extract subsequence starting at \c offset of \c length.
diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 14a06a5f7..4485a217f 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -646,7 +646,8 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) {
- // degrades simplification on if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs);
+ // degrades simplification
+ // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs);
return m().mk_eq(lhs, rhs);
}
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index c0a5db050..3ebb8280e 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -580,6 +580,8 @@ void seq_decl_plugin::init() {
m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
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_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);
@@ -695,9 +697,11 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_SEQ_UNIT:
case OP_STRING_ITOS:
case OP_STRING_STOI:
+ case OP_STRING_LT:
+ case OP_STRING_LE:
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));
-
+
case _OP_REGEXP_FULL_CHAR:
m_has_re = true;
if (!range) range = m_re;
@@ -1016,6 +1020,10 @@ app* seq_util::mk_le(expr* ch1, expr* ch2) const {
return bv.mk_ule(ch1, ch2);
}
+app* seq_util::mk_lt(expr* ch1, expr* ch2) const {
+ bv_util bv(m);
+ return m.mk_not(bv.mk_ule(ch2, ch1));
+}
bool seq_util::str::is_string(expr const* n, zstring& s) const {
if (is_string(n)) {
@@ -1037,7 +1045,6 @@ app* seq_util::str::mk_nth(expr* s, unsigned i) const {
return mk_nth(s, arith_util(m).mk_int(i));
}
-
void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {
expr* e1, *e2;
while (is_concat(e, e1, e2)) {
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index ad73d863d..df9b82af1 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -66,6 +66,8 @@ enum seq_op_kind {
OP_STRING_CONST,
OP_STRING_ITOS,
OP_STRING_STOI,
+ OP_STRING_LT,
+ OP_STRING_LE,
// internal only operators. Converted to SEQ variants.
_OP_STRING_STRREPL,
_OP_STRING_CONCAT,
@@ -226,6 +228,7 @@ public:
bool is_const_char(expr* e, unsigned& c) const;
app* mk_char(unsigned ch) const;
app* mk_le(expr* ch1, expr* ch2) const;
+ app* mk_lt(expr* ch1, expr* ch2) const;
app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
@@ -298,6 +301,8 @@ public:
bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); }
bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
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_string_term(expr const * n) const {
sort * s = get_sort(n);
@@ -321,6 +326,8 @@ public:
MATCH_TERNARY(is_replace);
MATCH_BINARY(is_prefix);
MATCH_BINARY(is_suffix);
+ MATCH_BINARY(is_lt);
+ MATCH_BINARY(is_le);
MATCH_UNARY(is_itos);
MATCH_UNARY(is_stoi);
MATCH_BINARY(is_in_re);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3f93b091c..bc4c611d1 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4941,6 +4941,7 @@ void theory_seq::add_extract_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
expr* s = nullptr, *i = nullptr, *l = nullptr;
VERIFY(m_util.str.is_extract(e, s, i, l));
+#if 0
if (is_tail(s, i, l)) {
add_tail_axiom(e, s);
return;
@@ -4957,7 +4958,7 @@ void theory_seq::add_extract_axiom(expr* e) {
add_extract_suffix_axiom(e, s, i);
return;
}
-
+#endif
expr_ref x(mk_skolem(m_pre, s, i), m);
expr_ref ls = mk_len(s);
expr_ref lx = mk_len(x);
@@ -5450,6 +5451,22 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
m_ncs.push_back(nc(expr_ref(e, m), len_gt, dep));
}
}
+ else if (m_util.str.is_lt(e, e1, e2)) {
+ if (is_true) {
+ propagate_lt(lit, e1, e2);
+ }
+ else {
+ propagate_le(lit, e2, e1);
+ }
+ }
+ else if (m_util.str.is_le(e, e1, e2)) {
+ if (is_true) {
+ propagate_le(lit, e1, e2);
+ }
+ else {
+ propagate_lt(lit, e2, e1);
+ }
+ }
else if (is_accept(e)) {
if (is_true) {
propagate_accept(lit, e);
@@ -5902,7 +5919,49 @@ void theory_seq::propagate_not_suffix(expr* e) {
add_axiom(lit, e1_gt_e2, ~mk_eq(c, d, false));
}
+/**
+ lit == e1 < e2:
+ lit => e1 = empty or e1 = xcy
+ lit => e1 = empty or e2 = xdz
+ lit => e1 = empty or c < d
+ lit => e1 != empty or e2 != empty
+ */
+void theory_seq::propagate_lt(literal lit, expr* e1, expr* e2) {
+ sort* s = m.get_sort(e1);
+ sort* char_sort = nullptr;
+ VERIFY(m_util.is_seq(s, char_sort));
+ expr_ref x = mk_skolem(symbol("str.lt.x"), e1, e2);
+ expr_ref y = mk_skolem(symbol("str.lt.y"), e1, e2);
+ expr_ref z = mk_skolem(symbol("str.lt.z"), e1, e2);
+ expr_ref c = mk_skolem(symbol("str.lt.c"), e1, e2, nullptr, nullptr, char_sort);
+ expr_ref d = mk_skolem(symbol("str.lt.d"), e1, e2, nullptr, nullptr, char_sort);
+ expr_ref empty_string(m_util.str.mk_empty(s), m);
+ literal emp = mk_eq(e1, empty_string, false);
+ add_axiom(~lit, ~mk_eq(e1, e2, false));
+ add_axiom(~lit, emp, mk_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y), false));
+ add_axiom(~lit, emp, mk_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z), false));
+ add_axiom(~lit, emp, mk_literal(m_util.mk_lt(c, d)));
+ add_axiom(~lit, ~emp, ~mk_eq(e2, empty_string, false));
+}
+/**
+ lit => e1 <= e2
+ e1 < e2 or e1 = e2 or e2 < e1
+ !(e1 = e2) or !(e1 < e2)
+ !(e1 = e2) or !(e2 < e1)
+ !(e1 < e2) or !(e2 < e1)
+ lit => e1 < e2 or e1 = e2
+ */
+void theory_seq::propagate_le(literal lit, expr* e1, expr* e2) {
+ literal lt_e1e2 = mk_literal(m_util.mk_lt(e1, e2));
+ literal lt_e2e1 = mk_literal(m_util.mk_lt(e2, e1));
+ literal eq = mk_eq(e1, e2, false);
+ add_axiom(eq, lt_e1e2, lt_e2e1);
+ add_axiom(lit, eq, lt_e1e2);
+ add_axiom(~eq, ~lt_e1e2);
+ add_axiom(~eq, ~lt_e2e1);
+ add_axiom(~lt_e1e2, ~lt_e2e1);
+}
bool theory_seq::canonizes(bool sign, expr* e) {
context& ctx = get_context();
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 2d9afc2cd..09b8d61b4 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -646,6 +646,8 @@ namespace smt {
void propagate_step(literal lit, expr* n);
void propagate_accept(literal lit, expr* e);
void new_eq_eh(dependency* dep, enode* n1, enode* n2);
+ void propagate_lt(literal lit, expr* e1, expr* e2);
+ void propagate_le(literal lit, expr* e1, expr* e2);
// diagnostics
std::ostream& display_equations(std::ostream& out) const;