fix #2892

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

src/ast/rewriter/seq_rewriter.cpp

@@ -526,6 +526,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         st = mk_str_le(args[0], args[1], result);
         break;
+    case OP_STRING_LT:
+        SASSERT(num_args == 2);
+        st = mk_str_lt(args[0], args[1], result);
+        break;
     case OP_STRING_CONST:
         return BR_FAILED;
     case OP_STRING_ITOS: 
@@ -1435,7 +1439,32 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
 
 br_status seq_rewriter::mk_str_le(expr* a, expr* b, expr_ref& result) {
     result = m().mk_not(m_util.str.mk_lex_lt(b, a));
-    return BR_DONE;
+    return BR_REWRITE2;
+}
+
+br_status seq_rewriter::mk_str_lt(expr* a, expr* b, expr_ref& result) {
+    zstring as, bs;
+    if (m_util.str.is_string(a, as) && m_util.str.is_string(b, bs)) {
+        unsigned sz = std::min(as.length(), bs.length());
+        for (unsigned i = 0; i < sz; ++i) {
+            if (as[i] < bs[i]) {
+                result = m().mk_true();
+                return BR_DONE;
+            }
+            if (as[i] > bs[i]) {
+                result = m().mk_false();
+                return BR_DONE;
+            }
+        }
+        if (sz <= as.length()) {
+            result = m().mk_false();
+        }
+        else {
+            result = m().mk_true();
+        }
+        return BR_DONE;
+    }
+    return BR_FAILED;
 }
 
 br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {

src/ast/rewriter/seq_rewriter.h

@@ -126,6 +126,7 @@ class seq_rewriter {
     br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
     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_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);

src/smt/theory_seq.cpp

@@ -6490,12 +6490,13 @@ void theory_seq::add_unit_axiom(expr* n) {
 }
 
 /**
-   e1 < e2 => e1 = empty or e1 = xcy
+   e1 < e2 => prefix(e1, e2) or e1 = xcy
-   e1 < e2 => e1 = empty or c < d
+   e1 < e2 => prefix(e1, e2) or c < d
-   e1 < e2 => e2 = xdz
+   e1 < e2 => prefix(e1, e2) or e2 = xdz
-   !(e1 < e2) => e1 = e2 or e2 = empty or e2 = xdz
+   e1 < e2 => e1 != e2 
-   !(e1 < e2) => e1 = e2 or e2 = empty or d < c
+   !(e1 < e2) => prefix(e2, e1) or e2 = xdz
-   !(e1 < e2) => e1 = e2 or e1 = xcy
+   !(e1 < e2) => prefix(e2, e1) or d < c
+   !(e1 < e2) => prefix(e2, e1) or e1 = xcy
    !(e1 = e2) or !(e1 < e2)
    
 optional:
@@ -6521,16 +6522,18 @@ void theory_seq::add_lt_axiom(expr* n) {
     literal emp1 = mk_eq(e1, empty_string, false);
     literal emp2 = mk_eq(e2, empty_string, false);
     literal eq   = mk_eq(e1, e2, false);
+    literal pref21 = mk_literal(m_util.str.mk_prefix(e2, e1));
+    literal pref12 = mk_literal(m_util.str.mk_prefix(e1, e2));
     literal e1xcy = mk_eq(e1, xcy, false);
     literal e2xdz = mk_eq(e2, xdz, false);
     literal ltcd = mk_literal(m_util.mk_lt(c, d));
     literal ltdc = mk_literal(m_util.mk_lt(d, c));
-    add_axiom(~lt, e2xdz);
+    add_axiom(~lt, pref12, e2xdz);
-    add_axiom(~lt, emp1, e1xcy);
+    add_axiom(~lt, pref12, e1xcy);
-    add_axiom(~lt, emp1, ltcd);
+    add_axiom(~lt, pref12, ltcd);
-    add_axiom(lt, eq, e1xcy);
+    add_axiom(lt, pref21, e1xcy);
-    add_axiom(lt, eq, emp2, ltdc);
+    add_axiom(lt, pref21, ltdc);
-    add_axiom(lt, eq, emp2, e2xdz);
+    add_axiom(lt, pref21, e2xdz);
     add_axiom(~eq, ~lt);
 }