mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
cache datatype util in context to avoid performance bug, codeplex issue 195
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
parent
1c77ad00c3
commit
2aa91eee70
|
@ -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) }
|
||||
|
|
|
@ -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() {
|
||||
|
|
|
@ -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; }
|
||||
|
|
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue