move eq solver functionality to common place, fixes to goal2sat

src/ast/rewriter/seq_eq_solver.cpp

@@ -19,27 +19,44 @@ Author:
 
 namespace seq {
 
+    bool eq_solver::reduce(expr* s, expr* t, eq_ptr& r) {
+        expr_ref_vector ls(m), rs(m);
+        ls.push_back(s);
+        rs.push_back(t);
+        eqr e(ls, rs);
+        return reduce(e, r);
+    }
 
-    bool eq_solver::solve(eq const& e, eq_ptr& r) {
-        if (solve_itos1(e, r))
+    bool eq_solver::reduce(eqr const& e, eq_ptr& r) {
+        r = nullptr;
+        if (reduce_unit(e, r))
             return true;
-        if (solve_itos2(e, r))
+        if (reduce_itos1(e, r))
             return true;
-
+        if (reduce_itos2(e, r))
+            return true;
+        if (reduce_binary_eq(e, r))
+            return true;
+        
         return false;
     }
 
+    void eq_solver::set_conflict() {
+        m_clause.reset();
+        ctx.add_consequence(true, m_clause);
+    }
+
     void eq_solver::add_consequence(expr_ref const& a) {
         m_clause.reset();
         m_clause.push_back(a);
-        m_add_consequence(true, m_clause);
+        ctx.add_consequence(true, m_clause);
     }
 
     void eq_solver::add_consequence(expr_ref const& a, expr_ref const& b) {
         m_clause.reset();
         m_clause.push_back(a);
         m_clause.push_back(b);
-        m_add_consequence(true, m_clause);
+        ctx.add_consequence(true, m_clause);
     }
 
     /**
@@ -48,17 +65,16 @@ namespace seq {
      * s = t or (s < 0 and t < 0)
      */
         
-    bool eq_solver::match_itos1(eq const& e, expr*& a, expr*& b) {
+    bool eq_solver::match_itos1(eqr const& e, expr*& a, expr*& b) {
         return 
             e.ls.size() == 1 && e.rs.size() == 1 && 
             seq.str.is_itos(e.ls[0], a) && seq.str.is_itos(e.rs[0], b);
     }
 
-    bool eq_solver::solve_itos1(eq const& e, eq_ptr& r) {
+    bool eq_solver::reduce_itos1(eqr const& e, eq_ptr& r) {
         expr* s = nullptr, *t = nullptr;
         if (!match_itos1(e, s, t))
             return false;
-        r = nullptr;
         expr_ref eq = mk_eq(s, t);
         add_consequence(eq, mk_le(s, -1));
         add_consequence(eq, mk_le(t, -1));
@@ -71,7 +87,7 @@ namespace seq {
      *       s < 0
      */
     
-    bool eq_solver::match_itos2(eq const& e, expr*& s) {
+    bool eq_solver::match_itos2(eqr const& e, expr*& s) {
         if (e.ls.size() == 1 && e.rs.empty() && seq.str.is_itos(e.ls[0], s))
             return true;
         if (e.rs.size() == 1 && e.ls.empty() && seq.str.is_itos(e.rs[0], s))
@@ -79,14 +95,308 @@ namespace seq {
         return false;
     }
 
-    bool eq_solver::solve_itos2(eq const& e, eq_ptr& r) {
+    bool eq_solver::reduce_itos2(eqr const& e, eq_ptr& r) {
         expr* s = nullptr;
         if (!match_itos2(e, s))
             return false;
-        r = nullptr;
         add_consequence(mk_le(s, -1));
         return true;
     }
 
+    /**
+     *    x = t, where x does not occur in t.
+     */
+    bool eq_solver::reduce_unit(eqr const& e, eq_ptr& r) {
+        if (e.ls == e.rs) 
+            return true;
+        if (e.ls.size() == 1 && is_var(e.ls[0]) && !occurs(e.ls[0], e.rs)) {
+            expr_ref y(seq.str.mk_concat(e.rs, e.ls[0]->get_sort()), m);
+            ctx.add_solution(e.ls[0], y);
+            return true;
+        }
+        if (e.rs.size() == 1 && is_var(e.rs[0]) && !occurs(e.rs[0], e.ls)) {
+            expr_ref y(seq.str.mk_concat(e.ls, e.rs[0]->get_sort()), m);
+            ctx.add_solution(e.rs[0], y);
+            return true;
+        }
+        return false;
+    }
+
+
+    /**
+     * Equation is of the form x ++ xs = ys ++ x
+     * where |xs| = |ys| are units of same length
+     * then xs is a wrap-around of ys
+     * x ++ ab = ba ++ x
+     *
+     * When it is of the form x ++ a = b ++ x
+     * Infer that a = b
+     * It is also the case that x is a repetition of a's
+     * But this information is not exposed with this inference.
+     *
+     */
+    bool eq_solver::reduce_binary_eq(eqr const& e, eq_ptr& r) {
+        ptr_vector<expr> xs, ys;
+        expr_ref x(m), y(m);
+        if (!match_binary_eq(e, x, xs, ys, y))
+            return false;
+
+        if (xs.size() != ys.size()) {
+            set_conflict();
+            return true;
+        }
+        if (xs.empty()) 
+            return true;
+
+        if (xs.size() != 1)
+            return false;
+
+        if (ctx.expr2rep(xs[0]) == ctx.expr2rep(ys[0]))
+            return false;
+        expr_ref eq(m.mk_eq(xs[0], ys[0]), m);
+        expr* veq = ctx.expr2rep(eq);
+        if (m.is_true(veq)) 
+            return false;
+        add_consequence(eq);
+        return m.is_false(veq);
+    }
+
+
+    bool eq_solver::is_var(expr* a) const {
+        return
+            seq.is_seq(a) &&
+            !seq.str.is_concat(a) &&
+            !seq.str.is_empty(a)  &&
+            !seq.str.is_string(a) &&
+            !seq.str.is_unit(a) &&
+            !seq.str.is_itos(a) &&
+            !seq.str.is_nth_i(a) && 
+            !m.is_ite(a);
+    }
+
+    bool eq_solver::occurs(expr* a, expr_ref_vector const& b) {
+        for (auto const& elem : b) 
+            if (a == elem || m.is_ite(elem)) 
+                return true;        
+        return false;
+    }
+
+    bool eq_solver::occurs(expr* a, expr* b) {
+        // true if a occurs under an interpreted function or under left/right selector.
+        SASSERT(is_var(a));
+        SASSERT(m_todo.empty());
+        expr* e1 = nullptr, *e2 = nullptr;
+        m_todo.push_back(b);
+        while (!m_todo.empty()) {
+            b = m_todo.back();
+            if (a == b || m.is_ite(b)) {
+                m_todo.reset();
+                return true;
+            }
+            m_todo.pop_back();
+            if (seq.str.is_concat(b, e1, e2)) {
+                m_todo.push_back(e1);
+                m_todo.push_back(e2);
+            }
+            else if (seq.str.is_unit(b, e1)) {
+                m_todo.push_back(e1);
+            }
+            else if (seq.str.is_nth_i(b, e1, e2)) {
+                m_todo.push_back(e1);
+            }
+        }
+        return false;
+    }
+
+    void eq_solver::set_prefix(expr_ref& x, expr_ref_vector const& xs, unsigned sz) const {
+        SASSERT(0 < xs.size() && sz <= xs.size());
+        x = seq.str.mk_concat(sz, xs.c_ptr(), xs[0]->get_sort());
+    }
+
+    void eq_solver::set_suffix(expr_ref& x, expr_ref_vector const& xs, unsigned sz) const {
+        SASSERT(0 < xs.size() && sz <= xs.size());
+        x = seq.str.mk_concat(sz, xs.c_ptr() + xs.size() - sz, xs[0]->get_sort());
+    }
+
+    unsigned eq_solver::count_units_l2r(expr_ref_vector const& es, unsigned offset) const {
+        unsigned i = offset, sz = es.size();
+        for (; i < sz && seq.str.is_unit(es[i]); ++i) ;
+        return i - offset;                        
+    }
+
+    unsigned eq_solver::count_units_r2l(expr_ref_vector const& es, unsigned offset) const {
+        SASSERT(offset < es.size());
+        unsigned i = offset, count = 0;
+        do {
+            if (!seq.str.is_unit(es[i]))
+                break;
+            ++count;
+        }
+        while (i-- > 0);
+        return count;
+    }
+
+    unsigned eq_solver::count_non_units_l2r(expr_ref_vector const& es, unsigned offset) const {
+        unsigned i = offset, sz = es.size();
+        for (; i < sz && !seq.str.is_unit(es[i]); ++i) ;
+        return i - offset;                        
+    }
+
+    unsigned eq_solver::count_non_units_r2l(expr_ref_vector const& es, unsigned offset) const {
+        SASSERT(offset < es.size());
+        unsigned i = offset, count = 0;
+        do {
+            if (seq.str.is_unit(es[i]))
+                break;
+            ++count;
+        }
+        while (i-- > 0);
+        return count;
+    }
+
+    /**
+     * match: .. X abc  = Y .. Z def U
+     * where U is a variable or concatenation of variables
+     */
+
+    bool eq_solver::match_ternary_eq_r(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                                       expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+        if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {            
+            unsigned num_ls_units = count_units_r2l(ls, ls.size() - 1);
+            if (num_ls_units == 0 || num_ls_units == ls.size())
+                return false;
+            unsigned ls_units_offset = ls.size() - num_ls_units;
+            unsigned num_rs_non_units = count_non_units_r2l(rs, rs.size() - 1);
+            if (num_rs_non_units == rs.size())
+                return false;
+            SASSERT(num_rs_non_units > 0);
+            unsigned num_rs_units = count_units_r2l(rs, rs.size() - 1 - num_rs_non_units);
+            if (num_rs_units == 0)
+                return false;
+            set_prefix(x,   ls, ls.size() - num_ls_units);
+            set_suffix(xs,  ls, num_ls_units);
+            unsigned offset = rs.size() - num_rs_non_units - num_rs_units;
+            set_prefix(y1,  rs, offset);
+            set_extract(ys, rs, offset, num_rs_units);
+            set_suffix(y2,  rs, num_rs_non_units);
+            return true;
+        }
+        return false;
+    }
+
+    bool eq_solver::match_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                                         expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+        if (match_ternary_eq_r(ls, rs, x, xs, y1, ys, y2))
+            return true;
+        if (match_ternary_eq_r(rs, ls, x, xs, y1, ys, y2))
+            return true;
+        return false;
+    }
+    
+    /*
+      match: abc X ..  = Y def Z ..
+         where Y is a variable or concatenation of variables
+    */
+
+    bool eq_solver::match_ternary_eq_l(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                                       expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+        if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+            unsigned num_ls_units = count_units_l2r(ls, 0);
+            if (num_ls_units == 0 || num_ls_units == ls.size())
+                return false;
+            unsigned num_rs_non_units = count_non_units_l2r(rs, 0);
+            if (num_rs_non_units == rs.size() || num_rs_non_units == 0)
+                return false;
+            unsigned num_rs_units = count_units_l2r(rs, num_rs_non_units);
+            if (num_rs_units == 0)
+                return false;
+            set_prefix(xs,  ls, num_ls_units);
+            set_suffix(x,   ls, ls.size() - num_ls_units);
+            set_prefix(y1,  rs, num_rs_non_units);
+            set_extract(ys, rs, num_rs_non_units, num_rs_units);
+            set_suffix(y2,  rs, rs.size() - num_rs_non_units - num_rs_units);
+            return true;
+        }
+        return false;
+    }
+
+    bool eq_solver::match_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                                         expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+        if (match_ternary_eq_l(ls, rs, xs, x, y1, ys, y2))
+            return true;
+        if (match_ternary_eq_l(rs, ls, xs, x, y1, ys, y2))
+            return true;
+        return false;
+    }
+
+
+    bool eq_solver::all_units(expr_ref_vector const& es, unsigned start, unsigned end) const {
+        for (unsigned i = start; i < end; ++i) 
+            if (!seq.str.is_unit(es[i])) 
+                return false;
+        return true;
+    }
+
+    /**
+       match X abc = defg Y, for abc, defg non-empty
+    */
+    
+    bool eq_solver::match_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                                    expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
+        if (ls.size() > 1 && is_var(ls[0]) &&
+            rs.size() > 1 && is_var(rs.back()) &&
+            all_units(ls, 1, ls.size()) &&
+            all_units(rs, 0, rs.size() - 1)) {
+            x = ls[0];
+            y = rs.back();
+            set_suffix(xs, ls, ls.size() - 1);
+            set_prefix(ys, rs, rs.size() - 1);
+            return true;
+        }
+        return false;
+    }
+
+    bool eq_solver::match_binary_eq(eqr const& e, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
+        if (match_binary_eq(e.ls, e.rs, x, xs, ys, y) && x == y)
+            return true;
+        if (match_binary_eq(e.rs, e.ls, x, xs, ys, y) && x == y)
+            return true;
+        return false;
+    }
+
+    /**
+     * match: X abc Y..Y' = Z def T..T', where X,Z are variables or concatenation of variables
+     */
+
+    bool eq_solver::match_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
+                                  expr_ref& x1, expr_ref_vector& xs, expr_ref& x2,
+                                  expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+        if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
+            rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+            unsigned ls_non_unit = count_non_units_l2r(ls, 0);
+            unsigned rs_non_unit = count_non_units_l2r(rs, 0);
+            if (ls_non_unit == ls.size())
+                return false;
+            if (rs_non_unit == rs.size())
+                return false;
+            unsigned ls_unit = count_units_l2r(ls, ls_non_unit);
+            unsigned rs_unit = count_units_l2r(rs, rs_non_unit);
+            if (ls_unit == 0)
+                return false;
+            if (rs_unit == 0)
+                return false;
+            set_prefix(x1,  ls, ls_non_unit);
+            set_extract(xs, ls, ls_non_unit, ls_unit);
+            set_suffix(x2,  ls, ls.size() - ls_non_unit - ls_unit);
+            set_prefix(y1,  rs, rs_non_unit);
+            set_extract(ys, rs, rs_non_unit, rs_unit);
+            set_suffix(y2,  rs, rs.size() - rs_non_unit - rs_unit);
+            return true;
+        }
+        return false;
+    }
+
+
+
 };
 

src/ast/rewriter/seq_eq_solver.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Solver-agnostic equality solving routines for sequences
+    Solver core-agnostic equality inference routines for sequences
     
 Author:
 
@@ -27,23 +27,73 @@ namespace seq {
             ls(l), rs(r) {}
     };
 
+    struct eqr {
+        expr_ref_vector const& ls;
+        expr_ref_vector const& rs;
+        eqr(expr_ref_vector const& l, expr_ref_vector const& r):
+            ls(l), rs(r) {}
+    };
+
     typedef scoped_ptr<eq> eq_ptr;
+
+    class eq_solver_context {
+    public:
+        virtual void  add_consequence(bool uses_dep, expr_ref_vector const& clause) = 0;
+        virtual void  add_solution(expr* var, expr* term) = 0;
+        virtual expr* expr2rep(expr* e) = 0;
+        virtual bool  get_length(expr* e, rational& r) = 0;
+    };
         
     class eq_solver {
-        ast_manager& m;
-        axioms&      m_ax;
-        seq_util     seq;
-        expr_ref_vector                        m_clause;
-        std::function<expr*(expr*)>            m_value;
-        std::function<bool(expr*, rational&)>  m_int_value;
-        std::function<void(bool, expr_ref_vector const&)>  m_add_consequence;
+        ast_manager&       m;
+        eq_solver_context& ctx;
+        axioms&            m_ax;
+        seq_util           seq;
+        expr_ref_vector    m_clause;
 
-        bool match_itos1(eq const& e, expr*& s, expr*& t);
-        bool solve_itos1(eq const& e, eq_ptr& r);
+        bool reduce_unit(eqr const& e, eq_ptr& r);
 
-        bool match_itos2(eq const& e, expr*& s);
-        bool solve_itos2(eq const& e, eq_ptr& r);
+        bool match_itos1(eqr const& e, expr*& s, expr*& t);
+        bool reduce_itos1(eqr const& e, eq_ptr& r);
 
+        bool match_itos2(eqr const& e, expr*& s);
+        bool reduce_itos2(eqr const& e, eq_ptr& r);
+
+        bool match_binary_eq(eqr const& e, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y);
+        bool reduce_binary_eq(eqr const& e, eq_ptr& r);
+
+        bool match_ternary_eq_r(expr_ref_vector const& ls, expr_ref_vector const& rs,
+                                expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
+
+        bool match_ternary_eq_l(expr_ref_vector const& ls, expr_ref_vector const& rs,
+                                expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
+
+
+        /**
+         * count unit or non-unit entries left-to-right or right-to-left starting at, and including offset.
+         */
+        unsigned count_units_l2r(expr_ref_vector const& es, unsigned offset) const;
+        unsigned count_units_r2l(expr_ref_vector const& es, unsigned offset) const;
+        unsigned count_non_units_l2r(expr_ref_vector const& es, unsigned offset) const;
+        unsigned count_non_units_r2l(expr_ref_vector const& es, unsigned offset) const;
+
+        void set_prefix(expr_ref& x, expr_ref_vector const& xs, unsigned sz) const;
+        void set_suffix(expr_ref& x, expr_ref_vector const& xs, unsigned sz) const;
+
+        template<typename V>
+        void set_prefix(V& dst, expr_ref_vector const& xs, unsigned sz) const { set_extract(dst, xs, 0, sz); }
+
+        template<typename V>
+        void set_suffix(V& dst, expr_ref_vector const& xs, unsigned sz) const { set_extract(dst, xs, xs.size() - sz, sz); }
+
+        template<typename V> 
+        void set_extract(V& dst, expr_ref_vector const& xs, unsigned offset, unsigned sz) const {
+            SASSERT(offset + sz <= xs.size());
+            dst.reset();
+            dst.append(sz, xs.c_ptr() + offset);
+        }
+
+        void set_conflict();
         void add_consequence(expr_ref const& a);
         void add_consequence(expr_ref const& a, expr_ref const& b);
 
@@ -53,21 +103,40 @@ namespace seq {
         expr_ref mk_ge(expr* x, rational const& n) { return m_ax.mk_ge(x, n); }
         expr_ref mk_le(expr* x, rational const& n) { return m_ax.mk_le(x, n); }
 
+        ptr_vector<expr> m_todo;
+        bool occurs(expr* a, expr_ref_vector const& b);
+        bool occurs(expr* a, expr* b);
+
+        bool all_units(expr_ref_vector const& es, unsigned start, unsigned end) const;
+
     public:
         
-        eq_solver(ast_manager& m, axioms& ax):
+        eq_solver(ast_manager& m, eq_solver_context& ctx, axioms& ax):
             m(m),
+            ctx(ctx),
             m_ax(ax),
             seq(m),
             m_clause(m)
         {}
 
-        void set_value(std::function<expr*(expr*)>& v) { m_value = v; }
-        void set_int_value(std::function<bool(expr*,rational&)>& iv) { m_int_value = iv; }
-        void set_add_consequence(std::function<void(bool, expr_ref_vector const&)>& ac) { m_add_consequence = ac; }
+        bool reduce(eqr const& e, eq_ptr& r);
 
-        bool solve(eq const& e, eq_ptr& r);
+        bool reduce(expr* s, expr* t, eq_ptr& r);
 
+        bool is_var(expr* a) const;
+
+        bool match_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                             expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y);
+
+        bool match_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs,
+                                  expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
+
+        bool match_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs,
+                                  expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
+
+        bool match_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
+                           expr_ref& x1, expr_ref_vector& xs, expr_ref& x2,
+                           expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
         
     };
 

src/sat/tactic/goal2sat.cpp

@@ -257,8 +257,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_num_scopes = 0;
         m_map.pop(n);
         unsigned k = m_cache_lim[m_cache_lim.size() - n];
-        for (; k-- > m_cache_trail.size(); ) {
-            app* t = m_cache_trail[k];
+        for (unsigned i = m_cache_trail.size(); i-- > k; ) {
+            app* t = m_cache_trail[i];
             sat::literal lit;
             if (m_app2lit.find(t, lit)) {
                 m_app2lit.remove(t);

src/smt/seq_eq_solver.cpp

@@ -60,56 +60,41 @@ bool theory_seq::solve_eq(unsigned idx) {
         TRACE("seq", tout << "simplified\n";);
         return true;
     }
+
     if (!ctx.inconsistent() && lift_ite(ls, rs, deps)) {
         return true;
     }
+    seq::eq_ptr r;
+    m_eq_deps = deps;
+    seq::eqr er(ls, rs);
+    if (!ctx.inconsistent() && m_eq.reduce(er, r)) {
+        if (!r) 
+            return true;
+        m_eqs.set(idx, depeq(m_eq_id++, r->ls, r->rs, deps));
+        return false;
+    }
+
     TRACE("seq_verbose", tout << ls << " = " << rs << "\n";);
-    if (ls.empty() && rs.empty()) {
-        return true;
-    }
-    if (!ctx.inconsistent() && solve_unit_eq(ls, rs, deps)) {
-        TRACE("seq", tout << "unit\n";);
-        return true;
-    }
-    if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) {
-        TRACE("seq", tout << "binary\n";);
-        return true;
-    }
     if (!ctx.inconsistent() && solve_nth_eq1(ls, rs, deps)) {
         return true;
     }
     if (!ctx.inconsistent() && solve_nth_eq1(rs, ls, deps)) {
         return true;
     }
-    seq::eq_ptr r;
-    m_eq_deps = deps;
-    if (!ctx.inconsistent() && m_eq.solve(e, r)) {
-        if (!r) 
-            return true;
-        m_eqs.set(idx, depeq(m_eq_id++, r->ls, r->rs, deps));
-        return false;
-    }
     if (!ctx.inconsistent() && solve_itos(rs, ls, deps)) {
         return true;
     }
     if (!ctx.inconsistent() && change) {
         // The propagation step from arithmetic state (e.g. length offset) to length constraints
         TRACE("seq", tout << "inserting equality\n";);
-        expr_ref_vector new_ls(m);
-        if (!m_offset_eq.empty() && find_better_rep(ls, rs, idx, deps, new_ls)) {
-            // Find a better equivalent term for lhs of an equation based on length constraints            
-            m_eqs.push_back(depeq(m_eq_id++, new_ls, rs, deps));
-            return true;
-        }
-        else {
-            m_eqs.set(idx, depeq(m_eq_id++, ls, rs, deps));
-        }
+        m_eqs.set(idx, depeq(m_eq_id++, ls, rs, deps));        
     }
     return false;
 }
 
 void theory_seq::add_consequence(bool uses_eq, expr_ref_vector const& clause) {
     dependency* dep = uses_eq ? m_eq_deps : nullptr;
+    m_new_propagation = true;
     if (clause.size() == 1) {
         propagate_lit(dep, 0, nullptr, mk_literal(clause[0]));
         return;
@@ -126,118 +111,24 @@ void theory_seq::add_consequence(bool uses_eq, expr_ref_vector const& clause) {
     add_axiom(lits);
 }
 
-bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
-    if (l == r) {
-        return true;
-    }
-    if (is_var(l) && !occurs(l, r) && add_solution(l, r, deps)) {
-        return true;
-    }
-    if (is_var(r) && !occurs(r, l) && add_solution(r, l, deps)) {
-        return true;
-    }
-    return false;
-}
-
-bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
-    if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, l[0]->get_sort()), deps)) {
-        return true;
-    }
-    if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, r[0]->get_sort()), deps)) {
-        return true;
-    }
-    return false;
-}
-
-bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
-    ptr_vector<expr> xs, ys;
-    expr_ref x(m), y(m);
-    if (!is_binary_eq(ls, rs, x, xs, ys, y) &&
-        !is_binary_eq(rs, ls, x, xs, ys, y)) {
-        return false;
-    }
-    // Equation is of the form x ++ xs = ys ++ y
-    // where xs, ys are units.
-    if (x != y) {
-        return false;
-    }
-    if (xs.size() != ys.size()) {
-        TRACE("seq", tout << "binary conflict\n";);
-        set_conflict(dep);
-        return false;
-    }
-    if (xs.empty()) {
-        // this should have been solved already
-        UNREACHABLE();
-        return false;
-    }
-
-    // Equation is of the form x ++ xs = ys ++ x
-    // where |xs| = |ys| are units of same length
-    // then xs is a wrap-around of ys
-    // x ++ ab = ba ++ x
-    // 
-    if (xs.size() == 1) {
-        enode* n1 = ensure_enode(xs[0]);
-        enode* n2 = ensure_enode(ys[0]);
-        if (n1->get_root() == n2->get_root()) {
-            return false;
-        }
-        literal eq = mk_eq(xs[0], ys[0], false);
-        switch (ctx.get_assignment(eq)) {
-        case l_false: {
-            literal_vector conflict;
-            conflict.push_back(~eq);
-            TRACE("seq", tout << conflict << "\n";);
-            set_conflict(dep, conflict);
-            break;
-        }
+expr* theory_seq::expr2rep(expr* e) { 
+    if (m.is_bool(e) && ctx.b_internalized(e)) {
+        bool_var b = ctx.get_bool_var(e);
+        switch (ctx.get_assignment(b)) {
         case l_true:
-            break;
-        case l_undef: 
-            propagate_lit(dep, 0, nullptr, eq);
-            m_new_propagation = true;
+            return m.mk_true();
+        case l_false:
+            return m.mk_false();
+        default:
             break;
         }
-    }
-    return false;
+    }        
+    if (!ctx.e_internalized(e))
+        return e;
+    return ctx.get_enode(e)->get_root()->get_expr();
 }
 
 
-bool theory_seq::occurs(expr* a, expr_ref_vector const& b) {
-    for (auto const& elem : b) {
-        if (a == elem || m.is_ite(elem)) return true;
-    }
-    return false;
-}
-
-bool theory_seq::occurs(expr* a, expr* b) {
-     // true if a occurs under an interpreted function or under left/right selector.
-    SASSERT(is_var(a));
-    SASSERT(m_todo.empty());
-    expr* e1 = nullptr, *e2 = nullptr;
-    m_todo.push_back(b);
-    while (!m_todo.empty()) {
-        b = m_todo.back();
-        if (a == b || m.is_ite(b)) {
-            m_todo.reset();
-            return true;
-        }
-        m_todo.pop_back();
-        if (m_util.str.is_concat(b, e1, e2)) {
-            m_todo.push_back(e1);
-            m_todo.push_back(e2);
-        }
-        else if (m_util.str.is_unit(b, e1)) {
-            m_todo.push_back(e1);
-        }
-        else if (m_util.str.is_nth_i(b, e1, e2)) {
-            m_todo.push_back(e1);
-        }
-    }
-    return false;
-}
-
 /**
    \brief
 
@@ -270,6 +161,7 @@ bool theory_seq::occurs(expr* a, expr* b) {
    TODO: propagate length offsets for last vars
 
 */
+#if 0
 bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx,
                                  dependency*& deps, expr_ref_vector & res) {
 
@@ -346,6 +238,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
     }
     return false;
 }
