Missing function: yices_model_set_bv_from_array

Author: BrunoDutertre

src/api/yices_api.c

@@ -10070,11 +10070,47 @@ int32_t _o_yices_model_set_bv_mpz(model_t *model, term_t var, mpz_t val) {
   }
 
   yices_model_set_bvconstant(model, var, &bv0);
+
   return 0;
 }
 
 
 
+/*
+ * 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
+ */
+EXPORTED int32_t yices_model_set_bv_from_array(model_t *model, term_t var, uint32_t n, const int32_t a[]) {
+  MT_PROTECT(int32_t, __yices_globals.lock, _o_yices_model_set_bv_from_array(model, var, n, a));
+}
+
+int32_t _o_yices_model_set_bv_from_array(model_t *model, term_t var, uint32_t n, const int32_t a[]) {
+  uint32_t nbits;
+
+  nbits = check_var_and_get_bitsize(model, var);
+  if (nbits == 0) return -1;
+
+  if (n != nbits) {
+    // could also report EMPTY_BITVECTOR if n == 0
+    set_error_code(INCOMPATIBLE_BVSIZES);
+    return -1;
+  }
+
+  bvconstant_set_bitsize(&bv0, n);
+  bvconst_set_array(bv0.data, a, n);
+  yices_model_set_bvconstant(model, var, &bv0);
+
+  return 0;
+}
+
 
 /*
  * Export the list of uninterpreted terms that have a value in mdl.

src/api/yices_api_lock_free.h

@@ -629,6 +629,7 @@ extern int32_t _o_yices_model_set_bv_uint64(model_t *model, term_t var, uint64_t
 
 extern int32_t _o_yices_model_set_bv_mpz(model_t *model, term_t var, mpz_t val);
 
+extern int32_t _o_yices_model_set_bv_from_array(model_t *model, term_t var, uint32_t n, const int32_t a[]);
 
 /************************
  *  VALUES IN A MODEL   *

src/include/yices_types.h

@@ -530,9 +530,9 @@ typedef enum error_code {
  *  TYPE_MISMATCH              term1, type1
  *  INCOMPATIBLE_TYPES         term1, type1, term2, type2
  *  DUPLICATE_VARIABLE         term1
- *  INCOMPATIBLE_BVSIZES       term1, type1, term2, type2
+ *  INCOMPATIBLE_BVSIZES       none
  *  EMPTY_BITVECTOR            none
- *  ARITHCONSTANT_REQUIRED    term1
+ *  ARITHCONSTANT_REQUIRED     term1
  *  INVALID_MACRO              badval
  *  TOO_MANY_MACRO_PARAMS      badval
  *  TYPE_VAR_REQUIRED          type1

src/terms/bv_constants.h

@@ -133,6 +133,7 @@ extern void bvconstant_set_all_one(bvconstant_t *b, uint32_t n);
  */
 extern void bvconstant_copy(bvconstant_t *b, uint32_t n, const uint32_t *a);
 
+
 /*
  * Variant: initialize with a 64bit constant a, and normalize.
  * - n = number of bits