seq

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

scripts/mk_util.py

@@ -65,6 +65,7 @@ IS_WINDOWS=False
 IS_LINUX=False
 IS_OSX=False
 IS_FREEBSD=False
+IS_OPENBSD=False
 VERBOSE=True
 DEBUG_MODE=False
 SHOW_CPPS = True
@@ -126,6 +127,9 @@ def is_linux():
 def is_freebsd():
     return IS_FREEBSD
 
+def is_openbsd():
+    return IS_OPENBSD
+
 def is_osx():
     return IS_OSX
 
@@ -582,6 +586,8 @@ elif os.name == 'posix':
         IS_LINUX=True
     elif os.uname()[0] == 'FreeBSD':
         IS_FREEBSD=True
+    elif os.uname()[0] == 'OpenBSD':
+        IS_OPENBSD=True
 
 def display_help(exit_code):
     print("mk_make.py: Z3 Makefile generator\n")
@@ -1596,6 +1602,8 @@ class JavaDLLComponent(Component):
                 t = t.replace('PLATFORM', 'linux')
             elif IS_FREEBSD:
                 t = t.replace('PLATFORM', 'freebsd')
+            elif IS_OPENBSD:
+                t = t.replace('PLATFORM', 'openbsd')
             else:
                 t = t.replace('PLATFORM', 'win32')
             out.write(t)

src/ast/rewriter/seq_rewriter.cpp

@@ -510,3 +510,167 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
 br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
+
+br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
+    expr_ref_vector lhs(m()), rhs(m()), res(m());
+    if (!reduce_eq(l, r, lhs, rhs)) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    if (lhs.size() == 1 && lhs[0].get() == l && rhs[0].get() == r) {
+        return BR_FAILED;
+    }
+    for (unsigned i = 0; i < lhs.size(); ++i) {
+        res.push_back(m().mk_eq(lhs[i].get(), rhs[i].get()));
+    }
+    result = mk_and(res);
+    return BR_REWRITE3;
+}
+
+bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) {
+    expr* a, *b;
+    bool change = false;
+    expr_ref_vector trail(m());
+    m_lhs.reset();
+    m_rhs.reset();
+    m_util.str.get_concat(l, m_lhs);
+    m_util.str.get_concat(r, m_rhs);
+ 
+    // solve from back
+    while (!m_lhs.empty() && !m_rhs.empty()) {
+        if (m_lhs.back() == m_rhs.back()) {
+            m_lhs.pop_back();
+            m_rhs.pop_back();
+        }
+        else if(m_util.str.is_unit(m_lhs.back(), a) &&
+                m_util.str.is_unit(m_rhs.back(), b)) {
+            lhs.push_back(a);
+            rhs.push_back(b);
+            m_lhs.pop_back();
+            m_rhs.pop_back();
+        }
+        else if (!m_rhs.empty() && m_util.str.is_empty(m_rhs.back())) {
+            m_rhs.pop_back();
+        }
+        else if (!m_lhs.empty() && m_util.str.is_empty(m_lhs.back())) {
+            m_lhs.pop_back();
+        }
+        else {
+            break;
+        }
+        change = true;
+    }
+
+    // solve from front
+    unsigned head1 = 0, head2 = 0;
+    while (head1 < m_lhs.size() && head2 < m_rhs.size()) {
+        if (m_lhs[head1] == m_rhs[head2]) {
+            ++head1;
+            ++head2;
+        }
+        else if(m_util.str.is_unit(m_lhs[head1], a) &&
+                m_util.str.is_unit(m_rhs[head2], b)) {
+            lhs.push_back(a);
+            rhs.push_back(b);
+            ++head1;
+            ++head2;
+        }
+        else if (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) {
+            ++head1;
+        }
+        else if (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) {
+            ++head2;
+        }
+        else {
+            break;
+        }
+        change = true;
+    }
+    // reduce strings
+    std::string s1, s2;
+    if (head1 < m_lhs.size() && 
+        head2 < m_rhs.size() && 
+        m_util.str.is_string(m_lhs[head1], s1) &&
+        m_util.str.is_string(m_rhs[head2], s2)) {
+        size_t l = std::min(s1.length(), s2.length());
+        for (size_t i = 0; i < l; ++i) {
+            if (s1[i] != s2[i]) {
+                return false;
+            }
+        }
+        if (l == s1.length()) {
+            ++head1;            
+        }
+        else {
+            m_lhs[head1] = m_util.str.mk_string(std::string(s1.c_str()+l,s1.length()-l));
+            trail.push_back(m_lhs[head1]);
+        }
+        if (l == s2.length()) {
+            ++head2;            
+        }
+        else {
+            m_rhs[head2] = m_util.str.mk_string(std::string(s2.c_str()+l,s2.length()-l));
+            trail.push_back(m_rhs[head2]);
+        }
+        change = true;
+    }
+    if (head1 < m_lhs.size() && 
+        head2 < m_rhs.size() &&
+        m_util.str.is_string(m_lhs.back(), s1) &&
+        m_util.str.is_string(m_rhs.back(), s2)) {
+        size_t l = std::min(s1.length(), s2.length());
+        for (size_t i = 0; i < l; ++i) {
+            if (s1[s1.length()-i-1] != s2[s2.length()-i-1]) {
+                return false;
+            }
+        }
+        m_lhs.pop_back();          
+        m_rhs.pop_back();
+        if (l < s1.length()) {
+            m_lhs.push_back(m_util.str.mk_string(std::string(s1.c_str(),s1.length()-l)));
+            trail.push_back(m_lhs.back());
+        }
+        if (l < s2.length()) {
+            m_rhs.push_back(m_util.str.mk_string(std::string(s2.c_str(),s2.length()-l)));
+            trail.push_back(m_rhs.back());
+        }
+        change = true;
+    }
+    if (!change) {
+        lhs.push_back(l);
+        rhs.push_back(r);
+    }
+    else if (head1 == m_lhs.size() && head2 == m_rhs.size()) {
+        // skip
+    }
+    else if (head1 == m_lhs.size()) {
+        return set_empty(m_rhs.size() - head2, m_rhs.c_ptr() + head2, lhs, rhs);
+    }
+    else if (head2 == m_rhs.size()) {
+        return set_empty(m_lhs.size() - head1, m_lhs.c_ptr() + head1, lhs, rhs);
+    }
+    else { // head1 < m_lhs.size() && head2 < m_rhs.size() // could solve if either side is fixed size.
+        lhs.push_back(m_util.str.mk_concat(m_lhs.size() - head1, m_lhs.c_ptr() + head1));
+        rhs.push_back(m_util.str.mk_concat(m_rhs.size() - head2, m_rhs.c_ptr() + head2));
+    }
+    return true;
+}
+
+bool seq_rewriter::set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs) {
+    std::string s;
+    for (unsigned i = 0; i < sz; ++i) {
+        if (m_util.str.is_unit(es[i])) {
+            return false;
+        }
+        if (m_util.str.is_empty(es[i])) {
+            continue;
+        }
+        if (m_util.str.is_string(es[i], s)) {
+            SASSERT(s.length() > 0);
+            return false;
+        }
+        lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i])));
+        rhs.push_back(es[i]);
+    }
+    return true;
+}