+#endif
 
 bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & offset) {
 
@@ -380,29 +273,9 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
 }
 
 bool theory_seq::len_based_split() {
-
-    if (false && m_offset_eq.propagate() && !m_offset_eq.empty()) {
-        // NB: disabled until find_better_rep is handled.
-#if 0
-        for (unsigned i = m_eqs.size(); i-- > 0; ) {
-            eq const& e = m_eqs[i];
-            expr_ref_vector new_ls(m);
-            dependency *deps = e.dep();
-            if (find_better_rep(e.ls, e.rs, i, deps, new_ls)) {
-                expr_ref_vector rs(m);
-                rs.append(e.rs);
-                m_eqs.set(i, eq(m_eq_id++, new_ls, rs, deps));
-                TRACE("seq", display_equation(tout, m_eqs[i]););
-            }
-        }
-#endif
-    }
-
-    for (auto const& e : m_eqs) {
-        if (len_based_split(e)) {
+    for (auto const& e : m_eqs) 
+        if (len_based_split(e)) 
             return true;
-        }
-    }
     return false;
 }
 
@@ -670,8 +543,8 @@ bool theory_seq::branch_binary_variable(depeq const& e) {
     }
     ptr_vector<expr> xs, ys;
     expr_ref x(m), y(m);
-    if (!is_binary_eq(e.ls, e.rs, x, xs, ys, y) &&
-        !is_binary_eq(e.rs, e.ls, x, xs, ys, y))
+    if (!m_eq.match_binary_eq(e.ls, e.rs, x, xs, ys, y) &&
+        !m_eq.match_binary_eq(e.rs, e.ls, x, xs, ys, y))
         return false;
     if (x == y) {
         return false;
@@ -889,10 +762,8 @@ bool theory_seq::can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector c
 bool theory_seq::branch_ternary_variable_rhs(depeq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x(m), y1(m), y2(m);
-    if (!is_ternary_eq_rhs(e.ls, e.rs, x, xs, y1, ys, y2) &&
-        !is_ternary_eq_rhs(e.rs, e.ls, x, xs, y1, ys, y2)) {
+    if (!m_eq.match_ternary_eq_rhs(e.ls, e.rs, x, xs, y1, ys, y2))
         return false;
-    }
     if (m_sk.is_align_l(y1) || m_sk.is_align_r(y1))
         return false;
 
@@ -933,8 +804,7 @@ bool theory_seq::branch_ternary_variable_rhs(depeq const& e) {
 bool theory_seq::branch_ternary_variable_lhs(depeq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x(m), y1(m), y2(m);
-    if (!is_ternary_eq_lhs(e.ls, e.rs, xs, x, y1, ys, y2) &&
-        !is_ternary_eq_lhs(e.rs, e.ls, xs, x, y1, ys, y2))
+    if (!m_eq.match_ternary_eq_lhs(e.ls, e.rs, xs, x, y1, ys, y2))
         return false;
     if (m_sk.is_align_l(y1) || m_sk.is_align_r(y1))
         return false;
@@ -998,7 +868,7 @@ literal theory_seq::mk_alignment(expr* e1, expr* e2) {
 bool theory_seq::branch_quat_variable(depeq const& e) {
     expr_ref_vector xs(m), ys(m);
     expr_ref x1(m), x2(m), y1(m), y2(m);
-    if (!is_quat_eq(e.ls, e.rs, x1, xs, x2, y1, ys, y2))
+    if (!m_eq.match_quat_eq(e.ls, e.rs, x1, xs, x2, y1, ys, y2))
         return false;
     dependency* dep = e.dep();
 
@@ -1478,150 +1348,7 @@ bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
     }
     return true;
 }
-
-/**
-   match X abc = defg Y, for abc, defg non-empty
-*/
-
-bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
-    if (ls.size() > 1 && is_var(ls[0]) &&
-        rs.size() > 1 && is_var(rs.back())) {
-        xs.reset();
-        ys.reset();
-        x = ls[0];
-        y = rs.back();
-        for (unsigned i = 1; i < ls.size(); ++i) {
-            if (!m_util.str.is_unit(ls[i])) return false;
-        }
-        for (unsigned i = 0; i < rs.size()-1; ++i) {
-            if (!m_util.str.is_unit(rs[i])) return false;
-        }
-        xs.append(ls.size()-1, ls.c_ptr() + 1);
-        ys.append(rs.size()-1, rs.c_ptr());
-        return true;
-    }
-    return false;
-}
-
-/*
-  match: X abc Y..Y' = Z def T..T', where X,Z are variables or concatenation of variables
-*/
-
-bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
-                            expr_ref& x1, expr_ref_vector& xs, expr_ref& x2,
-                            expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
-    if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
-        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
-        unsigned l_start = 1;
-        sort* srt = ls[0]->get_sort();
-        for (; l_start < ls.size()-1; ++l_start) {
-            if (m_util.str.is_unit(ls[l_start])) break;
-        }
-        if (l_start == ls.size()-1) return false;
-        unsigned l_end = l_start;
-        for (; l_end < ls.size()-1; ++l_end) {
-            if (!m_util.str.is_unit(ls[l_end])) break;
-        }
-        --l_end;
-        if (l_end < l_start) return false;
-        unsigned r_start = 1;
-        for (; r_start < rs.size()-1; ++r_start) {
-            if (m_util.str.is_unit(rs[r_start])) break;
-        }
-        if (r_start == rs.size()-1) return false;
-        unsigned r_end = r_start;
-        for (; r_end < rs.size()-1; ++r_end) {
-            if (!m_util.str.is_unit(rs[r_end])) break;
-        }
-        --r_end;
-        if (r_end < r_start) return false;
-        xs.reset();
-        xs.append(l_end-l_start+1, ls.c_ptr()+l_start);
-        x1 = mk_concat(l_start, ls.c_ptr(), srt);
-        x2 = mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1, srt);
-        ys.reset();
-        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
-        y1 = mk_concat(r_start, rs.c_ptr(), srt);
-        y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
-        return true;
-    }
-    return false;
-}
-
-/*
-  match: .. X abc  = .. Y def Z
-         where Z is a variable or concatenation of variables
-*/
-
-bool theory_seq::is_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                               expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
-    if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
-        sort* srt = ls[0]->get_sort();
-        unsigned l_start = ls.size()-1;
-        for (; l_start > 0; --l_start) {
-            if (!m_util.str.is_unit(ls[l_start])) break;
-        }
-        if (l_start == ls.size()-1) return false;
-        ++l_start;
-        unsigned r_end = rs.size()-2;
-        for (; r_end > 0; --r_end) {
-            if (m_util.str.is_unit(rs[r_end])) break;
-        }
-        if (r_end == 0) return false;
-        unsigned r_start = r_end;
-        for (; r_start > 0; --r_start) {
-            if (!m_util.str.is_unit(rs[r_start])) break;
-        }
-        ++r_start;
-
-        xs.reset();
-        xs.append(ls.size()-l_start, ls.c_ptr()+l_start);
-        x = mk_concat(l_start, ls.c_ptr(), srt);
-        ys.reset();
-        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
-        y1 = mk_concat(r_start, rs.c_ptr(), srt);
-        y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
-        return true;
-    }
-    return false;
-}
-
-/*
-  match: abc X ..  = Y def Z ..
-         where Y is a variable or concatenation of variables
-*/
-
-bool theory_seq::is_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                                expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
-    if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
-        sort* srt = ls[0]->get_sort();
-        unsigned l_start = 0;
-        for (; l_start < ls.size()-1; ++l_start) {
-            if (!m_util.str.is_unit(ls[l_start])) break;
-        }
-        if (l_start == 0) return false;
-        unsigned r_start = 1;
-        for (; r_start < rs.size()-1; ++r_start) {
-            if (m_util.str.is_unit(rs[r_start])) break;
-        }
-        if (r_start == rs.size()-1) return false;
-        unsigned r_end = r_start;
-        for (; r_end < rs.size()-1; ++r_end) {
-            if (!m_util.str.is_unit(rs[r_end])) break;
-        }
-        --r_end;
-
-        xs.reset();
-        xs.append(l_start, ls.c_ptr());
-        x = mk_concat(ls.size()-l_start, ls.c_ptr()+l_start, srt);
-        ys.reset();
-        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
-        y1 = mk_concat(r_start, rs.c_ptr(), srt);
-        y2 = mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1, srt);
-        return true;
-    }
-    return false;
-}
+ 
 
 struct remove_obj_pair_map : public trail {
     obj_pair_hashtable<expr, expr> & m_map;

src/smt/theory_seq.cpp

@@ -272,7 +272,7 @@ theory_seq::theory_seq(context& ctx):
     m_autil(m),
     m_sk(m, m_rewrite),
     m_ax(*this, m_rewrite),
-    m_eq(m, m_ax.ax()),
+    m_eq(m, *this, m_ax.ax()),
     m_regex(*this),
     m_arith_value(m),
     m_trail_stack(*this),
@@ -285,13 +285,6 @@ theory_seq::theory_seq(context& ctx):
     m_has_seq(m_util.has_seq()),
     m_new_solution(false),
     m_new_propagation(false) {
-
-    std::function<void(bool, expr_ref_vector const&)> _add_consequence = 
-        [&](bool uses_eq, expr_ref_vector const& clause) { 
-        add_consequence(uses_eq, clause);
-    };
-
-    m_eq.set_add_consequence(_add_consequence);
 }
 
 theory_seq::~theory_seq() {
@@ -913,8 +906,12 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
             break;
         expr_ref li(p.first, m);
         expr_ref ri(p.second, m);
-        if (solve_unit_eq(li, ri, deps)) {
-            // no-op
+        seq::eq_ptr r;
+        m_eq_deps = deps;
+        if (m_eq.reduce(li, ri, r)) {
+            if (r) {
+                m_eqs.push_back(mk_eqdep(r->ls, r->rs, deps));
+            }
         }
         else if (m_util.is_seq(li) || m_util.is_re(li)) {
             TRACE("seq_verbose", tout << "inserting " << li << " = " << ri << "\n";);
@@ -1000,15 +997,7 @@ bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) {
 
 
 bool theory_seq::is_var(expr* a) const {
-    return
-        m_util.is_seq(a) &&
-        !m_util.str.is_concat(a) &&
-        !m_util.str.is_empty(a)  &&
-        !m_util.str.is_string(a) &&
-        !m_util.str.is_unit(a) &&
-        !m_util.str.is_itos(a) &&
-        !m_util.str.is_nth_i(a) && 
-        !m.is_ite(a);
+    return m_eq.is_var(a);
 }
 
 

src/smt/theory_seq.h

@@ -37,7 +37,7 @@ Revision History:
 
 namespace smt {
 
-    class theory_seq : public theory {
+    class theory_seq : public theory, public seq::eq_solver_context {
         friend class seq_regex;
 
         struct assumption {
@@ -164,6 +164,15 @@ namespace smt {
             return depeq(m_eq_id++, ls, rs, dep);
         }        
 
+        depeq mk_eqdep(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep) {
+            expr_ref_vector ls(m), rs(m);
+            for (expr* e : l)
+                m_util.str.get_concat_units(e, ls);
+            for (expr* e : r)
+                m_util.str.get_concat_units(e, rs);
+            return depeq(m_eq_id++, ls, rs, dep);
+        }        
+
         // equalities that are decomposed by conacatenations
         typedef std::pair<expr_ref_vector, expr_ref_vector> decomposed_eq;
 
@@ -409,7 +418,6 @@ namespace smt {
         int find_fst_non_empty_idx(expr_ref_vector const& x);
         expr* find_fst_non_empty_var(expr_ref_vector const& x);
         bool has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & diff);
-        bool find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx, dependency*& deps, expr_ref_vector & res);
         
         // final check 
         bool simplify_and_solve_eqs();   // solve unitary equalities
@@ -456,17 +464,11 @@ namespace smt {
         bool solve_eq(unsigned idx);
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
         bool lift_ite(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
-        bool solve_unit_eq(expr* l, expr* r, dependency* dep);
-        bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         obj_pair_hashtable<expr, expr> m_nth_eq2_cache;
         bool solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         bool solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         bool solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep);
-        bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr_ref& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr_ref& y);
-        bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
-        bool is_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
-        bool is_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
 
         bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool propagate_max_length(expr* l, expr* r, dependency* dep);
@@ -538,8 +540,6 @@ namespace smt {
         bool assume_equality(expr* l, expr* r);
 
         // variable solving utilities
-        bool occurs(expr* a, expr* b);
-        bool occurs(expr* a, expr_ref_vector const& b);
         bool is_var(expr* b) const;
         bool add_solution(expr* l, expr* r, dependency* dep);
         bool is_unit_nth(expr* a) const;
@@ -558,7 +558,6 @@ namespace smt {
         void deque_axiom(expr* e);
         void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);        
         void add_axiom(literal_vector& lits);
-        void add_consequence(bool uses_eq, expr_ref_vector const& clause);
         
         bool has_length(expr *e) const { return m_has_length.contains(e); }
         void add_length(expr* e, expr* l);
@@ -591,7 +590,6 @@ namespace smt {
         bool lower_bound(expr* s, rational& lo) const;
         bool lower_bound2(expr* s, rational& lo);
         bool upper_bound(expr* s, rational& hi) const;
-        bool get_length(expr* s, rational& val);
 
         void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
 
@@ -633,6 +631,11 @@ namespace smt {
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
         void unmerge_eh(theory_var v1, theory_var v2) {}
 
+        // eq_solver callbacks
+        void add_consequence(bool uses_eq, expr_ref_vector const& clause) override;
+        void  add_solution(expr* var, expr* term) override { SASSERT(var != term); add_solution(var, term, m_eq_deps); }
+        expr* expr2rep(expr* e) override;
+        bool  get_length(expr* e, rational& r) override;
     };
 };