mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

make eval cache sensitive to model completion. Bug 110 reported by cipher1024

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-15 21:12:16 -07:00
parent 4d2d334999
commit 3d1ca5ecc9
3 changed files with 18 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/model/model.cpp
View file

@ -133,7 +133,8 @@ bool model::eval(expr * e, expr_ref & result, bool model_completion) {
ev(e, result); ev(e, result);
return true; return true;
} }
catch (model_evaluator_exception &) { catch (model_evaluator_exception & ex) {
TRACE("model_evaluator", tout << ex.msg() << "\n";);
return false; return false;
} }
} }

3
src/smt/proto_model/proto_model.cpp
View file

@ -247,6 +247,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
new_t = mk_some_interp_for(f); new_t = mk_some_interp_for(f);
} }
else { else {
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false; is_ok = false;
} }
} }
@ -294,6 +295,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
// f is an uninterpreted function, there is no need to use m_simplifier.mk_app // f is an uninterpreted function, there is no need to use m_simplifier.mk_app
new_t = m_manager.mk_app(f, num_args, args.c_ptr()); new_t = m_manager.mk_app(f, num_args, args.c_ptr());
trail.push_back(new_t); trail.push_back(new_t);
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false; is_ok = false;
} }
} }
@ -326,6 +328,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
todo.pop_back(); todo.pop_back();
break; break;
case AST_QUANTIFIER: case AST_QUANTIFIER:
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
is_ok = false; // evaluator does not handle quantifiers. is_ok = false; // evaluator does not handle quantifiers.
SASSERT(a != 0); SASSERT(a != 0);
eval_cache.insert(a, a); eval_cache.insert(a, a);

19
src/smt/smt_model_finder.cpp
View file

@ -396,7 +396,7 @@ namespace smt {
// Support for evaluating expressions in the current model. // Support for evaluating expressions in the current model.
proto_model * m_model; proto_model * m_model;
obj_map<expr, expr *> m_eval_cache; obj_map<expr, expr *> m_eval_cache[2];
expr_ref_vector m_eval_cache_range; expr_ref_vector m_eval_cache_range;
ptr_vector<node> m_root_nodes; ptr_vector<node> m_root_nodes;
@ -409,7 +409,8 @@ namespace smt {
} }
void reset_eval_cache() { void reset_eval_cache() {
m_eval_cache.reset(); m_eval_cache[0].reset();
m_eval_cache[1].reset();
m_eval_cache_range.reset(); m_eval_cache_range.reset();
} }
@ -468,6 +469,7 @@ namespace smt {
~auf_solver() { ~auf_solver() {
flush_nodes(); flush_nodes();
reset_eval_cache();
} }
void set_context(context * ctx) { void set_context(context * ctx) {
@ -547,7 +549,7 @@ namespace smt {
for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) { for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) {
expr * n = it->m_key; expr * n = it->m_key;
expr * n_val = eval(n, true); expr * n_val = eval(n, true);
if (!m_manager.is_value(n_val)) if (!n_val || !m_manager.is_value(n_val))
to_delete.push_back(n); to_delete.push_back(n);
} }
for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) { for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) {
@ -569,16 +571,19 @@ namespace smt {
virtual expr * eval(expr * n, bool model_completion) { virtual expr * eval(expr * n, bool model_completion) {
expr * r = 0; expr * r = 0;
if (m_eval_cache.find(n, r)) { if (m_eval_cache[model_completion].find(n, r)) {
return r; return r;
} }
expr_ref tmp(m_manager); expr_ref tmp(m_manager);
if (!m_model->eval(n, tmp, model_completion)) if (!m_model->eval(n, tmp, model_completion)) {
r = 0; r = 0;
else TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n-----> null\n";);
}
else {
r = tmp; r = tmp;
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";); TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
m_eval_cache.insert(n, r); }
m_eval_cache[model_completion].insert(n, r);
m_eval_cache_range.push_back(r); m_eval_cache_range.push_back(r);
return r; return r;
} }