src/ast/rewriter/seq_rewriter.h

@@ -32,7 +32,7 @@ Notes:
 class seq_rewriter {
     seq_util       m_util;
     arith_util     m_autil;
-    ptr_vector<expr> m_es;
+    ptr_vector<expr> m_es, m_lhs, m_rhs;
 
     br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_str_length(expr* a, expr_ref& result);
@@ -53,6 +53,7 @@ class seq_rewriter {
     br_status mk_re_plus(expr* a, expr_ref& result);
     br_status mk_re_opt(expr* a, expr_ref& result);
 
+    bool set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs);
 public:    
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         m_util(m), m_autil(m) {
@@ -64,6 +65,9 @@ public:
     static void get_param_descrs(param_descrs & r) {}
 
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+
+    bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs);
 
 };
 

src/ast/rewriter/th_rewriter.cpp

@@ -177,6 +177,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                     st = m_f_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_ar_rw.get_fid())
                     st = m_ar_rw.mk_eq_core(args[0], args[1], result);
+                else if (s_fid == m_seq_rw.get_fid())
+                    st = m_seq_rw.mk_eq_core(args[0], args[1], result);
                 
                 if (st != BR_FAILED)
                     return st;

src/ast/seq_decl_plugin.h

@@ -189,18 +189,19 @@ public:
         bool is_empty(expr const* n) const { symbol s; 
             return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); 
         }
-        bool is_concat(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
+        bool is_concat(expr const* n)   const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
-        bool is_length(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }
+        bool is_length(expr const* n)   const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }
         bool is_extract(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); }
