Merge pull request #480 from markpmitchell/ds-cleanup

Centralize extendable array logic

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 \

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)).
        */
@@ -12342,15 +12342,15 @@ 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) {
   MT_PROTECT(uint32_t,  __yices_globals.lock, _o_yices_num_types());
 }
 
 uint32_t _o_yices_num_types(void) {
-  return __yices_globals.types->live_types;
+  return live_types(__yices_globals.types);
 }
 
 

src/include/yices_limits.h

@@ -32,7 +32,7 @@
 #include <stdint.h>
 
 /*
- * 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)