mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

model evaluator: cleanup cache when model_eval param changes

Browse source
This commit is contained in:
Nuno Lopes 2019-03-02 16:42:18 +00:00
parent 210e448666
commit ccc170a06e
3 changed files with 15 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_model.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History: Revision History:
--*/ --*/
#include<iostream>
#include "api/z3.h" #include "api/z3.h"
#include "api/api_log_macros.h" #include "api/api_log_macros.h"
#include "api/api_context.h" #include "api/api_context.h"

25
src/model/model_evaluator.cpp
View file

@ -36,7 +36,7 @@ Revision History:
#include "model/model_smt2_pp.h" #include "model/model_smt2_pp.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
namespace {
struct evaluator_cfg : public default_rewriter_cfg { struct evaluator_cfg : public default_rewriter_cfg {
ast_manager & m; ast_manager & m;
model_core & m_model; model_core & m_model;
@ -53,7 +53,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
unsigned long long m_max_memory; unsigned long long m_max_memory;
unsigned m_max_steps; unsigned m_max_steps;
bool m_model_completion; bool m_model_completion;
bool m_cache;
bool m_array_equalities; bool m_array_equalities;
bool m_array_as_stores; bool m_array_as_stores;
obj_map<func_decl, expr*> m_def_cache; obj_map<func_decl, expr*> m_def_cache;
@ -91,7 +90,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
model_evaluator_params p(_p); model_evaluator_params p(_p);
m_max_memory = megabytes_to_bytes(p.max_memory()); m_max_memory = megabytes_to_bytes(p.max_memory());
m_max_steps = p.max_steps(); m_max_steps = p.max_steps();
m_cache = p.cache();
m_model_completion = p.completion(); m_model_completion = p.completion();
m_array_equalities = p.array_equalities(); m_array_equalities = p.array_equalities();
m_array_as_stores = p.array_as_stores(); m_array_as_stores = p.array_as_stores();
@ -328,8 +326,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
return num_steps > m_max_steps; return num_steps > m_max_steps;
} }
bool cache_results() const { return m_cache; }
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) { br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << "\n";); TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << "\n";);
if (a == b) { if (a == b) {
@ -544,8 +540,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
return true; return true;
} }
}; };
}
template class rewriter_tpl<evaluator_cfg>;
struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> { struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
evaluator_cfg m_cfg; evaluator_cfg m_cfg;
@ -557,6 +552,11 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
set_cancel_check(false); set_cancel_check(false);
} }
void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);} void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
void reset() {
rewriter_tpl<evaluator_cfg>::reset();
m_cfg.reset();
m_cfg.m_def_cache.reset();
}
}; };
model_evaluator::model_evaluator(model_core & md, params_ref const & p) { model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
@ -580,8 +580,11 @@ void model_evaluator::get_param_descrs(param_descrs & r) {
} }
void model_evaluator::set_model_completion(bool f) { void model_evaluator::set_model_completion(bool f) {
if (m_imp->cfg().m_model_completion != f) {
reset();
m_imp->cfg().m_model_completion = f; m_imp->cfg().m_model_completion = f;
} }
}
bool model_evaluator::get_model_completion() const { bool model_evaluator::get_model_completion() const {
return m_imp->cfg().m_model_completion; return m_imp->cfg().m_model_completion;
@ -597,8 +600,8 @@ unsigned model_evaluator::get_num_steps() const {
void model_evaluator::cleanup(params_ref const & p) { void model_evaluator::cleanup(params_ref const & p) {
model_core & md = m_imp->cfg().m_model; model_core & md = m_imp->cfg().m_model;
dealloc(m_imp); m_imp->~imp();
m_imp = alloc(imp, md, p); new (m_imp) imp(md, p);
} }
void model_evaluator::reset(params_ref const & p) { void model_evaluator::reset(params_ref const & p) {
@ -607,8 +610,8 @@ void model_evaluator::reset(params_ref const & p) {
} }
void model_evaluator::reset(model_core &model, params_ref const& p) { void model_evaluator::reset(model_core &model, params_ref const& p) {
dealloc(m_imp); m_imp->~imp();
m_imp = alloc(imp, model, p); new (m_imp) imp(model, p);
} }

1
src/model/model_evaluator_params.pyg
View file

@ -3,7 +3,6 @@ def_module_params('model_evaluator',
params=(max_memory_param(), params=(max_memory_param(),
max_steps_param(), max_steps_param(),
('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'), ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'),
('cache', BOOL, True, 'cache intermediate results in the model evaluator'),
('array_equalities', BOOL, True, 'evaluate array equalities'), ('array_equalities', BOOL, True, 'evaluate array equalities'),
('array_as_stores', BOOL, True, 'return array as a set of stores'), ('array_as_stores', BOOL, True, 'return array as a set of stores'),
)) ))