-        bool is_contains(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); }
+        bool is_contains(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); }
-        bool is_at(expr const* n)      const { return is_app_of(n, m_fid, OP_SEQ_AT); }
+        bool is_at(expr const* n)       const { return is_app_of(n, m_fid, OP_SEQ_AT); }
-        bool is_stridof(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); }
+        bool is_stridof(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); }
-        bool is_repl(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_STRREPL); }
+        bool is_repl(expr const* n)     const { return is_app_of(n, m_fid, OP_STRING_STRREPL); }
-        bool is_prefix(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); }
+        bool is_prefix(expr const* n)   const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); }
-        bool is_suffix(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); }
+        bool is_suffix(expr const* n)   const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); }
-        bool is_itos(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
+        bool is_itos(expr const* n)     const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
-        bool is_stoi(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_STOI); }
+        bool is_stoi(expr const* n)     const { return is_app_of(n, m_fid, OP_STRING_STOI); }
-        bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
+        bool is_in_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
+        bool is_unit(expr const* n)     const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
 
         
         MATCH_BINARY(is_concat);
@@ -215,6 +216,7 @@ public:
         MATCH_UNARY(is_itos);
         MATCH_UNARY(is_stoi);
         MATCH_BINARY(is_in_re);        
+        MATCH_UNARY(is_unit);
 
         void get_concat(expr* e, ptr_vector<expr>& es) const;
         expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; }

src/smt/theory_seq.cpp

@@ -21,11 +21,13 @@ Revision History:
 #include "smt_context.h"
 #include "smt_model_generator.h"
 #include "theory_seq.h"
+#include "seq_rewriter.h"
 
 using namespace smt;
 
 theory_seq::theory_seq(ast_manager& m):
     theory(m.mk_family_id("seq")), 
+    m(m),
     m_rep(m),    
     m_eqs_head(0),
     m_ineqs(m),
