mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add evaluation of array equalities to model evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
f6aaa5cc8d
commit
03336ab9f2
|
|
@ -30,6 +30,7 @@ Revision History:
|
|||
#include"fpa_rewriter.h"
|
||||
#include"rewriter_def.h"
|
||||
#include"cooperate.h"
|
||||
#include"ast_pp.h"
|
||||
|
||||
|
||||
struct evaluator_cfg : public default_rewriter_cfg {
|
||||
|
|
@ -42,6 +43,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
pb_rewriter m_pb_rw;
|
||||
fpa_rewriter m_f_rw;
|
||||
seq_rewriter m_seq_rw;
|
||||
array_util m_ar;
|
||||
unsigned long long m_max_memory;
|
||||
unsigned m_max_steps;
|
||||
bool m_model_completion;
|
||||
|
|
@ -59,7 +61,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
m_dt_rw(m),
|
||||
m_pb_rw(m),
|
||||
m_f_rw(m),
|
||||
m_seq_rw(m) {
|
||||
m_seq_rw(m),
|
||||
m_ar(m) {
|
||||
bool flat = true;
|
||||
m_b_rw.set_flat(flat);
|
||||
m_a_rw.set_flat(flat);
|
||||
|
|
@ -146,6 +149,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
st = m_f_rw.mk_eq_core(args[0], args[1], result);
|
||||
else if (s_fid == m_seq_rw.get_fid())
|
||||
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
|
||||
else if (fid == m_ar_rw.get_fid())
|
||||
st = mk_array_eq(args[0], args[1], result);
|
||||
if (st != BR_FAILED)
|
||||
return st;
|
||||
}
|
||||
|
|
@ -182,6 +187,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
return st;
|
||||
}
|
||||
|
||||
|
||||
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
|
||||
|
||||
#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
|
||||
|
|
@ -230,6 +236,85 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
|
||||
bool cache_results() const { return m_cache; }
|
||||
|
||||
|
||||
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
|
||||
if (a == b) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
vector<expr_ref_vector> stores;
|
||||
expr_ref else1(m()), else2(m());
|
||||
if (extract_array_func_interp(a, stores, else1) &&
|
||||
extract_array_func_interp(b, stores, else2)) {
|
||||
expr_ref_vector conj(m()), args1(m()), args2(m());
|
||||
conj.push_back(m().mk_eq(else1, else2));
|
||||
args1.push_back(a);
|
||||
args2.push_back(b);
|
||||
for (unsigned i = 0; i < stores.size(); ++i) {
|
||||
args1.resize(1); args1.append(stores[i].size() - 1, stores[i].c_ptr());
|
||||
args2.resize(1); args2.append(stores[i].size() - 1, stores[i].c_ptr());
|
||||
expr* s1 = m_ar.mk_select(args1.size(), args1.c_ptr());
|
||||
expr* s2 = m_ar.mk_select(args2.size(), args2.c_ptr());
|
||||
conj.push_back(m().mk_eq(s1, s2));
|
||||
}
|
||||
result = m().mk_and(conj.size(), conj.c_ptr());
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
|
||||
SASSERT(m_ar.is_array(a));
|
||||
|
||||
while (m_ar.is_store(a)) {
|
||||
expr_ref_vector store(m());
|
||||
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
|
||||
stores.push_back(store);
|
||||
a = to_app(a)->get_arg(0);
|
||||
}
|
||||
|
||||
if (m_ar.is_const(a)) {
|
||||
else_case = to_app(a)->get_arg(0);
|
||||
return true;
|
||||
}
|
||||
|
||||
if (m_ar.is_as_array(a)) {
|
||||
func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
|
||||
func_interp* g = m_model.get_func_interp(f);
|
||||
unsigned sz = g->num_entries();
|
||||
unsigned arity = f->get_arity();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr_ref_vector store(m());
|
||||
func_entry const* fe = g->get_entry(i);
|
||||
store.append(arity, fe->get_args());
|
||||
store.push_back(fe->get_result());
|
||||
for (unsigned j = 0; j < store.size(); ++j) {
|
||||
if (!is_ground(store[j].get())) {
|
||||
TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
stores.push_back(store);
|
||||
}
|
||||
else_case = g->get_else();
|
||||
if (!else_case) {
|
||||
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";);
|
||||
return false;
|
||||
}
|
||||
if (!is_ground(else_case)) {
|
||||
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << mk_pp(else_case, m()) << "\n";);
|
||||
return false;
|
||||
}
|
||||
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";);
|
||||
return true;
|
||||
}
|
||||
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
||||
template class rewriter_tpl<evaluator_cfg>;
|
||||
|
|
|
|||
|
|
@ -258,7 +258,7 @@ final_check_status theory_seq::final_check_eh() {
|
|||
TRACE("seq", tout << ">>fixed_length\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (branch_variable()) {
|
||||
if (reduce_length_eq() || branch_variable_mb() || branch_variable()) {
|
||||
++m_stats.m_branch_variable;
|
||||
TRACE("seq", tout << ">>branch_variable\n";);
|
||||
return FC_CONTINUE;
|
||||
|
|
@ -291,8 +291,7 @@ final_check_status theory_seq::final_check_eh() {
|
|||
return FC_GIVEUP;
|
||||
}
|
||||
|
||||
|
||||
bool theory_seq::branch_variable() {
|
||||
bool theory_seq::reduce_length_eq() {
|
||||
context& ctx = get_context();
|
||||
unsigned sz = m_eqs.size();
|
||||
int start = ctx.get_random_value();
|
||||
|
|
@ -304,7 +303,182 @@ bool theory_seq::branch_variable() {
|
|||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool theory_seq::branch_variable_mb() {
|
||||
context& ctx = get_context();
|
||||
unsigned sz = m_eqs.size();
|
||||
int start = ctx.get_random_value();
|
||||
bool change = false;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
unsigned k = (i + start) % sz;
|
||||
eq const& e = m_eqs[i];
|
||||
vector<rational> len1, len2;
|
||||
if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) {
|
||||
change = true;
|
||||
continue;
|
||||
}
|
||||
if (e.ls().empty() || e.rs().empty() || (!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) {
|
||||
continue;
|
||||
}
|
||||
rational l1, l2;
|
||||
for (unsigned i = 0; i < len1.size(); ++i) l1 += len1[i];
|
||||
for (unsigned i = 0; i < len2.size(); ++i) l2 += len2[i];
|
||||
if (l1 != l2) {
|
||||
TRACE("seq", tout << "lengths are not compatible\n";);
|
||||
expr_ref l = mk_concat(e.ls().size(), e.ls().c_ptr());
|
||||
expr_ref r = mk_concat(e.rs().size(), e.rs().c_ptr());
|
||||
expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m);
|
||||
add_axiom(~mk_eq(l, r, false), mk_eq(lnl, lnr, false));
|
||||
change = true;
|
||||
continue;
|
||||
}
|
||||
if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
return change;
|
||||
}
|
||||
|
||||
/*
|
||||
\brief Decompose ls = rs into Xa = bYc, such that
|
||||
1.
|
||||
- X != Y
|
||||
- |b| <= |X| <= |bY| in currrent model
|
||||
- b is non-empty.
|
||||
2. X != Y
|
||||
- b is empty
|
||||
- |X| <= |Y|
|
||||
3. |X| = 0
|
||||
- propagate X = empty
|
||||
*/
|
||||
bool theory_seq::split_lengths(dependency* dep,
|
||||
expr_ref_vector const& ls, expr_ref_vector const& rs,
|
||||
vector<rational> const& ll, vector<rational> const& rl) {
|
||||
context& ctx = get_context();
|
||||
expr_ref X(m), Y(m), b(m);
|
||||
if (ls.empty() || rs.empty()) {
|
||||
return false;
|
||||
}
|
||||
if (is_var(ls[0]) && ll[0].is_zero()) {
|
||||
return set_empty(ls[0]);
|
||||
}
|
||||
if (is_var(rs[0]) && rl[0].is_zero()) {
|
||||
return set_empty(rs[0]);
|
||||
}
|
||||
if (is_var(rs[0]) && !is_var(ls[0])) {
|
||||
return split_lengths(dep, rs, ls, rl, ll);
|
||||
}
|
||||
if (!is_var(ls[0])) {
|
||||
return false;
|
||||
}
|
||||
X = ls[0];
|
||||
rational lenX = ll[0];
|
||||
expr_ref_vector bs(m);
|
||||
SASSERT(lenX.is_pos());
|
||||
rational lenB(0), lenY(0);
|
||||
for (unsigned i = 0; lenX > lenB && i < rs.size(); ++i) {
|
||||
bs.push_back(rs[i]);
|
||||
lenY = rl[i];
|
||||
lenB += lenY;
|
||||
}
|
||||
SASSERT(lenX <= lenB);
|
||||
SASSERT(!bs.empty());
|
||||
Y = bs.back();
|
||||
bs.pop_back();
|
||||
if (!is_var(Y) && !m_util.str.is_unit(Y)) {
|
||||
TRACE("seq", tout << "TBD: non variable or unit split: " << Y << "\n";);
|
||||
return false;
|
||||
}
|
||||
if (X == Y) {
|
||||
TRACE("seq", tout << "Cycle: " << X << "\n";);
|
||||
return false;
|
||||
}
|
||||
if (lenY.is_zero()) {
|
||||
return set_empty(Y);
|
||||
}
|
||||
b = mk_concat(bs, m.get_sort(X));
|
||||
|
||||
SASSERT(X != Y);
|
||||
expr_ref split_pred = mk_skolem(symbol("seq.split"), X, b, Y, m.mk_bool_sort());
|
||||
literal split_predl = mk_literal(split_pred);
|
||||
lbool is_split = ctx.get_assignment(split_predl);
|
||||
if (is_split != l_true) {
|
||||
// split_pred <=> |b| < |X| <= |b| + |Y|
|
||||
expr_ref lenX(m_util.str.mk_length(X), m);
|
||||
expr_ref lenY(m_util.str.mk_length(Y), m);
|
||||
expr_ref lenb(m_util.str.mk_length(b), m);
|
||||
expr_ref le1(m_autil.mk_le(mk_sub(lenX, lenb), m_autil.mk_int(0)), m);
|
||||
expr_ref le2(m_autil.mk_le(mk_sub(mk_sub(lenX, lenb), lenY),
|
||||
m_autil.mk_int(0)), m);
|
||||
literal lit1(~mk_literal(le1));
|
||||
literal lit2(mk_literal(le2));
|
||||
add_axiom(~split_predl, lit1);
|
||||
add_axiom(~split_predl, lit2);
|
||||
add_axiom(split_predl, ~lit1, ~lit2);
|
||||
}
|
||||
else if (m_util.str.is_unit(Y)) {
|
||||
SASSERT(lenB == lenX);
|
||||
SASSERT(is_split == l_true);
|
||||
bs.push_back(Y);
|
||||
expr_ref bY(m_util.str.mk_concat(bs), m);
|
||||
literal_vector lits;
|
||||
lits.push_back(split_predl);
|
||||
propagate_eq(dep, lits, X, bY, true);
|
||||
}
|
||||
else {
|
||||
SASSERT(is_var(Y));
|
||||
// split_pred => X = bY1, Y = Y1Y2
|
||||
SASSERT(is_split == l_true);
|
||||
expr_ref Y1(mk_skolem(symbol("seq.left"), Y), m);
|
||||
expr_ref Y2(mk_skolem(symbol("seq.right"), Y), m);
|
||||
expr_ref bY1(m_util.str.mk_concat(b, Y1), m);
|
||||
expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
|
||||
literal_vector lits;
|
||||
lits.push_back(split_predl);
|
||||
propagate_eq(dep, lits, X, bY1, true);
|
||||
propagate_eq(dep, lits, Y, Y1Y2, true);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool theory_seq::set_empty(expr* x) {
|
||||
add_axiom(~mk_eq(m_autil.mk_int(0), m_util.str.mk_length(x), false), mk_eq_empty(x));
|
||||
return true;
|
||||
}
|
||||
|
||||
bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & len) {
|
||||
bool all_have_length = true;
|
||||
rational val;
|
||||
zstring s;
|
||||
for (unsigned i = 0; i < es.size(); ++i) {
|
||||
expr* e = es[i];
|
||||
if (m_util.str.is_unit(e)) {
|
||||
len.push_back(rational(1));
|
||||
}
|
||||
else if (m_util.str.is_empty(e)) {
|
||||
len.push_back(rational(0));
|
||||
}
|
||||
else if (m_util.str.is_string(e, s)) {
|
||||
len.push_back(rational(s.length()));
|
||||
}
|
||||
else if (get_length(e, val)) {
|
||||
len.push_back(val);
|
||||
}
|
||||
else {
|
||||
enforce_length(ensure_enode(e));
|
||||
all_have_length = false;
|
||||
}
|
||||
}
|
||||
return all_have_length;
|
||||
}
|
||||
|
||||
bool theory_seq::branch_variable() {
|
||||
context& ctx = get_context();
|
||||
unsigned sz = m_eqs.size();
|
||||
int start = ctx.get_random_value();
|
||||
|
||||
unsigned s = 0;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
|
|
@ -3050,6 +3224,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
else if (m_util.str.is_in_re(e)) {
|
||||
propagate_in_re(e, is_true);
|
||||
}
|
||||
else if (is_skolem(symbol("seq.split"), e)) {
|
||||
// propagate equalities
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -358,6 +358,8 @@ namespace smt {
|
|||
void init_model(expr_ref_vector const& es);
|
||||
// final check
|
||||
bool simplify_and_solve_eqs(); // solve unitary equalities
|
||||
bool reduce_length_eq();
|
||||
bool branch_variable_mb(); // branch on a variable, model based on length
|
||||
bool branch_variable(); // branch on a variable
|
||||
bool split_variable(); // split a variable
|
||||
bool is_solved();
|
||||
|
|
@ -367,6 +369,10 @@ namespace smt {
|
|||
bool fixed_length();
|
||||
bool fixed_length(expr* e);
|
||||
bool propagate_length_coherence(expr* e);
|
||||
bool split_lengths(dependency* dep,
|
||||
expr_ref_vector const& ls, expr_ref_vector const& rs,
|
||||
vector<rational> const& ll, vector<rational> const& rl);
|
||||
bool set_empty(expr* x);
|
||||
|
||||
bool check_extensionality();
|
||||
bool check_contains();
|
||||
|
|
@ -465,6 +471,7 @@ namespace smt {
|
|||
bool has_length(expr *e) const { return m_length.contains(e); }
|
||||
void add_length(expr* e);
|
||||
void enforce_length(enode* n);
|
||||
bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
|
||||
void enforce_length_coherence(enode* n1, enode* n2);
|
||||
|
||||
void add_elim_string_axiom(expr* n);
|
||||
|
|
|
|||
Loading…
Reference in a new issue