use theory agnostic axioms in more cases

src/ast/rewriter/seq_axioms.cpp

@@ -31,7 +31,8 @@ namespace seq {
         a(m),
         seq(m),
         m_sk(m, r),
-        m_clause(m)
+        m_clause(m),
+        m_trail(m)
     {}
 
     expr_ref axioms::mk_sub(expr* x, expr* y) {
@@ -45,10 +46,34 @@ namespace seq {
             return expr_ref(m);
         if (get_depth(e) == 1)
             return expr_ref(e, m);
-        expr_ref p = expr_ref(m.mk_fresh_const("seq.purify", e->get_sort()), m);
+        if (m.is_value(e))
+            return expr_ref(e, m);
+        expr_ref p(m);
+        expr* r = nullptr;
+        if (m_purified.find(e, r)) 
+            p = r;
+        else {
+            gc_purify();
+            p = expr_ref(m.mk_fresh_const("seq.purify", e->get_sort()), m);
+            m_purified.insert(e, p);
+            m_trail.push_back(e);
+            m_trail.push_back(p);
+        }
         add_clause(mk_eq(p, e));
         return expr_ref(p, m);
     }
+
+    void axioms::gc_purify() {
+        if (m_trail.size() != 4000)
+            return;
+        unsigned new_size = 2000;
+        expr_ref_vector new_trail(m, new_size, m_trail.c_ptr() + new_size);
+        m_purified.reset();
+        for (unsigned i = 0; i < new_size; i += 2) 
+            m_purified.insert(new_trail.get(i), new_trail.get(i + 1));
+        m_trail.reset();
+        m_trail.append(new_trail);
+    }
 
     expr_ref axioms::mk_len(expr* s) {
         expr_ref result(seq.str.mk_length(s), m); 
@@ -135,16 +160,14 @@ namespace seq {
             drop_last_axiom(e, s);
             return;
         }
-        if (is_extract_prefix0(s, _i, _l)) {
+        if (is_extract_prefix(s, _i, _l)) {
             extract_prefix_axiom(e, s, l);
             return;
         }
-#if 0
         if (is_extract_suffix(s, _i, _l)) {
             extract_suffix_axiom(e, s, i);
             return;
         }
-#endif
         TRACE("seq", tout << s << " " << i << " " << l << "\n";);
         expr_ref x = m_sk.mk_pre(s, i);
         expr_ref ls = mk_len(_s);
@@ -226,7 +249,7 @@ namespace seq {
         return l1 == l2;
     }
 
-    bool axioms::is_extract_prefix0(expr* s, expr* i, expr* l) {
+    bool axioms::is_extract_prefix(expr* s, expr* i, expr* l) {
         rational i1;
         return a.is_numeral(i, i1) && i1.is_zero();    
     }

src/ast/rewriter/seq_axioms.h

@@ -33,6 +33,8 @@ namespace seq {
         seq_util        seq;
         skolem          m_sk;
         expr_ref_vector m_clause;
+        expr_ref_vector m_trail;
+        obj_map<expr, expr*> m_purified;
         std::function<void(expr_ref_vector const&)> m_add_clause;
 
         expr_ref mk_len(expr* s);
@@ -49,6 +51,8 @@ namespace seq {
         expr_ref mk_ge(expr* x, rational const& n) { return expr_ref(a.mk_ge(x, a.mk_int(n)), m); }
         expr_ref mk_le(expr* x, rational const& n) { return expr_ref(a.mk_le(x, a.mk_int(n)), m); }
 
+        void gc_purify();
+
         expr_ref is_digit(expr* ch);
         expr_ref purify(expr* e);
         expr_ref mk_digit2int(expr* ch);
@@ -61,7 +65,7 @@ namespace seq {
 
         bool is_drop_last(expr* s, expr* i, expr* l);
         bool is_tail(expr* s, expr* i, expr* l);
-        bool is_extract_prefix0(expr* s, expr* i, expr* l);
+        bool is_extract_prefix(expr* s, expr* i, expr* l);
         bool is_extract_suffix(expr* s, expr* i, expr* l);
 
         void tail_axiom(expr* e, expr* s);

src/ast/rewriter/seq_rewriter.cpp

@@ -1147,6 +1147,13 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         return BR_REWRITE3;
     }
 
+    // extract(extract(a, 3, 6), 1, len(extract(a, 3, 6)) - 1) -> extract(a, 4, 5)
+    if (str().is_extract(a, a1, b1, c1) && is_suffix(a, b, c) && 
+        m_autil.is_numeral(c1) && m_autil.is_numeral(b1)) {
+        result = str().mk_substr(a1, m_autil.mk_add(b, b1), m_autil.mk_sub(c1, b));
+        return BR_REWRITE2;
+    }
+
     if (!constantPos) 
         return BR_FAILED;
 
@@ -1933,6 +1940,19 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE3;
     }
 
+    expr* a2 = nullptr, *a3 = nullptr;    
+    if (str().is_replace(a, a1, a2, a3) && a1 == a3 && a2 == b) {
+        // TBD: generalize to when a1 is a prefix of a3?
+        result = str().mk_prefix(a1, b);
+        return BR_DONE;
+    }
+
+    expr* b2 = nullptr, *b3 = nullptr;    
+    if (str().is_replace(b, b1, b2, b3) && b2 == a1 && str().is_empty(b3)) {
+        result = str().mk_prefix(str().mk_concat(a1, a1), b1);
+        return BR_REWRITE2;
+    }
+
     return BR_FAILED;    
 }
 
@@ -1995,6 +2015,14 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE3;
     }
 
+    expr* a1 = nullptr, *a2 = nullptr, *a3 = nullptr;    
+    if (str().is_replace(a, a1, a2, a3) && a1 == a3 && a2 == b) {
+        // TBD: generalize to when a1 is a prefix of a3?
+        result = str().mk_suffix(a1, b);
+        return BR_DONE;
+    }
+
+
     return BR_FAILED;
 }
 
@@ -2174,6 +2202,14 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
                             result);
         return BR_REWRITE_FULL;
     }
+    if (str().is_unit(as.get(0), u) && m_util.is_const_char(u, ch) && '0' == ch) {
+        result = str().mk_concat(as.size() - 1, as.c_ptr() + 1, as[0]->get_sort());
+        result = str().mk_stoi(result);
+        result = m().mk_ite(m_autil.mk_lt(result, m_autil.mk_int(0)),
+                            m_autil.mk_int(0),
+                            result);
+        return BR_REWRITE_FULL;
+    }
 
     return BR_FAILED;
 }