diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5639356cc..7ddd6ecac 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -90,6 +90,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { + SASSERT(dom[i]); is_match = match(binding, dom[i], sig.m_dom[0].get()); } if (range && is_match) { @@ -102,6 +103,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); + SASSERT(range_out); TRACE("seq_verbose", tout << mk_pp(range_out, m) << "\n";); } @@ -134,6 +136,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran m.raise_exception(strm.str().c_str()); } range_out = apply_binding(binding, sig.m_range); + SASSERT(range_out); } sort* seq_decl_plugin::apply_binding(ptr_vector const& binding, sort* s) { @@ -195,7 +198,7 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_CONTAINS] = alloc(psig, m, "seq.contains", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA); - m_sigs[OP_SEQ_REPLACE] = alloc(psig, m, "seq.replace", 1, 3, seq3A, strT); + m_sigs[OP_SEQ_REPLACE] = alloc(psig, m, "seq.replace", 1, 3, seq3A, seqA); m_sigs[OP_SEQ_INDEX] = alloc(psig, m, "seq.indexof", 1, 3, seq2AintT, intT); m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA); m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT); @@ -226,7 +229,7 @@ void seq_decl_plugin::init() { m_sigs[_OP_STRING_SUFFIX] = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT); m_sigs[_OP_STRING_IN_REGEXP] = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT); m_sigs[_OP_STRING_TO_REGEXP] = alloc(psig, m, "str.to.re", 0, 1, &strT, reT); - m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT); + m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); } void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { @@ -409,7 +412,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, 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)); + return m.mk_func_decl(symbol("seq.skolem"), arity, domain, range, func_decl_info(m_family_id, k)); default: UNREACHABLE(); return 0; @@ -444,6 +447,7 @@ bool seq_decl_plugin::is_value(app* e) const { } app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) { + SASSERT(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); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 2ed9ea1c7..fe6a0b12b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -269,9 +269,7 @@ bool theory_seq::assume_equality(expr* l, expr* r) { 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); + ctx.assume_eq(ctx.get_enode(l), ctx.get_enode(r)); } return true; } @@ -398,7 +396,12 @@ bool theory_seq::occurs(expr* a, expr* b) { } bool theory_seq::is_var(expr* a) { - return is_uninterp(a) || m_util.is_skolem(a); + 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); } bool theory_seq::is_left_select(expr* a, expr*& b) { @@ -411,15 +414,12 @@ bool theory_seq::is_right_select(expr* a, expr*& b) { to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_right_sym && (b = to_app(a)->get_arg(0), true); } - void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { context& ctx = get_context(); m_rep.update(l, r, deps); // TBD: skip new equalities for non-internalized terms. if (ctx.e_internalized(l) && ctx.e_internalized(r)) { - enode* n1 = ctx.get_enode(l); - enode* n2 = ctx.get_enode(r); - propagate_eq(deps, n1, n2); + propagate_eq(deps, ctx.get_enode(l), ctx.get_enode(r)); } } @@ -467,8 +467,6 @@ bool theory_seq::simplify_and_solve_eqs() { return change; } - - bool theory_seq::internalize_atom(app* a, bool) { return internalize_term(a); } @@ -484,17 +482,16 @@ bool theory_seq::internalize_term(app* term) { mk_var(ctx.get_enode(arg)); } } - enode* e = 0; - if (ctx.e_internalized(term)) { - e = ctx.get_enode(term); - } if (m.is_bool(term)) { bool_var bv = ctx.mk_bool_var(term); ctx.set_var_theory(bv, get_id()); - ctx.set_enode_flag(bv, true); } else { - if (!e) { + enode* e = 0; + if (ctx.e_internalized(term)) { + e = ctx.get_enode(term); + } + else { e = ctx.mk_enode(term, false, m.is_bool(term), true); } mk_var(e); @@ -580,8 +577,8 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { void theory_seq::set_incomplete(app* term) { - TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";); if (!m_incomplete) { + TRACE("seq", tout << "Incomplete operator: " << mk_pp(term, m) << "\n";); m_trail_stack.push(value_trail(m_incomplete)); m_incomplete = true; } @@ -691,6 +688,9 @@ void theory_seq::deque_axiom(expr* n) { */ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { context& ctx = get_context(); + if (n1->get_root() == n2->get_root()) { + return; + } SASSERT(n1->get_root() != n2->get_root()); if (!m_util.is_seq(n1->get_owner())) { return; @@ -713,10 +713,7 @@ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { enode* start2 = n2; do { expr* o = n2->get_owner(); - if (m_util.str.is_concat(o) || - m_util.str.is_unit(o) || - m_util.str.is_string(o) || - m_util.str.is_empty(o)) { + if (!is_var(o)) { expr_ref ln(m_util.str.mk_length(o), m); enque_axiom(ln); } @@ -790,8 +787,8 @@ void theory_seq::add_replace_axiom(expr* r) { VERIFY(m_util.str.is_replace(r, a, s, t)); expr_ref x = mk_skolem(m_contains_left_sym, s, a); expr_ref y = mk_skolem(m_contains_right_sym, s, a); - expr_ref xsy(m_util.str.mk_concat(x, t, y), m); - expr_ref xty(m_util.str.mk_concat(x, s, y), m); + expr_ref xty(m_util.str.mk_concat(x, t, y), m); + expr_ref xsy(m_util.str.mk_concat(x, s, y), m); literal cnt = mk_literal(m_util.str.mk_contains(s, a)); add_axiom(cnt, mk_eq(r, a, false)); add_axiom(~cnt, mk_eq(a, xsy, false)); @@ -840,6 +837,10 @@ void theory_seq::add_length_axiom(expr* n) { } } +expr* theory_seq::mk_sub(expr* a, expr* b) { + return m_autil.mk_add(a, m_autil.mk_mul(m_autil.mk_int(-1), b)); +} + /* TBD: check semantics of extract. @@ -860,14 +861,14 @@ void theory_seq::add_extract_axiom(expr* e) { expr_ref ls(m_util.str.mk_length(s), m); expr_ref lx(m_util.str.mk_length(x), m); expr_ref le(m_util.str.mk_length(e), m); - expr_ref ls_minus_i(m_autil.mk_sub(ls, i), m); + expr_ref ls_minus_i(mk_sub(ls, i), m); expr_ref xe(m_util.str.mk_concat(x, e), m); expr_ref zero(m_autil.mk_int(0), m); - literal i_ge_0 = mk_literal(m_autil.mk_ge(i, m_autil.mk_int(0))); - literal i_le_l = mk_literal(m_autil.mk_le(i, l)); - literal i_ge_ls = mk_literal(m_autil.mk_ge(i, ls)); - literal l_ge_ls = mk_literal(m_autil.mk_ge(l, ls)); + literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero)); + literal i_le_l = mk_literal(m_autil.mk_le(mk_sub(i, l), zero)); + literal i_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero)); + literal l_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(l, ls), zero)); literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero)); add_axiom(~i_ge_0, i_ge_ls, mk_literal(m_util.str.mk_prefix(xe, s))); @@ -885,16 +886,17 @@ void theory_seq::add_extract_axiom(expr* e) { void theory_seq::add_at_axiom(expr* e) { expr* s, *i; VERIFY(m_util.str.is_at(e, s, i)); - expr_ref x(m), y(m), lx(m), le(m), xey(m), one(m), len_e(m), len_x(m); + expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m); x = mk_skolem(symbol("at_left"), s); y = mk_skolem(symbol("at_right"), s); xey = m_util.str.mk_concat(x, e, y); + zero = m_autil.mk_int(0); one = m_autil.mk_int(1); len_e = m_util.str.mk_length(e); len_x = m_util.str.mk_length(x); - literal i_ge_0 = mk_literal(m_autil.mk_ge(i, m_autil.mk_int(0))); - literal i_ge_len_s = mk_literal(m_autil.mk_ge(i, m_util.str.mk_length(s))); + literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero)); + literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero)); add_axiom(~i_ge_0, i_ge_len_s, mk_eq(s, xey, false)); add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false)); @@ -910,12 +912,14 @@ literal theory_seq::mk_literal(expr* _e) { } void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { + context& ctx = get_context(); literal_vector lits; if (l1 != null_literal) lits.push_back(l1); if (l2 != null_literal) lits.push_back(l2); if (l3 != null_literal) lits.push_back(l3); if (l4 != null_literal) lits.push_back(l4); - get_context().mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index b5f8ac476..49a906e62 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -143,7 +143,8 @@ namespace smt { 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); - + + // final check bool check_ineqs(); // check if inequalities are violated. bool simplify_and_solve_eqs(); // solve unitary equalities bool branch_variable(); // branch on a variable @@ -154,6 +155,8 @@ namespace smt { 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(); + + // asserting consequences 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); @@ -162,16 +165,21 @@ namespace smt { bool find_branch_candidate(expr* l, ptr_vector const& rs); bool assume_equality(expr* l, expr* r); + // variable solving utilities 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); + expr_ref canonize(expr* e, enode_pair_dependency*& eqs); + expr_ref expand(expr* e, enode_pair_dependency*& eqs); + void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); + + // terms whose meaning are encoded using axioms. void enque_axiom(expr* e); void deque_axiom(expr* e); - void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal); - + void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal); void add_indexof_axiom(expr* e); void add_replace_axiom(expr* e); void add_extract_axiom(expr* e); @@ -179,17 +187,16 @@ namespace smt { void add_at_axiom(expr* n); literal mk_literal(expr* n); void tightest_prefix(expr* s, expr* x, literal lit); + expr* mk_sub(expr* a, expr* b); void new_eq_len_concat(enode* n1, enode* n2); - expr_ref canonize(expr* e, enode_pair_dependency*& eqs); - expr_ref expand(expr* e, enode_pair_dependency*& eqs); - void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0); void set_incomplete(app* term); + // diagnostics void display_equations(std::ostream& out) const; void display_deps(std::ostream& out, enode_pair_dependency* deps) const; public: