diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index ef73bd2f2..072471898 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -636,7 +636,12 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve } change = true; } + + bool is_sat; if (!change) { + if (is_subsequence(m_lhs.size(), m_lhs.c_ptr(), m_rhs.size(), m_rhs.c_ptr(), lhs, rhs, is_sat)) { + return is_sat; + } lhs.push_back(l); rhs.push_back(r); } @@ -649,7 +654,13 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve 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. + else { // could solve if either side is fixed size. + SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size()); + if (is_subsequence(m_lhs.size() - head1, m_lhs.c_ptr() + head1, + m_rhs.size() - head2, m_rhs.c_ptr() + head2, lhs, rhs, is_sat)) { + return is_sat; + } + 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)); } @@ -674,3 +685,39 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, } return true; } + +bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, expr* const* r, + expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) { + is_sat = true; + if (szl == szr) return false; + if (szr < szl) { + std::swap(szl, szr); + std::swap(l, r); + } + + for (unsigned i = 1; i + szl <= szr; ++i) { + bool eq = true; + for (unsigned j = 0; eq && j < szl; ++j) { + eq = l[j] == r[i+j]; + } + if (eq) { + SASSERT(szr >= i + szl); + is_sat = set_empty(i, r, lhs, rhs); + is_sat &= set_empty(szr - (i + szl), r + i + szl, lhs, rhs); + + TRACE("seq", + for (unsigned k = 0; k < szl; ++k) { + tout << mk_pp(l[k], m()) << " "; + } + tout << "\n"; + for (unsigned k = 0; k < szr; ++k) { + tout << mk_pp(r[k], m()) << " "; + } + tout << "\n"; + tout << lhs << "; " << rhs << "\n";); + + return true; + } + } + return false; +} diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 57926efdf..d4652f614 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -54,6 +54,8 @@ class seq_rewriter { 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); + bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, + expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat); public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m), m_autil(m) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 77e57b07c..7973d0b6e 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -47,7 +47,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { if (is_sort_param(sP, i)) { if (binding.size() <= i) binding.resize(i+1); if (binding[i] && (binding[i] != s)) return false; - TRACE("seq", tout << "setting binding @ " << i << " to " << mk_pp(s, m) << "\n";); + TRACE("seq_verbose", tout << "setting binding @ " << i << " to " << mk_pp(s, m) << "\n";); binding[i] = s; return true; } @@ -77,7 +77,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { ptr_vector binding; ast_manager& m = *m_manager; - TRACE("seq", + TRACE("seq_verbose", tout << sig.m_name << ": "; for (unsigned i = 0; i < dsz; ++i) tout << mk_pp(dom[i], m) << " "; if (range) tout << " range: " << mk_pp(range, m); @@ -102,7 +102,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom m.raise_exception(strm.str().c_str()); } range_out = apply_binding(binding, sig.m_range); - TRACE("seq", tout << mk_pp(range_out, m) << "\n";); + TRACE("seq_verbose", tout << mk_pp(range_out, m) << "\n";); } void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { @@ -321,18 +321,27 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters)); case OP_SEQ_CONCAT: { + if (arity < 2) { + m.raise_exception("invalid concatenation. At least two arguments expected"); + } match_left_assoc(*m_sigs[k], arity, domain, range, rng); func_decl_info info(m_family_id, k); info.set_left_associative(); return m.mk_func_decl(m_sigs[(rng == m_string)?_OP_STRING_CONCAT:k]->m_name, rng, rng, rng, info); } case OP_RE_CONCAT: { + if (arity < 2) { + m.raise_exception("invalid concatenation. At least two arguments expected"); + } match_left_assoc(*m_sigs[k], arity, domain, range, rng); func_decl_info info(m_family_id, k); info.set_left_associative(); return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); } case _OP_STRING_CONCAT: { + if (arity < 2) { + m.raise_exception("invalid string concatenation. At least two arguments expected"); + } match_left_assoc(*m_sigs[k], arity, domain, range, rng); func_decl_info info(m_family_id, OP_SEQ_CONCAT); info.set_left_associative(); @@ -386,6 +395,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + case _OP_SEQ_SKOLEM: + return m.mk_func_decl(symbol("seq.skolem"), arity, domain, rng, func_decl_info(m_family_id, k)); default: UNREACHABLE(); return 0; @@ -419,6 +430,13 @@ bool seq_decl_plugin::is_value(app* e) const { return is_app_of(e, m_family_id, OP_STRING_CONST); } +app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) { + parameter param(name); + func_decl* f = m.mk_func_decl(get_family_id(), _OP_SEQ_SKOLEM, 1, ¶m, n, args, range); + return m.mk_app(f, n, args); +} + + app* seq_util::str::mk_string(symbol const& s) { return u.seq.mk_string(s); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c317f8236..c11f830b4 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -74,6 +74,7 @@ enum seq_op_kind { _OP_STRING_TO_REGEXP, _OP_STRING_CHARAT, _OP_STRING_SUBSTR, + _OP_SEQ_SKOLEM, LAST_SEQ_OP }; @@ -155,6 +156,11 @@ public: bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); } bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); } bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); } + bool is_seq(expr* e) const { return is_seq(m.get_sort(e)); } + bool is_re(expr* e) const { return is_re(m.get_sort(e)); } + + app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range); + bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); } class str { seq_util& u; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 213e671db..befe7b419 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -72,6 +72,14 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) { m_limit.resize(m_limit.size() - num_scopes); } +void theory_seq::solution_map::display(std::ostream& out) const { + map_t::iterator it = m_map.begin(), end = m_map.end(); + for (; it != end; ++it) { + out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value.first, m) << "\n"; + } +} + + theory_seq::theory_seq(ast_manager& m): theory(m.mk_family_id("seq")), m(m), @@ -88,10 +96,17 @@ theory_seq::theory_seq(ast_manager& m): m_lhs.push_back(expr_array()); m_rhs.push_back(expr_array()); m_deps.push_back(enode_pair_dependency_array()); + m_prefix_sym = "prefix"; + m_suffix_sym = "suffix"; + m_left_sym = "left"; + m_right_sym = "right"; + m_contains_left_sym = "contains_left"; + m_contains_right_sym = "contains_right"; } final_check_status theory_seq::final_check_eh() { context & ctx = get_context(); + TRACE("seq", display(tout);); if (!check_ineqs()) { return FC_CONTINUE; } @@ -111,44 +126,50 @@ bool theory_seq::check_ineqs() { enode_pair_dependency* eqs = 0; expr_ref b = canonize(a, eqs); if (m.is_true(b)) { + TRACE("seq", tout << "Evaluates to false: " << a << "\n";); ctx.internalize(a, false); literal lit(ctx.get_literal(a)); - ctx.mark_as_relevant(lit); - vector _eqs; - m_dm.linearize(eqs, _eqs); - ctx.assign( - lit, - ctx.mk_justification( - ext_theory_propagation_justification( - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit))); + propagate(lit, eqs); return false; } } return true; } +void theory_seq::propagate(literal lit, enode_pair_dependency* dep) { + context& ctx = get_context(); + ctx.mark_as_relevant(lit); + vector _eqs; + m_dm.linearize(dep, _eqs); + TRACE("seq", + ctx.display_detailed_literal(tout, lit); + 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"; + } + ); + + ctx.assign( + lit, + ctx.mk_justification( + ext_theory_propagation_justification( + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit))); +} + + bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* 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)); - vector _eqs; - m_dm.linearize(deps, _eqs); - ctx.assign( - ~lit, - ctx.mk_justification( - ext_theory_propagation_justification( - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), ~lit))); + literal lit(mk_eq(l, r, false)); + propagate(~lit, deps); return true; } if (lhs.size() == 1 && l == lhs[0].get() && @@ -161,6 +182,13 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) { m.push_back(m_rhs.back(), rhs[i].get()); m_dam.push_back(m_deps.back(), deps); } + TRACE("seq", + tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " => "; + for (unsigned i = 0; i < lhs.size(); ++i) { + tout << mk_pp(lhs[i].get(), m) << " = " << mk_pp(rhs[i].get(), m) << "; "; + } + tout << "\n"; + ); return true; } @@ -187,31 +215,36 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps) { } 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)); - // true if a occurs under an interpreted function or under left/right selector. - if (a == b) { - return true; - } expr* e1, *e2; + while (is_left_select(a, e1) || is_right_select(a, e1)) { + a = e1; + } if (m_util.str.is_concat(b, e1, e2)) { return occurs(a, e1) || occurs(a, e2); } - if (is_left_select(b, e1) || is_right_select(b, e1)) { - return occurs(a, e1); - } + while (is_left_select(b, e1) || is_right_select(b, e1)) { + b = e1; + } + if (a == b) { + return true; + } return false; } bool theory_seq::is_var(expr* a) { - return is_uninterp(a); + return is_uninterp(a) || m_util.is_skolem(a); } bool theory_seq::is_left_select(expr* a, expr*& b) { - return false; + return m_util.is_skolem(a) && + to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_left_sym && (b = to_app(a)->get_arg(0), true); } bool theory_seq::is_right_select(expr* a, expr*& b) { - return false; + return m_util.is_skolem(a) && + to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_right_sym && (b = to_app(a)->get_arg(0), true); } @@ -224,10 +257,18 @@ void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { enode* n2 = ctx.get_enode(r); vector _eqs; m_dm.linearize(deps, _eqs); - // alloc? - ctx.assign_eq(n1, n2, eq_justification( - alloc(ext_theory_eq_propagation_justification, - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2))); + TRACE("seq", + tout << mk_pp(n1->get_owner(), m) << " " << mk_pp(n2->get_owner(), m) << " <- "; + 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_eq_propagation_justification( + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2)); + ctx.assign_eq(n1, n2, eq_justification(js)); } } @@ -254,6 +295,7 @@ bool theory_seq::pre_process_eqs(bool simplify_or_solve) { m.set(rhs, i, m.get(rhs, m.size(rhs)-1)); m_dam.set(deps, i, m_dam.get(deps, m_dam.size(deps)-1)); --i; + ++m_stats.m_num_reductions; change = true; } m.pop_back(lhs); @@ -312,7 +354,8 @@ bool theory_seq::internalize_term(app* term) { !m_util.str.is_unit(term) && !m_util.str.is_suffix(term) && !m_util.str.is_prefix(term) && - !m_util.str.is_contains(term)) { + !m_util.str.is_contains(term) && + !m_util.is_skolem(term)) { set_incomplete(term); } @@ -326,6 +369,70 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) { } } +void theory_seq::display(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(); + 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"; + enode_pair_dependency* dep = m_dam.get(deps, i); + if (dep) { + vector _eqs; + const_cast(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); +} + +void theory_seq::collect_statistics(::statistics & st) const { + st.update("seq num splits", m_stats.m_num_splits); + st.update("seq num reductions", m_stats.m_num_reductions); +} + +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(m); + canonize(e, deps); + SASSERT(is_app(e)); + m_factory->add_trail(e); + return alloc(expr_wrapper_proc, to_app(e)); +} + + void theory_seq::set_incomplete(app* term) { TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";); @@ -413,27 +520,29 @@ void theory_seq::assert_axiom(expr_ref& e) { literal lit(ctx.get_literal(e)); ctx.mark_as_relevant(lit); ctx.mk_th_axiom(get_id(), 1, &lit); - } -expr_ref theory_seq::mk_skolem(char const* name, expr* e1, expr* e2) { +expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2) { expr_ref result(m); - sort* s = m.get_sort(e1); - SASSERT(s == m.get_sort(e2)); - sort* ss[2] = { s, s }; - result = m.mk_app(m.mk_func_decl(symbol("#prefix_eq"), 2, ss, s), e1, e2); + expr* es[2] = { e1, e2 }; + result = m_util.mk_skolem(name, 2, es, m.get_sort(e1)); return result; } void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { context& ctx = get_context(); + TRACE("seq", + tout << mk_pp(ctx.bool_var2enode(v)->get_owner(), m) << " => " + << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";); + ctx.internalize(e1, false); enode* n1 = ctx.get_enode(e1); enode* n2 = ctx.get_enode(e2); literal lit(v); - ctx.assign_eq(n1, n2, eq_justification( - alloc(ext_theory_eq_propagation_justification, - get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2))); + justification* js = ctx.mk_justification(ext_theory_eq_propagation_justification( + get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2)); + + ctx.assign_eq(n1, n2, eq_justification(js)); } void theory_seq::assign_eq(bool_var v, bool is_true) { @@ -445,18 +554,18 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { expr* e1, *e2; expr_ref f(m); if (m_util.str.is_prefix(e, e1, e2)) { - f = mk_skolem("#prefix_eq", e1, e2); + f = mk_skolem(m_prefix_sym, e1, e2); f = m_util.str.mk_concat(e1, f); propagate_eq(v, f, e2); } else if (m_util.str.is_suffix(e, e1, e2)) { - f = mk_skolem("#suffix_eq", e1, e2); + f = mk_skolem(m_suffix_sym, e1, e2); f = m_util.str.mk_concat(f, e1); propagate_eq(v, f, e2); } else if (m_util.str.is_contains(e, e1, e2)) { - expr_ref f1 = mk_skolem("#contains_eq1", e1, e2); - expr_ref f2 = mk_skolem("#contains_eq2", e1, e2); + expr_ref f1 = mk_skolem(m_contains_left_sym, e1, e2); + expr_ref f2 = mk_skolem(m_contains_right_sym, e1, e2); f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e1), f2); propagate_eq(v, f, e2); } @@ -485,7 +594,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { expr* e1 = get_enode(v1)->get_owner(); expr* e2 = get_enode(v2)->get_owner(); m_trail_stack.push(push_back_vector(m_ineqs)); - m_ineqs.push_back(m.mk_eq(e1, e2)); + m_ineqs.push_back(mk_eq_atom(e1, e2)); } void theory_seq::push_scope_eh() { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 4aee7e61c..63dd2bdc6 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -49,25 +49,28 @@ namespace smt { class solution_map { enum map_update { INS, DEL }; - ast_manager& m; - enode_pair_dependency_manager& m_dm; - obj_map > m_map; - expr_ref_vector m_lhs, m_rhs; + typedef obj_map > map_t; + ast_manager& m; + enode_pair_dependency_manager& m_dm; + map_t m_map; + expr_ref_vector m_lhs, m_rhs; ptr_vector m_deps; - svector m_updates; - unsigned_vector m_limit; + svector m_updates; + unsigned_vector m_limit; 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); expr* find(expr* e, enode_pair_dependency*& d); void push_scope() { m_limit.push_back(m_updates.size()); } void pop_scope(unsigned num_scopes); + void display(std::ostream& out) const; }; struct stats { stats() { reset(); } void reset() { memset(this, 0, sizeof(stats)); } unsigned m_num_splits; + unsigned m_num_reductions; }; ast_manager& m; small_object_allocator m_alloc; @@ -78,7 +81,7 @@ namespace smt { vector m_lhs, m_rhs; // persistent sets of equalities. vector m_deps; // persistent sets of dependencies. - + seq_factory* m_factory; // value factory expr_ref_vector m_ineqs; // inequalities to check expr_ref_vector m_axioms; unsigned m_axioms_head; @@ -88,13 +91,19 @@ namespace smt { arith_util m_autil; th_trail_stack m_trail_stack; stats m_stats; + symbol m_prefix_sym; + symbol m_suffix_sym; + symbol m_contains_left_sym; + symbol m_contains_right_sym; + symbol m_left_sym; + symbol m_right_sym; virtual final_check_status final_check_eh(); virtual bool internalize_atom(app*, bool); virtual bool internalize_term(app*); virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); - virtual void assign_eq(bool_var v, bool is_true); + virtual void assign_eq(bool_var v, bool is_true); virtual bool can_propagate(); virtual void propagate(); virtual void push_scope_eh(); @@ -105,21 +114,25 @@ 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 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 pre_process_eqs(bool simplify_or_solve); bool simplify_eqs(); - bool simplify_eq(expr* l, expr* r, enode_pair_dependency* deps); - bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps); + 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(literal lit, enode_pair_dependency* dep); bool occurs(expr* a, expr* b); bool is_var(expr* b); void add_solution(expr* l, expr* r, enode_pair_dependency* dep); bool is_left_select(expr* a, expr*& b); bool is_right_select(expr* a, expr*& b); - final_check_status add_axioms(); void assert_axiom(expr_ref& e); @@ -131,21 +144,11 @@ namespace smt { enode_pair_dependency* join(enode_pair_dependency* a, enode_pair_dependency* b); void propagate_eq(bool_var v, expr* e1, expr* e2); - expr_ref mk_skolem(char const* name, expr* e1, expr* e2); + expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2); void set_incomplete(app* term); public: theory_seq(ast_manager& m); - virtual void init_model(model_generator & mg) { - mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model())); - } - -#if 0 - th_trail_stack & get_trail_stack() { return m_trail_stack; } - virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var); - static 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); -#endif }; }; diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index e8e619bf8..b1bab6c05 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -25,22 +25,44 @@ Revision History: namespace smt { class seq_factory : public value_factory { typedef hashtable symbol_set; + ast_manager& m; proto_model& m_model; seq_util u; symbol_set m_strings; unsigned m_next; + std::string m_unique_prefix; + obj_map m_unique_sequences; + expr_ref_vector m_trail; public: + seq_factory(ast_manager & m, family_id fid, proto_model & md): value_factory(m, fid), + m(m), m_model(md), u(m), - m_next(0) + m_next(0), + m_unique_prefix("#B"), + m_trail(m) { m_strings.insert(symbol("")); m_strings.insert(symbol("a")); m_strings.insert(symbol("b")); } + void add_trail(expr* e) { + m_trail.push_back(e); + } + + void set_prefix(char const* p) { + m_unique_prefix = p; + } + + // generic method for setting unique sequences + void set_prefix(expr* uniq) { + m_trail.push_back(uniq); + m_unique_sequences.insert(m.get_sort(uniq), uniq); + } + virtual expr* get_some_value(sort* s) { if (u.is_string(s)) return u.str.mk_string(symbol("")); @@ -60,7 +82,7 @@ namespace smt { if (u.is_string(s)) { while (true) { std::ostringstream strm; - strm << "S" << m_next++; + strm << m_unique_prefix << m_next++; symbol sym(strm.str().c_str()); if (m_strings.contains(sym)) continue; m_strings.insert(sym);