fix unit tests (#525)

* Update action.yml

* fix unit tests

* status_interrupted -> yices_status_interrupted

.github/actions/test/action.yml

@@ -14,3 +14,4 @@ runs:
         export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH}
         make MODE=${{ inputs.mode }} check
         make MODE=${{ inputs.mode }} check-api
+        make MODE=${{ inputs.mode }} test

doc/manual/manual.tex

@@ -4550,7 +4550,7 @@ \subsection*{Building a Context and Checking Satisfiability}
 
  case STATUS_IDLE:
  case STATUS_SEARCHING:
- case STATUS_INTERRUPTED:
+ case YICES_STATUS_INTERRUPTED:
  case STATUS_ERROR:
    fprintf(stderr, "Error in check_context\n");
    yices_print_error(stderr);

doc/sphinx/source/_static/example1.c

@@ -127,7 +127,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

doc/sphinx/source/_static/example1b.c

@@ -135,7 +135,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

doc/sphinx/source/api-types.rst

@@ -426,7 +426,7 @@ Contexts
        STATUS_UNKNOWN,
        STATUS_SAT,
        STATUS_UNSAT,
-       STATUS_INTERRUPTED,
+       YICES_STATUS_INTERRUPTED,
        STATUS_ERROR
      } smt_status_t;
 
@@ -470,13 +470,13 @@ Contexts
       asserted (if the inconsistency is detected by formula
       simplification), or when the search terminates.
 
-   .. c:enum:: STATUS_INTERRUPTED
+   .. c:enum:: YICES_STATUS_INTERRUPTED
 
       State entered when the search is interrupted.
 
       When a context is in the state :c:enum:`STATUS_SEARCHING` then the search
       can be interrupted through a call to :c:func:`yices_stop_search`. This
-      moves the context's state to :c:enum:`STATUS_INTERRUPTED`.
+      moves the context's state to :c:enum:`YICES_STATUS_INTERRUPTED`.
 
    .. c:enum:: STATUS_ERROR
 

doc/sphinx/source/basic-usage.rst

@@ -154,7 +154,7 @@ context, assert ``f`` in this context, then call function :c:func:`yices_check_c
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

doc/sphinx/source/context-operations.rst

@@ -550,7 +550,7 @@ assert formulas, check satisfiability, and query the context's status.
      These are the states after a search completes. :c:enum:`STATUS_UNKNOWN` means
      that the search was inconclusive, which may happen if the solver is not complete.
 
-   - :c:enum:`STATUS_INTERRUPTED`.
+   - :c:enum:`YICES_STATUS_INTERRUPTED`.
 
      This state is entered if a search is interrupted.
 
@@ -596,7 +596,7 @@ assert formulas, check satisfiability, and query the context's status.
 
      -- type1 := bool
 
-   - if *ctx*'s state is :c:enum:`STATUS_INTERRUPTED`
+   - if *ctx*'s state is :c:enum:`YICES_STATUS_INTERRUPTED`
 
      -- error code: :c:enum:`CTX_INVALID_OPERATION`
 
@@ -667,13 +667,13 @@ assert formulas, check satisfiability, and query the context's status.
      - :c:enum:`STATUS_UNKNOWN`: the solver can't prove whether the context is
        satisfiable or not.
 
-     - :c:enum:`STATUS_INTERRUPTED`: the search was interrupted by a
+     - :c:enum:`YICES_STATUS_INTERRUPTED`: the search was interrupted by a
        call to :c:func:`yices_stop_search`.
 
      This returned value is also stored as the context's status flag, with the following exception:
 
      - If the context is configured for mode *interactive* and the search is interrupted,
-       then the function returns :c:enum:`STATUS_INTERRUPTED` but the context's state is
+       then the function returns :c:enum:`YICES_STATUS_INTERRUPTED` but the context's state is
        restored to what it was before the call to :c:func:`yices_check_context`, and the
        internal status flag is reset to  :c:enum:`STATUS_IDLE`.
 
@@ -698,7 +698,7 @@ assert formulas, check satisfiability, and query the context's status.
 
    .. note:: If the search is interrupted and the context's mode is
              not *interactive* then the context's enters state
-             :c:enum:`STATUS_INTERRUPTED`. The only way to recover is
+             :c:enum:`YICES_STATUS_INTERRUPTED`. The only way to recover is
              then to call :c:func:`yices_reset_context` or
              :c:func:`yices_pop` (assuming the context supports push and pop).
 
@@ -782,7 +782,7 @@ be removed by :c:func:`yices_pop`.
      -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED`
 
    - if *ctx* supports push and pop but its status is :c:enum:`STATUS_UNSAT`,
-     :c:enum:`STATUS_SEARCHING`, or :c:enum:`STATUS_INTERRUPTED`:
+     :c:enum:`STATUS_SEARCHING`, or :c:enum:`YCIES_STATUS_INTERRUPTED`:
 
      -- error code: :c:enum:`CTX_INVALID_OPERATION`
 

examples/example1.c

@@ -145,7 +145,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

examples/example1b.c

@@ -157,7 +157,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

examples/example1c.c

@@ -150,7 +150,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error_fd(2);

examples/example2.c

@@ -104,7 +104,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

examples/example2b.c

@@ -124,7 +124,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

examples/example2c.c

@@ -124,7 +124,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

