From 9ae3339c330d6cf827fc9beecc200bdc2b1ec675 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Feb 2021 12:33:13 -0800
Subject: [PATCH] fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_axioms.cpp   |  2 ++
 src/ast/rewriter/seq_rewriter.cpp | 16 +++++++++++-----
 src/ast/rewriter/seq_rewriter.h   |  2 +-
 src/util/rational.h               | 13 +++++++------
 4 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index e7a4da35c..8fabe8163 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -140,8 +140,10 @@ namespace seq {
             return;
         }
         if (is_extract_suffix(s, _i, _l)) {
+            extract_suffix_axiom(e, i, l);
             return;
         }
+        TRACE("seq", tout << s << " " << i << " " << l << "\n";);
         expr_ref x = m_sk.mk_pre(s, i);
         expr_ref ls = mk_len(_s);
         expr_ref lx = mk_len(x);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index f2b22f41b..01dccfe91 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -987,7 +987,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         return BR_DONE;
     }
 
-    unsigned len_a;
+    rational len_a;
     if (constantPos && max_length(a, len_a) && rational(len_a) <= pos) {
         result = str().mk_empty(a_sort);
         return BR_DONE;
@@ -1162,7 +1162,7 @@ bool seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, rational& pos) {
     else if (str().is_length(e, arg)) {
         lens.push_back(arg);
     }
-    else if (m_autil.is_mul(e, e1, e2) && m_autil.is_numeral(e1, pos1) && str().is_length(e2, arg) && pos1 <= 10) {
+    else if (m_autil.is_mul(e, e1, e2) && m_autil.is_numeral(e1, pos1) && str().is_length(e2, arg) && 0 <= pos1 && pos1 <= 10) {
         while (pos1 > 0) {
             lens.push_back(arg);
             pos1 -= rational(1);
@@ -4531,7 +4531,7 @@ bool seq_rewriter::min_length(expr_ref_vector const& es, unsigned& len) {
     return bounded;
 }
 
-bool seq_rewriter::max_length(expr* e, unsigned& len) {
+bool seq_rewriter::max_length(expr* e, rational& len) {
     if (str().is_unit(e)) {
         len = 1;
         return true;
@@ -4542,15 +4542,21 @@ bool seq_rewriter::max_length(expr* e, unsigned& len) {
     }
     zstring s;
     if (str().is_string(e, s)) {
-        len = s.length();
+        len = rational(s.length());
         return true;
     }
     if (str().is_empty(e)) {
         len = 0;
         return true;
     }
+    expr* s1 = nullptr, *i = nullptr, *l = nullptr;
+    rational n;
+    if (str().is_extract(e, s1, i, l) && m_autil.is_numeral(l, n) && !n.is_neg()) {
+        len = n;
+        return true;
+    }
     if (str().is_concat(e)) {
-        unsigned l = 0;
+        rational l(0);
         len = 0;
         for (expr* arg : *to_app(e)) {
             if (!max_length(arg, l))
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 314a83d4f..add0143da 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -282,7 +282,7 @@ class seq_rewriter {
     bool reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
     bool reduce_eq_empty(expr* l, expr* r, expr_ref& result);    
     bool min_length(expr_ref_vector const& es, unsigned& len);
-    bool max_length(expr* e, unsigned& len);
+    bool max_length(expr* e, rational& len);
     expr* concat_non_empty(expr_ref_vector& es);
 
     bool is_string(unsigned n, expr* const* es, zstring& s) const;
diff --git a/src/util/rational.h b/src/util/rational.h
index 7bf800294..6585fe5a7 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -482,11 +482,6 @@ inline bool operator<=(rational const & r1, rational const & r2) {
     return !operator>(r1, r2); 
 }
 
-inline bool operator<=(rational const & r1, int r2) { 
-    return r1 <= rational(r2);
-}
-
-
 inline bool operator>=(rational const & r1, rational const & r2) { 
     return !operator<(r1, r2); 
 }
@@ -499,7 +494,6 @@ inline bool operator>(int a, rational const & b) {
     return rational(a) > b;
 }
 
-
 inline bool operator>=(rational const& a, int b) {
     return a >= rational(b);
 }
@@ -508,6 +502,13 @@ inline bool operator>=(int a, rational const& b) {
     return rational(a) >= b;
 }
 
+inline bool operator<=(rational const& a, int b) {
+    return a <= rational(b);
+}
+
+inline bool operator<=(int a, rational const& b) {
+    return rational(a) <= b;
+}
 
 inline bool operator!=(rational const& a, int b) {
     return !(a == rational(b));