seq

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

src/smt/smt_context.cpp

@@ -821,7 +821,7 @@ namespace smt {
             theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t2) : r2->m_th_var_list.get_th_var();
             theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : r1->m_th_var_list.get_th_var();
             TRACE("merge_theory_vars", 
-                  tout << "v2: " << v2 << " #" << r1->get_owner_id() << ", v1: " << v1 << " #" << r2->get_owner_id() 
+                  tout << "v2: " << v2 << " #" << r2->get_owner_id() << ", v1: " << v1 << " #" << r1->get_owner_id() 
                   << ", t2: " << t2 << ", t1: " << t1 << "\n";);
             if (v2 != null_theory_var && v1 != null_theory_var) {
                 if (t1 == t2) {

src/smt/theory_seq.cpp

@@ -28,18 +28,19 @@ using namespace smt;
 void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d) {
     std::pair<expr*, enode_pair_dependency*> value;
     if (m_map.find(e, value)) {
-        m_updates.push_back(DEL);
+        add_trail(DEL, e, value.first, value.second);
-        m_lhs.push_back(e);
-        m_rhs.push_back(value.first);
-        m_deps.push_back(value.second);
     }
     value.first = r;
     value.second = d;
     m_map.insert(e, value);
-    m_updates.push_back(INS);
+    add_trail(INS, e, r, d);
-    m_lhs.push_back(e);
+}
-    m_rhs.push_back(value.first);
+
-    m_deps.push_back(value.second);
+void theory_seq::solution_map::add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d) {
+    m_updates.push_back(op);
+    m_lhs.push_back(l);
+    m_rhs.push_back(r);
+    m_deps.push_back(d);
 }
 
 expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) {
@@ -84,6 +85,34 @@ void theory_seq::solution_map::display(std::ostream& out) const {
     }
 }
 
+void theory_seq::exclusion_table::update(expr* e, expr* r) {
+    if (e->get_id() > r->get_id()) {
+        std::swap(e, r);
+    }
+    if (e != r && !m_table.contains(std::make_pair(e, r))) {
+        m_lhs.push_back(e);
+        m_rhs.push_back(r);
+        m_table.insert(std::make_pair(e, r));
+    }
+}
+
+void theory_seq::exclusion_table::pop_scope(unsigned num_scopes) {
+    if (num_scopes == 0) return;
+    unsigned start = m_limit[m_limit.size() - num_scopes];
+    for (unsigned i = start; i < m_lhs.size(); ++i) {
+        m_table.erase(std::make_pair(m_lhs[i].get(), m_rhs[i].get()));
+    }
+    m_lhs.resize(start);
+    m_rhs.resize(start);
+    m_limit.resize(m_limit.size() - num_scopes);
+}
+
+void theory_seq::exclusion_table::display(std::ostream& out) const {
+    table_t::iterator it = m_table.begin(), end = m_table.end();
+    for (; it != end; ++it) {
+        out << mk_pp(it->first, m) << " != " << mk_pp(it->second, m) << "\n";
+    }
+}
 
 theory_seq::theory_seq(ast_manager& m):
     theory(m.mk_family_id("seq")), 
@@ -91,9 +120,12 @@ theory_seq::theory_seq(ast_manager& m):
     m_dam(m_dep_array_value_manager, m_alloc),
     m_rep(m, m_dm),    
     m_ineqs(m),
+    m_exclude(m),
     m_axioms(m),
     m_axioms_head(0),
+    m_branch_variable_head(0),
     m_incomplete(false), 
+    m_model_completion(false),
     m_rewrite(m), 
     m_util(m),
     m_autil(m),
