3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00

add equality propagation based on partial length information to sequence theory. Fix issue #429

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-04 08:12:46 -08:00
parent 9b979b6e1e
commit 9c7e5c37d1
8 changed files with 200 additions and 44 deletions

View file

@ -1484,6 +1484,7 @@ bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr
if (is_sat) {
lhs.push_back(concat_non_empty(szl, l));
rhs.push_back(concat_non_empty(szr, r));
//split_units(lhs, rhs);
}
return true;
}
@ -1492,13 +1493,39 @@ bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr
if (is_sat) {
lhs.push_back(concat_non_empty(szl, l));
rhs.push_back(concat_non_empty(szr, r));
//split_units(lhs, rhs);
}
return true;
}
}
return false;
}
void seq_rewriter::split_units(expr_ref_vector& lhs, expr_ref_vector& rhs) {
expr* a, *b, *a1, *b1, *a2, *b2;
while (true) {
if (m_util.str.is_unit(lhs.back(), a) &&
m_util.str.is_unit(rhs.back(), b)) {
lhs[lhs.size()-1] = a;
rhs[rhs.size()-1] = b;
break;
}
if (m_util.str.is_concat(lhs.back(), a, a2) &&
m_util.str.is_unit(a, a1) &&
m_util.str.is_concat(rhs.back(), b, b2) &&
m_util.str.is_unit(b, b1)) {
expr_ref _pin_a(lhs.back(), m()), _pin_b(rhs.back(), m());
lhs[lhs.size()-1] = a1;
rhs[rhs.size()-1] = b1;
lhs.push_back(a2);
rhs.push_back(b2);
}
else {
break;
}
}
}
bool seq_rewriter::is_epsilon(expr* e) const {
expr* e1;
return m_util.re.is_to_re(e, e1) && m_util.str.is_empty(e1);

View file

@ -113,6 +113,7 @@ class seq_rewriter {
bool is_sequence(expr* e, expr_ref_vector& seq);
bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
bool is_epsilon(expr* e) const;
void split_units(expr_ref_vector& lhs, expr_ref_vector& rhs);
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):

View file

@ -81,14 +81,6 @@ namespace smt {
}
};
arith_simplifier_plugin * arith_eq_adapter::get_simplifier() {
if (!m_as) {
simplifier & s = get_context().get_simplifier();
m_as = static_cast<arith_simplifier_plugin*>(s.get_plugin(m_owner.get_family_id()));
}
return m_as;
}
void arith_eq_adapter::mk_axioms(enode * n1, enode * n2) {
SASSERT(n1 != n2);
ast_manager & m = get_manager();
@ -103,6 +95,9 @@ namespace smt {
// We don't need to create axioms for 2 = 3
return;
}
if (t1 == t2) {
return;
}
context & ctx = get_context();
CTRACE("arith_eq_adapter_relevancy", !(ctx.is_relevant(n1) && ctx.is_relevant(n2)),
@ -192,6 +187,7 @@ namespace smt {
// Old version that used to be buggy.
// I fixed the theory arithmetic internalizer to accept non simplified terms of the form t1 - t2
// if t1 and t2 already have slacks (theory variables) associated with them.
// It also accepts terms with repeated variables (Issue #429).
app * le = 0;
app * ge = 0;
if (m_util.is_numeral(t1))
@ -199,12 +195,13 @@ namespace smt {
if (m_util.is_numeral(t2)) {
le = m_util.mk_le(t1, t2);
ge = m_util.mk_ge(t1, t2);
}
}
else {
sort * st = m.get_sort(t1);
app * minus_one = m_util.mk_numeral(rational::minus_one(), st);
app * zero = m_util.mk_numeral(rational::zero(), st);
app_ref s(m_util.mk_add(t1, m_util.mk_mul(minus_one, t2)), m);
app_ref minus_one(m_util.mk_numeral(rational::minus_one(), st), m);
app_ref zero(m_util.mk_numeral(rational::zero(), st), m);
app_ref t3(m_util.mk_mul(minus_one, t2), m);
app_ref s(m_util.mk_add(t1, t3), m);
le = m_util.mk_le(s, zero);
ge = m_util.mk_ge(s, zero);
}

View file

@ -75,8 +75,6 @@ namespace smt {
ast_manager & get_manager() const { return m_owner.get_manager(); }
enode * get_enode(theory_var v) const { return m_owner.get_enode(v); }
arith_simplifier_plugin * get_simplifier();
public:
arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u), m_as(0) {}
void new_eq_eh(theory_var v1, theory_var v2);

View file

@ -450,6 +450,9 @@ namespace smt {
svector<theory_var> m_nl_propagated; // non linear monomials that became linear
v_dependency_manager m_dep_manager; // for tracking bounds during non-linear reasoning
vector<uint_set> m_row_vars; // variables in a given row. Used during internalization to detect repeated variables.
unsigned m_row_vars_top;
var_heap m_to_patch; // heap containing all variables v s.t. m_value[v] does not satisfy bounds of v.
nat_set m_left_basis; // temporary: set of variables that already left the basis in make_feasible
bool m_blands_rule;
@ -583,6 +586,9 @@ namespace smt {
void mk_enode_if_reflect(app * n);
template<bool invert>
void add_row_entry(unsigned r_id, numeral const & coeff, theory_var v);
uint_set& row_vars();
class scoped_row_vars;
void internalize_internal_monomial(app * m, unsigned r_id);
theory_var internalize_add(app * n);
theory_var internalize_mul_core(app * m);

View file

@ -197,6 +197,15 @@ namespace smt {
}
}
/**
\brief access the current set of variables associated with row.
*/
template<typename Ext>
uint_set& theory_arith<Ext>::row_vars() {
SASSERT(m_row_vars_top > 0);
return m_row_vars[m_row_vars_top-1];
}
/**
\brief Add coeff * v to the row r.
The column is also updated.
@ -206,6 +215,26 @@ namespace smt {
void theory_arith<Ext>::add_row_entry(unsigned r_id, numeral const & coeff, theory_var v) {
row & r = m_rows[r_id];
column & c = m_columns[v];
if (row_vars().contains(v)) {
typename vector<row_entry>::iterator it = r.begin_entries();
typename vector<row_entry>::iterator end = r.end_entries();
bool found = false;
for (; !found && it != end; ++it) {
SASSERT(!it->is_dead());
if (it->m_var == v) {
if (invert) {
it->m_coeff -= coeff;
}
else {
it->m_coeff += coeff;
}
found = true;
}
}
SASSERT(found);
return;
}
row_vars().insert(v);
int r_idx;
row_entry & r_entry = r.add_row_entry(r_idx);
int c_idx;
@ -238,12 +267,13 @@ namespace smt {
}
}
rational _val;
if (m_util.is_mul(m) && m_util.is_numeral(m->get_arg(0), _val)) {
expr* arg1, *arg2;
if (m_util.is_mul(m, arg1, arg2) && m_util.is_numeral(arg1, _val)) {
SASSERT(m->get_num_args() == 2);
numeral val(_val);
theory_var v = internalize_term_core(to_app(m->get_arg(1)));
theory_var v = internalize_term_core(to_app(arg2));
if (reflection_enabled()) {
internalize_term_core(to_app(m->get_arg(0)));
internalize_term_core(to_app(arg1));
mk_enode(m);
}
add_row_entry<true>(r_id, val, v);
@ -264,6 +294,7 @@ namespace smt {
CTRACE("internalize_add_bug", n->get_num_args() == 2 && n->get_arg(0) == n->get_arg(1), tout << "n: " << mk_pp(n, get_manager()) << "\n";);
SASSERT(m_util.is_add(n));
unsigned r_id = mk_row();
scoped_row_vars _sc(m_row_vars, m_row_vars_top);
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
internalize_internal_monomial(to_app(n->get_arg(i)), r_id);
@ -324,6 +355,7 @@ namespace smt {
numeral val(_val);
SASSERT(!val.is_one());
unsigned r_id = mk_row();
scoped_row_vars _sc(m_row_vars, m_row_vars_top);
if (reflection_enabled())
internalize_term_core(to_app(m->get_arg(0)));
theory_var v = internalize_mul_core(to_app(m->get_arg(1)));
@ -617,6 +649,7 @@ namespace smt {
enode * e = mk_enode(n);
theory_var r = mk_var(e);
unsigned r_id = mk_row();
scoped_row_vars _sc(m_row_vars, m_row_vars_top);
add_row_entry<true>(r_id, numeral(1), arg);
add_row_entry<false>(r_id, numeral(1), r);
init_row(r_id);
@ -644,6 +677,25 @@ namespace smt {
return v;
}
template<typename Ext>
class theory_arith<Ext>::scoped_row_vars {
unsigned& m_top;
public:
scoped_row_vars(vector<uint_set>& row_vars, unsigned& top):
m_top(top)
{
SASSERT(row_vars.size() >= top);
if (row_vars.size() == top) {
row_vars.push_back(uint_set());
}
row_vars[top].reset();
++m_top;
}
~scoped_row_vars() {
--m_top;
}
};
/**
\brief Internalize the given term and return an alias for it.
Return null_theory_var if the term was not implemented by the theory yet.
@ -1579,6 +1631,7 @@ namespace smt {
m_liberal_final_check(true),
m_changed_assignment(false),
m_assume_eq_head(0),
m_row_vars_top(0),
m_nl_rounds(0),
m_nl_gb_exhausted(false),
m_nl_new_exprs(m),

View file

@ -533,11 +533,14 @@ bool theory_seq::is_eq(expr* e, expr*& a, expr*& b) const {
(a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true);
}
bool theory_seq::is_pre(expr* e, expr*& s, expr*& i) {
return is_skolem(m_pre, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
}
bool theory_seq::is_post(expr* e, expr*& s, expr*& i) {
return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
}
expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
@ -782,6 +785,9 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
if (lhs.empty()) {
return true;
}
TRACE("seq",
tout << ls << " = " << rs << "\n";
tout << lhs << " = " << rhs << "\n";);
for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) {
expr_ref li(lhs[i].get(), m);
expr_ref ri(rhs[i].get(), m);
@ -789,8 +795,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
// no-op
}
else if (m_util.is_seq(li) || m_util.is_re(li)) {
reduce_length(li, ri);
m_eqs.push_back(mk_eqdep(li, ri, deps));
m_eqs.push_back(mk_eqdep(li, ri, deps));
}
else {
propagate_eq(deps, ensure_enode(li), ensure_enode(ri));
@ -817,16 +822,11 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
return false;
}
bool theory_seq::reduce_length(expr* l, expr* r) {
expr* l2, *r2;
bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) {
expr_ref len1(m), len2(m);
literal_vector lits;
m_util.str.is_concat(l, l, l2);
m_util.str.is_concat(r, r, r2);
lits.reset();
if (get_length(l, len1, lits) &&
get_length(r, len2, lits) && len1 == len2) {
TRACE("seq", tout << "Propagate equal lengths\n";);
//propagate_eq(lits, l, r, true);
return true;
}
else {
@ -914,8 +914,8 @@ bool theory_seq::solve_eqs(unsigned i) {
eq e1 = m_eqs[m_eqs.size()-1];
m_eqs.set(i, e1);
--i;
++m_stats.m_num_reductions;
}
++m_stats.m_num_reductions;
m_eqs.pop_back();
change = true;
}
@ -945,6 +945,10 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
TRACE("seq", tout << "unit\n";);
return true;
}
if (!ctx.inconsistent() && reduce_length_eq(ls, rs, deps)) {
TRACE("seq", tout << "length\n";);
return true;
}
if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) {
TRACE("seq", tout << "binary\n";);
return true;
@ -990,6 +994,43 @@ bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const&
return false;
}
bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
if (ls.empty() || rs.empty()) {
return false;
}
if (ls.size() <= 1 && rs.size() <= 1) {
return false;
}
SASSERT(ls.size() > 1 || rs.size() > 1);
literal_vector lits;
expr_ref l(ls[0], m), r(rs[0], m);
if (reduce_length(l, r, lits)) {
expr_ref_vector lhs(m), rhs(m);
lhs.append(ls.size()-1, ls.c_ptr() + 1);
rhs.append(rs.size()-1, rs.c_ptr() + 1);
SASSERT(!lhs.empty() || !rhs.empty());
m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";);
propagate_eq(deps, lits, l, r, true);
return true;
}
l = ls.back(); r = rs.back();
if (reduce_length(l, r, lits)) {
expr_ref_vector lhs(m), rhs(m);
lhs.append(ls.size()-1, ls.c_ptr());
rhs.append(rs.size()-1, rs.c_ptr());
SASSERT(!lhs.empty() || !rhs.empty());
m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";);
propagate_eq(deps, lits, l, r, true);
return true;
}
return false;
}
bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
context& ctx = get_context();
ptr_vector<expr> xs, ys;
@ -1064,51 +1105,78 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
context& ctx = get_context();
expr* s, *i, *l;
rational r;
if (m_util.str.is_extract(e, s, i, l)) {
// 0 <= i <= len(s), 0 <= l, i + l <= len(s)
expr_ref zero(m_autil.mk_int(0), m);
expr_ref ls(m_util.str.mk_length(s), m);
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
literal _lits[4] = { i_ge_0, i_lt_len_s, li_ge_ls, l_ge_zero };
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true &&
ctx.get_assignment(li_ge_ls) == l_true &&
ctx.get_assignment(l_ge_zero) == l_true) {
len = l;
lits.push_back(i_ge_0); lits.push_back(i_lt_len_s); lits.push_back(li_ge_ls); lits.push_back(l_ge_zero);
lits.append(4, _lits);
return true;
}
TRACE("seq", tout << mk_pp(e, m) << "\n"; ctx.display_literals_verbose(tout, 4, _lits); tout << "\n";
for (unsigned i = 0; i < 4; ++i) tout << ctx.get_assignment(_lits[i]) << "\n";);
}
else if (m_util.str.is_at(e, s, i)) {
// has length 1 if 0 <= i < len(s)
expr_ref zero(m_autil.mk_int(0), m);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
literal _lits[2] = { i_ge_0, i_lt_len_s};
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true) {
len = m_autil.mk_int(1);
lits.push_back(i_ge_0); lits.push_back(i_lt_len_s);
lits.append(2, _lits);
return true;
}
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
}
else if (is_pre(e, s, i)) {
expr_ref zero(m_autil.mk_int(0), m);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
literal _lits[2] = { i_ge_0, i_lt_len_s };
if (ctx.get_assignment(i_ge_0) == l_true &&
ctx.get_assignment(i_lt_len_s) == l_true) {
len = i;
lits.push_back(i_ge_0); lits.push_back(i_lt_len_s);
lits.append(2, _lits);
return true;
}
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
}
else if (is_post(e, s, l)) {
expr_ref zero(m_autil.mk_int(0), m);
literal l_ge_0 = mk_literal(m_autil.mk_ge(l, zero));
literal l_le_len_s = mk_literal(m_autil.mk_ge(mk_sub(m_util.str.mk_length(s), l), zero));
literal _lits[2] = { l_ge_0, l_le_len_s };
if (ctx.get_assignment(l_ge_0) == l_true &&
ctx.get_assignment(l_le_len_s) == l_true) {
len = l;
lits.append(2, _lits);
return true;
}
TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
}
else if (m_util.str.is_unit(e)) {
len = m_autil.mk_int(1);
return true;
}
else {
TRACE("seq", tout << "unhandled: " << mk_pp(e, m) << "\n";);
}
return false;
}
@ -2526,10 +2594,10 @@ bool theory_seq::is_skolem(symbol const& s, expr* e) const {
void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs) {
literal_vector lits;
lits.push_back(lit);
propagate_eq(lits, e1, e2, add_to_eqs);
propagate_eq(0, lits, e1, e2, add_to_eqs);
}
void theory_seq::propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs) {
void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, expr* e1, expr* e2, bool add_to_eqs) {
context& ctx = get_context();
enode* n1 = ensure_enode(e1);
@ -2539,10 +2607,14 @@ void theory_seq::propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bo
}
ctx.mark_as_relevant(n1);
ctx.mark_as_relevant(n2);
literal_vector lits(_lits);
enode_pair_vector eqs;
linearize(deps, eqs, lits);
if (add_to_eqs) {
dependency* deps = 0;
for (unsigned i = 0; i < lits.size(); ++i) {
literal lit = lits[i];
for (unsigned i = 0; i < _lits.size(); ++i) {
literal lit = _lits[i];
SASSERT(l_true == ctx.get_assignment(lit));
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
}
@ -2554,7 +2626,7 @@ void theory_seq::propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bo
justification* js =
ctx.mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, n1, n2));
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
m_new_propagation = true;
ctx.assign_eq(n1, n2, eq_justification(js));

View file

@ -335,7 +335,8 @@ namespace smt {
bool propagate_max_length(expr* l, expr* r, dependency* dep);
bool get_length(expr* s, expr_ref& len, literal_vector& lits);
bool reduce_length(expr* l, expr* r);
bool reduce_length(expr* l, expr* r, literal_vector& lits);
bool reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
@ -365,7 +366,7 @@ namespace smt {
void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
void propagate_eq(dependency* dep, enode* n1, enode* n2);
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs);
void propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs);
void propagate_eq(dependency* dep, literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs);
void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
u_map<unsigned> m_branch_start;
@ -384,6 +385,7 @@ namespace smt {
bool is_tail(expr* a, expr*& s, unsigned& idx) const;
bool is_eq(expr* e, expr*& a, expr*& b) const;
bool is_pre(expr* e, expr*& s, expr*& i);
bool is_post(expr* e, expr*& s, expr*& i);
expr_ref mk_nth(expr* s, expr* idx);
expr_ref mk_last(expr* e);
expr_ref mk_first(expr* e);