From 3e61b88f15cf6602e51ccbb9e61f117e4fb2f2c1 Mon Sep 17 00:00:00 2001
From: Bruno Dutertre <dutebrun@amazon.com>
Date: Sat, 9 Oct 2021 10:41:04 -0700
Subject: [PATCH] Missing function: yices_model_set_bv_from_array

---
 src/api/yices_api.c           | 36 +++++++++++++++++++++++++++++++++++
 src/api/yices_api_lock_free.h |  1 +
 src/include/yices_types.h     |  4 ++--
 src/terms/bv_constants.h      |  1 +
 4 files changed, 40 insertions(+), 2 deletions(-)

diff --git a/src/api/yices_api.c b/src/api/yices_api.c
index edbe59233..940e25a95 100644
--- a/src/api/yices_api.c
+++ b/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.
diff --git a/src/api/yices_api_lock_free.h b/src/api/yices_api_lock_free.h
index 4bb8333f6..4261354a4 100644
--- a/src/api/yices_api_lock_free.h
+++ b/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   *
diff --git a/src/include/yices_types.h b/src/include/yices_types.h
index 535bae0c3..dfd28cb79 100644
--- a/src/include/yices_types.h
+++ b/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
diff --git a/src/terms/bv_constants.h b/src/terms/bv_constants.h
index 6fb4bdf9f..40466d46a 100644
--- a/src/terms/bv_constants.h
+++ b/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