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

Fixed performance problems with enumeration sorts (Codeplex #190).

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-03-25 18:08:56 +00:00
parent 1c77ad00c3
commit a792790882
2 changed files with 20 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/api/api_datatype.cpp
View file

@ -475,12 +475,12 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); unsigned n = dt_util.get_datatype_num_constructors(_t);
if (!decls || idx >= decls->size()) { if (idx >= n) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
func_decl* decl = (*decls)[idx]; func_decl* decl = dt_util.get_constructor(_t, idx);
mk_c(c)->save_ast_trail(decl); mk_c(c)->save_ast_trail(decl);
return of_func_decl(decl); return of_func_decl(decl);
} }
@ -505,12 +505,12 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); unsigned n = dt_util.get_datatype_num_constructors(_t);
if (!decls || idx >= decls->size()) { if (idx >= n) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); return 0;
} }
func_decl* decl = (*decls)[idx]; func_decl* decl = dt_util.get_constructor(_t, idx);
decl = dt_util.get_constructor_recognizer(decl); decl = dt_util.get_constructor_recognizer(decl);
mk_c(c)->save_ast_trail(decl); mk_c(c)->save_ast_trail(decl);
RETURN_Z3(of_func_decl(decl)); RETURN_Z3(of_func_decl(decl));
@ -528,12 +528,12 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); unsigned n = dt_util.get_datatype_num_constructors(_t);
if (!decls || idx_c >= decls->size()) { if (idx_c >= n) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); return 0;
} }
func_decl* decl = (*decls)[idx_c]; func_decl* decl = dt_util.get_constructor(_t, idx_c);
if (decl->get_arity() <= idx_a) { if (decl->get_arity() <= idx_a) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);

10
src/ast/datatype_decl_plugin.h
View file

@ -169,7 +169,6 @@ class datatype_util {
ast_ref_vector m_asts; ast_ref_vector m_asts;
ptr_vector<ptr_vector<func_decl> > m_vectors; ptr_vector<ptr_vector<func_decl> > m_vectors;
func_decl * get_constructor(sort * ty, unsigned c_id);
func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set); func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
public: public:
@ -185,7 +184,12 @@ public:
bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); } bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); }
bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
ptr_vector<func_decl> const * get_datatype_constructors(sort * ty); ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
unsigned get_datatype_num_constructors(sort * ty) { return get_datatype_constructors(ty)->size(); } unsigned get_datatype_num_constructors(sort * ty) {
SASSERT(is_datatype(ty));
unsigned tid = ty->get_parameter(1).get_int();
unsigned o = ty->get_parameter(3 + 2 * tid).get_int();
return ty->get_parameter(o).get_int();
}
unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(f)); return f->get_parameter(1).get_int(); } unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(f)); return f->get_parameter(1).get_int(); }
unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); } unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); }
func_decl * get_non_rec_constructor(sort * ty); func_decl * get_non_rec_constructor(sort * ty);
@ -197,6 +201,8 @@ public:
bool are_siblings(sort * s1, sort * s2); bool are_siblings(sort * s1, sort * s2);
void reset(); void reset();
void display_datatype(sort *s, std::ostream& strm); void display_datatype(sort *s, std::ostream& strm);
func_decl * get_constructor(sort * ty, unsigned c_id);
}; };
#endif /* _DATATYPE_DECL_PLUGIN_H_ */ #endif /* _DATATYPE_DECL_PLUGIN_H_ */