mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Added array index/element sort detection to static_features

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-02-09 13:41:45 +00:00
parent 0a22f1e0f5
commit 3a8a62fc4c
3 changed files with 31 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/ast/static_features.cpp
View file

@ -28,6 +28,7 @@ static_features::static_features(ast_manager & m):
m_bfid(m.get_basic_family_id()), m_bfid(m.get_basic_family_id()),
m_afid(m.mk_family_id("arith")), m_afid(m.mk_family_id("arith")),
m_lfid(m.mk_family_id("label")), m_lfid(m.mk_family_id("label")),
m_arrfid(m.mk_family_id("array")),
m_label_sym("label"), m_label_sym("label"),
m_pattern_sym("pattern"), m_pattern_sym("pattern"),
m_expr_list_sym("expr-list") { m_expr_list_sym("expr-list") {
@ -317,6 +318,16 @@ void static_features::update_core(expr * e) {
} }
} }
} }
if (m_arrayutil.is_array(e)) {
TRACE("sf_array", tout << mk_ismt2_pp(e, m_manager) << "\n";);
sort * ty = to_app(e)->get_decl()->get_range();
SASSERT(ty->get_num_parameters() == 2);
sort * inx_srt = to_sort(ty->get_parameter(0).get_ast());
sort * elm_srt = to_sort(ty->get_parameter(1).get_ast());
mark_theory(ty->get_family_id());
update_core(inx_srt);
update_core(elm_srt);
}
func_decl * d = to_app(e)->get_decl(); func_decl * d = to_app(e)->get_decl();
inc_num_apps(d); inc_num_apps(d);
if (d->get_arity() > 0 && !is_marked(d)) { if (d->get_arity() > 0 && !is_marked(d)) {
@ -351,6 +362,20 @@ void static_features::update_core(expr * e) {
} }
} }
void static_features::update_core(sort * s) {
mark_theory(s->get_family_id());
if (!m_has_int && m_autil.is_int(s))
m_has_int = true;
if (!m_has_real && m_autil.is_real(s))
m_has_real = true;
if (!m_has_bv && m_bvutil.is_bv_sort(s))
m_has_bv = true;
if (!m_has_fpa && (m_fpautil.is_float(s) || m_fpautil.is_rm(s)))
m_has_fpa = true;
if (!m_has_arrays && m_arrayutil.is_array(s))
m_has_arrays = true;
}
void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth) { void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth) {
TRACE("static_features", tout << "processing\n" << mk_pp(e, m_manager) << "\n";); TRACE("static_features", tout << "processing\n" << mk_pp(e, m_manager) << "\n";);
if (is_var(e)) if (is_var(e))

2
src/ast/static_features.h
View file

@ -35,6 +35,7 @@ struct static_features {
family_id m_bfid; family_id m_bfid;
family_id m_afid; family_id m_afid;
family_id m_lfid; family_id m_lfid;
family_id m_arrfid;
ast_mark m_already_visited; ast_mark m_already_visited;
bool m_cnf; bool m_cnf;
unsigned m_num_exprs; // unsigned m_num_exprs; //
@ -148,6 +149,7 @@ struct static_features {
void inc_theory_eqs(family_id fid) { m_num_theory_eqs.reserve(fid+1, 0); m_num_theory_eqs[fid]++; } void inc_theory_eqs(family_id fid) { m_num_theory_eqs.reserve(fid+1, 0); m_num_theory_eqs[fid]++; }
void inc_num_aliens(family_id fid) { m_num_aliens_per_family.reserve(fid+1, 0); m_num_aliens_per_family[fid]++; } void inc_num_aliens(family_id fid) { m_num_aliens_per_family.reserve(fid+1, 0); m_num_aliens_per_family[fid]++; }
void update_core(expr * e); void update_core(expr * e);
void update_core(sort * s);
void process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth); void process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth);
void process_root(expr * e); void process_root(expr * e);
unsigned get_depth(expr const * e) const { return m_expr2depth.get(e->get_id(), 1); } unsigned get_depth(expr const * e) const { return m_expr2depth.get(e->get_id(), 1); }

5
src/smt/smt_setup.cpp
View file

@ -830,7 +830,10 @@ namespace smt {
tout << "is_arith: " << is_arith(st) << "\n"; tout << "is_arith: " << is_arith(st) << "\n";
tout << "has UF: " << st.has_uf() << "\n"; tout << "has UF: " << st.has_uf() << "\n";
tout << "has real: " << st.m_has_real << "\n"; tout << "has real: " << st.m_has_real << "\n";
tout << "has int: " << st.m_has_int << "\n";); tout << "has int: " << st.m_has_int << "\n";
tout << "has bv: " << st.m_has_bv << "\n";
tout << "has fpa: " << st.m_has_fpa << "\n";
tout << "has arrays: " << st.m_has_arrays << "\n";);
if (st.num_non_uf_theories() == 0) { if (st.num_non_uf_theories() == 0) {
setup_QF_UF(st); setup_QF_UF(st);