some fixes

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

src/ast/rewriter/seq_rewriter.cpp

@@ -1146,7 +1146,7 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
 
     expr* es[2] = { a, b};
     expr* la = m_util.str.mk_length(a);
-    result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, m_autil.mk_int(0)), m().mk_not(m_autil.mk_ge(b, la))), 
+    result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, m_autil.mk_int(0)), m().mk_not(m_autil.mk_le(la, b))), 
                         m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_I, 2, es), 
                         m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_U, 2, es));
     return BR_REWRITE_FULL;

src/smt/seq_axioms.cpp

@@ -39,6 +39,13 @@ literal seq_axioms::mk_eq(expr* a, expr* b) {
     return th.mk_eq(a, b, false);
 }
 
+expr_ref seq_axioms::mk_sub(expr* x, expr* y) {
+    expr_ref result(a.mk_sub(x, y), m);
+    m_rewrite(result);
+    return result;
+}
+
+
 literal seq_axioms::mk_literal(expr* _e) {
     expr_ref e(_e, m);
     if (a.is_arith_expr(e)) {
@@ -510,7 +517,7 @@ void seq_axioms::add_itos_axiom(expr* e) {
     // itos(n) = "" or n >= 0
     add_axiom(~eq1, ~ge0);
     add_axiom(eq1, ge0);
-    add_axiom(mk_literal(a.mk_ge(mk_len(e), a.mk_int(0))));    
+    add_axiom(mk_literal(a.mk_ge(mk_len(e), zero)));    
     
     // n >= 0 => stoi(itos(n)) = n
     app_ref stoi(seq.str.mk_stoi(e), m);
@@ -519,9 +526,12 @@ void seq_axioms::add_itos_axiom(expr* e) {
     // itos(n) does not start with "0" when n > 0
     // n = 0 or at(itos(n),0) != "0"
     // alternative: n >= 0 => itos(stoi(itos(n))) = itos(n)
-    add_axiom(mk_eq(n, zero), 
-              ~mk_eq(seq.str.mk_at(e,zero), 
-                     seq.str.mk_string(symbol("0"))));
+    expr_ref zs(seq.str.mk_string(symbol("0")), m);
+    m_rewrite(zs);
+    literal eq0 = mk_eq(n, zero);
+    literal at0 = mk_eq(seq.str.mk_at(e, zero), zs);
+    add_axiom(eq0, ~at0);
+    add_axiom(~eq0, mk_eq(e, zs));
 }
 
 /**

src/smt/seq_axioms.h

@@ -42,7 +42,7 @@ namespace smt {
         literal mk_seq_eq(expr* a, expr* b) { SASSERT(seq.is_seq(a) && seq.is_seq(b)); return mk_literal(m_sk.mk_eq(a, b)); }
 
         expr_ref mk_len(expr* s) { return expr_ref(seq.str.mk_length(s), m); }
-        expr_ref mk_sub(expr* x, expr* y) { return expr_ref(a.mk_sub(x, y), m); }
+        expr_ref mk_sub(expr* x, expr* y);
         expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(seq.str.mk_concat(e1, e2, e3), m); }
         expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(seq.str.mk_concat(e1, e2), m); }
         expr_ref mk_nth(expr* e, expr* i) { return expr_ref(seq.str.mk_nth_i(e, i), m); }

src/smt/seq_skolem.cpp

@@ -12,6 +12,7 @@ Author:
 --*/
 
 #include "smt/seq_skolem.h"
+#include "ast/ast_pp.h"
 
 using namespace smt;
 
@@ -60,6 +61,8 @@ void seq_skolem::decompose(expr* e, expr_ref& head, expr_ref& tail) {
     expr* e1 = nullptr, *e2 = nullptr;
     zstring s;
     rational r;
+
+decompose_main:
     if (seq.str.is_empty(e)) {
         head = seq.str.mk_unit(seq.str.mk_nth(e, a.mk_int(0)));
         tail = e;
@@ -69,11 +72,13 @@ void seq_skolem::decompose(expr* e, expr_ref& head, expr_ref& tail) {
         tail = seq.str.mk_string(s.extract(1, s.length()-1));
     }
     else if (seq.str.is_unit(e)) {
-        head = e;
+        head = e;        
         tail = seq.str.mk_empty(m.get_sort(e));
+        m_rewrite(head);
     }
     else if (seq.str.is_concat(e, e1, e2) && seq.str.is_empty(e1)) {
-        decompose(e2, head, tail);
+        e = e2;
+        goto decompose_main;
     }
     else if (seq.str.is_concat(e, e1, e2) && seq.str.is_string(e1, s) && s.length() > 0) {
         head = seq.str.mk_unit(seq.str.mk_char(s, 0));
@@ -82,6 +87,8 @@ void seq_skolem::decompose(expr* e, expr_ref& head, expr_ref& tail) {
     else if (seq.str.is_concat(e, e1, e2) && seq.str.is_unit(e1)) {
         head = e1;
         tail = e2;
+        m_rewrite(head);
+        m_rewrite(tail);
     }
     else if (is_skolem(m_tail, e) && a.is_numeral(to_app(e)->get_arg(1), r)) {        
         expr* s = to_app(e)->get_arg(0);        
@@ -92,8 +99,9 @@ void seq_skolem::decompose(expr* e, expr_ref& head, expr_ref& tail) {
     }
     else {
         head = seq.str.mk_unit(seq.str.mk_nth(e, a.mk_int(0)));
-        m_rewrite(head);
         tail = mk(m_tail, e, a.mk_int(0));
+        m_rewrite(head);
+        m_rewrite(tail);
     }
 }
 

src/smt/theory_seq.cpp

@@ -5263,13 +5263,10 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
     return lit;
 }
 
-void theory_seq::push_lit_as_expr(literal l, expr_ref_vector& buf) {
-    expr* e = get_context().bool_var2expr(l.var());
-    if (l.sign()) e = m.mk_not(e);
-    buf.push_back(e);
-}
-
 void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) {
+    static unsigned s_count = 0;
+    ++s_count;
+    // SASSERT(s_count != 5);
     context& ctx = get_context();
     literal_vector lits;
     if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal || l5 == true_literal) return;

src/smt/theory_seq.h

@@ -602,7 +602,6 @@ namespace smt {
         // terms whose meaning are encoded using axioms.
         void enque_axiom(expr* e);
         void deque_axiom(expr* e);
-        void push_lit_as_expr(literal l, expr_ref_vector& buf);
         void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);        
         void add_length_axiom(expr* n);