3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 17:03:18 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-10 01:36:17 -08:00
parent f9ca66d90b
commit d81186eaca
3 changed files with 56 additions and 41 deletions

View file

@ -90,6 +90,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom
} }
bool is_match = true; bool is_match = true;
for (unsigned i = 0; is_match && i < dsz; ++i) { for (unsigned i = 0; is_match && i < dsz; ++i) {
SASSERT(dom[i]);
is_match = match(binding, dom[i], sig.m_dom[0].get()); is_match = match(binding, dom[i], sig.m_dom[0].get());
} }
if (range && is_match) { 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()); m.raise_exception(strm.str().c_str());
} }
range_out = apply_binding(binding, sig.m_range); range_out = apply_binding(binding, sig.m_range);
SASSERT(range_out);
TRACE("seq_verbose", tout << mk_pp(range_out, m) << "\n";); 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()); m.raise_exception(strm.str().c_str());
} }
range_out = apply_binding(binding, sig.m_range); range_out = apply_binding(binding, sig.m_range);
SASSERT(range_out);
} }
sort* seq_decl_plugin::apply_binding(ptr_vector<sort> const& binding, sort* s) { sort* seq_decl_plugin::apply_binding(ptr_vector<sort> 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_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_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_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_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_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA);
m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT); 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_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_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_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) { 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)); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
case _OP_SEQ_SKOLEM: 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: default:
UNREACHABLE(); UNREACHABLE();
return 0; 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) { app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
SASSERT(range);
parameter param(name); parameter param(name);
func_decl* f = m.mk_func_decl(get_family_id(), _OP_SEQ_SKOLEM, 1, &param, n, args, range); func_decl* f = m.mk_func_decl(get_family_id(), _OP_SEQ_SKOLEM, 1, &param, n, args, range);
return m.mk_app(f, n, args); return m.mk_app(f, n, args);

View file

@ -269,9 +269,7 @@ bool theory_seq::assume_equality(expr* l, expr* r) {
else { else {
SASSERT(ctx.e_internalized(l)); SASSERT(ctx.e_internalized(l));
if (!ctx.e_internalized(r)) ctx.internalize(r, false); if (!ctx.e_internalized(r)) ctx.internalize(r, false);
enode* n1 = ctx.get_enode(l); ctx.assume_eq(ctx.get_enode(l), ctx.get_enode(r));
enode* n2 = ctx.get_enode(r);
ctx.assume_eq(n1, n2);
} }
return true; return true;
} }
@ -398,7 +396,12 @@ bool theory_seq::occurs(expr* a, expr* b) {
} }
bool theory_seq::is_var(expr* a) { 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) { 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); 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) { void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) {
context& ctx = get_context(); context& ctx = get_context();
m_rep.update(l, r, deps); m_rep.update(l, r, deps);
// TBD: skip new equalities for non-internalized terms. // TBD: skip new equalities for non-internalized terms.
if (ctx.e_internalized(l) && ctx.e_internalized(r)) { if (ctx.e_internalized(l) && ctx.e_internalized(r)) {
enode* n1 = ctx.get_enode(l); propagate_eq(deps, ctx.get_enode(l), ctx.get_enode(r));
enode* n2 = ctx.get_enode(r);
propagate_eq(deps, n1, n2);
} }
} }
@ -467,8 +467,6 @@ bool theory_seq::simplify_and_solve_eqs() {
return change; return change;
} }
bool theory_seq::internalize_atom(app* a, bool) { bool theory_seq::internalize_atom(app* a, bool) {
return internalize_term(a); return internalize_term(a);
} }
@ -484,17 +482,16 @@ bool theory_seq::internalize_term(app* term) {
mk_var(ctx.get_enode(arg)); mk_var(ctx.get_enode(arg));
} }
} }
enode* e = 0;
if (ctx.e_internalized(term)) {
e = ctx.get_enode(term);
}
if (m.is_bool(term)) { if (m.is_bool(term)) {
bool_var bv = ctx.mk_bool_var(term); bool_var bv = ctx.mk_bool_var(term);
ctx.set_var_theory(bv, get_id()); ctx.set_var_theory(bv, get_id());
ctx.set_enode_flag(bv, true);
} }
else { 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); e = ctx.mk_enode(term, false, m.is_bool(term), true);
} }
mk_var(e); 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) { void theory_seq::set_incomplete(app* term) {
TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";);
if (!m_incomplete) { if (!m_incomplete) {
TRACE("seq", tout << "Incomplete operator: " << mk_pp(term, m) << "\n";);
m_trail_stack.push(value_trail<theory_seq, bool>(m_incomplete)); m_trail_stack.push(value_trail<theory_seq, bool>(m_incomplete));
m_incomplete = true; 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) { void theory_seq::new_eq_len_concat(enode* n1, enode* n2) {
context& ctx = get_context(); context& ctx = get_context();
if (n1->get_root() == n2->get_root()) {
return;
}
SASSERT(n1->get_root() != n2->get_root()); SASSERT(n1->get_root() != n2->get_root());
if (!m_util.is_seq(n1->get_owner())) { if (!m_util.is_seq(n1->get_owner())) {
return; return;
@ -713,10 +713,7 @@ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) {
enode* start2 = n2; enode* start2 = n2;
do { do {
expr* o = n2->get_owner(); expr* o = n2->get_owner();
if (m_util.str.is_concat(o) || if (!is_var(o)) {
m_util.str.is_unit(o) ||
m_util.str.is_string(o) ||
m_util.str.is_empty(o)) {
expr_ref ln(m_util.str.mk_length(o), m); expr_ref ln(m_util.str.mk_length(o), m);
enque_axiom(ln); 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)); VERIFY(m_util.str.is_replace(r, a, s, t));
expr_ref x = mk_skolem(m_contains_left_sym, s, a); expr_ref x = mk_skolem(m_contains_left_sym, s, a);
expr_ref y = mk_skolem(m_contains_right_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, t, y), m);
expr_ref xty(m_util.str.mk_concat(x, s, 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)); literal cnt = mk_literal(m_util.str.mk_contains(s, a));
add_axiom(cnt, mk_eq(r, a, false)); add_axiom(cnt, mk_eq(r, a, false));
add_axiom(~cnt, mk_eq(a, xsy, 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. 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 ls(m_util.str.mk_length(s), m);
expr_ref lx(m_util.str.mk_length(x), m); expr_ref lx(m_util.str.mk_length(x), m);
expr_ref le(m_util.str.mk_length(e), 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 xe(m_util.str.mk_concat(x, e), m);
expr_ref zero(m_autil.mk_int(0), 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_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
literal i_le_l = mk_literal(m_autil.mk_le(i, l)); 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(i, ls)); 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(l, ls)); 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)); 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))); 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) { void theory_seq::add_at_axiom(expr* e) {
expr* s, *i; expr* s, *i;
VERIFY(m_util.str.is_at(e, 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); x = mk_skolem(symbol("at_left"), s);
y = mk_skolem(symbol("at_right"), s); y = mk_skolem(symbol("at_right"), s);
xey = m_util.str.mk_concat(x, e, y); xey = m_util.str.mk_concat(x, e, y);
zero = m_autil.mk_int(0);
one = m_autil.mk_int(1); one = m_autil.mk_int(1);
len_e = m_util.str.mk_length(e); len_e = m_util.str.mk_length(e);
len_x = m_util.str.mk_length(x); 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_0 = mk_literal(m_autil.mk_ge(i, zero));
literal i_ge_len_s = mk_literal(m_autil.mk_ge(i, m_util.str.mk_length(s))); 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(s, xey, false));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, 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) { void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) {
context& ctx = get_context();
literal_vector lits; literal_vector lits;
if (l1 != null_literal) lits.push_back(l1); if (l1 != null_literal) lits.push_back(l1);
if (l2 != null_literal) lits.push_back(l2); if (l2 != null_literal) lits.push_back(l2);
if (l3 != null_literal) lits.push_back(l3); if (l3 != null_literal) lits.push_back(l3);
if (l4 != null_literal) lits.push_back(l4); 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());
} }

View file

@ -143,7 +143,8 @@ namespace smt {
virtual void collect_statistics(::statistics & st) const; virtual void collect_statistics(::statistics & st) const;
virtual model_value_proc * mk_value(enode * n, model_generator & mg); virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual void init_model(model_generator & mg); virtual void init_model(model_generator & mg);
// final check
bool check_ineqs(); // check if inequalities are violated. bool check_ineqs(); // check if inequalities are violated.
bool simplify_and_solve_eqs(); // solve unitary equalities bool simplify_and_solve_eqs(); // solve unitary equalities
bool branch_variable(); // branch on a variable 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 simplify_eq(expr* l, expr* r, enode_pair_dependency* dep);
bool solve_unit_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 solve_basic_eqs();
// asserting consequences
void propagate_lit(enode_pair_dependency* dep, literal lit); void propagate_lit(enode_pair_dependency* dep, literal lit);
void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2); void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2);
void propagate_eq(bool_var v, expr* e1, expr* e2); void propagate_eq(bool_var v, expr* e1, expr* e2);
@ -162,16 +165,21 @@ namespace smt {
bool find_branch_candidate(expr* l, ptr_vector<expr> const& rs); bool find_branch_candidate(expr* l, ptr_vector<expr> const& rs);
bool assume_equality(expr* l, expr* r); bool assume_equality(expr* l, expr* r);
// variable solving utilities
bool occurs(expr* a, expr* b); bool occurs(expr* a, expr* b);
bool is_var(expr* b); bool is_var(expr* b);
void add_solution(expr* l, expr* r, enode_pair_dependency* dep); void add_solution(expr* l, expr* r, enode_pair_dependency* dep);
bool is_left_select(expr* a, expr*& b); bool is_left_select(expr* a, expr*& b);
bool is_right_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 enque_axiom(expr* e);
void deque_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_indexof_axiom(expr* e);
void add_replace_axiom(expr* e); void add_replace_axiom(expr* e);
void add_extract_axiom(expr* e); void add_extract_axiom(expr* e);
@ -179,17 +187,16 @@ namespace smt {
void add_at_axiom(expr* n); void add_at_axiom(expr* n);
literal mk_literal(expr* n); literal mk_literal(expr* n);
void tightest_prefix(expr* s, expr* x, literal lit); 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); 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); expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0);
void set_incomplete(app* term); void set_incomplete(app* term);
// diagnostics
void display_equations(std::ostream& out) const; void display_equations(std::ostream& out) const;
void display_deps(std::ostream& out, enode_pair_dependency* deps) const; void display_deps(std::ostream& out, enode_pair_dependency* deps) const;
public: public: