mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Taught the model_evaluator to look for definitions of partial theory functions in the model upon evaluation failure.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-14 20:29:54 +01:00
parent a479fa610a
commit 2688fd55cf
1 changed files with 76 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

127
src/model/model_evaluator.cpp
View file

@ -33,9 +33,11 @@ Revision History:
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "model/model_smt2_pp.h"
#include "ast/rewriter/var_subst.h"
struct evaluator_cfg : public default_rewriter_cfg {
ast_manager & m;
model_core & m_model;
bool_rewriter m_b_rw;
arith_rewriter m_a_rw;
@ -53,6 +55,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool m_array_equalities;
evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
m(m),
m_model(md),
m_b_rw(m),
// We must allow customers to set parameters for arithmetic rewriter/evaluator.
@ -74,6 +77,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_ar_rw.set_expand_select_store(true);
m_ar_rw.set_expand_select_ite(true);
updt_params(p);
//add_unspecified_function_models(md);
}
void updt_params(params_ref const & _p) {
@ -85,10 +89,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_array_equalities = p.array_equalities();
}
ast_manager & m() const { return m_model.get_manager(); }
bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) {
func_interp* fi = m_model.get_func_interp(f);
bool evaluate(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
func_interp * fi = m_model.get_func_interp(f);
return (fi != 0) && eval_fi(fi, num, args, result);
}
@ -101,9 +103,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool actuals_are_values = true;
for (unsigned i = 0; actuals_are_values && i < num; i++) {
actuals_are_values = m().is_value(args[i]);
}
for (unsigned i = 0; actuals_are_values && i < num; i++)
actuals_are_values = m.is_value(args[i]);
if (!actuals_are_values)
return false; // let get_macro handle it
@ -120,7 +121,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
family_id fid = f->get_family_id();
bool is_uninterp = fid != null_family_id && m().get_plugin(fid)->is_considered_uninterpreted(f);
bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
if (num == 0 && (fid == null_family_id || is_uninterp)) {
expr * val = m_model.get_const_interp(f);
if (val != 0) {
@ -145,7 +146,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
if (k == OP_EQ) {
// theory dispatch for =
SASSERT(num == 2);
family_id s_fid = m().get_sort(args[0])->get_family_id();
family_id s_fid = m.get_sort(args[0])->get_family_id();
if (s_fid == m_a_rw.get_fid())
st = m_a_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_bv_rw.get_fid())
@ -178,16 +179,18 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_f_rw.mk_app_core(f, num, args, result);
else if (fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_app_core(f, num, args, result);
else if (fid == m().get_label_family_id() && num == 1) {
else if (fid == m.get_label_family_id() && num == 1) {
result = args[0];
st = BR_DONE;
}
else if (evaluate(f, num, args, result)) {
TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";);
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
return BR_DONE;
}
if (st == BR_FAILED && !m.is_builtin_family_id(fid))
st = evaluate_partial_theory_func(f, num, args, result, result_pr);
if (st == BR_DONE && is_app(result)) {
app* a = to_app(result);
if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
@ -200,14 +203,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
void expand_value(expr_ref& val) {
vector<expr_ref_vector> stores;
expr_ref else_case(m());
expr_ref else_case(m);
bool _unused;
if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) {
sort* srt = m().get_sort(val);
sort* srt = m.get_sort(val);
val = m_ar.mk_const_array(srt, else_case);
for (unsigned i = stores.size(); i > 0; ) {
--i;
expr_ref_vector args(m());
expr_ref_vector args(m);
args.push_back(val);
args.append(stores[i].size(), stores[i].c_ptr());
val = m_ar.mk_store(args.size(), args.c_ptr());
@ -220,6 +223,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
func_interp * fi = m_model.get_func_interp(f);
if (fi != 0) {
TRACE_MACRO;
if (fi->is_partial()) {
@ -228,31 +232,52 @@ struct evaluator_cfg : public default_rewriter_cfg {
expr * val = m_model.get_some_value(s);
fi->set_else(val);
}
else {
else
return false;
}
}
def = fi->get_interp();
def = fi->get_interp();
SASSERT(def != 0);
return true;
}
if (m_model_completion &&
(f->get_family_id() == null_family_id ||
m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
{
TRACE_MACRO;
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
func_interp * new_fi = alloc(func_interp, m, f->get_arity());
new_fi->set_else(val);
m_model.register_decl(f, new_fi);
def = val;
return true;
}
return false;
}
br_status evaluate_partial_theory_func(func_decl * f,
unsigned num, expr * const * args,
expr_ref & result, proof_ref & result_pr) {
SASSERT(f != 0);
SASSERT(!m.is_builtin_family_id(f->get_family_id()));
result = 0;
result_pr = 0;
func_interp * fi = m_model.get_func_interp(f);
if (fi) {
if (fi->is_partial())
fi->set_else(m.get_some_value(f->get_range()));
var_subst vs(m, false);
vs(fi->get_interp(), num, args, result);
return BR_REWRITE_FULL;
}
return BR_FAILED;
}
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("model evaluator");
@ -266,7 +291,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
if (a == b) {
result = m().mk_true();
result = m.mk_true();
return BR_DONE;
}
if (!m_array_equalities) {
@ -275,19 +300,19 @@ struct evaluator_cfg : public default_rewriter_cfg {
vector<expr_ref_vector> stores1, stores2;
bool args_are_unique1, args_are_unique2;
expr_ref else1(m()), else2(m());
expr_ref else1(m), else2(m);
if (extract_array_func_interp(a, stores1, else1, args_are_unique1) &&
extract_array_func_interp(b, stores2, else2, args_are_unique2)) {
expr_ref_vector conj(m()), args1(m()), args2(m());
if (m().are_equal(else1, else2)) {
expr_ref_vector conj(m), args1(m), args2(m);
if (m.are_equal(else1, else2)) {
// no op
}
else if (m().are_distinct(else1, else2) && !(m().get_sort(else1)->get_info()->get_num_elements().is_finite())) {
result = m().mk_false();
else if (m.are_distinct(else1, else2) && !(m.get_sort(else1)->get_info()->get_num_elements().is_finite())) {
result = m.mk_false();
return BR_DONE;
}
else {
conj.push_back(m().mk_eq(else1, else2));
conj.push_back(m.mk_eq(else1, else2));
}
if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
@ -300,11 +325,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
for (unsigned i = 0; i < stores1.size(); ++i) {
args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].c_ptr());
args2.resize(1); args2.append(stores1[i].size() - 1, stores1[i].c_ptr());
expr_ref s1(m_ar.mk_select(args1.size(), args1.c_ptr()), m());
expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m());
conj.push_back(m().mk_eq(s1, s2));
expr_ref s1(m_ar.mk_select(args1.size(), args1.c_ptr()), m);
expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m);
conj.push_back(m.mk_eq(s1, s2));
}
result = m().mk_and(conj.size(), conj.c_ptr());
result = m.mk_and(conj.size(), conj.c_ptr());
return BR_REWRITE_FULL;
}
return BR_FAILED;
@ -362,15 +387,15 @@ struct evaluator_cfg : public default_rewriter_cfg {
if (table1.find(stores2[i].c_ptr(), args)) {
switch (compare(args[arity], val)) {
case l_true: table1.remove(args); break;
case l_false: result = m().mk_false(); return BR_DONE;
default: conj.push_back(m().mk_eq(val, args[arity])); break;
case l_false: result = m.mk_false(); return BR_DONE;
default: conj.push_back(m.mk_eq(val, args[arity])); break;
}
}
else {
switch (compare(else1, val)) {
case l_true: break;
case l_false: result = m().mk_false(); return BR_DONE;
default: conj.push_back(m().mk_eq(else1, val)); break;
case l_false: result = m.mk_false(); return BR_DONE;
default: conj.push_back(m.mk_eq(else1, val)); break;
}
}
}
@ -378,8 +403,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
for (; it != end; ++it) {
switch (compare((*it)[arity], else2)) {
case l_true: break;
case l_false: result = m().mk_false(); return BR_DONE;
default: conj.push_back(m().mk_eq((*it)[arity], else2)); break;
case l_false: result = m.mk_false(); return BR_DONE;
default: conj.push_back(m.mk_eq((*it)[arity], else2)); break;
}
}
result = mk_and(conj);
@ -387,8 +412,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
lbool compare(expr* a, expr* b) {
if (m().are_equal(a, b)) return l_true;
if (m().are_distinct(a, b)) return l_false;
if (m.are_equal(a, b)) return l_true;
if (m.are_distinct(a, b)) return l_false;
return l_undef;
}
@ -396,8 +421,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool args_are_values(expr_ref_vector const& store, bool& are_unique) {
bool are_values = true;
for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) {
are_values = m().is_value(store[j]);
are_unique &= m().is_unique_value(store[j]);
are_values = m.is_value(store[j]);
are_unique &= m.is_unique_value(store[j]);
}
SASSERT(!are_unique || are_values);
return are_values;
@ -408,10 +433,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
SASSERT(m_ar.is_array(a));
bool are_values = true;
are_unique = true;
TRACE("model_evaluator", tout << mk_pp(a, m()) << "\n";);
TRACE("model_evaluator", tout << mk_pp(a, m) << "\n";);
while (m_ar.is_store(a)) {
expr_ref_vector store(m());
expr_ref_vector store(m);
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
are_values &= args_are_values(store, are_unique);
stores.push_back(store);
@ -424,7 +449,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
if (!m_ar.is_as_array(a)) {
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m) << "\n";);
return false;
}
@ -434,13 +459,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
unsigned arity = f->get_arity();
unsigned base_sz = stores.size();
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector store(m());
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";);
TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";);
return false;
}
}
@ -448,18 +473,18 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
else_case = g->get_else();
if (!else_case) {
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";
/*model_smt2_pp(tout, m(), m_model, 0);*/
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";
/*model_smt2_pp(tout, m, m_model, 0);*/
);
return false;
}
if (!is_ground(else_case)) {
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";);
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m) << "\n" << else_case << "\n";);
return false;
}
for (unsigned i = stores.size(); are_values && i > base_sz; ) {
--i;
if (m().are_equal(else_case, stores[i].back())) {
if (m.are_equal(else_case, stores[i].back())) {
for (unsigned j = i + 1; j < stores.size(); ++j) {
stores[j-1].reset();
stores[j-1].append(stores[j]);
@ -469,7 +494,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
are_values &= args_are_values(stores[i], are_unique);
}
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";);
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m) << "\n";);
return true;
}