From 2aa91eee70569d10f978aa46497d0215b13e0e56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2015 11:24:47 -0700 Subject: [PATCH 1/5] cache datatype util in context to avoid performance bug, codeplex issue 195 Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 1 + src/api/api_context.cpp | 1 + src/api/api_context.h | 2 ++ src/api/api_datatype.cpp | 18 +++++++++--------- 4 files changed, 13 insertions(+), 9 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index e48c23905..0f0dd5ebf 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -4,6 +4,7 @@ using namespace z3; + /** 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) } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 49fa10d94..cff59cd80 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -89,6 +89,7 @@ namespace api { m_bv_util(m()), m_datalog_util(m()), m_fpa_util(m()), + m_dtutil(m()), m_last_result(m()), m_ast_trail(m()), m_replay_stack() { diff --git a/src/api/api_context.h b/src/api/api_context.h index 58394c028..f02dc6f16 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -58,6 +58,7 @@ namespace api { bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; fpa_util m_fpa_util; + datatype_util m_dtutil; // Support for old solver API smt_params m_fparams; @@ -119,6 +120,7 @@ namespace api { bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } fpa_util & fpautil() { return m_fpa_util; } + datatype_util& dtutil() { return m_dtutil; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } family_id get_arith_fid() const { return m_arith_fid; } diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index f3a275508..7e9dc6689 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -36,7 +36,7 @@ extern "C" { RESET_ERROR_CODE(); mk_c(c)->reset_last_result(); ast_manager& m = mk_c(c)->m(); - datatype_util dt_util(m); + datatype_util& dt_util = mk_c(c)->dtutil(); sort_ref_vector tuples(m); sort* tuple; @@ -102,7 +102,7 @@ extern "C" { RESET_ERROR_CODE(); mk_c(c)->reset_last_result(); ast_manager& m = mk_c(c)->m(); - datatype_util dt_util(m); + datatype_util& dt_util = mk_c(c)->dtutil(); sort_ref_vector sorts(m); sort* e; @@ -451,7 +451,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_VALID_AST(t, 0); sort * _t = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -470,7 +470,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_VALID_AST(t, 0); sort * _t = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; @@ -499,7 +499,7 @@ extern "C" { LOG_Z3_get_datatype_sort_recognizer(c, t, idx); RESET_ERROR_CODE(); sort * _t = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -522,7 +522,7 @@ extern "C" { LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a); RESET_ERROR_CODE(); sort * _t = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -555,7 +555,7 @@ extern "C" { LOG_Z3_get_tuple_sort_mk_decl(c, t); RESET_ERROR_CODE(); sort * tuple = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); @@ -570,7 +570,7 @@ extern "C" { LOG_Z3_get_tuple_sort_num_fields(c, t); RESET_ERROR_CODE(); sort * tuple = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; @@ -593,7 +593,7 @@ extern "C" { LOG_Z3_get_tuple_sort_field_decl(c, t, i); RESET_ERROR_CODE(); sort * tuple = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); From 86ac20faf65ea3aaaed43aa17c3682e4e6a8dadf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2015 11:35:44 -0700 Subject: [PATCH 2/5] cache datatype util in context to avoid performance bug, codeplex issue 195 Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 0f0dd5ebf..1278a50e4 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1,10 +1,28 @@ #include #include"z3++.h" - +#include using namespace z3; +void slow() { + context ctx; + unsigned sortSize = 200000; + char** names = new char*[sortSize]; + func_decl_vector enum_consts(ctx); + func_decl_vector enum_testers(ctx); + for (unsigned i = 0; i < sortSize; ++i) { + std::stringstream strm; + strm << "c" << i; + names[i] = strdup(strm.str().c_str()); + } + sort s = ctx.enumeration_sort("enumT", sortSize, names, enum_consts, enum_testers); + std::vector decls; + for (unsigned i = 0; i < sortSize; ++i) { + decls.push_back(Z3_get_datatype_sort_constructor(ctx, s, i)); + } +} + /** 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) } @@ -986,6 +1004,8 @@ void extract_example() { } int main() { + slow(); + return 0; try { demorgan(); std::cout << "\n"; find_model_example1(); std::cout << "\n"; From 8059a5a0b75e1ff4bbf25e946efece8de7f25278 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2015 11:36:01 -0700 Subject: [PATCH 3/5] cache datatype util in context to avoid performance bug, codeplex issue 195 Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 1278a50e4..81af289d3 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1,27 +1,9 @@ #include #include"z3++.h" -#include using namespace z3; -void slow() { - context ctx; - unsigned sortSize = 200000; - char** names = new char*[sortSize]; - func_decl_vector enum_consts(ctx); - func_decl_vector enum_testers(ctx); - for (unsigned i = 0; i < sortSize; ++i) { - std::stringstream strm; - strm << "c" << i; - names[i] = strdup(strm.str().c_str()); - } - sort s = ctx.enumeration_sort("enumT", sortSize, names, enum_consts, enum_testers); - std::vector decls; - for (unsigned i = 0; i < sortSize; ++i) { - decls.push_back(Z3_get_datatype_sort_constructor(ctx, s, i)); - } -} /** Demonstration of how Z3 can be used to prove validity of @@ -1004,8 +986,6 @@ void extract_example() { } int main() { - slow(); - return 0; try { demorgan(); std::cout << "\n"; find_model_example1(); std::cout << "\n"; From 39892aae10c28810b8db5e4b9a6addda36a09520 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2015 11:46:17 -0700 Subject: [PATCH 4/5] cache datatype util in context to avoid performance bug, codeplex issue 195 Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 4 ++++ src/api/api_datatype.cpp | 18 +++++++++--------- src/ast/datatype_decl_plugin.h | 2 +- 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 81af289d3..67af5eb34 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -5,6 +5,7 @@ using namespace z3; + /** 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) } @@ -986,6 +987,9 @@ void extract_example() { } int main() { + slow(); + return 0; + try { demorgan(); std::cout << "\n"; find_model_example1(); std::cout << "\n"; diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 7acd93bf0..a9794c980 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -475,12 +475,12 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - unsigned n = dt_util.get_datatype_num_constructors(_t); - if (idx >= n) { + ptr_vector const * decls = dt_util.get_datatype_constructors(_t); + if (idx >= decls->size()) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - func_decl* decl = dt_util.get_constructor(_t, idx); + func_decl* decl = (*decls)[idx]; mk_c(c)->save_ast_trail(decl); return of_func_decl(decl); } @@ -505,12 +505,12 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - unsigned n = dt_util.get_datatype_num_constructors(_t); - if (idx >= n) { + ptr_vector const * decls = dt_util.get_datatype_constructors(_t); + if (idx >= decls->size()) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - func_decl* decl = dt_util.get_constructor(_t, idx); + func_decl* decl = (*decls)[idx]; decl = dt_util.get_constructor_recognizer(decl); mk_c(c)->save_ast_trail(decl); RETURN_Z3(of_func_decl(decl)); @@ -528,12 +528,12 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - unsigned n = dt_util.get_datatype_num_constructors(_t); - if (idx_c >= n) { + ptr_vector const * decls = dt_util.get_datatype_constructors(_t); + if (idx_c >= decls->size()) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - func_decl* decl = dt_util.get_constructor(_t, idx_c); + func_decl* decl = (*decls)[idx_c]; if (decl->get_arity() <= idx_a) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index af9c125f7..3f7f01364 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -170,6 +170,7 @@ class datatype_util { ptr_vector > m_vectors; func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); + func_decl * get_constructor(sort * ty, unsigned c_id); public: datatype_util(ast_manager & m); @@ -202,7 +203,6 @@ public: void reset(); void display_datatype(sort *s, std::ostream& strm); - func_decl * get_constructor(sort * ty, unsigned c_id); }; #endif /* _DATATYPE_DECL_PLUGIN_H_ */ From 0482e7fe727c75e259ac55a932b28cf1842c530e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2015 11:46:28 -0700 Subject: [PATCH 5/5] cache datatype util in context to avoid performance bug, codeplex issue 195 Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 67af5eb34..9f4f9431c 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -987,8 +987,6 @@ void extract_example() { } int main() { - slow(); - return 0; try { demorgan(); std::cout << "\n";