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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-09 20:41:30 -08:00
parent 8d3ed19981
commit 806ee85759
1 changed files with 16 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/model/model_evaluator.cpp
View file

@ -37,7 +37,7 @@ Revision History:
#include "model/model_v2_pp.h"
namespace {
namespace mev {
struct evaluator_cfg : public default_rewriter_cfg {
ast_manager & m;
@ -144,13 +144,22 @@ struct evaluator_cfg : public default_rewriter_cfg {
return th.reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
auto st = reduce_app_core(f, num, args, result, result_pr);
CTRACE("model_evaluator", st != BR_FAILED,
tout << f->get_name() << " ";
for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " ";
tout << "\n";
tout << result << "\n";);
return st;
}
br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = nullptr;
family_id fid = f->get_family_id();
bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
br_status st = BR_FAILED;
TRACE("model_evaluator", tout << f->get_name() << " " << is_uninterp << "\n";);
if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)
expr * val = m_model.get_const_interp(f);
if (val != nullptr) {
@ -197,15 +206,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
result = m.mk_false();
st = BR_DONE;
}
TRACE("model_evaluator",
tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " "
<< mk_pp(args[0], m) << " " << mk_pp(args[1], m) << " " << result << "\n";);
if (st != BR_FAILED)
return st;
}
return m_b_rw.mk_app_core(f, num, args, result);
}
CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
if (fid == m_a_rw.get_fid())
st = m_a_rw.mk_app_core(f, num, args, result);
else if (fid == m_bv_rw.get_fid())
@ -227,10 +232,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
else if (evaluate(f, num, args, result)) {
st = BR_REWRITE1;
}
CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
if (st == BR_FAILED && !m.is_builtin_family_id(fid)) {
st = evaluate_partial_theory_func(f, num, args, result, result_pr);
CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
}
if (st == BR_DONE && is_app(result)) {
app* a = to_app(result);
@ -256,7 +259,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
}
CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
return st;
}
@ -576,10 +578,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
};
}
struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
evaluator_cfg m_cfg;
struct model_evaluator::imp : public rewriter_tpl<mev::evaluator_cfg> {
mev::evaluator_cfg m_cfg;
imp(model_core & md, params_ref const & p):
rewriter_tpl<evaluator_cfg>(md.get_manager(),
rewriter_tpl<mev::evaluator_cfg>(md.get_manager(),
false, // no proofs for evaluator
m_cfg),
m_cfg(md.get_manager(), md, p) {
@ -587,7 +589,7 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
}
void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
void reset() {
rewriter_tpl<evaluator_cfg>::reset();
rewriter_tpl<mev::evaluator_cfg>::reset();
m_cfg.reset();
m_cfg.m_def_cache.reset();
}