Add constant-bound shortcut for string comparison constraints

src/smt/theory_seq.cpp

@@ -696,6 +696,14 @@ bool theory_seq::check_lts() {
 
                 literal eq = (b == c) ? true_literal : mk_eq(b, c, false);
                 bool is_strict = is_strict1 || is_strict2; 
+                zstring sa, sd;
+                if (m_util.str.is_string(a, sa) && m_util.str.is_string(d, sd)) {
+                    bool ok = is_strict ? sa < sd : !(sd < sa);
+                    if (!ok) {
+                        add_axiom(~r1, ~r2, ~eq);
+                    }
+                    continue;
+                }
                 if (is_strict) {
                     add_axiom(~r1, ~r2, ~eq, mk_literal(m_util.str.mk_lex_lt(a, d)));
                 }
@@ -3155,6 +3163,57 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     }
     else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) {
         m_lts.push_back(e);
+        expr* a = nullptr, *b = nullptr;
+        zstring c;
+        bool is_lower = false;
+        expr* x = nullptr;
+        if (is_true && m_util.str.is_lt(e, a, b)) {
+            if (m_util.str.is_string(a, c) && !m_util.str.is_string(b)) {
+                is_lower = true;
+                x = b;
+            }
+            else if (!m_util.str.is_string(a) && m_util.str.is_string(b, c)) {
+                is_lower = false;
+                x = a;
+            }
+        }
+        if (x && ctx.get_enode(x)) {
+            enode* x_root = ctx.get_enode(x)->get_root();
+            for (expr* p : m_lts) {
+                if (p == e)
+                    continue;
+                expr* pa = nullptr, *pb = nullptr;
+                zstring pc;
+                bool p_is_lower = false;
+                expr* px = nullptr;
+                if (!m_util.str.is_lt(p, pa, pb))
+                    continue;
+                literal p_lit = ctx.get_literal(p);
+                if (p_lit == true_literal || p_lit == false_literal || ctx.get_assignment(p_lit) != l_true)
+                    continue;
+                if (m_util.str.is_string(pa, pc) && !m_util.str.is_string(pb)) {
+                    p_is_lower = true;
+                    px = pb;
+                }
+                else if (!m_util.str.is_string(pa) && m_util.str.is_string(pb, pc)) {
+                    p_is_lower = false;
+                    px = pa;
+                }
+                if (!px || p_is_lower == is_lower || !ctx.get_enode(px))
+                    continue;
+                if (ctx.get_enode(px)->get_root() != x_root)
+                    continue;
+                zstring const& lower = is_lower ? c : pc;
+                zstring const& upper = is_lower ? pc : c;
+                if (!(lower < upper)) {
+                    literal_vector lits;
+                    lits.push_back(lit);
+                    lits.push_back(p_lit);
+                    set_conflict(nullptr, lits);
+                    return;
+                }
+            }
+        }
     }
     else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) {
         // no-op

src/test/seq_rewriter.cpp

@@ -15,6 +15,7 @@ Tests:
  17. Solver: (str.in_re x (re.range x x)) sat when len(x)=1
  18. Solver: (str.in_re x (re.range x x)) unsat when len(x)=2
  19. Solver: inverted symbolic bounds make membership unsatisfiable
+ 20. Solver: contradictory constant lexical bounds are unsatisfiable
 --*/
 
 #include "ast/arith_decl_plugin.h"
@@ -253,6 +254,23 @@ void tst_seq_rewriter() {
             std::cout << "symbolic range solver inverted bounds unsat: " << res << "\n";
             ENSURE(res == l_false);
         }
+
+        // 20. unsat: contradictory constant lexical bounds.
+        //     "2024-01-01" < x < "2024-12-31" and x < "2023-01-01".
+        {
+            smt_params sp;
+            smt::context ctx(m, sp);
+            app_ref x(m.mk_fresh_const("x", str_sort), m);
+            expr_ref b1(su.str.mk_string("2024-01-01"), m);
+            expr_ref b2(su.str.mk_string("2024-12-31"), m);
+            expr_ref b3(su.str.mk_string("2023-01-01"), m);
+            ctx.assert_expr(su.str.mk_lex_lt(b1, x));
+            ctx.assert_expr(su.str.mk_lex_lt(x, b2));
+            ctx.assert_expr(su.str.mk_lex_lt(x, b3));
+            lbool res = ctx.check();
+            std::cout << "constant lexical bounds unsat: " << res << "\n";
+            ENSURE(res == l_false);
+        }
     }
 
     std::cout << "tst_seq_rewriter: all tests passed\n";