@@ -43,7 +45,6 @@ theory_seq::theory_seq(ast_manager& m):
 
 final_check_status theory_seq::final_check_eh() { 
     context & ctx   = get_context();
-    ast_manager& m  = get_manager();
     final_check_status st = check_ineqs();
     if (st == FC_CONTINUE) {
         return FC_CONTINUE;
@@ -53,7 +54,6 @@ final_check_status theory_seq::final_check_eh() {
 
 final_check_status theory_seq::check_ineqs() {
     context & ctx   = get_context();
-    ast_manager& m  = get_manager();
     enode_pair_vector eqs;
     for (unsigned i = 0; i < m_ineqs.size(); ++i) {
         expr_ref a(m_ineqs[i].get(), m);
@@ -75,27 +75,58 @@ final_check_status theory_seq::check_ineqs() {
 
 bool theory_seq::simplify_eqs() {
     context & ctx   = get_context();
-    ast_manager& m  = get_manager();
     bool simplified = false;
     expr_array& lhs = m_lhs.back();
     expr_array& rhs = m_rhs.back();
-    for (unsigned i = m_eqs_head; i < m.size(lhs); ++i) {
+    for (unsigned i = 0; !ctx.inconsistent() && i < m.size(lhs); ++i) {
-        expr* l = m.get(lhs, i);
+        if (simplify_eq(m.get(lhs, i), m.get(rhs, i), m_deps)) {
-        expr* r = m.get(rhs, i);
+            if (i + 1 != m.size(lhs)) {
-#if 0
+                m.set(lhs, i, m.get(lhs, m.size(lhs)-1));
-        if (reduce(l, r)) {
+                m.set(rhs, i, m.get(rhs, m.size(rhs)-1));
-            ++m_eq_head;
+                --i;
+                simplified = true;
+            }
+            m.pop_back(lhs);
+            m.pop_back(rhs);
         }
-        else {
-            // equality is not simplified
-            // move forward pointer
-        }
-#endif
-    
     }
     return simplified;
 }
 
+bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) {
+    context& ctx = get_context();
+    seq_rewriter rw(m);
+    expr_ref_vector lhs(m), rhs(m);
+    SASSERT(ctx.e_internalized(l));
+    SASSERT(ctx.e_internalized(r));
+    expr_ref lh = canonize(l, deps);
+    expr_ref rh = canonize(r, deps);
+    if (!rw.reduce_eq(l, r, lhs, rhs)) {
+        // equality is inconsistent.
+        // create conflict assignment.  
+        expr_ref a(m);
+        a = m.mk_eq(l, r);
+        literal lit(ctx.get_literal(a));
+        ctx.assign(
+            ~lit,
+            ctx.mk_justification(
+                ext_theory_propagation_justification(
+                    get_id(), ctx.get_region(), 0, 0, deps.size(), deps.c_ptr(), ~lit)));
+        return true;
+    }
+    if (lhs.size() == 1 && l == lhs[0].get() &&
+        rhs.size() == 1 && r == rhs[0].get()) {
+        return false;
+    }
+    SASSERT(lhs.size() == rhs.size());
+    for (unsigned i = 0; i < lhs.size(); ++i) {
+        m.push_back(m_lhs.back(), lhs[i].get());
+        m.push_back(m_rhs.back(), rhs[i].get());
+        // TBD m_deps.push_back(deps);
+    }    
+    return true;
+}
+
 final_check_status theory_seq::add_axioms() {
     for (unsigned i = 0; i < get_num_vars(); ++i) {
 
@@ -111,7 +142,6 @@ bool theory_seq::internalize_atom(app* a, bool) {
 bool theory_seq::internalize_term(app* term) { 
     m_used = true;
     context & ctx   = get_context();
-    ast_manager& m  = get_manager();
     unsigned num_args = term->get_num_args();
     for (unsigned i = 0; i < num_args; i++) {
         ctx.internalize(term->get_arg(i), false);
@@ -154,7 +184,6 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_vector& eqs) {
 
 expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) {
     context& ctx = get_context();
-    ast_manager& m = get_manager();
     expr* e1, *e2;
     SASSERT(ctx.e_internalized(e));
     enode* n = ctx.get_enode(e);
@@ -200,7 +229,6 @@ expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) {
 
 void theory_seq::propagate() {
     context & ctx = get_context();
-    ast_manager& m  = get_manager();    
     while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
         expr_ref e(m);
         e = m_axioms[m_axioms_head].get();
@@ -216,7 +244,6 @@ void theory_seq::create_axiom(expr_ref& e) {
 
 void theory_seq::assert_axiom(expr_ref& e) {
     context & ctx = get_context();
-    ast_manager& m  = get_manager();    
     if (m.is_true(e)) return;
     TRACE("seq", tout << "asserting " << e << "\n";);
     ctx.internalize(e, false);
@@ -227,7 +254,6 @@ void theory_seq::assert_axiom(expr_ref& e) {
 }
 
 expr_ref theory_seq::mk_skolem(char const* name, expr* e1, expr* e2) {
-    ast_manager& m  = get_manager();    
     expr_ref result(m);
     sort* s = m.get_sort(e1);
     SASSERT(s == m.get_sort(e2));
@@ -249,7 +275,6 @@ void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) {
 
 void theory_seq::assign_eq(bool_var v, bool is_true) {
     context & ctx = get_context();
-    ast_manager& m  = get_manager();    
 
     enode* n = ctx.bool_var2enode(v);
     app*  e = n->get_owner();
@@ -286,7 +311,6 @@ void theory_seq::assign_eq(bool_var v, bool is_true) {
 }
 
 void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { 
-    ast_manager& m  = get_manager();    
     m_find.merge(v1, v2);
     expr_ref e1(m), e2(m);
     e1 = get_enode(v1)->get_owner();
@@ -296,7 +320,6 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
 }
 
 void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
-    ast_manager& m  = get_manager();    
     expr* e1 = get_enode(v1)->get_owner();
     expr* e2 = get_enode(v2)->get_owner();
     m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_ineqs));
@@ -304,7 +327,6 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
 }
 
 void theory_seq::push_scope_eh() {
-    ast_manager& m  = get_manager();    
     theory::push_scope_eh();
     m_trail_stack.push_scope();
     m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
@@ -317,7 +339,6 @@ void theory_seq::push_scope_eh() {
 }
 
 void theory_seq::pop_scope_eh(unsigned num_scopes) {
-    ast_manager& m  = get_manager();    
     m_trail_stack.pop_scope(num_scopes);
     theory::pop_scope_eh(num_scopes);    
     m_rep.resize(get_num_vars());
@@ -335,7 +356,6 @@ void theory_seq::restart_eh() {
 }
 
 void theory_seq::relevant_eh(app* n) {
-    ast_manager& m = get_manager();
     if (m_util.str.is_length(n)) {
         expr_ref e(m);
         e = m_autil.mk_le(m_autil.mk_numeral(rational(0), true), n);

src/smt/theory_seq.h

@@ -35,9 +35,12 @@ namespace smt {
             void reset() { memset(this, 0, sizeof(stats)); }
             unsigned m_num_splits;
         };
+        ast_manager&    m;
         expr_ref_vector m_rep;        // unification representative.
         vector<expr_array> m_lhs, m_rhs; // persistent sets of equalities.
         unsigned        m_eqs_head;      // index of unprocessed equation.
+        enode_pair_vector m_deps;    // TBD - convert to dependency structure.
+
 
         expr_ref_vector m_ineqs;      // inequalities to check
         expr_ref_vector m_axioms;     
@@ -68,6 +71,7 @@ namespace smt {
 
         final_check_status check_ineqs();
         bool simplify_eqs();
+        bool simplify_eq(expr* l, expr* r, enode_pair_vector& deps);
         final_check_status add_axioms();
 
         void assert_axiom(expr_ref& e);