adding comparison #2360

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);

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));
         }
 
+        /// <summary>
+        /// Check if the string s1 is lexicographically strictly less than s2.
+        /// </summary>
+	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));
+        }
+
+        /// <summary>
+        /// Check if the string s1 is lexicographically strictly less than s2.
+        /// </summary>
+	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));
+        }
+
         /// <summary>
         /// Retrieve sequence of length one at index.
         /// </summary>

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)

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.
 

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);
 }
 

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)) {

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);

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();

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;