examples/example2d.c

@@ -117,7 +117,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

examples/example2e.c

@@ -117,7 +117,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

examples/example_unsat_core.c

@@ -109,7 +109,7 @@ static void check_and_get_core(context_t *ctx, uint32_t n, const term_t *a) {
     yices_delete_term_vector(&core);
     break;
 
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     printf("the check was interrupted\n");
     break;
 

tests/unit/test_core3.c

@@ -168,7 +168,7 @@ static void sat_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *redu
   uint32_t r_threshold;
   literal_t l;
 
-  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
+  assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);
 
   max_conflicts = num_conflicts(core) + conflict_bound;
   r_threshold = *reduce_threshold;

tests/unit/test_dl_profiler.c

@@ -196,7 +196,7 @@ static int32_t test_dl_profiling(smt_benchmark_t *bench) {
     print_internalization_code(code);
   }
 
-  printf("term table: %"PRIu32" elements\n", context.terms->nelems);
+  printf("term table: %"PRIu32" elements\n", nterms(context.terms));
 
   profile = context.dl_profile;
   if (profile != NULL) {

tests/unit/test_int_queues.c

@@ -27,7 +27,7 @@ static void print_queue(int_queue_t *q) {
   uint32_t i;
 
   printf("queue %p\n", q);
-  printf("  size = %"PRIu32"\n", q->size);
+  printf("  size = %"PRIu32"\n", q->capacity);
   printf("  head = %"PRIu32"\n", q->head);
   printf("  tail = %"PRIu32"\n", q->tail);
   printf("  content:");
@@ -37,7 +37,7 @@ static void print_queue(int_queue_t *q) {
     }
     printf("\n");
   } else if (q->tail < q->head) {
-    for (i=q->head; i<q->size; i++) {
+    for (i=q->head; i<q->capacity; i++) {
       printf(" %"PRId32, q->data[i]);
     }
     for (i=0; i<q->tail; i++) {
@@ -53,7 +53,7 @@ static void print_queue_data(int_queue_t *q) {
   uint32_t i;
   printf("head = %"PRIu32", tail = %"PRIu32"\n", q->head, q->tail);
   printf("data:");
-  for (i=0; i<q->size; i++) printf(" %"PRId32, q->data[i]);
+  for (i=0; i<q->capacity; i++) printf(" %"PRId32, q->data[i]);
   printf("\n");
 }
 

tests/unit/test_pprod_table.c

@@ -25,6 +25,7 @@
 #include <inttypes.h>
 
 #include "terms/pprod_table.h"
+#include "terms/terms.h"
 
 
 /*
@@ -77,25 +78,25 @@ static void print_pprod_table(FILE *f, pprod_table_t *table) {
   int32_t l;
 
   fprintf(f, "pprod_table %p\n", table);
-  fprintf(f, "  size = %"PRIu32"\n", table->size);
-  fprintf(f, "  nelems = %"PRIu32"\n", table->nelems);
-  fprintf(f, "  free_idx = %"PRId32"\n", table->free_idx);
+  fprintf(f, "  size = %"PRIu32"\n", table->pprods.size);
+  fprintf(f, "  nelems = %"PRIu32"\n", indexed_table_nelems(&table->pprods));
+  fprintf(f, "  free_idx = %"PRId32"\n", table->pprods.free_idx);
   fprintf(f, "  content:\n");
-  n = table->nelems;
+  n = indexed_table_nelems(&table->pprods);
   for (i=0; i<n; i++) {
-    p = table->data[i];
+    p = indexed_table_elem(pprod_table_elem_t, &table->pprods, i)->pprod;
     if (!has_int_tag(p)) {
       fprintf(f, "  data[%"PRIu32"] = ", i);
       print_varexp_array(f, p->prod, p->len);
       fprintf(f, "\n");
     }
   }
-  if (table->free_idx >= 0) {
+  if (table->pprods.free_idx >= 0) {
     fprintf(f, "  free list:");
-    l = table->free_idx;
+    l = table->pprods.free_idx;
     do {
       fprintf(f, " %"PRId32, l);
-      l = untag_i32(table->data[l]);
+      l = untag_i32(indexed_table_elem(pprod_table_elem_t, &table->pprods, l)->pprod);
     } while (l >= 0);
     fprintf(f, "\n");
   }

tests/unit/test_smt_blaster.c

@@ -373,7 +373,7 @@ int main(int argc, char *argv[]) {
   code = parse_smt_benchmark(&parser, &bench);
   if (code == 0) {
     printf("No syntax error found\n");
-    printf("term table: %"PRIu32" elements\n", __yices_globals.terms->nelems);
+    printf("term table: %"PRIu32" elements\n", nterms(__yices_globals.terms));
     fflush(stdout);
   } else {
     exit(YICES_EXIT_SYNTAX_ERROR);

tests/unit/test_smt_internalizer.c

@@ -528,7 +528,7 @@ int main(int argc, char *argv[]) {
   code = parse_smt_benchmark(&parser, &bench);
   if (code == 0) {
     printf("No syntax error found\n");
-    printf("term table: %"PRIu32" elements\n", __yices_globals.terms->nelems);
+    printf("term table: %"PRIu32" elements\n", nterms(__yices_globals.terms));
   } else {
     exit(YICES_EXIT_SYNTAX_ERROR);
   }