Vectors

Several functions in the API return a set of terms, types, or value descriptors in a vector object. The vector structures are defined in yices_types.h and explained in API Types.

Before calling a function that fills in a vector v, the vector must be initialized. When the vector is no longer used, it must be deleted to avoid memory leaks. It is also possible to empty the vector using a reset function.

The following code fragment illustrates the typical use pattern for a term vector. The pattern is the same for the other types of vectors:

term_vector_t v;

// initialize v
yices_init_term_vector(&v);

// call a function that fills in vector v
yices_implicant_for_formula(mdl, t, &v);

// the number of elements returned is v.size
// the elements themselves are stored in v.data[0 ... v.size-1]
// so we can scan them like this
for (i=0; i<v.size; i++) {
   // do something with v.data[i]
}

// delete v
yices_delete_term_vector(&v);

Note

Unlike the data structures that are internal to Yices (e.g., contexts and models), a vector v is not freed by a call to yices_exit or yices_reset.

The operations for initializing, deleting, and resetting vectors are listed in the next sections.

Type Vectors

void yices_init_type_vector(type_vector_t *v)

Initialize type vector v. This allocates an array v->data with a default capacity and sets v->size to 0.

void yices_reset_type_vector(type_vector_t *v)

Reset type vector v. This sets v->size to 0.

void yices_delete_type_vector(type_vector_t *v)

Delete type vector v. This frees array v->data.

Term Vectors

void yices_init_term_vector(term_vector_t *v)

Initialize term vector v. This allocates an array v->data with a default capacity and sets v->size to 0.

void yices_reset_term_vector(term_vector_t *v)

Reset term vector v. This sets v->size to 0.

void yices_delete_term_vector(term_vector_t *v)

Delete term vector v. This frees array v->data.

Vectors of Node Descriptors

void yices_init_yval_vector(yval_vector_t *v)

Initialize vector v. This allocates an array v->data with a default capacity and sets v->size to 0.

void yices_reset_yval_vector(yval_vector_t *v)

Reset vector v. This sets v->size to 0.

void yices_delete_yval_vector(yval_vector_t *v)

Delete vector v. This frees array v->data.