mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

fix indentation for mbp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-03 12:47:08 -07:00
parent 3586b613f7
commit e58eb9f302
1 changed files with 38 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

72
src/qe/qe_mbp.cpp
View file

@ -77,50 +77,50 @@ namespace {
}; };
// rewrite all occurrences of (as const arr c) to (as const arr v) where v = m_eval(c) // rewrite all occurrences of (as const arr c) to (as const arr v) where v = m_eval(c)
struct app_const_arr_rewriter : public default_rewriter_cfg { struct app_const_arr_rewriter : public default_rewriter_cfg {
ast_manager &m; ast_manager &m;
array_util m_arr; array_util m_arr;
datatype_util m_dt_util; datatype_util m_dt_util;
model_evaluator m_eval; model_evaluator m_eval;
expr_ref val; expr_ref val;
app_const_arr_rewriter(ast_manager& man, model& mdl): m(man), m_arr(m), m_dt_util(m), m_eval(mdl), val(m) { app_const_arr_rewriter(ast_manager& man, model& mdl): m(man), m_arr(m), m_dt_util(m), m_eval(mdl), val(m) {
m_eval.set_model_completion(false); m_eval.set_model_completion(false);
}
br_status reduce_app(func_decl *f, unsigned num, expr *const *args,
expr_ref &result, proof_ref &result_pr) {
if (m_arr.is_const(f) && !m.is_value(args[0])) {
val = m_eval(args[0]);
SASSERT(m.is_value(val));
result = m_arr.mk_const_array(f->get_range(), val);
return BR_DONE;
} }
br_status reduce_app(func_decl *f, unsigned num, expr *const *args, if (m_dt_util.is_constructor(f)) {
expr_ref &result, proof_ref &result_pr) { // cons(head(x), tail(x)) --> x
if (m_arr.is_const(f) && !m.is_value(args[0])) { ptr_vector<func_decl> const *accessors =
val = m_eval(args[0]); m_dt_util.get_constructor_accessors(f);
SASSERT(m.is_value(val));
result = m_arr.mk_const_array(f->get_range(), val); SASSERT(num == accessors->size());
return BR_DONE; // -- all accessors must have exactly one argument
if (any_of(*accessors, [&](const func_decl* acc) { return acc->get_arity() != 1; })) {
return BR_FAILED;
} }
if (m_dt_util.is_constructor(f)) {
// cons(head(x), tail(x)) --> x
ptr_vector<func_decl> const *accessors =
m_dt_util.get_constructor_accessors(f);
SASSERT(num == accessors->size()); if (num >= 1 && is_app(args[0]) && to_app(args[0])->get_decl() == accessors->get(0)) {
// -- all accessors must have exactly one argument bool is_all = true;
if (any_of(*accessors, [&](const func_decl* acc) { return acc->get_arity() != 1; })) { expr* t = to_app(args[0])->get_arg(0);
return BR_FAILED; for(unsigned i = 1; i < num && is_all; ++i) {
is_all &= (is_app(args[i]) &&
to_app(args[i])->get_decl() == accessors->get(i) &&
to_app(args[i])->get_arg(0) == t);
} }
if (is_all) {
if (num >= 1 && is_app(args[0]) && to_app(args[0])->get_decl() == accessors->get(0)) { result = t;
bool is_all = true; return BR_DONE;
expr* t = to_app(args[0])->get_arg(0);
for(unsigned i = 1; i < num && is_all; ++i) {
is_all &= (is_app(args[i]) &&
to_app(args[i])->get_decl() == accessors->get(i) &&
to_app(args[i])->get_arg(0) == t);
}
if (is_all) {
result = t;
return BR_DONE;
}
} }
} }
return BR_FAILED;
} }
return BR_FAILED;
}
}; };
} }