From 9f3cc353104e37b6d9577e21a89c504fdcc893d0 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Mon, 25 Sep 2023 21:36:25 -0700 Subject: [PATCH 1/7] Remove extra factor of 4. --- src/mcsat/bv/explain/arith_norm.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mcsat/bv/explain/arith_norm.c b/src/mcsat/bv/explain/arith_norm.c index d78d31f10..4ef1c7e6c 100644 --- a/src/mcsat/bv/explain/arith_norm.c +++ b/src/mcsat/bv/explain/arith_norm.c @@ -796,7 +796,7 @@ term_t arith_normalise_upto(arith_norm_t* norm, term_t u, uint32_t w){ term_t *preproc[4]; for (int i = 0; i < 4; i ++) - preproc[i] = (term_t *) safe_malloc(4 * w * sizeof(term_t)); + preproc[i] = (term_t *) safe_malloc(w * sizeof(term_t)); // We initialise the hashmap fix_htbl_init(preproc[0], w); From 5e19ff67dc0e4cc0b1e06614cda2842df8f8c142 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Thu, 26 Oct 2023 20:33:07 -0700 Subject: [PATCH 2/7] Base term term on index table. --- src/Makefile | 1 + src/api/yices_api.c | 6 +- src/include/yices_limits.h | 2 +- src/io/term_printer.c | 177 +++++++------- src/mcsat/solver.c | 2 +- src/solvers/quant/quant_solver.c | 8 +- src/terms/bit_term_conversion.c | 2 +- src/terms/bvarith64_buffer_terms.c | 10 +- src/terms/bvarith_buffer_terms.c | 10 +- src/terms/bvlogic_buffers.c | 16 +- src/terms/rba_buffer_terms.c | 10 +- src/terms/terms.c | 372 +++++++++++++---------------- src/terms/terms.h | 111 +++++---- src/utils/indexed_table.c | 81 +++++++ src/utils/indexed_table.h | 117 +++++++++ src/utils/int_powers.h | 8 + 16 files changed, 561 insertions(+), 372 deletions(-) create mode 100644 src/utils/indexed_table.c create mode 100644 src/utils/indexed_table.h diff --git a/src/Makefile b/src/Makefile index 9a14fc6ba..c6bb6aad0 100644 --- a/src/Makefile +++ b/src/Makefile @@ -281,6 +281,7 @@ core_src_c := \ utils/generic_heap.c \ utils/hash_functions.c \ utils/index_vectors.c \ + utils/indexed_table.c \ utils/int_array_hsets.c \ utils/int_array_sort2.c \ utils/int_array_sort.c \ diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 06b8b35f9..5631ee93d 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -2637,11 +2637,11 @@ static bool check_all_distinct(term_table_t *terms, uint32_t n, const term_t *va result = true; if (n > 1) { - if (n > terms->live_terms) { + if (n > live_terms(terms)) { /* * there must be duplicates * we check this first just to be safe - * since n <= terms->live_terms <= YICES_MAX_TERMS, + * since n <= live_terms <= YICES_MAX_TERMS, * we know that n * sizeof(term_t) fits in 32bits * (which matters when we call safe_malloc(n * sizeof(term_t)). */ @@ -12241,7 +12241,7 @@ EXPORTED uint32_t yices_num_terms(void) { } uint32_t _o_yices_num_terms(void) { - return __yices_globals.terms->live_terms; + return live_terms(__yices_globals.terms); } EXPORTED uint32_t yices_num_types(void) { diff --git a/src/include/yices_limits.h b/src/include/yices_limits.h index 6bf9906c1..1463fb506 100644 --- a/src/include/yices_limits.h +++ b/src/include/yices_limits.h @@ -32,7 +32,7 @@ #include /* - * Maximal number of types or terms + * Maximal number of types or terms. */ #define YICES_MAX_TYPES (UINT32_MAX/8) #define YICES_MAX_TERMS (UINT32_MAX/8) diff --git a/src/io/term_printer.c b/src/io/term_printer.c index 7eabb8140..beae8291b 100644 --- a/src/io/term_printer.c +++ b/src/io/term_printer.c @@ -868,13 +868,13 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t char *name; name = term_name(tbl, pos_term(i)); - switch (tbl->kind[i]) { + switch (unchecked_kind_for_idx(tbl, i)) { case CONSTANT_TERM: if (name != NULL) { fputs(name, f); } else { - fprintf(f, "(const %"PRId32" of type ", tbl->desc[i].integer); - print_type_name(f, tbl->types, tbl->type[i]); + fprintf(f, "(const %"PRId32" of type ", integer_value_for_idx(tbl, i)); + print_type_name(f, tbl->types, type_for_idx(tbl, i)); fputc(')', f); } break; @@ -884,7 +884,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t fputs(name, f); } else { fprintf(f, "(unint of type "); - print_type_name(f, tbl->types, tbl->type[i]); + print_type_name(f, tbl->types, type_for_idx(tbl, i)); fputc(')', f); } break; @@ -893,22 +893,22 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL) { fputs(name, f); } else { - fprintf(f, "(var %"PRId32" of type ", tbl->desc[i].integer); - print_type_name(f, tbl->types, tbl->type[i]); + fprintf(f, "(var %"PRId32" of type ", integer_value_for_idx(tbl, i)); + print_type_name(f, tbl->types, type_for_idx(tbl, i)); fputc(')', f); } break; case ARITH_CONSTANT: - q_print(f, &tbl->desc[i].rational); + q_print(f, rational_for_idx(tbl, i)); break; case BV64_CONSTANT: - print_bvconst64_term(f, tbl->desc[i].ptr); + print_bvconst64_term(f, bvconst64_for_idx(tbl, i)); break; case BV_CONSTANT: - print_bvconst_term(f, tbl->desc[i].ptr); + print_bvconst_term(f, bvconst_for_idx(tbl, i)); break; case ARITH_EQ_ATOM: @@ -916,7 +916,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t fputs(name, f); } else { fputs("(arith-eq ", f); - print_term_recur(f, tbl, tbl->desc[i].integer, level - 1); + print_term_recur(f, tbl, integer_value_for_idx(tbl, i), level - 1); fputs(" 0)", f); } break; @@ -926,7 +926,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t fputs(name, f); } else { fputs("(arith-ge ", f); - print_term_recur(f, tbl, tbl->desc[i].integer, level - 1); + print_term_recur(f, tbl, integer_value_for_idx(tbl, i), level - 1); fputs(" 0)", f); } break; @@ -935,7 +935,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL && level <= 0) { fputs(name, f); } else { - print_root_atom_term(f, tbl, tbl->desc[i].ptr, level - 1); + print_root_atom_term(f, tbl, root_atom_for_idx(tbl, i), level - 1); } break; @@ -947,9 +947,9 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t fputs(name, f); } else { fputc('(', f); - fputs(tag2string[tbl->kind[i]], f); + fputs(tag2string[kind_for_idx(tbl, i)], f); fputc(' ', f); - print_term_recur(f, tbl, tbl->desc[i].integer, level - 1); + print_term_recur(f, tbl, integer_value_for_idx(tbl, i), level - 1); fputc(')', f); } break; @@ -959,7 +959,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL && level <= 0) { fputs(name, f); } else { - print_app_term(f, tbl, tbl->desc[i].ptr, level - 1); + print_app_term(f, tbl, composite_for_idx(tbl, i), level - 1); } break; @@ -994,7 +994,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL && level <= 0) { fputs(name, f); } else { - print_composite_term(f, tbl, tbl->kind[i], tbl->desc[i].ptr, level - 1); + print_composite_term(f, tbl, kind_for_idx(tbl, i), composite_for_idx(tbl, i), level - 1); } break; @@ -1003,7 +1003,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL && level <= 0) { fputs(name, f); } else { - print_select_term(f, tbl, tbl->kind[i], &tbl->desc[i].select, level - 1); + print_select_term(f, tbl, kind_for_idx(tbl, i), select_for_idx(tbl, i), level - 1); } break; @@ -1011,7 +1011,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL && level <= 0) { fputs(name, f); } else { - print_power_product_term(f, tbl, tbl->desc[i].ptr, level - 1); + print_power_product_term(f, tbl, pprod_for_idx(tbl, i), level - 1); } break; @@ -1019,7 +1019,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL && level <= 0) { fputs(name, f); } else { - print_polynomial_term(f, tbl, tbl->desc[i].ptr, level - 1); + print_polynomial_term(f, tbl, polynomial_for_idx(tbl, i), level - 1); } break; @@ -1027,7 +1027,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL && level <= 0) { fputs(name, f); } else { - print_bvpoly64_term(f, tbl, tbl->desc[i].ptr, level - 1); + print_bvpoly64_term(f, tbl, bvpoly64_for_idx(tbl, i), level - 1); } break; @@ -1035,7 +1035,7 @@ static void print_term_idx_recur(FILE *f, term_table_t *tbl, int32_t i, int32_t if (name != NULL && level <= 0) { fputs(name, f); } else { - print_bvpoly_term(f, tbl, tbl->desc[i].ptr, level - 1); + print_bvpoly_term(f, tbl, bvpoly_for_idx(tbl, i), level - 1); } break; @@ -1187,9 +1187,9 @@ static uint32_t max_term_name_length(term_table_t *tbl) { uint32_t max, l, n, i; max = 0; - n = tbl->nelems; + n = nterms(tbl); for (i=0; ikind[i] != UNUSED_TERM) { + if (unchecked_kind_for_idx(tbl, i) != UNUSED_TERM) { name = term_name(tbl, pos_term(i)); if (name != NULL) { l = strlen(name); @@ -1496,15 +1496,15 @@ void print_term_table(FILE *f, term_table_t *tbl) { name_size = 20; } - n = tbl->nelems; + n = nterms(tbl); for (i=0; ikind[i] != UNUSED_TERM) { + if (unchecked_kind_for_idx(tbl, i) != UNUSED_TERM) { // id + name fprintf(f, "%4"PRIu32" ", i); print_padded_string(f, term_name(tbl, pos_term(i)), name_size); // definition - switch (tbl->kind[i]) { + switch (unchecked_kind_for_idx(tbl, i)) { case RESERVED_TERM: fprintf(f, "reserved"); break; @@ -1513,45 +1513,45 @@ void print_term_table(FILE *f, term_table_t *tbl) { if (i == bool_const) { fprintf(f, "true"); } else { - fprintf(f, "(const %"PRId32" of type ", tbl->desc[i].integer); - print_type_name(f, tbl->types, tbl->type[i]); + fprintf(f, "(const %"PRId32" of type ", integer_value_for_idx(tbl, i)); + print_type_name(f, tbl->types, type_for_idx(tbl, i)); fputc(')', f); } break; case UNINTERPRETED_TERM: fprintf(f, "(unint of type "); - print_type_name(f, tbl->types, tbl->type[i]); + print_type_name(f, tbl->types, type_for_idx(tbl, i)); fputc(')', f); break; case VARIABLE: - fprintf(f, "(var %"PRId32" of type ", tbl->desc[i].integer); - print_type_name(f, tbl->types, tbl->type[i]); + fprintf(f, "(var %"PRId32" of type ", integer_value_for_idx(tbl, i)); + print_type_name(f, tbl->types, type_for_idx(tbl, i)); fputc(')', f); break; case ARITH_CONSTANT: - q_print(f, &tbl->desc[i].rational); + q_print(f, rational_for_idx(tbl, i)); break; case BV64_CONSTANT: - print_bvconst64_term(f, tbl->desc[i].ptr); + print_bvconst64_term(f, bvconst64_for_idx(tbl, i)); break; case BV_CONSTANT: - print_bvconst_term(f, tbl->desc[i].ptr); + print_bvconst_term(f, bvconst_for_idx(tbl, i)); break; case ARITH_EQ_ATOM: fputs("(arith-eq ", f); - print_id_or_constant(f, tbl, tbl->desc[i].integer); + print_id_or_constant(f, tbl, integer_value_for_idx(tbl, i)); fputs(" 0)", f); break; case ARITH_GE_ATOM: fputs("(arith-ge ", f); - print_id_or_constant(f, tbl, tbl->desc[i].integer); + print_id_or_constant(f, tbl, integer_value_for_idx(tbl, i)); fputs(" 0)", f); break; @@ -1560,14 +1560,14 @@ void print_term_table(FILE *f, term_table_t *tbl) { case ARITH_CEIL: case ARITH_ABS: fputc('(', f); - fputs(tag2string[tbl->kind[i]], f); + fputs(tag2string[kind_for_idx(tbl, i)], f); fputc(' ', f); - print_id_or_constant(f, tbl, tbl->desc[i].integer); + print_id_or_constant(f, tbl, integer_value_for_idx(tbl, i)); fputc(')', f); break; case APP_TERM: - print_app(f, tbl, tbl->desc[i].ptr); + print_app(f, tbl, composite_for_idx(tbl, i)); break; case ITE_TERM: @@ -1598,28 +1598,29 @@ void print_term_table(FILE *f, term_table_t *tbl) { case BV_GE_ATOM: case BV_SGE_ATOM: // i's descriptor is a composite term - print_composite(f, tbl, tbl->kind[i], tbl->desc[i].ptr); - break; + print_composite(f, tbl, kind_for_idx(tbl, i), + composite_for_idx(tbl, i)); + break; case SELECT_TERM: case BIT_TERM: - print_select(f, tbl, tbl->kind[i], &tbl->desc[i].select); + print_select(f, tbl, kind_for_idx(tbl, i), select_for_idx(tbl, i)); break; case POWER_PRODUCT: - print_named_pprod(f, tbl, tbl->desc[i].ptr); + print_named_pprod(f, tbl, pprod_for_idx(tbl, i)); break; case ARITH_POLY: - print_named_polynomial(f, tbl, tbl->desc[i].ptr); + print_named_polynomial(f, tbl, polynomial_for_idx(tbl, i)); break; case BV64_POLY: - print_named_bvpoly64(f, tbl, tbl->desc[i].ptr); + print_named_bvpoly64(f, tbl, bvpoly64_for_idx(tbl, i)); break; case BV_POLY: - print_named_bvpoly(f, tbl, tbl->desc[i].ptr); + print_named_bvpoly(f, tbl, bvpoly_for_idx(tbl, i)); break; default: @@ -1642,7 +1643,7 @@ void print_term_table(FILE *f, term_table_t *tbl) { * Descriptor of term idx i */ static void print_term_idx_desc(FILE *f, term_table_t *tbl, int32_t i) { - switch (tbl->kind[i]) { + switch (unchecked_kind_for_idx(tbl, i)) { case UNUSED_TERM: case RESERVED_TERM: fprintf(f, "bad-term%"PRId32, i); @@ -1655,31 +1656,31 @@ static void print_term_idx_desc(FILE *f, term_table_t *tbl, int32_t i) { break; case ARITH_CONSTANT: - q_print(f, &tbl->desc[i].rational); + q_print(f, rational_for_idx(tbl, i)); break; case BV64_CONSTANT: - print_bvconst64_term(f, tbl->desc[i].ptr); + print_bvconst64_term(f, bvconst64_for_idx(tbl, i)); break; case BV_CONSTANT: - print_bvconst_term(f, tbl->desc[i].ptr); + print_bvconst_term(f, bvconst_for_idx(tbl, i)); break; case ARITH_EQ_ATOM: fputs("(arith-eq ", f); - print_id_or_constant(f, tbl, tbl->desc[i].integer); + print_id_or_constant(f, tbl, integer_value_for_idx(tbl, i)); fputs(" 0)", f); break; case ARITH_GE_ATOM: fputs("(arith-ge ", f); - print_id_or_constant(f, tbl, tbl->desc[i].integer); + print_id_or_constant(f, tbl, integer_value_for_idx(tbl, i)); fputs(" 0)", f); break; case ARITH_ROOT_ATOM: - print_root_atom(f, tbl, tbl->desc[i].ptr); + print_root_atom(f, tbl, root_atom_for_idx(tbl, i)); break; case ARITH_IS_INT_ATOM: @@ -1687,14 +1688,14 @@ static void print_term_idx_desc(FILE *f, term_table_t *tbl, int32_t i) { case ARITH_CEIL: case ARITH_ABS: fputc('(', f); - fputs(tag2string[tbl->kind[i]], f); + fputs(tag2string[kind_for_idx(tbl, i)], f); fputc(' ', f); - print_id_or_constant(f, tbl, tbl->desc[i].integer); + print_id_or_constant(f, tbl, integer_value_for_idx(tbl, i)); fputc(')', f); break; case APP_TERM: - print_app(f, tbl, tbl->desc[i].ptr); + print_app(f, tbl, composite_for_idx(tbl, i)); break; case ITE_TERM: @@ -1725,28 +1726,28 @@ static void print_term_idx_desc(FILE *f, term_table_t *tbl, int32_t i) { case BV_GE_ATOM: case BV_SGE_ATOM: // i's descriptor is a composite term - print_composite(f, tbl, tbl->kind[i], tbl->desc[i].ptr); + print_composite(f, tbl, kind_for_idx(tbl, i), composite_for_idx(tbl, i)); break; case SELECT_TERM: case BIT_TERM: - print_select(f, tbl, tbl->kind[i], &tbl->desc[i].select); + print_select(f, tbl, kind_for_idx(tbl, i), select_for_idx(tbl, i)); break; case POWER_PRODUCT: - print_named_pprod(f, tbl, tbl->desc[i].ptr); + print_named_pprod(f, tbl, pprod_for_idx(tbl, i)); break; case ARITH_POLY: - print_named_polynomial(f, tbl, tbl->desc[i].ptr); + print_named_polynomial(f, tbl, polynomial_for_idx(tbl, i)); break; case BV64_POLY: - print_named_bvpoly64(f, tbl, tbl->desc[i].ptr); + print_named_bvpoly64(f, tbl, bvpoly64_for_idx(tbl, i)); break; case BV_POLY: - print_named_bvpoly(f, tbl, tbl->desc[i].ptr); + print_named_bvpoly(f, tbl, bvpoly_for_idx(tbl, i)); break; default: @@ -2484,14 +2485,14 @@ static void pp_term_idx_name(yices_pp_t *printer, term_table_t *tbl, int32_t i, static void pp_term_idx(yices_pp_t *printer, term_table_t *tbl, int32_t i, int32_t level, bool polarity) { pp_open_type_t op; - assert(is_boolean_type(tbl->type[i]) || polarity); + assert(is_boolean_type(type_for_idx(tbl, i)) || polarity); if (level <= 0) { pp_term_idx_name(printer, tbl, i, polarity); return; } - switch (tbl->kind[i]) { + switch (unchecked_kind_for_idx(tbl, i)) { case CONSTANT_TERM: case UNINTERPRETED_TERM: case VARIABLE: @@ -2500,23 +2501,23 @@ static void pp_term_idx(yices_pp_t *printer, term_table_t *tbl, int32_t i, int32 case ARITH_CONSTANT: assert(polarity); - pp_rational(printer, &tbl->desc[i].rational); + pp_rational(printer, rational_for_idx(tbl, i)); break; case BV64_CONSTANT: assert(polarity); - pp_bvconst64_term(printer, tbl->desc[i].ptr); + pp_bvconst64_term(printer, bvconst64_for_idx(tbl, i)); break; case BV_CONSTANT: assert(polarity); - pp_bvconst_term(printer, tbl->desc[i].ptr); + pp_bvconst_term(printer, bvconst_for_idx(tbl, i)); break; case ARITH_EQ_ATOM: op = polarity ? PP_OPEN_EQ : PP_OPEN_NEQ; pp_open_block(printer, op); - pp_term_recur(printer, tbl, tbl->desc[i].integer, level - 1, true); + pp_term_recur(printer, tbl, integer_value_for_idx(tbl, i), level - 1, true); pp_int32(printer, 0); pp_close_block(printer, true); break; @@ -2524,14 +2525,14 @@ static void pp_term_idx(yices_pp_t *printer, term_table_t *tbl, int32_t i, int32 case ARITH_GE_ATOM: op = polarity ? PP_OPEN_GE : PP_OPEN_LT; pp_open_block(printer, op); - pp_term_recur(printer, tbl, tbl->desc[i].integer, level - 1, true); + pp_term_recur(printer, tbl, integer_value_for_idx(tbl, i), level - 1, true); pp_int32(printer, 0); pp_close_block(printer, true); break; case ARITH_ROOT_ATOM: if (!polarity) pp_open_block(printer, PP_OPEN_NOT); - pp_root_atom(printer, tbl, tbl->desc[i].ptr, level - 1); + pp_root_atom(printer, tbl, root_atom_for_idx(tbl, i), level - 1); if (!polarity) pp_close_block(printer, true); break; @@ -2539,48 +2540,48 @@ static void pp_term_idx(yices_pp_t *printer, term_table_t *tbl, int32_t i, int32 case ARITH_FLOOR: case ARITH_CEIL: case ARITH_ABS: - op = term_kind2block[tbl->kind[i]]; + op = term_kind2block[kind_for_idx(tbl, i)]; if (!polarity) pp_open_block(printer, PP_OPEN_NOT); pp_open_block(printer, op); - pp_term_recur(printer, tbl, tbl->desc[i].integer, level - 1, true); + pp_term_recur(printer, tbl, integer_value_for_idx(tbl, i), level - 1, true); pp_close_block(printer, true); if (!polarity) pp_close_block(printer, true); break; case FORALL_TERM: - pp_forall_term(printer, tbl, tbl->desc[i].ptr, level - 1, polarity); + pp_forall_term(printer, tbl, composite_for_idx(tbl, i), level - 1, polarity); break; case LAMBDA_TERM: if (! polarity) pp_open_block(printer, PP_OPEN_NOT); - pp_lambda_term(printer, tbl, tbl->desc[i].ptr, level - 1); + pp_lambda_term(printer, tbl, composite_for_idx(tbl, i), level - 1); if (!polarity) pp_close_block(printer, true); break; case OR_TERM: - pp_or_term(printer, tbl, tbl->desc[i].ptr, level - 1, polarity); + pp_or_term(printer, tbl, composite_for_idx(tbl, i), level - 1, polarity); break; case EQ_TERM: case ARITH_BINEQ_ATOM: case BV_EQ_ATOM: op = polarity ? PP_OPEN_EQ : PP_OPEN_NEQ; - pp_binary_atom(printer, tbl, op, tbl->desc[i].ptr, level - 1); + pp_binary_atom(printer, tbl, op, composite_for_idx(tbl, i), level - 1); break; case BV_GE_ATOM: op = polarity ? PP_OPEN_BV_GE : PP_OPEN_BV_LT; - pp_binary_atom(printer, tbl, op, tbl->desc[i].ptr, level - 1); + pp_binary_atom(printer, tbl, op, composite_for_idx(tbl, i), level - 1); break; case BV_SGE_ATOM: op = polarity ? PP_OPEN_BV_SGE : PP_OPEN_BV_SLT; - pp_binary_atom(printer, tbl, op, tbl->desc[i].ptr, level - 1); + pp_binary_atom(printer, tbl, op, composite_for_idx(tbl, i), level - 1); break; case UPDATE_TERM: assert(polarity); - pp_update_term(printer, tbl, tbl->desc[i].ptr, level - 1); + pp_update_term(printer, tbl, composite_for_idx(tbl, i), level - 1); break; case APP_TERM: @@ -2603,40 +2604,40 @@ static void pp_term_idx(yices_pp_t *printer, term_table_t *tbl, int32_t i, int32 case BV_ASHR: // i's descriptor is a composite term if (! polarity) pp_open_block(printer, PP_OPEN_NOT); - pp_composite_term(printer, tbl, tbl->kind[i], tbl->desc[i].ptr, level - 1); + pp_composite_term(printer, tbl, kind_for_idx(tbl, i), composite_for_idx(tbl, i), level - 1); if (! polarity) pp_close_block(printer, true); break; case BV_ARRAY: assert(polarity); - pp_bvarray_term(printer, tbl, tbl->desc[i].ptr, level - 1); + pp_bvarray_term(printer, tbl, composite_for_idx(tbl, i), level - 1); break; case SELECT_TERM: case BIT_TERM: if (!polarity) pp_open_block(printer, PP_OPEN_NOT); - pp_select_term(printer, tbl, tbl->kind[i], &tbl->desc[i].select, level - 1); + pp_select_term(printer, tbl, kind_for_idx(tbl, i), select_for_idx(tbl, i), level - 1); if (!polarity) pp_close_block(printer, true); break; case POWER_PRODUCT: assert(polarity); - pp_pprod(printer, tbl, tbl->desc[i].ptr, level - 1); + pp_pprod(printer, tbl, pprod_for_idx(tbl, i), level - 1); break; case ARITH_POLY: assert(polarity); - pp_poly(printer, tbl, tbl->desc[i].ptr, level - 1); + pp_poly(printer, tbl, polynomial_for_idx(tbl, i), level - 1); break; case BV64_POLY: assert(polarity); - pp_bvpoly64(printer, tbl, tbl->desc[i].ptr, level - 1); + pp_bvpoly64(printer, tbl, bvpoly64_for_idx(tbl, i), level - 1); break; case BV_POLY: assert(polarity); - pp_bvpoly(printer, tbl, tbl->desc[i].ptr, level - 1); + pp_bvpoly(printer, tbl, bvpoly_for_idx(tbl, i), level - 1); break; case UNUSED_TERM: @@ -2777,9 +2778,9 @@ void pp_term_table(FILE *f, term_table_t *tbl) { init_yices_pp(&printer, f, &area, PP_VMODE, 0); - n = tbl->nelems; + n = nterms(tbl); for (i=0; ikind[i]; + kind = unchecked_kind_for_idx(tbl, i); if (kind != UNUSED_TERM && kind != RESERVED_TERM) { t = pos_term(i); fprintf(f, "term[%"PRId32"]: ", i); diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 085cdeed7..e76da94ba 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2577,7 +2577,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin } // Remember existing terms - mcsat->terms_size_on_solver_entry = mcsat->terms->nelems; + mcsat->terms_size_on_solver_entry = nterms(mcsat->terms); // Initialize for search mcsat_heuristics_init(mcsat); diff --git a/src/solvers/quant/quant_solver.c b/src/solvers/quant/quant_solver.c index ca0bd4762..395a23c38 100644 --- a/src/solvers/quant/quant_solver.c +++ b/src/solvers/quant/quant_solver.c @@ -607,7 +607,7 @@ static bool ematch_cnstr_instantiate(quant_solver_t *solver, uint32_t cidx, patt intern = &ctx->intern; instbl = &em->instbl; t = cnstr->t; - term_cost = ctx->terms->nelems; + term_cost = nterms(ctx->terms); assert(midx < instbl->ninstances); inst = instbl->data + midx; @@ -652,7 +652,7 @@ static bool ematch_cnstr_instantiate(quant_solver_t *solver, uint32_t cidx, patt t = term_substitution(solver, keys, values, n, t); - term_cost = ctx->terms->nelems - term_cost; + term_cost = nterms(ctx->terms) - term_cost; if (term_cost > 0) { cnstr_learner_update_term_reward(&solver->cnstr_learner, term_cost, cidx); } @@ -690,11 +690,11 @@ static void ematch_add_quant_cnstr(quant_solver_t *solver, uint32_t cidx, term_t assert(cidx < solver->qtbl.nquant); cnstr = solver->qtbl.data + cidx; -// term_cost = ctx->terms->nelems; +// term_cost = nterms(ctx->terms); quant_assert_formulas(ctx, 1, &t); -// term_cost = ctx->terms->nelems - term_cost; +// term_cost = nterms(ctx->terms) - term_cost; // if (term_cost > 0) { // learner_update_term_reward(&solver->learner, term_cost, cidx); // } diff --git a/src/terms/bit_term_conversion.c b/src/terms/bit_term_conversion.c index 6680ed88b..41c1ade8b 100644 --- a/src/terms/bit_term_conversion.c +++ b/src/terms/bit_term_conversion.c @@ -42,7 +42,7 @@ bit_t convert_term_to_bit(term_table_t *table, node_table_t *nodes, term_t t, ui assert(good_term(table, t) && is_boolean_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case CONSTANT_TERM: assert(i == bool_const); x = true_bit; diff --git a/src/terms/bvarith64_buffer_terms.c b/src/terms/bvarith64_buffer_terms.c index 1a50cec9d..520a9a802 100644 --- a/src/terms/bvarith64_buffer_terms.c +++ b/src/terms/bvarith64_buffer_terms.c @@ -97,7 +97,7 @@ void bvarith64_buffer_add_term(bvarith64_buffer_t *b, term_table_t *table, term_ term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: bvarith64_buffer_add_pp(b, pprod_for_idx(table, i)); break; @@ -151,7 +151,7 @@ void bvarith64_buffer_sub_term(bvarith64_buffer_t *b, term_table_t *table, term_ term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: bvarith64_buffer_sub_pp(b, pprod_for_idx(table, i)); break; @@ -205,7 +205,7 @@ void bvarith64_buffer_mul_term(bvarith64_buffer_t *b, term_table_t *table, term_ term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: bvarith64_buffer_mul_pp(b, pprod_for_idx(table, i)); break; @@ -255,7 +255,7 @@ void bvarith64_buffer_add_const_times_term(bvarith64_buffer_t *b, term_table_t * term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: bvarith64_buffer_add_mono(b, a, pprod_for_idx(table, i)); break; @@ -311,7 +311,7 @@ void bvarith64_buffer_mul_term_power(bvarith64_buffer_t *b, term_table_t *table, term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: r = pprod_exp(b->ptbl, pprod_for_idx(table, i), d); // r = t^d bvarith64_buffer_mul_pp(b, r); diff --git a/src/terms/bvarith_buffer_terms.c b/src/terms/bvarith_buffer_terms.c index 201a3ec59..bef1b6af9 100644 --- a/src/terms/bvarith_buffer_terms.c +++ b/src/terms/bvarith_buffer_terms.c @@ -99,7 +99,7 @@ void bvarith_buffer_add_term(bvarith_buffer_t *b, term_table_t *table, term_t t) term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: bvarith_buffer_add_pp(b, pprod_for_idx(table, i)); break; @@ -153,7 +153,7 @@ void bvarith_buffer_sub_term(bvarith_buffer_t *b, term_table_t *table, term_t t) term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: bvarith_buffer_sub_pp(b, pprod_for_idx(table, i)); break; @@ -207,7 +207,7 @@ void bvarith_buffer_mul_term(bvarith_buffer_t *b, term_table_t *table, term_t t) term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: bvarith_buffer_mul_pp(b, pprod_for_idx(table, i)); break; @@ -259,7 +259,7 @@ void bvarith_buffer_add_const_times_term(bvarith_buffer_t *b, term_table_t *tabl term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: bvarith_buffer_add_mono(b, a, pprod_for_idx(table, i)); break; @@ -322,7 +322,7 @@ void bvarith_buffer_mul_term_power(bvarith_buffer_t *b, term_table_t *table, ter term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: r = pprod_exp(b->ptbl, pprod_for_idx(table, i), d); // r = t^d bvarith_buffer_mul_pp(b, r); diff --git a/src/terms/bvlogic_buffers.c b/src/terms/bvlogic_buffers.c index 15c56df54..c98573ea4 100644 --- a/src/terms/bvlogic_buffers.c +++ b/src/terms/bvlogic_buffers.c @@ -1862,7 +1862,7 @@ void bvlogic_buffer_set_term(bvlogic_buffer_t *b, term_table_t *table, term_t t) assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case BV64_CONSTANT: c64 = bvconst64_for_idx(table, i); bvlogic_buffer_set_constant64(b, c64->bitsize, c64->value); @@ -1910,7 +1910,7 @@ void bvlogic_buffer_set_slice_term(bvlogic_buffer_t *b, term_table_t *table, uin assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) && i <= j); k = index_of(t); - switch (table->kind[k]) { + switch (kind_for_idx(table, k)) { case BV64_CONSTANT: c64 = bvconst64_for_idx(table, k); assert(j < c64->bitsize); @@ -1965,7 +1965,7 @@ void bvlogic_buffer_and_term(bvlogic_buffer_t *b, term_table_t *table, term_t t) term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case BV64_CONSTANT: c64 = bvconst64_for_idx(table, i); bvlogic_buffer_and_constant64(b, c64->bitsize, c64->value); @@ -2012,7 +2012,7 @@ void bvlogic_buffer_or_term(bvlogic_buffer_t *b, term_table_t *table, term_t t) term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case BV64_CONSTANT: c64 = bvconst64_for_idx(table, i); bvlogic_buffer_or_constant64(b, c64->bitsize, c64->value); @@ -2059,7 +2059,7 @@ void bvlogic_buffer_xor_term(bvlogic_buffer_t *b, term_table_t *table, term_t t) term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case BV64_CONSTANT: c64 = bvconst64_for_idx(table, i); bvlogic_buffer_xor_constant64(b, c64->bitsize, c64->value); @@ -2109,7 +2109,7 @@ void bvlogic_buffer_comp_term(bvlogic_buffer_t *b, term_table_t *table, term_t t term_bitsize(table, t) == b->bitsize); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case BV64_CONSTANT: c64 = bvconst64_for_idx(table, i); bvlogic_buffer_comp_constant64(b, c64->bitsize, c64->value); @@ -2159,7 +2159,7 @@ void bvlogic_buffer_concat_left_term(bvlogic_buffer_t *b, term_table_t *table, t assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case BV64_CONSTANT: c64 = bvconst64_for_idx(table, i); bvlogic_buffer_concat_left_constant64(b, c64->bitsize, c64->value); @@ -2204,7 +2204,7 @@ void bvlogic_buffer_concat_right_term(bvlogic_buffer_t *b, term_table_t *table, assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case BV64_CONSTANT: c64 = bvconst64_for_idx(table, i); bvlogic_buffer_concat_right_constant64(b, c64->bitsize, c64->value); diff --git a/src/terms/rba_buffer_terms.c b/src/terms/rba_buffer_terms.c index d04049519..5744502b4 100644 --- a/src/terms/rba_buffer_terms.c +++ b/src/terms/rba_buffer_terms.c @@ -39,7 +39,7 @@ void rba_buffer_add_term(rba_buffer_t *b, term_table_t *table, term_t t) { assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: rba_buffer_add_pp(b, pprod_for_idx(table, i)); break; @@ -76,7 +76,7 @@ void rba_buffer_sub_term(rba_buffer_t *b, term_table_t *table, term_t t) { assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: rba_buffer_sub_pp(b, pprod_for_idx(table, i)); break; @@ -113,7 +113,7 @@ void rba_buffer_mul_term(rba_buffer_t *b, term_table_t *table, term_t t) { assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: rba_buffer_mul_pp(b, pprod_for_idx(table, i)); break; @@ -151,7 +151,7 @@ void rba_buffer_add_const_times_term(rba_buffer_t *b, term_table_t *table, ratio assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: rba_buffer_add_mono(b, a, pprod_for_idx(table, i)); break; @@ -196,7 +196,7 @@ void rba_buffer_mul_term_power(rba_buffer_t *b, term_table_t *table, term_t t, u assert(pos_term(t) && good_term(table, t) && is_arithmetic_term(table, t)); i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: r = pprod_exp(b->ptbl, pprod_for_idx(table, i), d); // r = t^d rba_buffer_mul_pp(b, r); diff --git a/src/terms/terms.c b/src/terms/terms.c index 2bb635714..12903b90a 100644 --- a/src/terms/terms.c +++ b/src/terms/terms.c @@ -115,6 +115,23 @@ static void default_special_finalizer(special_term_t *s, term_kind_t tag) { } +/* + * Callback for indexed_table::extend. + */ +static void term_table_extend(indexed_table_t *t) { + uint32_t n = t->size; + + // force abort if n is too large + if (n > YICES_MAX_TERMS) { + out_of_memory(); + } + + term_table_t *terms = (term_table_t *)t; + + terms->mark = extend_bitvector(terms->mark, n); +} + + /* * Initialize table, with initial size n. * - ttbl = attached type table. @@ -126,16 +143,18 @@ static void term_table_init(term_table_t *table, uint32_t n, type_table_t *ttbl, out_of_memory(); } - table->kind = (unsigned char *) safe_malloc(n * sizeof(unsigned char)); - table->type = (type_t *) safe_malloc(n * sizeof(type_t)); - table->desc = (term_desc_t *) safe_malloc(n * sizeof(term_desc_t)); + /* The indexed_table_elem_t must be first. */ + assert(offsetof(term_desc_t, elem) == 0); + + static const indexed_table_vtbl_t vtbl = { + .elem_size = sizeof(term_desc_t), + .extend = term_table_extend + }; + + indexed_table_init(&table->terms, n, &vtbl); + table->mark = allocate_bitvector(n); - table->size = n; - table->nelems = 0; - table->free_idx = -1; // empty free list - table->live_terms = 0; - table->types = ttbl; table->pprods = ptbl; table->finalize = default_special_finalizer; @@ -156,29 +175,6 @@ static void term_table_init(term_table_t *table, uint32_t n, type_table_t *ttbl, } -/* - * Extend the table: make it 50% larger - */ -static void term_table_extend(term_table_t *table) { - uint32_t n; - - n = table->size + 1; - n += n >> 1; - - // force abort if n is too large - if (n > YICES_MAX_TERMS) { - out_of_memory(); - } - - table->kind = (unsigned char *) safe_realloc(table->kind, n * sizeof(unsigned char)); - table->type = (type_t *) safe_realloc(table->type, n * sizeof(type_t)); - table->desc = (term_desc_t *) safe_realloc(table->desc, n * sizeof(term_desc_t)); - table->mark = extend_bitvector(table->mark, n); - table->size = n; -} - - - /* * TERM ALLOCATION */ @@ -187,28 +183,20 @@ static void term_table_extend(term_table_t *table) { * Allocate a new term id * - clear its mark. Nothing else is initialized. */ -static int32_t allocate_term_id(term_table_t *table) { - int32_t i; - - i = table->free_idx; - if (i >= 0) { - table->free_idx = table->desc[i].integer; - } else { - i = table->nelems; - table->nelems ++; - if (i == table->size) { - term_table_extend(table); - } - assert(i < table->size); - } +static int32_t allocate_term_id(term_table_t *table, + term_kind_t kind, + type_t tau) { + int32_t i = indexed_table_alloc(&table->terms); + *term_desc(table, i) = (term_desc_t) { + .kind = kind, + .type = tau + }; clr_bit(table->mark, i); - table->live_terms ++; return i; } - /* * Terms with integer descriptor * - tag = kind @@ -218,10 +206,8 @@ static int32_t allocate_term_id(term_table_t *table) { static int32_t new_integer_term(term_table_t *table, term_kind_t tag, type_t tau, int32_t id) { int32_t i; - i = allocate_term_id(table); - table->kind[i] = tag; - table->type[i] = tau; - table->desc[i].integer = id; + i = allocate_term_id(table, tag, tau); + term_desc(table, i)->integer = id; return i; } @@ -236,10 +222,8 @@ static int32_t new_integer_term(term_table_t *table, term_kind_t tag, type_t tau static int32_t new_ptr_term(term_table_t *table, term_kind_t tag, type_t tau, void *d) { int32_t i; - i = allocate_term_id(table); - table->kind[i] = tag; - table->type[i] = tau; - table->desc[i].ptr = d; + i = allocate_term_id(table, tag, tau); + term_desc(table, i)->ptr = d; return i; } @@ -254,11 +238,9 @@ static int32_t new_ptr_term(term_table_t *table, term_kind_t tag, type_t tau, vo static int32_t new_rational_term(term_table_t *table, term_kind_t tag, type_t tau, rational_t *a) { int32_t i; - i = allocate_term_id(table); - table->kind[i] = tag; - table->type[i] = tau; - q_init(&table->desc[i].rational); - q_set(&table->desc[i].rational, a); + i = allocate_term_id(table, tag, tau); + q_init(rational_for_idx(table, i)); + q_set(rational_for_idx(table, i), a); return i; } @@ -274,11 +256,11 @@ static int32_t new_rational_term(term_table_t *table, term_kind_t tag, type_t ta static int32_t new_select_term(term_table_t *table, term_kind_t tag, type_t tau, uint32_t k, term_t t) { int32_t i; - i = allocate_term_id(table); - table->kind[i] = tag; - table->type[i] = tau; - table->desc[i].select.idx = k; - table->desc[i].select.arg = t; + i = allocate_term_id(table, tag, tau); + term_desc(table, i)->select = (select_term_t) { + .idx = k, + .arg = t + }; return i; } @@ -944,19 +926,19 @@ static bool eq_integer_hobj(integer_term_hobj_t *o, int32_t i) { term_table_t *table; table = o->tbl; - assert(good_term_idx(table, i)); - return table->kind[i] == o->tag && table->type[i] == o->tau - && table->desc[i].integer == o->id; + return kind_for_idx(table, i) == o->tag + && type_for_idx(table, i) == o->tau + && integer_value_for_idx(table, i) == o->id; } static bool eq_rational_hobj(rational_term_hobj_t *o, int32_t i) { term_table_t *table; table = o->tbl; - assert(good_term_idx(table, i)); - return table->kind[i] == o->tag && q_eq(&table->desc[i].rational, o->a); + return kind_for_idx(table, i) == o->tag + && q_eq(rational_for_idx(table, i), o->a); } @@ -976,11 +958,10 @@ static bool eq_composite_hobj(composite_term_hobj_t *o, int32_t i) { uint32_t n; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != o->tag) return false; + if (kind_for_idx(table, i) != o->tag) return false; - d = table->desc[i].ptr; + d = ptr_for_idx(table, i); n = d->arity; return n == o->arity && eq_term_arrays(o->arg, d->arg, n); } @@ -991,11 +972,10 @@ static bool eq_app_hobj(app_term_hobj_t *o, int32_t i) { uint32_t n; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != APP_TERM) return false; + if (kind_for_idx(table, i) != APP_TERM) return false; - d = table->desc[i].ptr; + d = composite_for_idx(table, i); n = o->n; return d->arity == n+1 && d->arg[0] == o->f && eq_term_arrays(o->arg, d->arg + 1, n); @@ -1007,11 +987,10 @@ static bool eq_update_hobj(update_term_hobj_t *o, int32_t i) { uint32_t n; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != UPDATE_TERM) return false; + if (kind_for_idx(table, i) != UPDATE_TERM) return false; - d = table->desc[i].ptr; + d = composite_for_idx(table, i); n = o->n; return d->arity == n+2 && d->arg[0] == o->f && d->arg[n + 1] == o->v && @@ -1024,11 +1003,10 @@ static bool eq_forall_hobj(forall_term_hobj_t *o, int32_t i) { uint32_t n; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != FORALL_TERM) return false; + if (kind_for_idx(table, i) != FORALL_TERM) return false; - d = table->desc[i].ptr; + d = composite_for_idx(table, i); n = o->n; return d->arity == n+1 && d->arg[n] == o->p && eq_term_arrays(o->v, d->arg, n); @@ -1040,11 +1018,10 @@ static bool eq_lambda_hobj(lambda_term_hobj_t *o, int32_t i) { uint32_t n; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != LAMBDA_TERM) return false; + if (kind_for_idx(table, i) != LAMBDA_TERM) return false; - d = table->desc[i].ptr; + d = composite_for_idx(table, i); n = o->n; return d->arity == n+1 && d->arg[n] == o->t && eq_term_arrays(o->v, d->arg, n); } @@ -1054,11 +1031,10 @@ static bool eq_select_hobj(select_term_hobj_t *o, int32_t i) { select_term_t *d; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != o->tag) return false; + if (kind_for_idx(table, i) != o->tag) return false; - d = &table->desc[i].select; + d = select_for_idx(table, i); return d->idx == o->k && d->arg == o->arg; } @@ -1067,11 +1043,10 @@ static bool eq_root_atom_hobj(root_atom_hobj_t *o, int32_t i) { root_atom_t *r; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != ARITH_ROOT_ATOM) return false; + if (kind_for_idx(table, i) != ARITH_ROOT_ATOM) return false; - r = table->desc[i].ptr; + r = root_atom_for_idx(table, i); return r->k == o->k && r->p == o->p && r->r == o->r && r->x == o->x; } @@ -1080,52 +1055,48 @@ static bool eq_pprod_hobj(pprod_term_hobj_t *o, int32_t i) { term_table_t *table; table = o->tbl; - assert(good_term_idx(table, i)); - return table->kind[i] == POWER_PRODUCT && table->desc[i].ptr == o->r; + + return kind_for_idx(table, i) == POWER_PRODUCT && pprod_for_idx(table, i); } static bool eq_poly_hobj(poly_term_hobj_t *o, int32_t i) { term_table_t *table; table = o->tbl; - assert(good_term_idx(table, i)); - return table->kind[i] == ARITH_POLY && - rba_buffer_equal_poly(o->b, o->v, table->desc[i].ptr); + return kind_for_idx(table, i) == ARITH_POLY && + rba_buffer_equal_poly(o->b, o->v, polynomial_for_idx(table, i)); } static bool eq_bvpoly_hobj(bvpoly_term_hobj_t *o, int32_t i) { term_table_t *table; table = o->tbl; - assert(good_term_idx(table, i)); - return table->kind[i] == BV_POLY && - bvarith_buffer_equal_bvpoly(o->b, o->v, table->desc[i].ptr); + return kind_for_idx(table, i) == BV_POLY && + bvarith_buffer_equal_bvpoly(o->b, o->v, bvpoly_for_idx(table, i)); } static bool eq_bvpoly64_hobj(bvpoly64_term_hobj_t *o, int32_t i) { term_table_t *table; table = o->tbl; - assert(good_term_idx(table, i)); - return table->kind[i] == BV64_POLY && - bvarith64_buffer_equal_bvpoly(o->b, o->v, table->desc[i].ptr); + return kind_for_idx(table, i) == BV64_POLY && + bvarith64_buffer_equal_bvpoly(o->b, o->v, bvpoly64_for_idx(table, i)); } static bool eq_bvpoly_buffer_hobj(bvpoly_buffer_hobj_t *o, int32_t i) { term_table_t *table; table = o->tbl; - assert(good_term_idx(table, i)); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case BV64_POLY: - return bvpoly_buffer_equal_poly64(o->b, table->desc[i].ptr); + return bvpoly_buffer_equal_poly64(o->b, bvpoly64_for_idx(table, i)); case BV_POLY: - return bvpoly_buffer_equal_poly(o->b, table->desc[i].ptr); + return bvpoly_buffer_equal_poly(o->b, bvpoly_for_idx(table, i)); default: return false; @@ -1138,11 +1109,10 @@ static bool eq_bvconst_hobj(bvconst_term_hobj_t *o, int32_t i) { uint32_t n; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != BV_CONSTANT) return false; + if (kind_for_idx(table, i) != BV_CONSTANT) return false; - d = table->desc[i].ptr; + d = bvconst_for_idx(table, i); n = d->bitsize; return n == o->bitsize && bvconst_eq(d->data, o->v, (n + 31) >> 5); } @@ -1152,11 +1122,10 @@ static bool eq_bvconst64_hobj(bvconst64_term_hobj_t *o, int32_t i) { bvconst64_term_t *d; table = o->tbl; - assert(good_term_idx(table, i)); - if (table->kind[i] != BV64_CONSTANT) return false; + if (kind_for_idx(table, i) != BV64_CONSTANT) return false; - d = table->desc[i].ptr; + d = bvconst64_for_idx(table, i); return d->bitsize == o->bitsize && d->value == o->v; } @@ -1543,7 +1512,7 @@ static void delete_term(term_table_t *table, int32_t i) { if (i <= zero_const) return; // deal with unit types - tau = table->type[i]; + tau = type_for_idx(table, i); if (is_unit_type(table->types, tau)) { assert(is_unit_type_rep(table, tau, pos_term(i))); remove_unit_type_rep(table, tau); @@ -1559,7 +1528,7 @@ static void delete_term(term_table_t *table, int32_t i) { h = 0; // stops GCC warning // compute hash and free descriptor - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case UNINTERPRETED_TERM: // No descriptor, no hash consing goto recycle; @@ -1573,7 +1542,8 @@ static void delete_term(term_table_t *table, int32_t i) { case ARITH_CEIL: case ARITH_ABS: // The descriptor is an integer nothing to delete. - h = hash_integer_term(table->kind[i], table->type[i], table->desc[i].integer); + h = hash_integer_term(kind_for_idx(table, i), type_for_idx(table, i), + integer_value_for_idx(table, i)); break; case ITE_TERM: @@ -1600,22 +1570,22 @@ static void delete_term(term_table_t *table, int32_t i) { case BV_GE_ATOM: case BV_SGE_ATOM: // Generic composite - d = table->desc[i].ptr; - h = hash_composite_term(table->kind[i], d->arity, d->arg); + d = composite_for_idx(table, i); + h = hash_composite_term(kind_for_idx(table, i), d->arity, d->arg); safe_free(d); break; case ITE_SPECIAL: // Special composite: // call the finalizer before deleting the descriptor - d = table->desc[i].ptr; - h = hash_composite_term(table->kind[i], d->arity, d->arg); + d = composite_for_idx(table, i); + h = hash_composite_term(kind_for_idx(table, i), d->arity, d->arg); table->finalize(special_desc(d), ITE_SPECIAL); safe_free(special_desc(d)); break; case APP_TERM: - d = table->desc[i].ptr; + d = composite_for_idx(table, i); n = d->arity; assert(n >= 2); h = hash_app_term(d->arg[0], n-1, d->arg + 1); @@ -1623,7 +1593,7 @@ static void delete_term(term_table_t *table, int32_t i) { break; case UPDATE_TERM: - d = table->desc[i].ptr; + d = composite_for_idx(table, i); n = d->arity; assert(n >= 3); h = hash_update_term(d->arg[0], n-2, d->arg + 1, d->arg[n-1]); @@ -1631,7 +1601,7 @@ static void delete_term(term_table_t *table, int32_t i) { break; case FORALL_TERM: - d = table->desc[i].ptr; + d = composite_for_idx(table, i); n = d->arity; assert(n >= 2); h = hash_forall_term(n-1, d->arg, d->arg[n-1]); @@ -1639,7 +1609,7 @@ static void delete_term(term_table_t *table, int32_t i) { break; case LAMBDA_TERM: - d = table->desc[i].ptr; + d = composite_for_idx(table, i); n = d->arity; assert(n >= 2); h = hash_lambda_term(n-1, d->arg, d->arg[n-1]); @@ -1649,57 +1619,56 @@ static void delete_term(term_table_t *table, int32_t i) { case SELECT_TERM: case BIT_TERM: // Select terms: nothing to delete. - s = &table->desc[i].select; - h = hash_select_term(table->kind[i], s->idx, s->arg); + s = select_for_idx(table, i); + h = hash_select_term(kind_for_idx(table, i), s->idx, s->arg); break; case ARITH_ROOT_ATOM: // Root atoms - r = table->desc[i].ptr; + r = root_atom_for_idx(table, i); h = hash_root_atom(r->k, r->x, r->p, r->r); safe_free(r); break; case POWER_PRODUCT: // Power products are deleted in garbage collection of pprod. - h = hash_power_product(table->desc[i].ptr); + h = hash_power_product(pprod_for_idx(table, i)); break; case ARITH_CONSTANT: // Free the rational - h = hash_rational_term(ARITH_CONSTANT, table->type[i], &table->desc[i].rational); - q_clear(&table->desc[i].rational); + h = hash_rational_term(ARITH_CONSTANT, type_for_idx(table, i), + rational_for_idx(table, i)); + q_clear(rational_for_idx(table, i)); break; case ARITH_POLY: - h = hash_polynomial(table->desc[i].ptr); - free_polynomial(table->desc[i].ptr); + h = hash_polynomial(polynomial_for_idx(table, i)); + free_polynomial(polynomial_for_idx(table, i)); break; case BV64_CONSTANT: - c64 = table->desc[i].ptr; + c64 = bvconst64_for_idx(table, i); h = hash_bvconst64_term(c64->bitsize, c64->value); safe_free(c64); break; case BV_CONSTANT: - c = table->desc[i].ptr; + c = bvconst_for_idx(table, i); h = hash_bvconst_term(c->bitsize, c->data); safe_free(c); break; case BV64_POLY: - h = hash_bvpoly64(table->desc[i].ptr); - free_bvpoly64(table->desc[i].ptr); + h = hash_bvpoly64(bvpoly64_for_idx(table, i)); + free_bvpoly64(bvpoly64_for_idx(table, i)); break; case BV_POLY: - h = hash_bvpoly(table->desc[i].ptr); - free_bvpoly(table->desc[i].ptr); + h = hash_bvpoly(bvpoly_for_idx(table, i)); + free_bvpoly(bvpoly_for_idx(table, i)); break; - case UNUSED_TERM: - case RESERVED_TERM: default: assert(false); break; @@ -1710,12 +1679,8 @@ static void delete_term(term_table_t *table, int32_t i) { // Put i in the free list recycle: - table->desc[i].integer = table->free_idx; - table->free_idx = i; - table->kind[i] = UNUSED_TERM; - - assert(table->live_terms > 0); - table->live_terms --; + term_desc(table, i)->kind = UNUSED_TERM; + indexed_table_free(&table->terms, i); } @@ -1738,11 +1703,9 @@ static void add_primitive_terms(term_table_t *table) { rational_t q; int32_t i; - i = allocate_term_id(table); + i = allocate_term_id(table, RESERVED_TERM, NULL_TYPE); assert(i == const_idx); - table->kind[i] = RESERVED_TERM; - table->type[i] = NULL_TYPE; - table->desc[i].ptr = NULL; + term_desc(table, i)->ptr = NULL; i = constant_term(table, bool_type(table->types), 0); assert(i == true_term); @@ -1794,9 +1757,9 @@ static void delete_name_table(ptr_hmap_t *table) { static void delete_term_descriptors(term_table_t *table) { uint32_t i, n; - n = table->nelems; + n = nterms(table); for (i=0; ikind[i]) { + switch (unchecked_kind_for_idx(table, i)) { case UNUSED_TERM: case RESERVED_TERM: case CONSTANT_TERM: @@ -1843,29 +1806,29 @@ static void delete_term_descriptors(term_table_t *table) { case BV_EQ_ATOM: case BV_GE_ATOM: case BV_SGE_ATOM: - safe_free(table->desc[i].ptr); + safe_free(composite_for_idx(table, i)); break; case ITE_SPECIAL: - table->finalize(special_desc(table->desc[i].ptr), ITE_SPECIAL); - safe_free(special_desc(table->desc[i].ptr)); + table->finalize(special_desc(composite_for_idx(table, i)), ITE_SPECIAL); + safe_free(special_desc(composite_for_idx(table, i))); break; case ARITH_CONSTANT: // Free the rational - q_clear(&table->desc[i].rational); + q_clear(rational_for_idx(table, i)); break; case ARITH_POLY: - free_polynomial(table->desc[i].ptr); + free_polynomial(polynomial_for_idx(table, i)); break; case BV64_POLY: - free_bvpoly64(table->desc[i].ptr); + free_bvpoly64(bvpoly64_for_idx(table, i)); break; case BV_POLY: - free_bvpoly(table->desc[i].ptr); + free_bvpoly(bvpoly_for_idx(table, i)); break; default: @@ -1890,17 +1853,10 @@ void delete_term_table(term_table_t *table) { delete_ivector(&table->ibuffer); delete_pvector(&table->pbuffer); - safe_free(table->kind); - safe_free(table->type); - safe_free(table->desc); delete_bitvector(table->mark); - - table->kind = NULL; - table->type = NULL; - table->desc = NULL; table->mark = NULL; - + indexed_table_destroy(&table->terms); } @@ -1938,9 +1894,7 @@ void reset_term_table(term_table_t *table) { ivector_reset(&table->ibuffer); pvector_reset(&table->pbuffer); - table->nelems = 0; - table->free_idx = -1; - table->live_terms = 0; + indexed_table_clear(&table->terms); add_primitive_terms(table); } @@ -2061,10 +2015,8 @@ term_t constant_term(term_table_t *table, type_t tau, int32_t index) { term_t new_uninterpreted_term(term_table_t *table, type_t tau) { int32_t i; - i = allocate_term_id(table); - table->kind[i] = UNINTERPRETED_TERM; - table->type[i] = tau; - table->desc[i].ptr = NULL; + i = allocate_term_id(table, UNINTERPRETED_TERM, tau); + term_desc(table, i)->ptr = NULL; return pos_term(i); } @@ -2077,10 +2029,8 @@ term_t new_uninterpreted_term(term_table_t *table, type_t tau) { term_t new_variable(term_table_t *table, type_t tau) { int32_t i; - i = allocate_term_id(table); - table->kind[i] = VARIABLE; - table->type[i] = tau; - table->desc[i].integer = i; + i = allocate_term_id(table, VARIABLE, tau); + term_desc(table, i)->integer = i; return pos_term(i); } @@ -3050,8 +3000,8 @@ pprod_t *pprod_for_term(const term_table_t *table, term_t t) { r = var_pp(t); i = index_of(t); - if (table->kind[i] == POWER_PRODUCT) { - r = table->desc[i].ptr; + if (kind_for_idx(table, i) == POWER_PRODUCT) { + r = pprod_for_idx(table, i); } return r; } @@ -3069,8 +3019,8 @@ static uint32_t main_var_degree(const term_table_t *table, int32_t x) { } else { assert(is_pos_term(x) && good_term(table, x)); x = index_of(x); - if (table->kind[x] == POWER_PRODUCT) { - d = pprod_degree(table->desc[x].ptr); + if (kind_for_idx(table, x) == POWER_PRODUCT) { + d = pprod_degree(pprod_for_idx(table, x)); } } @@ -3091,9 +3041,9 @@ uint32_t term_degree(const term_table_t *table, term_t t) { d = 1; i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case POWER_PRODUCT: - d = pprod_degree(table->desc[i].ptr); + d = pprod_degree(pprod_for_idx(table, i)); break; case ARITH_CONSTANT: @@ -3103,15 +3053,19 @@ uint32_t term_degree(const term_table_t *table, term_t t) { break; case ARITH_POLY: - d = main_var_degree(table, polynomial_main_var(table->desc[i].ptr)); + d = main_var_degree(table, + polynomial_main_var(polynomial_for_idx(table, i))); break; - + case BV64_POLY: - d = main_var_degree(table, bvpoly64_main_var(table->desc[i].ptr)); + d = main_var_degree(table, bvpoly64_main_var(bvpoly64_for_idx(table, i))); break; case BV_POLY: - d = main_var_degree(table, bvpoly_main_var(table->desc[i].ptr)); + d = main_var_degree(table, bvpoly_main_var(bvpoly_for_idx(table, i))); + break; + + default: break; } @@ -3124,7 +3078,7 @@ uint32_t term_degree(const term_table_t *table, term_t t) { */ static bool not_pprod(const term_table_t *table, int32_t x) { assert(is_pos_term(x) && good_term(table, x)); - return table->kind[index_of(x)] != POWER_PRODUCT; + return term_kind(table, x) != POWER_PRODUCT; } /* @@ -3143,17 +3097,20 @@ bool is_linear_poly(const term_table_t *table, term_t t) { result = false; i = index_of(t); - switch (table->kind[i]) { + switch (kind_for_idx(table, i)) { case ARITH_POLY: - result = not_pprod(table, polynomial_main_var(table->desc[i].ptr)); + result = not_pprod(table, + polynomial_main_var(polynomial_for_idx(table, i))); break; case BV64_POLY: - result = not_pprod(table, bvpoly64_main_var(table->desc[i].ptr)); + result = not_pprod(table, + bvpoly64_main_var(bvpoly64_for_idx(table, i))); break; case BV_POLY: - result = not_pprod(table, bvpoly_main_var(table->desc[i].ptr)); + result = not_pprod(table, + bvpoly_main_var(bvpoly_for_idx(table, i))); break; default: @@ -3530,7 +3487,7 @@ static void mark_power_product(term_table_t *table, int32_t ptr, pprod_t *r) { static void mark_reachable_terms(term_table_t *table, int32_t ptr, int32_t i) { assert(term_idx_is_marked(table, i)); - switch (table->kind[i]) { + switch (unchecked_kind_for_idx(table, i)) { case UNUSED_TERM: case RESERVED_TERM: case CONSTANT_TERM: @@ -3549,12 +3506,12 @@ static void mark_reachable_terms(term_table_t *table, int32_t ptr, int32_t i) { case ARITH_CEIL: case ARITH_ABS: // i has a single subterm stored in desc[i].integer - mark_and_explore_term(table, ptr, table->desc[i].integer); + mark_and_explore_term(table, ptr, integer_value_for_idx(table, i)); break; case ARITH_ROOT_ATOM: // i is a root atom - mark_root_atom(table, ptr, table->desc[i].ptr); + mark_root_atom(table, ptr, root_atom_for_idx(table, i)); break; case ITE_TERM: @@ -3585,34 +3542,34 @@ static void mark_reachable_terms(term_table_t *table, int32_t ptr, int32_t i) { case BV_GE_ATOM: case BV_SGE_ATOM: // i's descriptor is a composite term - mark_composite_term(table, ptr, table->desc[i].ptr); + mark_composite_term(table, ptr, composite_for_idx(table, i)); break; case ITE_SPECIAL: // TODO: do we need a callback here for scanning the extra component? - mark_composite_term(table, ptr, table->desc[i].ptr); + mark_composite_term(table, ptr, composite_for_idx(table, i)); break; case SELECT_TERM: case BIT_TERM: // i's descriptor is a select term - mark_select_term(table, ptr, &table->desc[i].select); + mark_select_term(table, ptr, select_for_idx(table, i)); break; case POWER_PRODUCT: - mark_power_product(table, ptr, table->desc[i].ptr); + mark_power_product(table, ptr, pprod_for_idx(table, i)); break; case ARITH_POLY: - mark_polynomial(table, ptr, table->desc[i].ptr); + mark_polynomial(table, ptr, polynomial_for_idx(table, i)); break; case BV64_POLY: - mark_bvpoly64(table, ptr, table->desc[i].ptr); + mark_bvpoly64(table, ptr, bvpoly64_for_idx(table, i)); break; case BV_POLY: - mark_bvpoly(table, ptr, table->desc[i].ptr); + mark_bvpoly(table, ptr, bvpoly_for_idx(table, i)); break; default: @@ -3635,7 +3592,7 @@ static void mark_live_terms(term_table_t *table) { type_table_t *types; uint32_t i, n; - n = table->nelems; + n = nterms(table); for (i=0; itypes; for (i=1; itype[i]); + type_table_set_gc_mark(types, type_for_idx(table, i)); } } } @@ -3709,13 +3666,14 @@ void term_table_gc(term_table_t *table, bool keep_named) { pprod_table_gc(table->pprods); // delete the unmarked terms - n = table->nelems; + n = nterms(table); for (i=0; ikind[i] != UNUSED_TERM) { + if (! term_idx_is_marked(table, i) + && unchecked_kind_for_idx(table, i) != UNUSED_TERM) { delete_term(table, i); } } // clear the marks - clear_bitvector(table->mark, table->size); + clear_bitvector(table->mark, n); } diff --git a/src/terms/terms.h b/src/terms/terms.h index 721adcbef..d05c08124 100644 --- a/src/terms/terms.h +++ b/src/terms/terms.h @@ -190,6 +190,7 @@ #include "terms/pprod_table.h" #include "terms/types.h" #include "utils/bitvectors.h" +#include "utils/indexed_table.h" #include "utils/int_hash_map.h" #include "utils/int_hash_tables.h" #include "utils/int_vectors.h" @@ -434,14 +435,24 @@ typedef struct special_term_s { * - pair (idx, arg) for select term * - ptr to a composite, polynomial, power-product, or bvconst */ -typedef union { - int32_t integer; - void *ptr; - rational_t rational; - select_term_t select; +typedef struct { + /* The term descriptor. */ + union { + int32_t integer; + void *ptr; + rational_t rational; + select_term_t select; + /* This must be the first element. */ + indexed_table_elem_t elem; + }; + + /* The kind of term. */ + uint8_t kind; + + /* The type of the term. */ + type_t type; } term_desc_t; - /* * Finalizer function: this is called when a special_term * is deleted (to cleanup the spec->extra field). @@ -487,15 +498,9 @@ typedef void (*special_finalizer_t)(special_term_t *spec, term_kind_t tag); * - pbuffer: to store an array of pprods */ typedef struct term_table_s { - uint8_t *kind; - term_desc_t *desc; - type_t *type; - byte_t *mark; + indexed_table_t terms; - uint32_t size; - uint32_t nelems; - int32_t free_idx; - uint32_t live_terms; + byte_t *mark; type_table_t *types; pprod_table_t *pprods; @@ -511,8 +516,6 @@ typedef struct term_table_s { } term_table_t; - - /* * INITIALIZATION */ @@ -531,6 +534,19 @@ extern void init_term_table(term_table_t *table, uint32_t n, type_table_t *ttbl, */ extern void delete_term_table(term_table_t *table); +/* + * Returns the number of terms in the table. + */ +static inline uint32_t nterms(const term_table_t *table) { + return indexed_table_nelems(&table->terms); +} + +/* + * Returns the number of live terms in the table. + */ +static inline uint32_t live_terms(const term_table_t *table) { + return indexed_table_live_elems(&table->terms); +} /* * Install f as the special finalizer @@ -1134,88 +1150,96 @@ static inline void term_table_reset_pbuffer(term_table_t *table) { * From a term index i */ static inline bool valid_term_idx(const term_table_t *table, int32_t i) { - return 0 <= i && i < table->nelems; + return 0 <= i && i < nterms(table); +} + +static inline term_desc_t *term_desc(const term_table_t *table, + int32_t i) { + return &((term_desc_t *) table->terms.elems)[i]; +} + +static inline term_kind_t unchecked_kind_for_idx(const term_table_t *table, + int32_t i) { + return term_desc(table, i)->kind; } static inline bool live_term_idx(const term_table_t *table, int32_t i) { - return valid_term_idx(table, i) && table->kind[i] != UNUSED_TERM; + return valid_term_idx(table, i) + && term_desc(table, i)->kind != UNUSED_TERM; } static inline bool good_term_idx(const term_table_t *table, int32_t i) { - return valid_term_idx(table, i) && table->kind[i] > RESERVED_TERM; + return valid_term_idx(table, i) + && term_desc(table, i)->kind > RESERVED_TERM; } static inline type_t type_for_idx(const term_table_t *table, int32_t i) { assert(good_term_idx(table, i)); - return table->type[i]; + return term_desc(table, i)->type; } static inline term_kind_t kind_for_idx(const term_table_t *table, int32_t i) { assert(good_term_idx(table, i)); - return table->kind[i]; + return unchecked_kind_for_idx(table, i); } // descriptor converted to an appropriate type static inline int32_t integer_value_for_idx(const term_table_t *table, int32_t i) { assert(good_term_idx(table, i)); - return table->desc[i].integer; + return term_desc(table, i)->integer; } -static inline composite_term_t *composite_for_idx(const term_table_t *table, int32_t i) { +static inline void *ptr_for_idx(const term_table_t *table, int32_t i) { assert(good_term_idx(table, i)); - return (composite_term_t *) table->desc[i].ptr; + return term_desc(table, i)->ptr; +} + +static inline composite_term_t *composite_for_idx(const term_table_t *table, int32_t i) { + return (composite_term_t *) ptr_for_idx(table, i); } static inline select_term_t *select_for_idx(const term_table_t *table, int32_t i) { assert(good_term_idx(table, i)); - return &table->desc[i].select; + return &term_desc(table, i)->select; } static inline root_atom_t *root_atom_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return (root_atom_t *) table->desc[i].ptr; + return (root_atom_t *) ptr_for_idx(table, i); } static inline pprod_t *pprod_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return (pprod_t *) table->desc[i].ptr; + return (pprod_t *) ptr_for_idx(table, i); } static inline rational_t *rational_for_idx(const term_table_t *table, int32_t i) { assert(good_term_idx(table, i)); - return &table->desc[i].rational; + return &term_desc(table, i)->rational; } static inline polynomial_t *polynomial_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return (polynomial_t *) table->desc[i].ptr; + return (polynomial_t *) ptr_for_idx(table, i); } static inline bvconst64_term_t *bvconst64_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return (bvconst64_term_t *) table->desc[i].ptr; + return (bvconst64_term_t *) ptr_for_idx(table, i); } static inline bvconst_term_t *bvconst_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return (bvconst_term_t *) table->desc[i].ptr; + return (bvconst_term_t *) ptr_for_idx(table, i); } static inline bvpoly64_t *bvpoly64_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return (bvpoly64_t *) table->desc[i].ptr; + return (bvpoly64_t *) ptr_for_idx(table, i); } static inline bvpoly_t *bvpoly_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return (bvpoly_t *) table->desc[i].ptr; + return (bvpoly_t *) ptr_for_idx(table, i); } // bitsize of bitvector terms static inline uint32_t bitsize_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return bv_type_size(table->types, table->type[i]); + return bv_type_size(table->types, type_for_idx(table, i)); } @@ -1665,8 +1689,7 @@ static inline special_term_t *special_desc(composite_term_t *p) { } static inline special_term_t *special_for_idx(const term_table_t *table, int32_t i) { - assert(good_term_idx(table, i)); - return special_desc(table->desc[i].ptr); + return special_desc(ptr_for_idx(table, i)); } static inline composite_term_t *ite_special_term_desc(const term_table_t *table, term_t t) { diff --git a/src/utils/indexed_table.c b/src/utils/indexed_table.c new file mode 100644 index 000000000..8b7751a1e --- /dev/null +++ b/src/utils/indexed_table.c @@ -0,0 +1,81 @@ +#include + +#include "indexed_table.h" +#include "memalloc.h" +#include "yices_limits.h" + +#define MAX_ELEMS YICES_MAX_TYPES + +static inline void check_nelems(uindex_t n) { + if (n > MAX_ELEMS) + out_of_memory(); +} + +static inline size_t elem_size(indexed_table_t *t) { + return t->vtbl->elem_size; +} + +static inline indexed_table_elem_t *elem(indexed_table_t *t, index_t i) { + return (indexed_table_elem_t *) (((char *) t->elems) + i * elem_size(t)); +} + +static void extend(indexed_table_t *t) { + uindex_t n; + + n = t->size + 1; + n += n >> 1; + + check_nelems(n); + + t->elems = safe_realloc(t->elems, n * elem_size(t)); + t->size = n; + + t->vtbl->extend(t); +} + +void indexed_table_init(indexed_table_t *t, uindex_t n, + const indexed_table_vtbl_t *vtbl) { + check_nelems(n); + + *t = (indexed_table_t) { + .elems = safe_malloc(n * vtbl->elem_size), + .size = n, + .vtbl = vtbl + }; + + indexed_table_clear(t); +} + +void indexed_table_destroy(indexed_table_t *t) { + safe_free(t->elems); +} + +index_t indexed_table_alloc(indexed_table_t *t) { + index_t i = t->free_idx; + + if (i >= 0) { + t->free_idx = elem(t, i)->next; + } else { + i = t->nelems++; + if (i == t->size) + extend(t); + assert(i < t->size); + } + + t->live_elems++; + + return i; +} + +void indexed_table_free(indexed_table_t *t, index_t i) { + elem(t, i)->next = t->free_idx; + t->free_idx = i; + + t->live_elems--; +} + +void indexed_table_clear(indexed_table_t *t) { + t->nelems = 0; + t->free_idx = -1; + t->live_elems = 0; +} diff --git a/src/utils/indexed_table.h b/src/utils/indexed_table.h new file mode 100644 index 000000000..33a5c05da --- /dev/null +++ b/src/utils/indexed_table.h @@ -0,0 +1,117 @@ +/* + * This file is part of the Yices SMT Solver. + * Copyright (C) 2023 SRI International. + * + * Yices is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Yices is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Yices. If not, see . + */ + +#ifndef __INDEXED_TABLE_H +#define __INDEXED_TABLE_H + +#include +#include + +/* An index into the table. */ +typedef int32_t index_t; + +/* An unsigned index into the table. */ +typedef uint32_t uindex_t; + +typedef struct indexed_table_s indexed_table_t; + +typedef struct indexed_table_vtbl_s { + /* The size of an individual element. */ + size_t elem_size; + + /* Called after extending the table. */ + void (*extend)(indexed_table_t *t); +} indexed_table_vtbl_t; + +/* The type of elements on the free list. */ +typedef struct indexed_table_elem_s { + index_t next; +} indexed_table_elem_t; + +/* + * An index_table_t is an expandable array, with idices of type + * index_t. + */ +struct indexed_table_s { + /* The elements themselves. + + Declared as "void *" to prevent accidental pointer arithmetic or + array access. */ + void *elems; + + /* The number of elements allocated in the table. */ + uindex_t size; + + /* The number of elements that have (at some point) been + used. Elements with this index (or greater) are unused. */ + uindex_t nelems; + + /* The number of active elements in the table. The sum of live_elems + and the length of the free list is always equal to nelems. */ + uindex_t live_elems; + + /* If greater than or equal to zero, the head of the free list. The + free list is composed of deleted entries. */ + index_t free_idx; + + /* Callbacks for derived classes. */ + const indexed_table_vtbl_t *vtbl; +}; + +/* + * Initialize the table, making room for N elements. + */ +extern void indexed_table_init(indexed_table_t *t, + uindex_t n, + const indexed_table_vtbl_t *vtbl); + +/* + * Delete the table, freeing all associated storage. + */ +extern void indexed_table_destroy(indexed_table_t *t); + +/* + * Allocate a new entry in the table. + */ +extern index_t indexed_table_alloc(indexed_table_t *t); + +/* + * Free an entry in the table. + */ +extern void indexed_table_free(indexed_table_t *t, index_t i); + +/* + * Remove all entries from the table. + */ +extern void indexed_table_clear(indexed_table_t *t); + +/* + * The number of elements in the table. + */ +static inline uindex_t indexed_table_nelems(const indexed_table_t *t) { + return t->nelems; +} + +/* + * The number of live entries. + */ +static inline uindex_t indexed_table_live_elems(const indexed_table_t *t) { + return t->live_elems; +} + +#endif /* !defined(__INDEXED_TABLE_H) */ diff --git a/src/utils/int_powers.h b/src/utils/int_powers.h index d795c81f6..6265654d9 100644 --- a/src/utils/int_powers.h +++ b/src/utils/int_powers.h @@ -23,8 +23,16 @@ #ifndef __INT_POWERS_H #define __INT_POWERS_H +#include #include +/* + * Return true iff N is a power of two. + */ +static inline bool is_power_of_two(uint32_t n) { + return (n & (n - 1)) == 0; +} + /* * Return x^d (modulo 2^32 or 2^64) */ From d85e128262cbbbe986f1a555294e5eaffee12848 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Tue, 31 Oct 2023 11:55:20 -0700 Subject: [PATCH 3/7] Convert type table to used indexed_table. --- src/api/yices_api.c | 2 +- src/io/type_printer.c | 8 +- src/terms/terms.c | 10 +- src/terms/terms.h | 20 +-- src/terms/types.c | 333 ++++++++++++++++-------------------------- src/terms/types.h | 203 ++++++++++++------------- 6 files changed, 241 insertions(+), 335 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 5631ee93d..46374cf98 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -12249,7 +12249,7 @@ EXPORTED uint32_t yices_num_types(void) { } uint32_t _o_yices_num_types(void) { - return __yices_globals.types->live_types; + return live_types(__yices_globals.types); } diff --git a/src/io/type_printer.c b/src/io/type_printer.c index 4a45df14d..c9c325a5b 100644 --- a/src/io/type_printer.c +++ b/src/io/type_printer.c @@ -250,10 +250,10 @@ static uint32_t max_name_length(type_table_t *tbl) { uint32_t max, l, n, i; max = 0; - n = tbl->nelems; + n = ntypes(tbl); for (i=0; iname[i]; + name = type_name(tbl, i); if (name != NULL) { l = strlen(name); if (l > max) { @@ -311,7 +311,7 @@ void print_type_table(FILE *f, type_table_t *tbl) { name_size = 20; } - n = tbl->nelems; + n = ntypes(tbl); for (i=0; inelems; + n = ntypes(tbl); for (i=0; istbl, table, dead_term_symbol); } - // force garbage collection in the type and power-product tables - type_table_gc(table->types, keep_named); - pprod_table_gc(table->pprods); - // delete the unmarked terms n = nterms(table); for (i=0; itypes, keep_named); + pprod_table_gc(table->pprods); + // clear the marks clear_bitvector(table->mark, n); } diff --git a/src/terms/terms.h b/src/terms/terms.h index d05c08124..9880cacdd 100644 --- a/src/terms/terms.h +++ b/src/terms/terms.h @@ -438,12 +438,13 @@ typedef struct special_term_s { typedef struct { /* The term descriptor. */ union { + /* This must be the first element in term_desc_t. */ + indexed_table_elem_t elem; + int32_t integer; void *ptr; rational_t rational; select_term_t select; - /* This must be the first element. */ - indexed_table_elem_t elem; }; /* The kind of term. */ @@ -464,21 +465,6 @@ typedef void (*special_finalizer_t)(special_term_t *spec, term_kind_t tag); /* * Term table: valid terms have indices between 0 and nelems - 1 * - * For each i between 0 and nelems - 1 - * - kind[i] = term kind - * - type[i] = type - * - desc[i] = term descriptor - * - mark[i] = one bit used during garbage collection - * - size = size of these arrays. - * - * After deletion, term indices are recycled into a free list. - * - free_idx = start of the free list (-1 if the list is empty) - * - if i is in the free list then kind[i] is UNUSED and - * desc[i].integer is the index of the next term in the free list - * (or -1 if i is the last element in the free list). - * - * - live_terms = number of actual terms = nelems - size of the free list - * * Symbol table and name table: * - stbl is a symbol table that maps names (strings) to term occurrences. * - the name table is the reverse. If maps term occurrence to a name. diff --git a/src/terms/types.c b/src/terms/types.c index 5f3b0f095..32f1450c5 100644 --- a/src/terms/types.c +++ b/src/terms/types.c @@ -247,6 +247,11 @@ static void typename_finalizer(stbl_rec_t *r) { string_decref(r->string); } +static void type_table_exend(indexed_table_t *t) { + if (t->nelems > YICES_MAX_TYPES) { + out_of_memory(); + } +} /* * Initialize table, with initial size = n. @@ -257,17 +262,15 @@ static void type_table_init(type_table_t *table, uint32_t n) { out_of_memory(); } - table->kind = (uint8_t *) safe_malloc(n * sizeof(uint8_t)); - table->desc = (type_desc_t *) safe_malloc(n * sizeof(type_desc_t)); - table->card = (uint32_t *) safe_malloc(n * sizeof(uint32_t)); - table->flags = (uint8_t *) safe_malloc(n * sizeof(uint8_t)); - table->name = (char **) safe_malloc(n * sizeof(char *)); - table->depth = (uint32_t *) safe_malloc(n * sizeof(uint32_t)); + /* The indexed_table_elem_t must be first. */ + assert(offsetof(type_desc_t, elem) == 0); - table->size = n; - table->nelems = 0; - table->free_idx = NULL_TYPE; - table->live_types = 0; + static const indexed_table_vtbl_t vtbl = { + .elem_size = sizeof(type_desc_t), + .extend = type_table_exend + }; + + indexed_table_init(&table->types, n, &vtbl); init_int_htbl(&table->htbl, 0); // use default size init_stbl(&table->stbl, 0); // default size too @@ -285,53 +288,24 @@ static void type_table_init(type_table_t *table, uint32_t n) { } -/* - * Extend the table: make it 50% larger - */ -static void type_table_extend(type_table_t *table) { - uint32_t n; - - /* - * new size = 1.5 * (old_size + 1) approximately - * this computation can't overflow since old_size < YICES_MAX_TYPE - * this also ensures that new size > old size (even if old_size <= 1). - */ - n = table->size + 1; - n += n >> 1; - if (n > YICES_MAX_TYPES) { - out_of_memory(); - } - - table->kind = (uint8_t *) safe_realloc(table->kind, n * sizeof(uint8_t)); - table->desc = (type_desc_t *) safe_realloc(table->desc, n * sizeof(type_desc_t)); - table->card = (uint32_t *) safe_realloc(table->card, n * sizeof(uint32_t)); - table->flags = (uint8_t *) safe_realloc(table->flags, n * sizeof(uint8_t)); - table->name = (char **) safe_realloc(table->name, n * sizeof(char *)); - table->depth = (uint32_t *) safe_realloc(table->depth, n * sizeof(uint32_t)); - - table->size = n; -} - - /* * Get a free type id and initializes its name to NULL. * The other fields are not initialized. */ -static type_t allocate_type_id(type_table_t *table) { - type_t i; - - i = table->free_idx; - if (i >= 0) { - table->free_idx = table->desc[i].next; - } else { - i = table->nelems; - table->nelems ++; - if (i >= table->size) { - type_table_extend(table); - } - } - table->name[i] = NULL; - table->live_types ++; +static type_t allocate_type_id(type_table_t *table, + type_kind_t kind, + uint32_t card, + uint32_t depth, + uint8_t flags) { + type_t i = indexed_table_alloc(&table->types); + + *type_desc(table, i) = (type_desc_t) { + .kind = kind, + .card = card, + .depth = depth, + .flags = flags, + .name = NULL + }; return i; } @@ -341,7 +315,9 @@ static type_t allocate_type_id(type_table_t *table) { * Erase type i: free its descriptor and add i to the free list */ static void erase_type(type_table_t *table, type_t i) { - switch (table->kind[i]) { + type_desc_t *desc = type_desc(table, i); + + switch (desc->kind) { case UNUSED_TYPE: // already deleted case BOOL_TYPE: case INT_TYPE: @@ -356,21 +332,18 @@ static void erase_type(type_table_t *table, type_t i) { case TUPLE_TYPE: case FUNCTION_TYPE: case INSTANCE_TYPE: - safe_free(table->desc[i].ptr); + safe_free(desc->ptr); break; } - if (table->name[i] != NULL) { - string_decref(table->name[i]); - table->name[i] = NULL; + if (desc->name != NULL) { + string_decref(desc->name); + desc->name = NULL; } - table->kind[i] = UNUSED_TYPE; - table->desc[i].next = table->free_idx; - table->free_idx = i; + desc->kind = UNUSED_TYPE; - assert(table->live_types > 0); - table->live_types --; + indexed_table_free(&table->types, i); } @@ -578,29 +551,20 @@ static inline uint32_t depth_instance_type(type_table_t *table, uint32_t n, cons static void add_primitive_types(type_table_t *table) { type_t i; - i = allocate_type_id(table); + i = allocate_type_id(table, BOOL_TYPE, /*card=*/2, /*depth=*/0, + SMALL_TYPE_FLAGS); + type_desc(table, i)->ptr = NULL; assert(i == bool_id); - table->kind[i] = BOOL_TYPE; - table->desc[i].ptr = NULL; - table->card[i] = 2; - table->flags[i] = SMALL_TYPE_FLAGS; - table->depth[i] = 0; - i = allocate_type_id(table); + i = allocate_type_id(table, INT_TYPE, /*card=*/UINT32_MAX, /*depth=*/0, + INFINITE_TYPE_FLAGS | TYPE_IS_MINIMAL_MASK); + type_desc(table, i)->ptr = NULL; assert(i == int_id); - table->kind[i] = INT_TYPE; - table->desc[i].ptr = NULL; - table->card[i] = UINT32_MAX; - table->flags[i] = (INFINITE_TYPE_FLAGS | TYPE_IS_MINIMAL_MASK); - table->depth[i] = 0; - i = allocate_type_id(table); + i = allocate_type_id(table, REAL_TYPE, /*card=*/UINT32_MAX, /*depth=*/0, + INFINITE_TYPE_FLAGS | TYPE_IS_MAXIMAL_MASK); + type_desc(table, i)->ptr = NULL; assert(i == real_id); - table->kind[i] = REAL_TYPE; - table->desc[i].ptr = NULL; - table->card[i] = UINT32_MAX; - table->flags[i] = (INFINITE_TYPE_FLAGS | TYPE_IS_MAXIMAL_MASK); - table->depth[i] = 0; } @@ -611,21 +575,13 @@ static void add_primitive_types(type_table_t *table) { * - k must be positive and no more than YICES_MAX_BVSIZE */ static type_t new_bitvector_type(type_table_t *table, uint32_t k) { - type_t i; - assert(0 < k && k <= YICES_MAX_BVSIZE); - i = allocate_type_id(table); - table->kind[i] = BITVECTOR_TYPE; - table->desc[i].integer = k; - table->depth[i] = 0; - if (k < 32) { - table->card[i] = ((uint32_t) 1) << k; - table->flags[i] = SMALL_TYPE_FLAGS; - } else { - table->card[i] = UINT32_MAX; - table->flags[i] = LARGE_TYPE_FLAGS; - } + type_t i = allocate_type_id(table, BITVECTOR_TYPE, + /*card=*/k < 32 ? ((uint32_t) 1) << k : UINT32_MAX, + /*depth=*/0, + k < 32 ? SMALL_TYPE_FLAGS : LARGE_TYPE_FLAGS); + type_desc(table, i)->integer = k; return i; } @@ -637,20 +593,11 @@ static type_t new_bitvector_type(type_table_t *table, uint32_t k) { * - k must be positive. */ type_t new_scalar_type(type_table_t *table, uint32_t k) { - type_t i; - assert(k > 0); - i = allocate_type_id(table); - table->kind[i] = SCALAR_TYPE; - table->desc[i].integer = k; - table->card[i] = k; - table->depth[i] = 0; - if (k == 1) { - table->flags[i] = UNIT_TYPE_FLAGS; - } else { - table->flags[i] = SMALL_TYPE_FLAGS; - } + type_t i = allocate_type_id(table, SCALAR_TYPE, /*card=*/k, /*depth=*/0, + k == 1 ? UNIT_TYPE_FLAGS : SMALL_TYPE_FLAGS); + type_desc(table, i)->integer = k; return i; } @@ -661,14 +608,10 @@ type_t new_scalar_type(type_table_t *table, uint32_t k) { * - the type is infinite and both minimal and maximal */ type_t new_uninterpreted_type(type_table_t *table) { - type_t i; - - i = allocate_type_id(table); - table->kind[i] = UNINTERPRETED_TYPE; - table->desc[i].ptr = NULL; - table->card[i] = UINT32_MAX; - table->flags[i] = (INFINITE_TYPE_FLAGS | TYPE_IS_MAXIMAL_MASK | TYPE_IS_MINIMAL_MASK); - table->depth[i] = 0; + type_t i = allocate_type_id(table, UNINTERPRETED_TYPE, /*card=*/UINT32_MAX, + /*depth=*/0, + /*flags=*/INFINITE_TYPE_FLAGS | TYPE_IS_MAXIMAL_MASK | TYPE_IS_MINIMAL_MASK); + type_desc(table, i)->ptr = NULL; return i; } @@ -680,7 +623,6 @@ type_t new_uninterpreted_type(type_table_t *table) { static type_t new_tuple_type(type_table_t *table, uint32_t n, const type_t *e) { tuple_type_t *d; uint64_t card; - type_t i; uint32_t j, flag; assert(0 < n && n <= YICES_MAX_ARITY); @@ -689,10 +631,6 @@ static type_t new_tuple_type(type_table_t *table, uint32_t n, const type_t *e) { d->nelem = n; for (j=0; jelem[j] = e[j]; - i = allocate_type_id(table); - table->kind[i] = TUPLE_TYPE; - table->desc[i].ptr = d; - /* * set flags and card * - type_flags_conjunct sets all the bits correctly @@ -725,9 +663,11 @@ static type_t new_tuple_type(type_table_t *table, uint32_t n, const type_t *e) { } assert(0 < card && card <= UINT32_MAX); - table->card[i] = card; - table->flags[i] = flag; - table->depth[i] = depth_tuple_type(table, n, e); + + type_t i = allocate_type_id(table, TUPLE_TYPE, card, + depth_tuple_type(table, n, e), + flag); + type_desc(table, i)->ptr = d; return i; } @@ -739,7 +679,6 @@ static type_t new_tuple_type(type_table_t *table, uint32_t n, const type_t *e) { static type_t new_function_type(type_table_t *table, uint32_t n, const type_t *e, type_t r) { function_type_t *d; uint64_t card; - type_t i; uint32_t j, flag, rflag, minmax; assert(0 < n && n <= YICES_MAX_ARITY); @@ -749,10 +688,6 @@ static type_t new_function_type(type_table_t *table, uint32_t n, const type_t *e d->ndom = n; for (j=0; jdomain[j] = e[j]; - i = allocate_type_id(table); - table->kind[i] = FUNCTION_TYPE; - table->desc[i].ptr = d; - /* * Three of the function type's flags are inherited from the range: * - fun type is unit iff range is unit (and the domains are ground) @@ -807,9 +742,11 @@ static type_t new_function_type(type_table_t *table, uint32_t n, const type_t *e } assert(0 < card && card <= UINT32_MAX); - table->card[i] = card; - table->flags[i] = flag; - table->depth[i] = depth_function_type(table, n, e, r); + + type_t i = allocate_type_id(table, FUNCTION_TYPE, card, + depth_function_type(table, n, e, r), + flag); + type_desc(table, i)->ptr = d; return i; } @@ -819,14 +756,9 @@ static type_t new_function_type(type_table_t *table, uint32_t n, const type_t *e * Add a new type variable of the given id */ static type_t new_type_variable(type_table_t *table, uint32_t id) { - type_t i; - - i = allocate_type_id(table); - table->kind[i] = VARIABLE_TYPE; - table->desc[i].integer = id; - table->card[i] = UINT32_MAX; // card is not defined - table->flags[i] = FREE_TYPE_FLAGS; - table->depth[i] = 0; + type_t i = allocate_type_id(table, VARIABLE_TYPE, /*card=*/UINT32_MAX, + /*depth=*/0, FREE_TYPE_FLAGS); + type_desc(table, i)->integer = id; return i; } @@ -843,7 +775,6 @@ static type_t new_type_variable(type_table_t *table, uint32_t id) { */ static type_t new_instance_type(type_table_t *table, int32_t cid, uint32_t n, const type_t *param) { instance_type_t *d; - type_t i; uint32_t j, flag; assert(0 < n && n <= YICES_MAX_ARITY); @@ -856,19 +787,17 @@ static type_t new_instance_type(type_table_t *table, int32_t cid, uint32_t n, co d->param[j] = param[j]; } - i = allocate_type_id(table); - table->kind[i] = INSTANCE_TYPE; - table->desc[i].ptr = d; - table->card[i] = UINT32_MAX; - flag = type_flags_conjunct(table, n, param); assert((flag & TYPE_IS_GROUND_MASK) || flag == FREE_TYPE_FLAGS); if (flag & TYPE_IS_GROUND_MASK) { // set flags as for uninterpreted types flag = (INFINITE_TYPE_FLAGS | TYPE_IS_MAXIMAL_MASK | TYPE_IS_MINIMAL_MASK); } - table->flags[i] = flag; - table->depth[i] = depth_instance_type(table, n, param); + + type_t i = allocate_type_id(table, INSTANCE_TYPE, /*card=*/UINT32_MAX, + depth_instance_type(table, n, param), + flag); + type_desc(table, i)->ptr = d; return i; } @@ -986,7 +915,7 @@ static bool eq_bv_type(bv_type_hobj_t *p, type_t i) { type_table_t *table; table = p->tbl; - return table->kind[i] == BITVECTOR_TYPE && table->desc[i].integer == p->size; + return type_desc(table, i)->kind == BITVECTOR_TYPE && type_desc(table, i)->integer == p->size; } static bool eq_tuple_type(tuple_type_hobj_t *p, type_t i) { @@ -995,9 +924,9 @@ static bool eq_tuple_type(tuple_type_hobj_t *p, type_t i) { int32_t j; table = p->tbl; - if (table->kind[i] != TUPLE_TYPE) return false; + if (type_desc(table, i)->kind != TUPLE_TYPE) return false; - d = (tuple_type_t *) table->desc[i].ptr; + d = (tuple_type_t *) type_desc(table, i)->ptr; if (d->nelem != p->n) return false; for (j=0; jn; j++) { @@ -1013,9 +942,9 @@ static bool eq_function_type(function_type_hobj_t *p, type_t i) { int32_t j; table = p->tbl; - if (table->kind[i] != FUNCTION_TYPE) return false; + if (type_desc(table, i)->kind != FUNCTION_TYPE) return false; - d = (function_type_t *) table->desc[i].ptr; + d = (function_type_t *) type_desc(table, i)->ptr; if (d->range != p->range || d->ndom != p->n) return false; for (j=0; jn; j++) { @@ -1029,7 +958,7 @@ static bool eq_type_var(type_var_hobj_t *p, type_t i) { type_table_t *table; table = p->tbl; - return table->kind[i] == VARIABLE_TYPE && table->desc[i].integer == p->id; + return type_desc(table, i)->kind == VARIABLE_TYPE && type_desc(table, i)->integer == p->id; } static bool eq_instance_type(instance_type_hobj_t *p, type_t i) { @@ -1038,9 +967,9 @@ static bool eq_instance_type(instance_type_hobj_t *p, type_t i) { uint32_t j; table = p->tbl; - if (table->kind[i] != INSTANCE_TYPE) return false; + if (type_desc(table, i)->kind != INSTANCE_TYPE) return false; - d = (instance_type_t *) table->desc[i].ptr; + d = (instance_type_t *) type_desc(table, i)->ptr; if (d->cid != p->cid || d->arity != p->arity) return false; for (j=0; jarity; j++) { @@ -1097,19 +1026,19 @@ void delete_type_table(type_table_t *table) { uint32_t i; // decrement refcount for all names - for (i=0; inelems; i++) { - if (table->name[i] != NULL) { - string_decref(table->name[i]); + for (i=0; iname != NULL) { + string_decref(type_desc(table, i)->name); } } // delete all allocated descriptors - for (i=0; inelems; i++) { - switch (table->kind[i]) { + for (i=0; ikind) { case TUPLE_TYPE: case FUNCTION_TYPE: case INSTANCE_TYPE: - safe_free(table->desc[i].ptr); + safe_free(type_desc(table, i)->ptr); break; default: @@ -1117,20 +1046,6 @@ void delete_type_table(type_table_t *table) { } } - safe_free(table->kind); - safe_free(table->desc); - safe_free(table->card); - safe_free(table->flags); - safe_free(table->name); - safe_free(table->depth); - - table->kind = NULL; - table->desc = NULL; - table->card = NULL; - table->flags = NULL; - table->name = NULL; - table->depth = NULL; - delete_int_htbl(&table->htbl); delete_stbl(&table->stbl); @@ -1157,6 +1072,8 @@ void delete_type_table(type_table_t *table) { safe_free(table->macro_tbl); table->macro_tbl = NULL; } + + indexed_table_destroy(&table->types); } @@ -1167,19 +1084,19 @@ void reset_type_table(type_table_t *table) { uint32_t i; // decrement ref counts - for (i=0; inelems; i++) { - if (table->name[i] != NULL) { - string_decref(table->name[i]); + for (i=0; iname != NULL) { + string_decref(type_desc(table, i)->name); } } // delete descriptors - for (i=0; inelems; i++) { - switch (table->kind[i]) { + for (i=0; ikind) { case TUPLE_TYPE: case FUNCTION_TYPE: case INSTANCE_TYPE: - safe_free(table->desc[i].ptr); + safe_free(type_desc(table, i)->ptr); break; default: @@ -1203,9 +1120,7 @@ void reset_type_table(type_table_t *table) { reset_type_mtbl(table->macro_tbl); } - table->nelems = 0; - table->free_idx = NULL_TYPE; - table->live_types = 0; + indexed_table_clear(&table->types); add_primitive_types(table); } @@ -2005,8 +1920,8 @@ bool types_match(type_table_t *table, type_t tau, type_t sigma, int_hmap_t *subs * in memalloc.h). */ void set_type_name(type_table_t *table, type_t i, char *name) { - if (table->name[i] == NULL) { - table->name[i] = name; + if (type_desc(table, i)->name == NULL) { + type_desc(table, i)->name = name; string_incref(name); } stbl_add(&table->stbl, name, i); @@ -2035,12 +1950,12 @@ void remove_type_name(type_table_t *table, const char *name) { void clear_type_name(type_table_t *table, type_t t) { char *name; - name = table->name[t]; + name = type_desc(table, t)->name; if (name != NULL) { if (stbl_find(&table->stbl, name) == t) { stbl_remove(&table->stbl, name); } - table->name[t] = NULL; + type_desc(table, t)->name = NULL; string_decref(name); } } @@ -2131,16 +2046,16 @@ static type_t cheap_sup(type_table_t *table, type_t tau1, type_t tau2) { return real_id; } - switch (table->kind[tau1]) { + switch (type_desc(table, tau1)->kind) { case TUPLE_TYPE: - if (table->kind[tau2] != TUPLE_TYPE || + if (type_desc(table, tau2)->kind != TUPLE_TYPE || tuple_type_arity(table, tau1) != tuple_type_arity(table, tau2)) { return NULL_TYPE; } break; case FUNCTION_TYPE: - if (table->kind[tau2] != FUNCTION_TYPE || + if (type_desc(table, tau2)->kind != FUNCTION_TYPE || function_type_arity(table, tau1) != function_type_arity(table, tau2)) { return NULL_TYPE; } @@ -2266,7 +2181,7 @@ type_t super_type(type_table_t *table, type_t tau1, type_t tau2) { /* * The result is not in the cache. */ - if (table->kind[tau1] == TUPLE_TYPE) { + if (type_desc(table, tau1)->kind == TUPLE_TYPE) { tup1 = tuple_type_desc(table, tau1); tup2 = tuple_type_desc(table, tau2); assert(tup1->nelem == tup2->nelem); @@ -2313,16 +2228,16 @@ static type_t cheap_inf(type_table_t *table, type_t tau1, type_t tau2) { return int_id; } - switch (table->kind[tau1]) { + switch (type_desc(table, tau1)->kind) { case TUPLE_TYPE: - if (table->kind[tau2] != TUPLE_TYPE || + if (type_desc(table, tau2)->kind != TUPLE_TYPE || tuple_type_arity(table, tau1) != tuple_type_arity(table, tau2)) { return NULL_TYPE; } break; case FUNCTION_TYPE: - if (table->kind[tau2] != FUNCTION_TYPE || + if (type_desc(table, tau2)->kind != FUNCTION_TYPE || function_type_arity(table, tau1) != function_type_arity(table, tau2)) { return NULL_TYPE; } @@ -2434,7 +2349,7 @@ type_t inf_type(type_table_t *table, type_t tau1, type_t tau2) { /* * The result is not in the cache. */ - if (table->kind[tau1] == TUPLE_TYPE) { + if (type_desc(table, tau1)->kind == TUPLE_TYPE) { tup1 = tuple_type_desc(table, tau1); tup2 = tuple_type_desc(table, tau2); assert(tup1->nelem == tup2->nelem); @@ -2542,7 +2457,7 @@ type_t max_super_type(type_table_t *table, type_t tau) { aux = r->val; } else { // max is not in the cache - if (table->kind[tau] == TUPLE_TYPE) { + if (type_desc(table, tau)->kind == TUPLE_TYPE) { aux = max_tuple_super_type(table, tuple_type_desc(table, tau)); } else { aux = max_function_super_type(table, function_type_desc(table,tau)); @@ -2832,25 +2747,25 @@ type_t instantiate_type_macro(type_table_t *table, int32_t id, uint32_t n, const static void erase_hcons_type(type_table_t *table, type_t i) { uint32_t k; - switch (table->kind[i]) { + switch (type_desc(table, i)->kind) { case BITVECTOR_TYPE: - k = hash_bvtype(table->desc[i].integer); + k = hash_bvtype(type_desc(table, i)->integer); break; case VARIABLE_TYPE: - k = hash_typevar(table->desc[i].integer); + k = hash_typevar(type_desc(table, i)->integer); break; case TUPLE_TYPE: - k = hash_tupletype(table->desc[i].ptr); + k = hash_tupletype(type_desc(table, i)->ptr); break; case FUNCTION_TYPE: - k = hash_funtype(table->desc[i].ptr); + k = hash_funtype(type_desc(table, i)->ptr); break; case INSTANCE_TYPE: - k = hash_instancetype(table->desc[i].ptr); + k = hash_instancetype(type_desc(table, i)->ptr); break; default: @@ -2888,11 +2803,11 @@ static void mark_reachable_types(type_table_t *table, type_t ptr, type_t i) { instance_type_t *inst; uint32_t n, j; - assert(type_is_marked(table, i) && table->kind[i] != UNUSED_TYPE); + assert(type_is_marked(table, i) && type_desc(table, i)->kind != UNUSED_TYPE); - switch (table->kind[i]) { + switch (type_desc(table, i)->kind) { case TUPLE_TYPE: - tup = table->desc[i].ptr; + tup = type_desc(table, i)->ptr; n = tup->nelem; for (j=0; jelem[j]); @@ -2900,7 +2815,7 @@ static void mark_reachable_types(type_table_t *table, type_t ptr, type_t i) { break; case FUNCTION_TYPE: - fun = table->desc[i].ptr; + fun = type_desc(table, i)->ptr; mark_and_explore(table, ptr, fun->range); n = fun->ndom; for (j=0; jdesc[i].ptr; + inst = type_desc(table, i)->ptr; n = inst->arity; for (j=0; jparam[j]); @@ -2930,7 +2845,7 @@ static void mark_reachable_types(type_table_t *table, type_t ptr, type_t i) { static void mark_live_types(type_table_t *table) { uint32_t i, n; - n = table->nelems; + n = ntypes(table); for (i=0; inelems; + n = ntypes(table); for (i=0; i= UINT32_MAX. */ + uint32_t card; + + /* string id or NULL */ + char *name; + /* + * syntactic depth: + * for atomic types and type variables: depth = 0 + * or tuple type (tau_1 x ... x tau_n): depth = 1 + max depth(tau_i) + * for function type (tau_1 ... tau_n -> tau_0): depth = 1 + max depth(tau_i) + * for instance type F(tau_1, ... , tau_n): depth = 1 + max depth(tau_i) + */ + uint32_t depth; +} type_desc_t; /* * Type table: valid type indices are between 0 and nelems - 1 * - * For each i between 0 and nelems - 1, - * - kind[i] = type kind - * - desc[i] = type descriptor - * - card[i] = cardinality of type i or - * UINT32_MAX if i is infinite or has card > UINT32_MAX - * - name[i] = string id or NULL. - * - flags[i] = 8bit flags: - * bit 0 of flag[i] is 1 if i is finite - * bit 1 of flag[i] is 1 if i is a unit type - * bit 2 of flag[i] is 1 if card[i] is exact - * bit 3 of flag[i] is 1 if i has no strict supertype - * bit 4 of flag[i] is 1 if i has no strict subtype - * - * bit 5 of flag[i] is 1 if i is a ground type (i.e., no variables - * occur in i). If this bit is '0', then bits 0 to 4 are not used, - * but they must all be set to '0' too. - * - * bit 7 is used as a mark during garbage collection - * - depth[i] = syntactic depth: - * for atomic types and type variables: depth = 0 - * for tuple type (tau_1 x ... x tau_n): depth = 1 + max depth(tau_i) - * for function type (tau_1 ... tau_n -> tau_0): depth = 1 + max depth(tau_i) - * for instance type F(tau_1, ... , tau_n): depth = 1 + max depth(tau_i) - * - * Other components: - * - size = size of all arrays above - * - nelems = number of elements in the array - * - free_idx = start of the free list (-1 means empty free list). - * The free list contains the deleted types: for each i in the list, - * kind[i] = UNUSED_TYPE - * desc[i].next = index of i's successor in the list (or -1). - * - live_types = number of types = nelems - size of the free_list + * - types = indexed_table_t of type_desc_t * - htbl = hash table for hash consing * - stbl = symbol table for named types * stbl stores a mapping from strings to type ids. @@ -307,17 +300,7 @@ typedef struct type_mtbl_s { * Macro table: also allocated on demand */ typedef struct type_table_s { - uint8_t *kind; - type_desc_t *desc; - uint32_t *card; - uint8_t *flags; - char **name; - uint32_t *depth; - - uint32_t size; - uint32_t nelems; - int32_t free_idx; - uint32_t live_types; + indexed_table_t types; int_htbl_t htbl; stbl_t stbl; @@ -447,13 +430,41 @@ extern void init_type_table(type_table_t *table, uint32_t n); */ extern void delete_type_table(type_table_t *table); +/* + * Returns the number of types. + */ +static inline uint32_t ntypes(const type_table_t *table) { + return indexed_table_nelems(&table->types); +} + +/* + * Returns the number of live types. + */ +static inline uint32_t live_types(const type_table_t *table) { + return indexed_table_live_elems(&table->types); +} /* * Reset: remove all types and macros, and empty the symbol_table */ extern void reset_type_table(type_table_t *table); +/* + * Return the ith type descriptor. + */ +static inline type_desc_t *type_desc(const type_table_t *table, + int32_t i) { + return &((type_desc_t *) table->types.elems)[i]; +} + +static inline bool valid_type(type_table_t *tbl, type_t i) { + return 0 <= i && i < ntypes(tbl); +} +static inline type_kind_t type_kind(type_table_t *tbl, type_t i) { + assert(valid_type(tbl, i)); + return type_desc(tbl, i)->kind; +} /* * TYPE CONSTRUCTORS @@ -463,17 +474,17 @@ extern void reset_type_table(type_table_t *table); * Predefined types */ static inline type_t bool_type(type_table_t *table) { - assert(table->nelems > bool_id && table->kind[bool_id] == BOOL_TYPE); + assert(type_kind(table, bool_id) == BOOL_TYPE); return bool_id; } static inline type_t int_type(type_table_t *table) { - assert(table->nelems > int_id && table->kind[int_id] == INT_TYPE); + assert(type_kind(table, int_id) == INT_TYPE); return int_id; } static inline type_t real_type(type_table_t *table) { - assert(table->nelems > real_id && table->kind[real_id] == REAL_TYPE); + assert(type_kind(table, real_id) == REAL_TYPE); return real_id; } @@ -754,18 +765,10 @@ static inline bool is_arithmetic_type(type_t i) { /* * Extract components from the table */ -static inline bool valid_type(type_table_t *tbl, type_t i) { - return 0 <= i && i < tbl->nelems; -} - -static inline type_kind_t type_kind(type_table_t *tbl, type_t i) { - assert(valid_type(tbl, i)); - return tbl->kind[i]; -} // check for deleted types static inline bool good_type(type_table_t *tbl, type_t i) { - return valid_type(tbl, i) && (tbl->kind[i] != UNUSED_TYPE); + return valid_type(tbl, i) && type_kind(tbl, i) != UNUSED_TYPE; } static inline bool bad_type(type_table_t *tbl, type_t i) { @@ -773,38 +776,38 @@ static inline bool bad_type(type_table_t *tbl, type_t i) { } +static inline uint8_t type_flags(type_table_t *tbl, type_t i) { + assert(good_type(tbl, i)); + return type_desc(tbl, i)->flags; +} + // ground type: does not contain variables static inline bool ground_type(type_table_t *tbl, type_t i) { assert(good_type(tbl, i)); - return tbl->flags[i] & TYPE_IS_GROUND_MASK; + return type_flags(tbl, i) & TYPE_IS_GROUND_MASK; } // access card, flags, name, depth of non-deleted type static inline uint32_t type_card(type_table_t *tbl, type_t i) { assert(good_type(tbl, i)); - return tbl->card[i]; -} - -static inline uint8_t type_flags(type_table_t *tbl, type_t i) { - assert(good_type(tbl, i)); - return tbl->flags[i]; + return type_desc(tbl, i)->card; } static inline char *type_name(type_table_t *tbl, type_t i) { assert(good_type(tbl, i)); - return tbl->name[i]; + return type_desc(tbl, i)->name; } static inline uint32_t type_depth(type_table_t *tbl, type_t i) { assert(good_type(tbl, i)); - return tbl->depth[i]; + return type_desc(tbl, i)->depth; } // check whether i is atomic (i.e., not a tuple or function type) static inline bool is_atomic_type(type_table_t *tbl, type_t i) { assert(ground_type(tbl, i)); - return tbl->kind[i] <= UNINTERPRETED_TYPE; + return type_kind(tbl, i) <= UNINTERPRETED_TYPE; } // bit vector types @@ -814,7 +817,7 @@ static inline bool is_bv_type(type_table_t *tbl, type_t i) { static inline uint32_t bv_type_size(type_table_t *tbl, type_t i) { assert(is_bv_type(tbl, i)); - return tbl->desc[i].integer; + return type_desc(tbl, i)->integer; } // uninterpreted types @@ -829,7 +832,7 @@ static inline bool is_scalar_type(type_table_t *tbl, type_t i) { static inline uint32_t scalar_type_cardinal(type_table_t *tbl, type_t i) { assert(is_scalar_type(tbl, i)); - return tbl->desc[i].integer; + return type_desc(tbl, i)->integer; } @@ -840,7 +843,7 @@ static inline bool is_type_variable(type_table_t *tbl, type_t i) { static inline uint32_t type_variable_id(type_table_t *tbl, type_t i) { assert(is_type_variable(tbl, i)); - return tbl->desc[i].integer; + return type_desc(tbl, i)->integer; } @@ -851,17 +854,17 @@ static inline bool is_tuple_type(type_table_t *tbl, type_t i) { static inline tuple_type_t *tuple_type_desc(type_table_t *tbl, type_t i) { assert(is_tuple_type(tbl, i)); - return (tuple_type_t *) tbl->desc[i].ptr; + return (tuple_type_t *) type_desc(tbl, i)->ptr; } static inline uint32_t tuple_type_arity(type_table_t *tbl, type_t i) { assert(is_tuple_type(tbl, i)); - return ((tuple_type_t *) tbl->desc[i].ptr)->nelem; + return ((tuple_type_t *) type_desc(tbl, i)->ptr)->nelem; } static inline type_t tuple_type_component(type_table_t *tbl, type_t i, int32_t j) { assert(0 <= j && j < tuple_type_arity(tbl, i)); - return ((tuple_type_t *) tbl->desc[i].ptr)->elem[j]; + return ((tuple_type_t *) type_desc(tbl, i)->ptr)->elem[j]; } @@ -872,22 +875,22 @@ static inline bool is_function_type(type_table_t *tbl, type_t i) { static inline function_type_t *function_type_desc(type_table_t *tbl, type_t i) { assert(is_function_type(tbl, i)); - return (function_type_t *) tbl->desc[i].ptr; + return (function_type_t *) type_desc(tbl, i)->ptr; } static inline type_t function_type_range(type_table_t *tbl, type_t i) { assert(is_function_type(tbl, i)); - return ((function_type_t *) tbl->desc[i].ptr)->range; + return ((function_type_t *) type_desc(tbl, i)->ptr)->range; } static inline uint32_t function_type_arity(type_table_t *tbl, type_t i) { assert(is_function_type(tbl, i)); - return ((function_type_t *) tbl->desc[i].ptr)->ndom; + return ((function_type_t *) type_desc(tbl, i)->ptr)->ndom; } static inline type_t function_type_domain(type_table_t *tbl, type_t i, int32_t j) { assert(0 <= j && j < function_type_arity(tbl, i)); - return ((function_type_t *) tbl->desc[i].ptr)->domain[j]; + return ((function_type_t *) type_desc(tbl, i)->ptr)->domain[j]; } @@ -898,7 +901,7 @@ static inline bool is_instance_type(type_table_t *tbl, type_t i) { static inline instance_type_t *instance_type_desc(type_table_t *tbl, type_t i) { assert(is_instance_type(tbl, i)); - return (instance_type_t *) tbl->desc[i].ptr; + return (instance_type_t *) type_desc(tbl, i)->ptr; } static inline int32_t instance_type_cid(type_table_t *tbl, type_t i) { @@ -939,17 +942,17 @@ static inline type_t instance_type_param(type_table_t *tbl, type_t i, int32_t j) */ static inline bool is_finite_type(type_table_t *tbl, type_t i) { assert(valid_type(tbl, i)); - return tbl->flags[i] & TYPE_IS_FINITE_MASK; + return type_flags(tbl, i) & TYPE_IS_FINITE_MASK; } static inline bool is_unit_type(type_table_t *tbl, type_t i) { assert(valid_type(tbl, i)); - return tbl->flags[i] & TYPE_IS_UNIT_MASK; + return type_flags(tbl, i) & TYPE_IS_UNIT_MASK; } static inline bool type_card_is_exact(type_table_t *tbl, type_t i) { assert(valid_type(tbl, i)); - return tbl->flags[i] & CARD_IS_EXACT_MASK; + return type_flags(tbl, i) & CARD_IS_EXACT_MASK; } @@ -1009,7 +1012,7 @@ extern bool type_has_finite_range(type_table_t *table, type_t tau); */ static inline bool is_maxtype(type_table_t *tbl, type_t i) { assert(valid_type(tbl, i)); - return tbl->flags[i] & TYPE_IS_MAXIMAL_MASK; + return type_flags(tbl, i) & TYPE_IS_MAXIMAL_MASK; } /* @@ -1017,7 +1020,7 @@ static inline bool is_maxtype(type_table_t *tbl, type_t i) { */ static inline bool is_mintype(type_table_t *tbl, type_t i) { assert(valid_type(tbl, i)); - return tbl->flags[i] & TYPE_IS_MINIMAL_MASK; + return type_flags(tbl, i) & TYPE_IS_MINIMAL_MASK; } @@ -1146,7 +1149,7 @@ extern type_t apply_type_matching(type_matcher_t *matcher, type_t tau); */ static inline void type_table_set_gc_mark(type_table_t *tbl, type_t i) { assert(good_type(tbl, i)); - tbl->flags[i] |= TYPE_GC_MARK; + type_desc(tbl, i)->flags |= TYPE_GC_MARK; } /* @@ -1154,7 +1157,7 @@ static inline void type_table_set_gc_mark(type_table_t *tbl, type_t i) { */ static inline void type_table_clr_gc_mark(type_table_t *tbl, type_t i) { assert(valid_type(tbl, i)); - tbl->flags[i] &= ~TYPE_GC_MARK; + type_desc(tbl, i)->flags &= ~TYPE_GC_MARK; } /* @@ -1162,7 +1165,7 @@ static inline void type_table_clr_gc_mark(type_table_t *tbl, type_t i) { */ static inline bool type_is_marked(type_table_t *tbl, type_t i) { assert(valid_type(tbl, i)); - return tbl->flags[i] & TYPE_GC_MARK; + return type_flags(tbl, i) & TYPE_GC_MARK; } From 5aeacefc273cf1a70f87f26c392912f9c98902b6 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Tue, 21 Nov 2023 11:11:55 -0800 Subject: [PATCH 4/7] Used indexed_table in type macro table. --- src/io/type_printer.c | 2 +- src/terms/types.c | 146 +++++++++++++------------------------- src/terms/types.h | 51 +++++++------ src/utils/indexed_table.c | 17 +++++ src/utils/indexed_table.h | 18 +++++ 5 files changed, 109 insertions(+), 125 deletions(-) diff --git a/src/io/type_printer.c b/src/io/type_printer.c index c9c325a5b..06679825b 100644 --- a/src/io/type_printer.c +++ b/src/io/type_printer.c @@ -389,7 +389,7 @@ void print_type_macros(FILE *f, type_table_t *tbl) { mtbl = tbl->macro_tbl; if (mtbl != NULL) { - n = mtbl->nelems; + n = type_macro_nelems(mtbl); for (i=0; inelems > TYPE_MACRO_MAX_SIZE) + out_of_memory(); +} + + /* * Initialize the macro table * - n = initial size @@ -100,20 +106,16 @@ static inline void delete_descriptor(type_macro_t *d) { * on the first addition. */ static void init_type_mtbl(type_mtbl_t *table, uint32_t n) { - void **tmp; - - tmp = NULL; - if (n > 0) { - if (n > TYPE_MACRO_MAX_SIZE) { - out_of_memory(); - } - tmp = (void **) safe_malloc(n * sizeof(void*)); + if (n > TYPE_MACRO_MAX_SIZE) { + out_of_memory(); } + + static const indexed_table_vtbl_t vtbl = { + .elem_size = sizeof(type_mtbl_elem_t), + .extend = type_mtbl_extend + }; - table->data = tmp; - table->size = n; - table->nelems = 0; - table->free_idx = -1; + indexed_table_init(&table->macros, n, &vtbl); init_stbl(&table->stbl, 0); init_tuple_hmap(&table->cache, 0); @@ -121,24 +123,32 @@ static void init_type_mtbl(type_mtbl_t *table, uint32_t n) { stbl_set_finalizer(&table->stbl, macro_name_finalizer); } +static void type_mtbl_clear_elem(indexed_table_elem_t *elem, + void *data) { + ((type_mtbl_elem_t *) elem)->data = NULL; +} + +static void type_mtbl_delete_macros(type_mtbl_t *table) { + /* Clear elements used for the free list. */ + indexed_table_for_each_free_elem(&table->macros, + type_mtbl_clear_elem, + /*data=*/NULL); + + /* Remove all of the macros. */ + uint32_t i; + for (i=0; inelems; - for (i=0; idata[i]; - if (! has_int_tag(p)) { - delete_descriptor(p); - } - } - - safe_free(table->data); - table->data = NULL; + type_mtbl_delete_macros(table); + indexed_table_destroy(&table->macros); delete_stbl(&table->stbl); delete_tuple_hmap(&table->cache); @@ -149,71 +159,22 @@ static void delete_type_mtbl(type_mtbl_t *table) { * Empty the table: delete all macros and macro instances */ static void reset_type_mtbl(type_mtbl_t *table) { - void *p; - uint32_t i, n; - - n = table->nelems; - for (i=0; idata[i]; - if (! has_int_tag(p)) { - delete_descriptor(p); - } - } - - table->nelems = 0; - table->free_idx = -1; + type_mtbl_delete_macros(table); + indexed_table_clear(&table->macros); reset_stbl(&table->stbl); reset_tuple_hmap(&table->cache); } -/* - * Make the table larger - * - if this is the first allocation: allocate a data array of default size - * - otherwise, make the data array 50% larger - */ -static void extend_type_mtbl(type_mtbl_t *table) { - void **tmp; - uint32_t n; - - n = table->size; - if (n == 0) { - n = TUPLE_HMAP_DEF_SIZE; - assert(n <= TYPE_MACRO_MAX_SIZE); - tmp = (void **) safe_malloc(n * sizeof(void*)); - } else { - n ++; - n += n>>1; - if (n > TYPE_MACRO_MAX_SIZE) { - out_of_memory(); - } - tmp = (void **) safe_realloc(table->data, n * sizeof(void*)); - } - - table->data = tmp; - table->size = n; -} - - /* * Get a macro index */ -static int32_t allocate_macro_id(type_mtbl_t *table) { - int32_t i; +static inline int32_t allocate_macro_id(type_mtbl_t *table, + type_macro_t *d) { + int32_t i = indexed_table_alloc(&table->macros); - i = table->free_idx; - if (i >= 0) { - assert(i < table->nelems); - table->free_idx = untag_i32(table->data[i]); - } else { - i = table->nelems; - table->nelems ++; - if (i >= table->size) { - extend_type_mtbl(table); - assert(i < table->size); - } - } + indexed_table_elem(type_mtbl_elem_t, table->macros, i)->data = d; return i; } @@ -224,10 +185,8 @@ static int32_t allocate_macro_id(type_mtbl_t *table) { * - this must be the index of a live descriptor */ static void free_macro_id(type_mtbl_t *table, int32_t id) { - assert(good_type_macro(table, id)); - delete_descriptor(table->data[id]); - table->data[id] = tag_i32(table->free_idx); - table->free_idx = id; + delete_descriptor(type_macro_def(table, id)); + indexed_table_free(&table->macros, id); } @@ -2537,10 +2496,8 @@ int32_t add_type_macro(type_table_t *table, char *name, uint32_t n, const type_t assert(body != NULL_TYPE); - i = allocate_macro_id(mtbl); d = new_descriptor(name, n, vars, body); - assert(! has_int_tag(d)); - mtbl->data[i] = d; + i = allocate_macro_id(mtbl, d); stbl_add(&mtbl->stbl, name, i); string_incref(name); @@ -2561,10 +2518,8 @@ int32_t add_type_constructor(type_table_t *table, char *name, uint32_t n) { mtbl = get_macro_table(table); - i = allocate_macro_id(mtbl); d = new_constructor(name, n); - assert(! has_int_tag(d)); - mtbl->data[i] = d; + i = allocate_macro_id(mtbl, d); stbl_add(&mtbl->stbl, name, i); string_incref(name); @@ -2602,7 +2557,7 @@ type_macro_t *type_macro(type_table_t *table, int32_t id) { mtbl = table->macro_tbl; macro = NULL; if (mtbl != NULL && good_type_macro(mtbl, id)) { - macro = mtbl->data[id]; + macro = type_macro_unchecked(mtbl, id); } return macro; @@ -2651,9 +2606,9 @@ void delete_type_macro(type_table_t *table, int32_t id) { mtbl = table->macro_tbl; - assert(mtbl != NULL && good_type_macro(mtbl, id)); + assert(mtbl != NULL); - macro = mtbl->data[id]; + macro = type_macro_def(mtbl, id); stbl_remove(&mtbl->stbl, macro->name); tuple_hmap_gc(&mtbl->cache, &id, keep_cached_tuple_alive); free_macro_id(mtbl, id); @@ -2689,9 +2644,6 @@ type_t instantiate_type_macro(type_table_t *table, int32_t id, uint32_t n, const type_t result; - // id is a good macro with arity n - assert(type_macro(table, id)->arity == n); - /* * By default, we use a buffer of 10 integers to store id + actuals * If more is needed, a larger array is allocated here. @@ -2708,7 +2660,7 @@ type_t instantiate_type_macro(type_table_t *table, int32_t id, uint32_t n, const mtbl = table->macro_tbl; assert(mtbl != NULL); - d = mtbl->data[id]; + d = type_macro_def(mtbl, id); assert(d->arity == n); if (d->body == NULL_TYPE) { // type constructor: new instance diff --git a/src/terms/types.h b/src/terms/types.h index 9e5c9e44a..661bae1c5 100644 --- a/src/terms/types.h +++ b/src/terms/types.h @@ -69,7 +69,6 @@ #include "utils/int_hash_tables.h" #include "utils/indexed_table.h" #include "utils/symbol_tables.h" -#include "utils/tagged_pointers.h" #include "utils/tuple_hash_map.h" #include "yices_types.h" @@ -201,6 +200,15 @@ typedef struct type_macro_s { */ #define TYPE_MACRO_MAX_ARITY 128 +/* + * The type of an element in the macro table. + */ +typedef struct type_mtbl_elem_s { + union { + indexed_table_elem_t elem; + type_macro_t *data; + }; +} type_mtbl_elem_t; /* * Table of macros @@ -208,22 +216,9 @@ typedef struct type_macro_s { * - the table maps the index to a macro descriptor * - it also includes a symbol table that maps a macro name * to its id, and a hash table that stores macro instances - * - deleted descriptors are stored in a free list. - * - * For an index id between 0 and table->nelems, - * table->data[id] is a tagged pointer. - * - if the lower bit is 0, then id is a live macro index, - * and table->data[id] is a pointer to the macro descriptor. - * - if the lower bit is 1, then id is the index of a deleted - * macro and table->data[id] stores a 31bit integer. This - * integer is the successor of id in the free list (or -1 - * if id is last in the free list). */ typedef struct type_mtbl_s { - void **data; // descriptors - uint32_t size; // size of the data array - uint32_t nelems; // number of descriptor/macros stored - int32_t free_idx; // first index in the free list (or -1) + indexed_table_t macros; stbl_t stbl; // symbol table tuple_hmap_t cache; // existing macro instances } type_mtbl_t; @@ -706,36 +701,38 @@ extern void delete_type_macro(type_table_t *table, int32_t id); */ extern type_t instantiate_type_macro(type_table_t *table, int32_t id, uint32_t n, const type_t *actual); +static inline type_macro_t *type_macro_unchecked(type_mtbl_t *table, + int32_t id) { + return indexed_table_elem(type_mtbl_elem_t, table->macros, id)->data; +} +static inline uint32_t type_macro_nelems(type_mtbl_t *table) { + return indexed_table_nelems(&table->macros); +} /* * Check that id is good */ static inline bool good_type_macro(type_mtbl_t *table, int32_t id) { - return 0 <= id && id < table->nelems && !has_int_tag(table->data[id]); + return 0 <= id && id < type_macro_nelems(table); } +static inline type_macro_t *type_macro_def(type_mtbl_t *table, int32_t id) { + assert(good_type_macro(table, id)); + return type_macro_unchecked(table, id); +} /* * Arity and name of macro */ static inline char *type_macro_name(type_mtbl_t *table, int32_t id) { - assert(good_type_macro(table, id)); - return ((type_macro_t *) table->data[id])->name; + return type_macro_def(table, id)->name; } static inline uint32_t type_macro_arity(type_mtbl_t *table, int32_t id) { - assert(good_type_macro(table, id)); - return ((type_macro_t *) table->data[id])->arity; + return type_macro_def(table, id)->arity; } -static inline type_macro_t *type_macro_def(type_mtbl_t *table, int32_t id) { - assert(good_type_macro(table, id)); - return table->data[id]; -} - - - /* diff --git a/src/utils/indexed_table.c b/src/utils/indexed_table.c index 8b7751a1e..3a3954a26 100644 --- a/src/utils/indexed_table.c +++ b/src/utils/indexed_table.c @@ -1,4 +1,5 @@ #include +#include #include "indexed_table.h" #include "memalloc.h" @@ -79,3 +80,19 @@ void indexed_table_clear(indexed_table_t *t) { t->free_idx = -1; t->live_elems = 0; } + +void indexed_table_for_each_free_elem(indexed_table_t *t, + indexed_table_elem_fn f, + void *data) { + index_t i, next; + + for (i = t->free_idx; i >= 0; i = next) { + indexed_table_elem_t *e = elem(t, i); + + /* Obtain the next index before calling F in case F mutates the + element. */ + next = e->next; + + f(e, data); + } +} diff --git a/src/utils/indexed_table.h b/src/utils/indexed_table.h index 33a5c05da..6c0be80e4 100644 --- a/src/utils/indexed_table.h +++ b/src/utils/indexed_table.h @@ -43,6 +43,9 @@ typedef struct indexed_table_elem_s { index_t next; } indexed_table_elem_t; +/* The type of a function called on elements of the table. */ +typedef void (*indexed_table_elem_fn)(indexed_table_elem_t *, void *); + /* * An index_table_t is an expandable array, with idices of type * index_t. @@ -114,4 +117,19 @@ static inline uindex_t indexed_table_live_elems(const indexed_table_t *t) { return t->live_elems; } +/* + * Return the Ith element in TABLE. TYPE is the true type of the + * elements in the table. The return value is a TYPE *. + */ +#define indexed_table_elem(type, table, i) \ + (&(((type *) (table).elems)[i])) + +/* + * For each element X on the free list, call F(X, DATA). F is + * permitted to muate the element. + */ +void indexed_table_for_each_free_elem(indexed_table_t *t, + indexed_table_elem_fn f, + void *data); + #endif /* !defined(__INDEXED_TABLE_H) */ From b6385aa21c4687e324272e4592a0f6632c39e098 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Wed, 22 Nov 2023 09:41:07 -0800 Subject: [PATCH 5/7] Clean up the pprod_table. --- src/terms/pprod_table.c | 131 ++++++++++++++++++++------------------ src/terms/pprod_table.h | 24 +++---- src/terms/terms.h | 4 +- src/terms/types.c | 3 +- src/terms/types.h | 4 +- src/utils/indexed_table.c | 22 +++---- src/utils/indexed_table.h | 6 +- 7 files changed, 98 insertions(+), 96 deletions(-) diff --git a/src/terms/pprod_table.c b/src/terms/pprod_table.c index e279231f9..1decb5c89 100644 --- a/src/terms/pprod_table.c +++ b/src/terms/pprod_table.c @@ -27,6 +27,16 @@ #include "utils/memalloc.h" +/* + * Extend the table. + */ +static void extend_pprod_table(indexed_table_t *t) { + uint32_t n = t->size; + pprod_table_t *pprods = (pprod_table_t *) t; + + pprods->mark = extend_bitvector(pprods->mark, n); +} + /* * Initialization: create an empty table. @@ -40,48 +50,51 @@ void init_pprod_table(pprod_table_t *table, uint32_t n) { out_of_memory(); } - table->data = (pprod_t **) safe_malloc(n * sizeof(pprod_t *)); + static const indexed_table_vtbl_t vtbl = { + .elem_size = sizeof(pprod_table_elem_t), + .extend = extend_pprod_table + }; + + indexed_table_init(&table->pprods, n, &vtbl); table->mark = allocate_bitvector(n); - table->size = n; - table->nelems = 0; - table->free_idx = -1; init_int_htbl(&table->htbl, 0); // default size init_pp_buffer(&table->buffer, 10); } +static inline uint32_t pprod_table_nelems(pprod_table_t *t) { + return indexed_table_nelems(&t->pprods); +} -/* - * Extend the table: make it 50% larger - */ -static void extend_pprod_table(pprod_table_t *table) { - uint32_t n; - - n = table->size + 1; - n += n >> 1; - if (n >= PPROD_TABLE_MAX_SIZE) { - out_of_memory(); - } +static inline pprod_table_elem_t *pprod_table_elem(pprod_table_t *t, + uint32_t i) { + return indexed_table_elem(pprod_table_elem_t, &t->pprods, i); +} - table->data = (pprod_t **) safe_realloc(table->data, n * sizeof(pprod_t *)); - table->mark = extend_bitvector(table->mark, n); - table->size = n; +static void clear_pprod(indexed_table_elem_t *elem, + index_t i, + void *data) { + ((pprod_table_elem_t *) elem)->pprod = NULL; } + /* - * Remove all products from table->data + * Remove all products. */ static void free_pprods(pprod_table_t *table) { pprod_t *p; uint32_t i, n; - n = table->nelems; + indexed_table_for_each_free_elem(&table->pprods, + clear_pprod, + /*data=*/NULL); + + n = pprod_table_nelems(table); for (i=0; idata[i]; - if (! has_int_tag(p)) { + p = pprod_table_elem(table, i)->pprod; + if (p) safe_free(p); - } } } @@ -90,8 +103,7 @@ static void free_pprods(pprod_table_t *table) { */ void reset_pprod_table(pprod_table_t *table) { free_pprods(table); - table->nelems = 0; - table->free_idx = -1; + indexed_table_clear(&table->pprods); reset_int_htbl(&table->htbl); pp_buffer_reset(&table->buffer); } @@ -102,9 +114,8 @@ void reset_pprod_table(pprod_table_t *table) { */ void delete_pprod_table(pprod_table_t *table) { free_pprods(table); - safe_free(table->data); + indexed_table_destroy(&table->pprods); delete_bitvector(table->mark); - table->data = NULL; table->mark = NULL; delete_int_htbl(&table->htbl); @@ -114,24 +125,15 @@ void delete_pprod_table(pprod_table_t *table) { /* - * Allocate an index i such that data[i] is empty + * Allocate an index i containing PPROD. * - clear mark[i] */ -static int32_t allocate_pprod_id(pprod_table_t *table) { +static int32_t allocate_pprod_id(pprod_table_t *table, + pprod_t *pprod) { int32_t i; - i = table->free_idx; - if (i >= 0) { - assert(i < table->nelems); - table->free_idx = untag_i32(table->data[i]); - } else { - i = table->nelems; - table->nelems ++; - if (i == table->size) { - extend_pprod_table(table); - } - assert(i < table->size); - } + i = indexed_table_alloc(&table->pprods); + pprod_table_elem(table, i)->pprod = pprod; clr_bit(table->mark, i); @@ -145,11 +147,10 @@ static int32_t allocate_pprod_id(pprod_table_t *table) { * - free prod[i] and add i to the free list */ static void erase_pprod_id(pprod_table_t *table, int32_t i) { - assert(0 <= i && i < table->nelems && !has_int_tag(table->data[i])); + assert(0 <= i && i < pprod_table_nelems(table)); - safe_free(table->data[i]); - table->data[i] = tag_i32(table->free_idx); - table->free_idx = i; + safe_free(pprod_table_elem(table, i)->pprod); + indexed_table_free(&table->pprods, i); } @@ -191,9 +192,9 @@ static bool eq_pprod(pprod_hobj_t *o, int32_t i) { uint32_t n; table = o->tbl; - assert(0 <= i && i < table->nelems && !has_int_tag(table->data[i])); + assert(0 <= i && i < pprod_table_nelems(table)); - p = table->data[i]; + p = pprod_table_elem(table, i)->pprod; n = o->len; return (n == p->len) && varexp_array_equal(o->array, p->prod, n); } @@ -207,8 +208,8 @@ static int32_t build_pprod(pprod_hobj_t *o) { int32_t i; table = o->tbl; - i = allocate_pprod_id(table); - table->data[i] = make_pprod(o->array, o->len); + i = allocate_pprod_id(table, + make_pprod(o->array, o->len)); return i; } @@ -234,7 +235,7 @@ static pprod_t *get_pprod(pprod_table_t *table, varexp_t *a, uint32_t n) { i = int_htbl_get_obj(&table->htbl, &pprod_hobj.m); - return table->data[i]; + return pprod_table_elem(table, i)->pprod; } @@ -337,7 +338,7 @@ void delete_pprod(pprod_table_t *table, pprod_t *p) { * we search the hash table again to delete the record (h, i). */ i = find_pprod_id(table, p); - assert(i >= 0 && table->data[i] == p); + assert(i >= 0 && pprod_table_elem(table, i)->pprod == p); // keep h = hash code of p h = hash_varexp_array(p->prod, p->len); @@ -360,10 +361,16 @@ void pprod_table_set_gc_mark(pprod_table_t *table, pprod_t *p) { int32_t i; i = find_pprod_id(table, p); - assert(i >= 0 && table->data[i] == p); + assert(i >= 0 && pprod_table_elem(table, i)->pprod == p); set_bit(table->mark, i); } +static void pprod_table_mark_free_elem(indexed_table_elem_t *t, + int32_t i, + void *data) { + pprod_table_t *table = (pprod_table_t *) data; + set_bit(table->mark, i); +} /* * Garbage collection: delete all unmarked products @@ -373,20 +380,22 @@ void pprod_table_gc(pprod_table_t *table) { pprod_t *p; uint32_t i, n, h; - n = table->nelems; + /* Mark all of the elements on the free list. */ + indexed_table_for_each_free_elem(&table->pprods, + pprod_table_mark_free_elem, + table); + + n = pprod_table_nelems(table); for (i=0; imark, i)) { // i is not marked - p = table->data[i]; - if (!has_int_tag(p)) { - // not already deleted - h = hash_varexp_array(p->prod, p->len); - erase_pprod_id(table, i); - int_htbl_erase_record(&table->htbl, h, i); - } + p = pprod_table_elem(table, i)->pprod; + h = hash_varexp_array(p->prod, p->len); + erase_pprod_id(table, i); + int_htbl_erase_record(&table->htbl, h, i); } } // clear all the marks - clear_bitvector(table->mark, table->size); + clear_bitvector(table->mark, table->pprods.size); } diff --git a/src/terms/pprod_table.h b/src/terms/pprod_table.h index b864248c3..6988bd5aa 100644 --- a/src/terms/pprod_table.h +++ b/src/terms/pprod_table.h @@ -27,34 +27,28 @@ #include "terms/power_products.h" #include "utils/bitvectors.h" +#include "utils/indexed_table.h" #include "utils/int_hash_tables.h" +typedef struct pprod_table_elem_s { + union { + indexed_table_elem_t elem; + pprod_t *pprod; + }; +} pprod_table_elem_t; /* - * For each i between 0 and nelems - 1, data[i] stores the - * power product of index i. - * - data[i] is valid if its tag bit is 0. - * Then data[i] is a pointer to a valid pprod_t structure of degree >= 2. - * There's a corresponding record (with index i) in the htbl. - * - data[i] is a deleted product if its tag bit is 1. - * In that case, data[i] encodes the next element in a global free list. + * - pprods stores the power products. * - mark[i] is used during garbage collection. * * Other components: - * - size = size of array data and bitvector mark - * - nelems = number of array elements used - * - free_idx = start of the free list (-1 means that the free list is empty) * - htbl = hash table for hash consing * - buffer = buffer for constructing power products */ typedef struct pprod_table_s { - pprod_t **data; + indexed_table_t pprods; byte_t *mark; - uint32_t size; - uint32_t nelems; - int32_t free_idx; - int_htbl_t htbl; pp_buffer_t buffer; } pprod_table_t; diff --git a/src/terms/terms.h b/src/terms/terms.h index 9880cacdd..aaaacdfed 100644 --- a/src/terms/terms.h +++ b/src/terms/terms.h @@ -1140,8 +1140,8 @@ static inline bool valid_term_idx(const term_table_t *table, int32_t i) { } static inline term_desc_t *term_desc(const term_table_t *table, - int32_t i) { - return &((term_desc_t *) table->terms.elems)[i]; + int32_t i) { + return indexed_table_elem(term_desc_t, &table->terms, i); } static inline term_kind_t unchecked_kind_for_idx(const term_table_t *table, diff --git a/src/terms/types.c b/src/terms/types.c index 4cd6c1abc..e2dd2e643 100644 --- a/src/terms/types.c +++ b/src/terms/types.c @@ -124,6 +124,7 @@ static void init_type_mtbl(type_mtbl_t *table, uint32_t n) { } static void type_mtbl_clear_elem(indexed_table_elem_t *elem, + index_t i, void *data) { ((type_mtbl_elem_t *) elem)->data = NULL; } @@ -174,7 +175,7 @@ static inline int32_t allocate_macro_id(type_mtbl_t *table, type_macro_t *d) { int32_t i = indexed_table_alloc(&table->macros); - indexed_table_elem(type_mtbl_elem_t, table->macros, i)->data = d; + indexed_table_elem(type_mtbl_elem_t, &table->macros, i)->data = d; return i; } diff --git a/src/terms/types.h b/src/terms/types.h index 661bae1c5..cfe97ccd0 100644 --- a/src/terms/types.h +++ b/src/terms/types.h @@ -449,7 +449,7 @@ extern void reset_type_table(type_table_t *table); */ static inline type_desc_t *type_desc(const type_table_t *table, int32_t i) { - return &((type_desc_t *) table->types.elems)[i]; + return indexed_table_elem(type_desc_t, &table->types, i); } static inline bool valid_type(type_table_t *tbl, type_t i) { @@ -703,7 +703,7 @@ extern type_t instantiate_type_macro(type_table_t *table, int32_t id, uint32_t n static inline type_macro_t *type_macro_unchecked(type_mtbl_t *table, int32_t id) { - return indexed_table_elem(type_mtbl_elem_t, table->macros, id)->data; + return indexed_table_elem(type_mtbl_elem_t, &table->macros, id)->data; } static inline uint32_t type_macro_nelems(type_mtbl_t *table) { diff --git a/src/utils/indexed_table.c b/src/utils/indexed_table.c index 3a3954a26..24669eeb0 100644 --- a/src/utils/indexed_table.c +++ b/src/utils/indexed_table.c @@ -5,15 +5,13 @@ #include "memalloc.h" #include "yices_limits.h" -#define MAX_ELEMS YICES_MAX_TYPES - -static inline void check_nelems(uindex_t n) { - if (n > MAX_ELEMS) - out_of_memory(); +static inline size_t elem_size(const indexed_table_t *t) { + return t->vtbl->elem_size; } -static inline size_t elem_size(indexed_table_t *t) { - return t->vtbl->elem_size; +static inline void check_nelems(const indexed_table_t *t) { + if (t->size > UINT32_MAX / elem_size(t)) + out_of_memory(); } static inline indexed_table_elem_t *elem(indexed_table_t *t, index_t i) { @@ -25,24 +23,22 @@ static void extend(indexed_table_t *t) { n = t->size + 1; n += n >> 1; - - check_nelems(n); + t->size = n; + check_nelems(t); t->elems = safe_realloc(t->elems, n * elem_size(t)); - t->size = n; t->vtbl->extend(t); } void indexed_table_init(indexed_table_t *t, uindex_t n, const indexed_table_vtbl_t *vtbl) { - check_nelems(n); - *t = (indexed_table_t) { .elems = safe_malloc(n * vtbl->elem_size), .size = n, .vtbl = vtbl }; + check_nelems(t); indexed_table_clear(t); } @@ -93,6 +89,6 @@ void indexed_table_for_each_free_elem(indexed_table_t *t, element. */ next = e->next; - f(e, data); + f(e, i, data); } } diff --git a/src/utils/indexed_table.h b/src/utils/indexed_table.h index 6c0be80e4..62860fa17 100644 --- a/src/utils/indexed_table.h +++ b/src/utils/indexed_table.h @@ -44,7 +44,9 @@ typedef struct indexed_table_elem_s { } indexed_table_elem_t; /* The type of a function called on elements of the table. */ -typedef void (*indexed_table_elem_fn)(indexed_table_elem_t *, void *); +typedef void (*indexed_table_elem_fn)(indexed_table_elem_t *, + index_t, + void *); /* * An index_table_t is an expandable array, with idices of type @@ -122,7 +124,7 @@ static inline uindex_t indexed_table_live_elems(const indexed_table_t *t) { * elements in the table. The return value is a TYPE *. */ #define indexed_table_elem(type, table, i) \ - (&(((type *) (table).elems)[i])) + (&(((type *) (table)->elems)[i])) /* * For each element X on the free list, call F(X, DATA). F is From f98e83d7ba92cb2a37cee042c04bbe12d3308720 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Sun, 26 Nov 2023 16:55:07 -0800 Subject: [PATCH 6/7] Used indexed_table. --- src/terms/bit_expr.c | 142 +++++++++++++++++-------------------------- src/terms/bit_expr.h | 49 ++++++++------- 2 files changed, 85 insertions(+), 106 deletions(-) diff --git a/src/terms/bit_expr.c b/src/terms/bit_expr.c index 85313395d..6594d4064 100644 --- a/src/terms/bit_expr.c +++ b/src/terms/bit_expr.c @@ -44,6 +44,17 @@ #include "utils/memalloc.h" +/* + * Extend table. + */ +static void extend_node_table(indexed_table_t *table) { + // abort if the new size is too large + if (table->size > MAX_NODE_TABLE_SIZE) { + out_of_memory(); + } +} + + /* * Initialize a node table (empty) * - n = initial size @@ -57,12 +68,12 @@ static void alloc_node_table(node_table_t *table, uint32_t n) { out_of_memory(); } - table->kind = (uint8_t *) safe_malloc(n * sizeof(uint8_t)); - table->desc = (node_desc_t *) safe_malloc(n * sizeof(node_desc_t)); - table->map = (int32_t *) safe_malloc(n * sizeof(int32_t)); - table->size = n; - table->nelems = 0; - table->free_idx = -1; + static const indexed_table_vtbl_t vtbl = { + .elem_size = sizeof(node_desc_t), + .extend = extend_node_table + }; + + indexed_table_init(&table->nodes, n, &vtbl); table->ref_counter = 0; @@ -71,47 +82,16 @@ static void alloc_node_table(node_table_t *table, uint32_t n) { } -/* - * Extend table: make it 50% larger - */ -static void extend_node_table(node_table_t *table) { - uint32_t n; - - n = table->size + 1; - n += n >> 1; - - // abort if the new size is too large - if (n > MAX_NODE_TABLE_SIZE) { - out_of_memory(); - } - - table->kind = (uint8_t *) safe_realloc(table->kind, n * sizeof(uint8_t)); - table->desc = (node_desc_t *) safe_realloc(table->desc, n * sizeof(node_desc_t)); - table->map = (int32_t *) safe_realloc(table->map, n * sizeof(int32_t)); - table->size = n; -} - - /* * Allocate a node id * - set map[i] to the default (i.e., -1) - * - kind and desc are not initialized */ -static node_t allocate_node_id(node_table_t *table) { - node_t i; +static node_t allocate_node_id(node_table_t *table, uint8_t kind) { + node_t i = indexed_table_alloc(&table->nodes); + node_desc_t *n = node_table_elem(table, i); - i = table->free_idx; - if (i >= 0) { - table->free_idx = table->desc[i].var; - } else { - i = table->nelems; - table->nelems ++; - if (i == table->size) { - extend_node_table(table); - } - } - assert(i < table->size); - table->map[i] = -1; + n->kind = kind; + n->map = -1; return i; } @@ -125,11 +105,11 @@ static node_t allocate_node_id(node_table_t *table) { static node_t build_constant_node(node_table_t *table) { node_t i; - i = allocate_node_id(table); + i = allocate_node_id(table, CONSTANT_NODE); assert(i == constant_node); - table->kind[i] = CONSTANT_NODE; - table->desc[i].c[0] = null_bit; - table->desc[i].c[1] = null_bit; + + bit_t *c = node_table_elem(table, i)->c; + c[0] = c[1] = null_bit; return i; } @@ -141,10 +121,9 @@ static node_t build_constant_node(node_table_t *table) { static node_t new_variable_node(node_table_t *table, int32_t x) { node_t i; - i = allocate_node_id(table); - table->kind[i] = VARIABLE_NODE; - table->desc[i].var = x; - + i = allocate_node_id(table, VARIABLE_NODE); + node_table_elem(table, i)->var = x; + return i; } @@ -155,10 +134,11 @@ static node_t new_variable_node(node_table_t *table, int32_t x) { static node_t new_select_node(node_table_t *table, uint32_t k, int32_t x) { node_t i; - i = allocate_node_id(table); - table->kind[i] = SELECT_NODE; - table->desc[i].sel.index = k; - table->desc[i].sel.var = x; + i = allocate_node_id(table, SELECT_NODE); + + select_node_t *s = &node_table_elem(table, i)->sel; + s->index = k; + s->var = x; return i; } @@ -173,10 +153,11 @@ static node_t new_binary_node(node_table_t *table, node_kind_t op, bit_t a, bit_ assert(op == OR_NODE || op == XOR_NODE); - i = allocate_node_id(table); - table->kind[i] = op; - table->desc[i].c[0] = a; - table->desc[i].c[1] = b; + i = allocate_node_id(table, op); + + bit_t *c = node_table_elem(table, i)->c; + c[0] = a; + c[1] = b; return i; } @@ -240,10 +221,9 @@ static uint32_t hash_var_node(var_node_hobj_t *p) { } static bool eq_var_node(var_node_hobj_t *p, node_t i) { - node_table_t *table; + node_desc_t *node = node_table_elem(p->tbl, i); - table = p->tbl; - return table->kind[i] == VARIABLE_NODE && table->desc[i].var == p->var; + return node->kind == VARIABLE_NODE && node->var == p->var; } static node_t build_var_node(var_node_hobj_t *p) { @@ -271,12 +251,11 @@ static uint32_t hash_select_node(select_node_hobj_t *p) { } static bool eq_select_node(select_node_hobj_t *p, node_t i) { - node_table_t *table; + node_desc_t *node = node_table_elem(p->tbl, i); - table = p->tbl; - return table->kind[i] == SELECT_NODE && - table->desc[i].sel.index == p->index && - table->desc[i].sel.var == p->var; + return node->kind == SELECT_NODE && + node->sel.index == p->index && + node->sel.var == p->var; } static node_t build_select_node(select_node_hobj_t *p) { @@ -304,12 +283,11 @@ static uint32_t hash_or_node(node_hobj_t *p) { } static bool eq_or_node(node_hobj_t *p, node_t i) { - node_table_t *table; + node_desc_t *node = node_table_elem(p->tbl, i); - table = p->tbl; - return table->kind[i] == OR_NODE && - table->desc[i].c[0] == p->child[0] && - table->desc[i].c[1] == p->child[1]; + return node->kind == OR_NODE && + node->c[0] == p->child[0] && + node->c[1] == p->child[1]; } static node_t build_or_node(node_hobj_t *p) { @@ -337,12 +315,11 @@ static uint32_t hash_xor_node(node_hobj_t *p) { } static bool eq_xor_node(node_hobj_t *p, node_t i) { - node_table_t *table; + node_desc_t *node = node_table_elem(p->tbl, i); - table = p->tbl; - return table->kind[i] == XOR_NODE && - table->desc[i].c[0] == p->child[0] && - table->desc[i].c[1] == p->child[1]; + return node->kind == XOR_NODE && + node->c[0] == p->child[0] && + node->c[1] == p->child[1]; } static node_t build_xor_node(node_hobj_t *p) { @@ -382,14 +359,9 @@ void init_node_table(node_table_t *table, uint32_t n) { * Delete all nodes and the table */ void delete_node_table(node_table_t *table) { - safe_free(table->kind); - safe_free(table->desc); - safe_free(table->map); - table->kind = NULL; - table->desc = NULL; - table->map = NULL; delete_ivector(&table->aux_buffer); delete_int_htbl(&table->htbl); + indexed_table_destroy(&table->nodes); } @@ -399,9 +371,9 @@ void delete_node_table(node_table_t *table) { void reset_node_table(node_table_t *table) { assert(table->ref_counter == 0); - table->free_idx = -1; - table->nelems = 1; // keep the constant node - assert(table->kind[0] == CONSTANT_NODE); + indexed_table_clear(&table->nodes); + table->nodes.nelems = 1; // keep the constant node + assert(node_table_elem(table, 0)->kind == CONSTANT_NODE); ivector_reset(&table->aux_buffer); reset_int_htbl(&table->htbl); diff --git a/src/terms/bit_expr.h b/src/terms/bit_expr.h index 83b53bf78..69884e69b 100644 --- a/src/terms/bit_expr.h +++ b/src/terms/bit_expr.h @@ -46,6 +46,7 @@ #include #include +#include "utils/indexed_table.h" #include "utils/int_hash_tables.h" #include "utils/int_vectors.h" @@ -167,10 +168,15 @@ typedef struct select_node_s { int32_t var; } select_node_t; -typedef union node_desc_u { - int32_t var; - select_node_t sel; - bit_t c[2]; +typedef struct node_desc_s { + union { + indexed_table_elem_t elem; + int32_t var; + select_node_t sel; + bit_t c[2]; + }; + int32_t map; + uint8_t kind; } node_desc_t; @@ -199,12 +205,7 @@ typedef union node_desc_u { * - when the counter is zero we reset the whole table */ typedef struct node_table_s { - uint8_t *kind; - node_desc_t *desc; - int32_t *map; - uint32_t size; - uint32_t nelems; - int32_t free_idx; + indexed_table_t nodes; uint32_t ref_counter; @@ -243,7 +244,9 @@ extern void delete_node_table(node_table_t *table); */ extern void reset_node_table(node_table_t *table); - +static inline uint32_t node_table_nelems(const node_table_t *table) { + return indexed_table_nelems(&table->nodes); +} /* @@ -362,16 +365,20 @@ static inline void node_table_clear_refcount(node_table_t *table) { * ACCESS TO THE TABLE */ static inline bool valid_node(node_table_t *table, node_t x) { - return 0 <= x && x < table->nelems; + return 0 <= x && x < node_table_nelems(table); +} + +static inline node_desc_t *node_table_elem(node_table_t *table, node_t x) { + return indexed_table_elem(node_desc_t, &table->nodes, x); } static inline node_kind_t node_kind(node_table_t *table, node_t x) { assert(valid_node(table, x)); - return table->kind[x]; + return node_table_elem(table, x)->kind; } static inline bool good_node(node_table_t *table, node_t x) { - return valid_node(table, x) && table->kind[x] != UNUSED_NODE; + return valid_node(table, x) && node_kind(table, x) != UNUSED_NODE; } static inline bool is_constant_node(node_table_t *table, node_t x) { @@ -414,12 +421,12 @@ static inline bool is_nonleaf_node(node_table_t *table, node_t x) { */ static inline int32_t map_of_node(node_table_t *table, node_t x) { assert(good_node(table, x)); - return table->map[x]; + return node_table_elem(table, x)->map; } static inline void set_map_of_node(node_table_t *table, node_t x, int32_t v) { assert(good_node(table, x)); - table->map[x] = v; + node_table_elem(table, x)->map = v; } @@ -429,7 +436,7 @@ static inline void set_map_of_node(node_table_t *table, node_t x, int32_t v) { */ static inline int32_t var_of_node(node_table_t *table, node_t x) { assert(is_variable_node(table, x)); - return table->desc[x].var; + return node_table_elem(table, x)->var; } @@ -438,7 +445,7 @@ static inline int32_t var_of_node(node_table_t *table, node_t x) { */ static inline select_node_t *select_of_node(node_table_t *table, node_t x) { assert(is_select_node(table, x)); - return &table->desc[x].sel; + return &node_table_elem(table, x)->sel; } static inline int32_t var_of_select_node(node_table_t *table, node_t x) { @@ -457,13 +464,13 @@ static inline uint32_t index_of_select_node(node_table_t *table, node_t x) { */ static inline bit_t *children_of_node(node_table_t *table, node_t x) { assert(is_nonleaf_node(table, x)); - return table->desc[x].c; + return node_table_elem(table, x)->c; } // child 0 or 1 static inline bit_t child_of_node(node_table_t *table, node_t x, uint32_t k) { - assert(is_nonleaf_node(table, x) && k < 2); - return table->desc[x].c[k]; + assert(k < 2); + return children_of_node(table, x)[k]; } // left child = child 0, right child = child 1 From 8a46390987f98c052bdeedbdff7a5a496e6a3d79 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Wed, 29 Nov 2023 17:00:39 -0600 Subject: [PATCH 7/7] Centralize check for maximum number of elements. --- src/terms/bit_expr.c | 18 ++---------------- src/terms/pprod_table.c | 8 ++------ src/terms/terms.c | 16 ++-------------- src/terms/types.c | 20 ++------------------ src/utils/indexed_table.c | 5 +++-- src/utils/indexed_table.h | 3 +++ 6 files changed, 14 insertions(+), 56 deletions(-) diff --git a/src/terms/bit_expr.c b/src/terms/bit_expr.c index 6594d4064..fd32816ca 100644 --- a/src/terms/bit_expr.c +++ b/src/terms/bit_expr.c @@ -44,17 +44,6 @@ #include "utils/memalloc.h" -/* - * Extend table. - */ -static void extend_node_table(indexed_table_t *table) { - // abort if the new size is too large - if (table->size > MAX_NODE_TABLE_SIZE) { - out_of_memory(); - } -} - - /* * Initialize a node table (empty) * - n = initial size @@ -64,13 +53,10 @@ static void alloc_node_table(node_table_t *table, uint32_t n) { n = DEF_NODE_TABLE_SIZE; } - if (n > MAX_NODE_TABLE_SIZE) { - out_of_memory(); - } - static const indexed_table_vtbl_t vtbl = { .elem_size = sizeof(node_desc_t), - .extend = extend_node_table + .max_elems = MAX_NODE_TABLE_SIZE, + .extend = NULL }; indexed_table_init(&table->nodes, n, &vtbl); diff --git a/src/terms/pprod_table.c b/src/terms/pprod_table.c index 1decb5c89..b203487a3 100644 --- a/src/terms/pprod_table.c +++ b/src/terms/pprod_table.c @@ -31,10 +31,8 @@ * Extend the table. */ static void extend_pprod_table(indexed_table_t *t) { - uint32_t n = t->size; pprod_table_t *pprods = (pprod_table_t *) t; - - pprods->mark = extend_bitvector(pprods->mark, n); + pprods->mark = extend_bitvector(pprods->mark, t->size); } @@ -46,12 +44,10 @@ void init_pprod_table(pprod_table_t *table, uint32_t n) { if (n == 0) { n = PPROD_TABLE_DEF_SIZE; } - if (n >= PPROD_TABLE_MAX_SIZE) { - out_of_memory(); - } static const indexed_table_vtbl_t vtbl = { .elem_size = sizeof(pprod_table_elem_t), + .max_elems = PPROD_TABLE_MAX_SIZE, .extend = extend_pprod_table }; diff --git a/src/terms/terms.c b/src/terms/terms.c index b62a66f13..6f6bfae8f 100644 --- a/src/terms/terms.c +++ b/src/terms/terms.c @@ -119,16 +119,8 @@ static void default_special_finalizer(special_term_t *s, term_kind_t tag) { * Callback for indexed_table::extend. */ static void term_table_extend(indexed_table_t *t) { - uint32_t n = t->size; - - // force abort if n is too large - if (n > YICES_MAX_TERMS) { - out_of_memory(); - } - term_table_t *terms = (term_table_t *)t; - - terms->mark = extend_bitvector(terms->mark, n); + terms->mark = extend_bitvector(terms->mark, t->size); } @@ -138,16 +130,12 @@ static void term_table_extend(indexed_table_t *t) { * - ptbl = attached power-product table. */ static void term_table_init(term_table_t *table, uint32_t n, type_table_t *ttbl, pprod_table_t *ptbl) { - // abort if n is too large - if (n > YICES_MAX_TERMS) { - out_of_memory(); - } - /* The indexed_table_elem_t must be first. */ assert(offsetof(term_desc_t, elem) == 0); static const indexed_table_vtbl_t vtbl = { .elem_size = sizeof(term_desc_t), + .max_elems = YICES_MAX_TERMS, .extend = term_table_extend }; diff --git a/src/terms/types.c b/src/terms/types.c index e2dd2e643..7b1ce9ef7 100644 --- a/src/terms/types.c +++ b/src/terms/types.c @@ -91,12 +91,6 @@ static inline void delete_descriptor(type_macro_t *d) { } -static void type_mtbl_extend(indexed_table_t *table) { - if (table->nelems > TYPE_MACRO_MAX_SIZE) - out_of_memory(); -} - - /* * Initialize the macro table * - n = initial size @@ -106,13 +100,9 @@ static void type_mtbl_extend(indexed_table_t *table) { * on the first addition. */ static void init_type_mtbl(type_mtbl_t *table, uint32_t n) { - if (n > TYPE_MACRO_MAX_SIZE) { - out_of_memory(); - } - static const indexed_table_vtbl_t vtbl = { .elem_size = sizeof(type_mtbl_elem_t), - .extend = type_mtbl_extend + .max_elems = TYPE_MACRO_MAX_SIZE, }; indexed_table_init(&table->macros, n, &vtbl); @@ -207,12 +197,6 @@ static void typename_finalizer(stbl_rec_t *r) { string_decref(r->string); } -static void type_table_exend(indexed_table_t *t) { - if (t->nelems > YICES_MAX_TYPES) { - out_of_memory(); - } -} - /* * Initialize table, with initial size = n. */ @@ -227,7 +211,7 @@ static void type_table_init(type_table_t *table, uint32_t n) { static const indexed_table_vtbl_t vtbl = { .elem_size = sizeof(type_desc_t), - .extend = type_table_exend + .max_elems = YICES_MAX_TYPES, }; indexed_table_init(&table->types, n, &vtbl); diff --git a/src/utils/indexed_table.c b/src/utils/indexed_table.c index 24669eeb0..24dc3300d 100644 --- a/src/utils/indexed_table.c +++ b/src/utils/indexed_table.c @@ -10,7 +10,7 @@ static inline size_t elem_size(const indexed_table_t *t) { } static inline void check_nelems(const indexed_table_t *t) { - if (t->size > UINT32_MAX / elem_size(t)) + if (t->size > t->vtbl->max_elems) out_of_memory(); } @@ -28,7 +28,8 @@ static void extend(indexed_table_t *t) { t->elems = safe_realloc(t->elems, n * elem_size(t)); - t->vtbl->extend(t); + if (t->vtbl->extend) + t->vtbl->extend(t); } void indexed_table_init(indexed_table_t *t, uindex_t n, diff --git a/src/utils/indexed_table.h b/src/utils/indexed_table.h index 62860fa17..994949a6a 100644 --- a/src/utils/indexed_table.h +++ b/src/utils/indexed_table.h @@ -34,6 +34,9 @@ typedef struct indexed_table_vtbl_s { /* The size of an individual element. */ size_t elem_size; + /* The maximum number of elements permitted in the table. */ + uindex_t max_elems; + /* Called after extending the table. */ void (*extend)(indexed_table_t *t); } indexed_table_vtbl_t;