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

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-27 14:10:56 -08:00
parent 5a357f9998
commit 3afb78416f
3 changed files with 38 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.h
View file

@ -1517,6 +1517,8 @@ public:
void update_fresh_id(ast_manager const& other); void update_fresh_id(ast_manager const& other);
unsigned mk_fresh_id() { return ++m_fresh_id; }
protected: protected:
reslimit m_limit; reslimit m_limit;
small_object_allocator m_alloc; small_object_allocator m_alloc;

36
src/ast/recfun_decl_plugin.cpp
View file

@ -450,7 +450,7 @@ namespace recfun {
* \brief compute ite nesting depth scores with each sub-expression of e. * \brief compute ite nesting depth scores with each sub-expression of e.
*/ */
void plugin::compute_scores(expr* e, obj_map<expr, unsigned>& scores) { void plugin::compute_scores(expr* e, obj_map<expr, unsigned>& scores) {
unsigned max_depth = e->get_depth(e); unsigned max_depth = get_depth(e);
u_map<ptr_vector<expr>> by_depth; u_map<ptr_vector<expr>> by_depth;
obj_map<expr, ptr_vector<expr>> parents; obj_map<expr, ptr_vector<expr>> parents;
expr_mark marked; expr_mark marked;
@ -462,7 +462,39 @@ namespace recfun {
} }
} }
void plugin::expand_ expr_ref plugin::redirect_ite(replace& subst, unsigned n, var ** vars, expr * e) {
expr_ref result(e, m());
while (true) {
obj_map<expr, unsigned> scores;
compute_scores(e, scores);
unsigned max_score = 0;
expr* max_expr = nullptr;
for (auto const& kv : scores) {
if (kv.m_value > max_score) {
max_expr = kv.m_key;
max_score = kv.m_value;
}
}
if (max_score <= 4) {
break;
}
ptr_vector<sort> domain;
ptr_vector<expr> args;
for (unsigned i = 0; i < n; ++i) {
domain.push_back(vars[i]->get_sort());
args.push_back(vars[i]);
}
symbol fresh_name(m().mk_fresh_id());
auto pd = mk_def(fresh_name, n, domain.c_ptr(), m().get_sort(max_expr));
func_decl* f = pd.get_def()->get_decl();
expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m());
set_definition(subst, pd, n, vars, new_body);
subst.insert(max_expr, new_body);
subst(result);
}
return result;
}
} }
} }

2
src/ast/recfun_decl_plugin.h
View file

@ -157,7 +157,9 @@ namespace recfun {
ast_manager & m() { return *m_manager; } ast_manager & m() { return *m_manager; }
expr_ref redirect_ite(replace& subst, unsigned n, var ** vars, expr * e);
void compute_scores(expr* e, obj_map<expr, unsigned>& scores); void compute_scores(expr* e, obj_map<expr, unsigned>& scores);
public: public:
plugin(); plugin();
~plugin() override; ~plugin() override;