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

cache datatype util in context to avoid performance bug, codeplex issue 195

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-03-25 11:46:17 -07:00
parent 8059a5a0b7
commit 39892aae10
3 changed files with 14 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/c++/example.cpp
View file

@ -5,6 +5,7 @@ using namespace z3;
/** /**
Demonstration of how Z3 can be used to prove validity of Demonstration of how Z3 can be used to prove validity of
De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) } De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
@ -986,6 +987,9 @@ void extract_example() {
} }
int main() { int main() {
slow();
return 0;
try { try {
demorgan(); std::cout << "\n"; demorgan(); std::cout << "\n";
find_model_example1(); std::cout << "\n"; find_model_example1(); std::cout << "\n";

18
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;
} }
unsigned n = dt_util.get_datatype_num_constructors(_t); ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
if (idx >= n) { if (idx >= decls->size()) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
func_decl* decl = dt_util.get_constructor(_t, idx); func_decl* decl = (*decls)[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);
} }
unsigned n = dt_util.get_datatype_num_constructors(_t); ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
if (idx >= n) { if (idx >= decls->size()) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
func_decl* decl = dt_util.get_constructor(_t, idx); func_decl* decl = (*decls)[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);
} }
unsigned n = dt_util.get_datatype_num_constructors(_t); ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
if (idx_c >= n) { if (idx_c >= decls->size()) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
func_decl* decl = dt_util.get_constructor(_t, idx_c); func_decl* decl = (*decls)[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);

2
src/ast/datatype_decl_plugin.h
View file

@ -170,6 +170,7 @@ class datatype_util {
ptr_vector<ptr_vector<func_decl> > m_vectors; ptr_vector<ptr_vector<func_decl> > m_vectors;
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);
func_decl * get_constructor(sort * ty, unsigned c_id);
public: public:
datatype_util(ast_manager & m); datatype_util(ast_manager & m);
@ -202,7 +203,6 @@ public:
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_ */