add missing simplification; handle nit #6952

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Oct 25, 2023 · 7b49054 · 7b49054
1 parent 0859be5
commit 7b49054
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 15 deletions.
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -1245,6 +1245,15 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         result = str().mk_substr(a1, m_autil.mk_add(b1, b), m_autil.mk_sub(c1, b));
         return BR_REWRITE3;
     }
+    rational r1, r2;
+    if (str().is_extract(a, a1, b1, c1) &&
+        m_autil.is_numeral(b1, r1) && r1.is_unsigned() &&
+        m_autil.is_numeral(c1, r2) && r2.is_unsigned() &&
+        constantPos && constantLen &&
+        r1 == 0 && r2 >= pos + len) {        
+        result = str().mk_substr(a1, b, c);
+        return BR_REWRITE1;            
+    }
 
     if (str().is_extract(a, a1, b1, c1) && 
         is_prefix(a1, b1, c1) && is_prefix(a, b, c)) {

diff --git a/src/math/polynomial/rpolynomial.cpp b/src/math/polynomial/rpolynomial.cpp
@@ -658,9 +658,7 @@ namespace rpolynomial {
         void display(std::ostream & out, polynomial const * p, display_var_proc const & proc, bool use_star) {
             var x      = p->max_var();
             bool first = true;
-            unsigned i = p->size();
-            while (i > 0) {
-                --i;
+            for (unsigned i = p->size(); i-- > 0; ) {
                 poly_or_num * pn = p->arg(i);
                 if (pn == nullptr)
                     continue;
@@ -697,23 +695,19 @@ namespace rpolynomial {
                         display(out, to_poly(pn), proc, use_star);
                     }
                     else {
-                        bool add_paren = false;
-                        if (i > 0)
-                            add_paren = !is_monomial(to_poly(pn));
+                        bool add_paren = !is_monomial(to_poly(pn));
                         if (add_paren)
                             out << "(";
                         display(out, to_poly(pn), proc, use_star);
                         if (add_paren)
                             out << ")";
-                        if (i > 0) {
-                            if (use_star)
-                                out << "*";
-                            else
-                                out << " ";
-                            proc(out, x);
-                            if (i > 1)
-                                out << "^" << i;
-                        }
+                        if (use_star)
+                            out << "*";
+                        else
+                            out << " ";
+                        proc(out, x);
+                        if (i > 1)
+                            out << "^" << i;
                     }
                 }
             }