mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-05 13:48:47 +00:00
parent b87f4ca677
commit 88f007e9da
1 changed files with 13 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/model/model_evaluator.cpp
View file

@ -49,9 +49,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
evaluator_cfg(ast_manager & m, model & md, params_ref const & p):
m_model(md),
m_b_rw(m),
// We must allow customers to set parameters for arithmetic rewriter/evaluator.
// We must allow customers to set parameters for arithmetic rewriter/evaluator.
// In particular, the maximum degree of algebraic numbers that will be evaluated.
m_a_rw(m, p),
m_a_rw(m, p),
m_bv_rw(m),
// See comment above. We want to allow customers to set :sort-store
m_ar_rw(m, p),
@ -73,7 +73,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_model_completion = p.completion();
m_cache = p.cache();
}
ast_manager & m() const { return m_model.get_manager(); }
bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) {
@ -89,11 +89,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
SASSERT(fi->get_arity() == num);
bool actuals_are_values = true;
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
@ -115,7 +115,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
result = val;
return BR_DONE;
}
if (m_model_completion) {
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
@ -154,7 +154,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_a_rw.mk_app_core(f, num, args, result);
else if (fid == m_bv_rw.get_fid())
st = m_bv_rw.mk_app_core(f, num, args, result);
else if (fid == m_ar_rw.get_fid())
else if (fid == m_ar_rw.get_fid())
st = m_ar_rw.mk_app_core(f, num, args, result);
else if (fid == m_dt_rw.get_fid())
st = m_dt_rw.mk_app_core(f, num, args, result);
@ -180,9 +180,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
return st;
}
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
func_interp * fi = m_model.get_func_interp(f);
func_interp * fi = m_model.get_func_interp(f);
if (fi != 0) {
if (fi->is_partial()) {
if (m_model_completion) {
@ -193,7 +193,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
else {
return false;
}
}
}
def = fi->get_interp();
SASSERT(def != 0);
return true;
@ -211,8 +211,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
return false;
}
bool max_steps_exceeded(unsigned num_steps) const {
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("model evaluator");
if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(Z3_MAX_MEMORY_MSG);
@ -228,7 +228,7 @@ template class rewriter_tpl<evaluator_cfg>;
struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
evaluator_cfg m_cfg;
imp(model & md, params_ref const & p):
rewriter_tpl<evaluator_cfg>(md.get_manager(),
rewriter_tpl<evaluator_cfg>(md.get_manager(),
false, // no proofs for evaluator
m_cfg),
m_cfg(md.get_manager(), md, p) {