@@ -130,6 +162,15 @@ final_check_status theory_seq::final_check_eh() {
     if (ctx.inconsistent()) {
         return FC_CONTINUE;
     }
+    if (branch_variable()) {
+        return FC_CONTINUE;
+    }
+    if (split_variable()) {
+        return FC_CONTINUE;
+    }
+    if (ctx.inconsistent()) {
+        return FC_CONTINUE;
+    }
     if (m.size(m_lhs.back()) > 0 || m_incomplete) {
         return FC_GIVEUP;        
     }
@@ -152,19 +193,98 @@ bool theory_seq::check_ineqs() {
     return true;
 }
 
+bool theory_seq::branch_variable() {
+    context& ctx = get_context();
+    TRACE("seq", ctx.display(tout););
+    expr_array& lhs = m_lhs.back();
+    expr_array& rhs = m_rhs.back();
+    unsigned sz = m.size(lhs);
+    ptr_vector<expr> ls, rs;
+    for (unsigned i = 0; i < sz; ++i) {
+        unsigned k = (i + m_branch_variable_head) % sz;
+        expr* l = m.get(lhs, k);
+        expr* r = m.get(rhs, k);
+        TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";);
+        ls.reset(); rs.reset();
+        m_util.str.get_concat(l, ls);
+        m_util.str.get_concat(r, rs);
+        
+        if (!ls.empty() && find_branch_candidate(ls[0], rs)) {
+            m_branch_variable_head = k;
+            return true;
+        }
+        if (!rs.empty() && find_branch_candidate(rs[0], ls)) {
+            m_branch_variable_head = k;
+            return true;
+        }
+    }
+    return false;
+}
+
+bool theory_seq::find_branch_candidate(expr* l, ptr_vector<expr> const& rs) {
+
+    TRACE("seq", tout << mk_pp(l, m) << " " 
+          << (is_var(l)?"var":"not var") << "\n";);
+
+    if (!is_var(l)) {
+        return false;
+    }
+
+    expr_ref v0(m), v(m);
+    v0 = m_util.str.mk_empty(m.get_sort(l));
+    if (assume_equality(l, v0)) {
+        return true;
+    }
+    for (unsigned j = 0; j < rs.size(); ++j) {
+        if (occurs(l, rs[j])) {
+            return false;
+        }
+        std::string s;
+        if (m_util.str.is_string(rs[j], s)) {
+            for (size_t k = 1; k < s.length(); ++k) {
+                v = m_util.str.mk_string(std::string(s.c_str(), k));
+                if (v0) v = m_util.str.mk_concat(v0, v);
+                if (assume_equality(l, v)) {
+                    return true;
+                }
+            }
+        }
+        v0 = (j == 0)? rs[0] : m_util.str.mk_concat(v0, rs[j]); 
+        if (assume_equality(l, v0)) {
+            return true;
+        }
+    }           
+    return false;
+}
+
+bool theory_seq::assume_equality(expr* l, expr* r) {
+    TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";);
+    context& ctx = get_context();
+    if (m_exclude.contains(l, r)) {
+        return false;
+    }
+    else {
+        SASSERT(ctx.e_internalized(l));
+        if (!ctx.e_internalized(r)) ctx.internalize(r, false);
+        enode* n1 = ctx.get_enode(l);
+        enode* n2 = ctx.get_enode(r);
+        ctx.assume_eq(n1, n2);        
+    }
+    return true;
+}
+
+bool theory_seq::split_variable() {
+
+    return false;
+}
+
 void theory_seq::propagate_lit(enode_pair_dependency* dep, literal lit) {
     context& ctx = get_context();
     ctx.mark_as_relevant(lit);
     vector<enode_pair, false> _eqs;
     m_dm.linearize(dep, _eqs);
-    TRACE("seq", 
+    TRACE("seq", ctx.display_detailed_literal(tout, lit); 
-          ctx.display_detailed_literal(tout, lit);
+          tout << " <-\n"; display_deps(tout, dep);); 
-          tout << " <- ";
-          for (unsigned i = 0; i < _eqs.size(); ++i) {
-              tout << mk_pp(_eqs[i].first->get_owner(), m) << " = " 
-                   << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
-          }
-          ); 
     justification* js = 
         ctx.mk_justification(
             ext_theory_propagation_justification(
@@ -177,12 +297,7 @@ void theory_seq::set_conflict(enode_pair_dependency* dep) {
     context& ctx = get_context();
     vector<enode_pair, false> _eqs;
     m_dm.linearize(dep, _eqs);
-    TRACE("seq", 
+    TRACE("seq", display_deps(tout, dep);); 
-          for (unsigned i = 0; i < _eqs.size(); ++i) {
-              tout << mk_pp(_eqs[i].first->get_owner(), m) << " = " 
-                   << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
-          }
-          ); 
     ctx.set_conflict(
         ctx.mk_justification(
             ext_theory_conflict_justification(
@@ -195,10 +310,7 @@ void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2)
     m_dm.linearize(dep, _eqs);
     TRACE("seq",
           tout << mk_pp(n1->get_owner(), m) << " " << mk_pp(n2->get_owner(), m) << " <- ";
-          for (unsigned i = 0; i < _eqs.size(); ++i) {
+          display_deps(tout, dep);
-              tout << mk_pp(_eqs[i].first->get_owner(), m) << " = " 
-                   << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
-          }
           ); 
     
     justification* js = ctx.mk_justification(
@@ -366,13 +478,19 @@ bool theory_seq::internalize_atom(app* a, bool) {
 }
 
 bool theory_seq::internalize_term(app* term) { 
+    TRACE("seq", tout << mk_pp(term, m) << "\n";);
     context & ctx   = get_context();
     unsigned num_args = term->get_num_args();
     for (unsigned i = 0; i < num_args; i++) {
-        ctx.internalize(term->get_arg(i), false);
+        expr* arg = term->get_arg(i);
+        ctx.internalize(arg, false);
+        if (ctx.e_internalized(arg)) {
+            mk_var(ctx.get_enode(arg));
+        }
     }
+    enode* e = 0;
     if (ctx.e_internalized(term)) {
-        return true;
+        e = ctx.get_enode(term);
     }
     if (m.is_bool(term)) {
         bool_var bv = ctx.mk_bool_var(term);
@@ -380,9 +498,10 @@ bool theory_seq::internalize_term(app* term) {
         ctx.set_enode_flag(bv, true);
     }
     else {
-        enode * e = ctx.mk_enode(term, false, m.is_bool(term), true); 
+        if (!e) {
-        theory_var v = mk_var(e);
+            e = ctx.mk_enode(term, false, m.is_bool(term), true);
-        ctx.attach_th_var(e, this, v);
+        } 
+        mk_var(e);
     }
     if (!m_util.str.is_concat(term) &&
         !m_util.str.is_string(term) &&
@@ -400,33 +519,43 @@ bool theory_seq::internalize_term(app* term) {
 }
 
 void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
-    if (!is_attached_to_var(n)) {
+    mk_var(n);    
-        mk_var(n);
-    }
 }
 
 void theory_seq::display(std::ostream & out) const {
-    expr_array const& lhs = m_lhs.back();
+    display_equations(out);
-    expr_array const& rhs = m_rhs.back();
+    if (!m_ineqs.empty()) {
-    enode_pair_dependency_array const& deps = m_deps.back();
+        out << "Negative constraints:\n";
-    out << "Equations:\n";
+        for (unsigned i = 0; i < m_ineqs.size(); ++i) {
-    for (unsigned i = 0; i < m.size(lhs); ++i) {
+            out << mk_pp(m_ineqs[i], m) << "\n";
-        out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n";
-        enode_pair_dependency* dep = m_dam.get(deps, i);
-        if (dep) {
-            vector<enode_pair, false> _eqs;
-            const_cast<enode_pair_dependency_manager&>(m_dm).linearize(dep, _eqs);
-            for (unsigned i = 0; i < _eqs.size(); ++i) {
-                out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
-            }
         }
     }
-    out << "Negative constraints:\n";
-    for (unsigned i = 0; i < m_ineqs.size(); ++i) {
-        out << mk_pp(m_ineqs[i], m) << "\n";
-    }
     out << "Solved equations:\n";
     m_rep.display(out);
+    m_exclude.display(out);
+}
+
+void theory_seq::display_equations(std::ostream& out) const {
+    expr_array const& lhs = m_lhs.back();
+    expr_array const& rhs = m_rhs.back();
+    enode_pair_dependency_array const& deps = m_deps.back();
+    if (m.size(lhs) == 0) {
+        return;
+    }
+    out << "Equations:\n";
+    for (unsigned i = 0; i < m.size(lhs); ++i) {
+        out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n";
+        display_deps(out, m_dam.get(deps, i));
+    }       
+}
+
+void theory_seq::display_deps(std::ostream& out, enode_pair_dependency* dep) const {
+    if (!dep) return;
+    vector<enode_pair, false> _eqs;
+    const_cast<enode_pair_dependency_manager&>(m_dm).linearize(dep, _eqs);
+    for (unsigned i = 0; i < _eqs.size(); ++i) {
+        out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
+    }
 }
 
 void theory_seq::collect_statistics(::statistics & st) const {
@@ -438,31 +567,13 @@ void theory_seq::init_model(model_generator & mg) {
     m_factory = alloc(seq_factory, get_manager(), 
                       get_family_id(), mg.get_model());
     mg.register_factory(m_factory);
-    // TBD: this is still unsound model generation.
-    // disequalities are not guaranteed. we need to
-    // prime the factory with a prefix that cannot be
-    // constructed using any existing combinations of the
-    // strings (or units) that are used.
-    for (unsigned i = 0; i < get_num_vars(); ++i) {
-        expr* e = get_enode(i)->get_owner();
-        if (m_util.is_seq(e)) {
-            enode_pair_dependency* deps = 0;
-            e = m_rep.find(e, deps);
-            if (is_var(e)) {
-                expr* val = m_factory->get_fresh_value(m.get_sort(e));
-                m_rep.update(e, val, 0);
-            }
-        }
-        else if (m_util.is_re(e)) {
-            // TBD
-        }
-    }
 }
 
 model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
     enode_pair_dependency* deps = 0;
     expr_ref e(n->get_owner(), m);
-    canonize(e, deps);
+    flet<bool> _model_completion(m_model_completion, true);
+    e = canonize(e, deps);
     SASSERT(is_app(e));
     m_factory->add_trail(e);
     return alloc(expr_wrapper_proc, to_app(e));
@@ -479,7 +590,14 @@ void theory_seq::set_incomplete(app* term) {
 }
 
 theory_var theory_seq::mk_var(enode* n) {
-    return theory::mk_var(n);
+    if (is_attached_to_var(n)) {
+        return n->get_th_var(get_id());
+    }
+    else {
+        theory_var v = theory::mk_var(n);
+        get_context().attach_th_var(n, this, v);
+        return v;
+    }
 }
 
 bool theory_seq::can_propagate() {
@@ -515,6 +633,15 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
     if (m_util.str.is_contains(e, e1, e2)) {
         return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m);
     }
+    if (m_model_completion && is_var(e)) {
+        SASSERT(m_factory);
+        expr_ref val(m);
+        val = m_factory->get_fresh_value(m.get_sort(e));
+        if (val) {
+            m_rep.update(e, val, 0);
+            return val;
+        }
+    }
     return expr_ref(e, m);
 }
 
@@ -625,11 +752,14 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     expr* e2 = get_enode(v2)->get_owner();
     m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_ineqs));
     m_ineqs.push_back(mk_eq_atom(e1, e2));
+    m_exclude.update(e1, e2);
 }
 
 void theory_seq::push_scope_eh() {
+    TRACE("seq", tout << "push " << m_lhs.size() << "\n";);
     theory::push_scope_eh();
     m_rep.push_scope();
+    m_exclude.push_scope();
     m_dm.push_scope();
     m_trail_stack.push_scope();
     m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
@@ -644,10 +774,12 @@ void theory_seq::push_scope_eh() {
 }
 
 void theory_seq::pop_scope_eh(unsigned num_scopes) {
+    TRACE("seq", tout << "pop " << m_lhs.size() << "\n";);
     m_trail_stack.pop_scope(num_scopes);
     theory::pop_scope_eh(num_scopes);   
     m_dm.pop_scope(num_scopes); 
     m_rep.pop_scope(num_scopes);
+    m_exclude.pop_scope(num_scopes);
     while (num_scopes > 0) {
         --num_scopes;
         m.del(m_lhs.back());

src/smt/theory_seq.h

@@ -53,10 +53,12 @@ namespace smt {
             ast_manager&                      m;
             enode_pair_dependency_manager&    m_dm;
             map_t                             m_map;            
-            expr_ref_vector m_lhs,            m_rhs;
+            expr_ref_vector                   m_lhs, m_rhs;
             ptr_vector<enode_pair_dependency> m_deps;
             svector<map_update>               m_updates;
             unsigned_vector                   m_limit;
+
+            void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d);
         public:
             solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
             void  update(expr* e, expr* r, enode_pair_dependency* d);
@@ -66,6 +68,24 @@ namespace smt {
             void display(std::ostream& out) const;
         };
 
+        class exclusion_table {
+            typedef obj_pair_hashtable<expr, expr> table_t;
+            ast_manager&                      m;
+            table_t                           m_table;
+            expr_ref_vector                   m_lhs, m_rhs;
+            unsigned_vector                   m_limit;
+        public:
+            exclusion_table(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {}
+            ~exclusion_table() { }
+            void update(expr* e, expr* r);
+            bool contains(expr* e, expr* r) {
+                return m_table.contains(std::make_pair(e, r));
+            }
+            void push_scope() { m_limit.push_back(m_lhs.size()); }
+            void pop_scope(unsigned num_scopes);
+            void display(std::ostream& out) const;            
+        };
+
         struct stats {
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(stats)); }
@@ -81,11 +101,14 @@ namespace smt {
         vector<expr_array>                  m_lhs, m_rhs; // persistent sets of equalities.
         vector<enode_pair_dependency_array> m_deps;       // persistent sets of dependencies.
 
-        seq_factory*    m_factory;    // value factory
+        seq_factory*    m_factory;               // value factory
-        expr_ref_vector m_ineqs;      // inequalities to check
+        expr_ref_vector m_ineqs;                 // inequalities to check solution against
-        expr_ref_vector m_axioms;     
+        exclusion_table m_exclude;               // set of asserted disequalities.
-        unsigned        m_axioms_head;        
+        expr_ref_vector m_axioms;                // list of axioms to add.
-        bool            m_incomplete; 
+        unsigned        m_axioms_head;           // index of first axiom to add.
+        unsigned        m_branch_variable_head;  // index of first equation to examine.
+        bool            m_incomplete;            // is the solver (clearly) incomplete for the fragment.
+        bool            m_model_completion;      // during model construction, invent values in canonizer
         th_rewriter     m_rewrite;
         seq_util        m_util;
         arith_util      m_autil;
@@ -95,8 +118,8 @@ namespace smt {
         symbol          m_suffix_sym;
         symbol          m_contains_left_sym;
         symbol          m_contains_right_sym;
-        symbol          m_left_sym;
+        symbol          m_left_sym;               // split variable left part
-        symbol          m_right_sym;
+        symbol          m_right_sym;              // split variable right part
 
         virtual final_check_status final_check_eh();
         virtual bool internalize_atom(app*, bool);
@@ -114,23 +137,29 @@ namespace smt {
         virtual char const * get_name() const { return "seq"; }
         virtual theory_var mk_var(enode* n);
         virtual void apply_sort_cnstr(enode* n, sort* s);
-        virtual void display(std::ostream & out) const;
+        virtual void display(std::ostream & out) const;        
         virtual void collect_statistics(::statistics & st) const;
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
         virtual void init_model(model_generator & mg);
        
-        bool check_ineqs();
+        bool check_ineqs();              // check if inequalities are violated.
+        bool simplify_and_solve_eqs();   // solve unitary equalities
+        bool branch_variable();          // branch on a variable
+        bool split_variable();           // split a variable
+
         bool pre_process_eqs(bool simplify_or_solve);
         bool simplify_eqs();
         bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep);
         bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep);
         bool solve_basic_eqs();
-        bool simplify_and_solve_eqs();
         void propagate_lit(enode_pair_dependency* dep, literal lit);
         void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2);
         void propagate_eq(bool_var v, expr* e1, expr* e2);
         void set_conflict(enode_pair_dependency* dep);
 
+        bool find_branch_candidate(expr* l, ptr_vector<expr> const& rs);
+        bool assume_equality(expr* l, expr* r);
+
         bool occurs(expr* a, expr* b);
         bool is_var(expr* b);
         void add_solution(expr* l, expr* r, enode_pair_dependency* dep);
@@ -148,6 +177,9 @@ namespace smt {
         expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2);
 
         void set_incomplete(app* term);
+
+        void display_equations(std::ostream& out) const;
+        void display_deps(std::ostream& out, enode_pair_dependency* deps) const;
     public:
         theory_seq(ast_manager& m);
         virtual ~theory_seq();