SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Missing API implementation. #386

Closed ianamason closed 2 years ago

ianamason commented 2 years ago

The api has:

/*
 * Assign a bitvector variable using an array of bits.
 * - var = bitvector variable
 * - a = array of n bits
 * - var must be an uninterpreted term of type (bitvector n)
 *   (and var must not have a value in model).
 *
 * Elements of a are interpreted as in yices_bvconst_from_array:
 * - bit i is 0 if a[i] == 0 and bit i is 1 if a[i] != 0
 * - a[0] is the low-order bit
 * - a[n-1] is the high-order bit
 *
 *
 * Since 2.6.4.
 */
__YICES_DLLSPEC__ extern int32_t yices_model_set_bv_from_array(model_t *model, term_t var, uint32_t n, const int32_t a[]);

But alas I cannot find it anywhere in yices_api.c and neither can the linker.

BrunoDutertre commented 2 years ago

I probably wrote this. I'll add the implementation.

ianamason commented 2 years ago

Closed in 3e61b88f15cf6602e51ccbb9e61f117e4fb2f2c1 Thanks @BrunoDutertre