boolector: Add support for const arrays.

This commit adds boolector_const_array to create arrays that are
initialized by a given (constant or symbolic) value. Also adds the resp.
bits to the Python API.

src/api/python/btorapi.pxd

@@ -183,6 +183,13 @@ cdef extern from "boolector.h":
         Btor * btor, BoolectorSort  sort, const char *symbol) \
       except +raise_py_error
 
+    BoolectorNode *boolector_const_array (
+        Btor * btor,
+        BoolectorSort  sort,
+        BoolectorNode * value,
+        const char *symbol) \
+      except +raise_py_error
+
     BoolectorNode *boolector_not (
         Btor * btor, BoolectorNode * node) \
       except +raise_py_error

src/api/python/pyboolector.pyx

@@ -1352,6 +1352,49 @@ cdef class Boolector:
                                             _ChPtr(symbol)._c_str)
         return r
 
+    def ConstArray(self, BoolectorSort sort, BoolectorNode value,
+                   str symbol = None):
+        """ ConstArray(sort, value, symbol = None)
+
+            Create a one-dimensional bit-vector array with sort ``sort``
+            initialized with value ``value``.
+
+            An array variable's symbol is used as a simple means of
+            identfication, either when printing a model via
+            :func:`~pyboolector.Boolector.Print_model`,
+            or generating file dumps via
+            :func:`~pyboolector.Boolector.Dump`.
+            A symbol must be unique but may be None in case that no
+            symbol should be assigned.
+
+            :param btor: Boolector instance.
+            :param sort: Array sort which maps bit-vectors to bit-vectors.
+            :param value: Value to initialize array.
+            :param symbol: Name of array variable.
+            :return: Bit-vector array of sort ``sort`` and with symbol ``symbol``.
+
+            .. note::
+                In contrast to composite expressions, which are
+                maintained uniquely w.r.t. to their kind, inputs (and
+                consequently, bit width), array variables are not.
+                Hence, each call to this function returns a fresh bit vector
+                array variable.
+
+            .. seealso::
+              boolector_array
+
+        """
+        if not isinstance(sort, _BoolectorArraySort):
+            raise BoolectorException(
+                    "Sort must be of sort '_BoolectorArraySort'")
+        r = BoolectorArrayNode(self)
+        r._sort = sort
+        r._c_node = btorapi.boolector_const_array(self._c_btor,
+                                                  sort._c_sort,
+                                                  value._c_node,
+                                                  _ChPtr(symbol)._c_str)
+        return r
+
     def UF(self, BoolectorSort sort, str symbol = None):
         """ UF(sort, symbol)
 

src/boolector.c

@@ -1784,6 +1784,66 @@ boolector_array (Btor *btor, BoolectorSort sort, const char *symbol)
   return BTOR_EXPORT_BOOLECTOR_NODE (res);
 }
 
+BoolectorNode *
+boolector_const_array (Btor *btor,
+                       BoolectorSort sort,
+                       BoolectorNode *value,
+                       const char *symbol)
+{
+  BTOR_ABORT_ARG_NULL (btor);
+
+  BtorNode *res, *const_res, *val;
+  char *symb;
+  BtorSortId s;
+
+  val = BTOR_IMPORT_BOOLECTOR_NODE (value);
+
+  symb = mk_unique_symbol (btor, symbol);
+  s    = BTOR_IMPORT_BOOLECTOR_SORT (sort);
+  BTOR_ABORT (!btor_sort_is_valid (btor, s), "'sort' is not a valid sort");
+  BTOR_ABORT (!btor_sort_is_fun (btor, s)
+                  || btor_sort_tuple_get_arity (
+                         btor, btor_sort_fun_get_domain (btor, s))
+                         != 1,
+              "'sort' is not an array sort");
+  BTOR_TRAPI (
+      BTOR_TRAPI_SORT_FMT BTOR_TRAPI_NODE_FMT " %s", sort, btor, val, symb);
+  BTOR_ABORT (symb && btor_hashptr_table_get (btor->symbols, symb),
+              "symbol '%s' is already in use in the current context",
+              symb);
+  BTOR_ABORT_ARG_NULL (val);
+  BTOR_ABORT_REFS_NOT_POS (val);
+  BTOR_ABORT_BTOR_MISMATCH (btor, val);
+  BTOR_ABORT_IS_NOT_BV (val);
+  BTOR_ABORT (
+      btor_node_get_sort_id (val) != btor_sort_array_get_element (btor, s),
+      "sort of 'value' does not match element sort of array");
+
+  /* Create a const array as lambda. Since we apply structural hashing for
+   * lambdas, the created node can already exist (in case const arrays with the
+   * same value have been created). Hence, we can't directly set the symbol of
+   * 'const_res', but instead create a fresh array variable and assert it to be
+   * equal to 'const_res' and return it to the user. */
+  const_res = btor_exp_const_array (btor, s, val);
+  res       = btor_exp_array (btor, s, symb);
+  btor_mem_freestr (btor->mm, symb);
+
+  btor_node_inc_ext_ref_counter (btor, res);
+  BTOR_TRAPI_RETURN_NODE (res);
+  (void) btor_hashptr_table_add (btor->inputs, btor_node_copy (btor, res));
+
+  /* Assert that 'res' and 'const_res' (lambda) are equal and return 'res'. */
+  BtorNode *eq = btor_exp_eq (btor, res, const_res);
+  btor_assert_exp (btor, eq);
+  btor_node_release (btor, eq);
+  btor_node_release (btor, const_res);
+
+#ifndef NDEBUG
+  BTOR_CHKCLONE_RES_PTR (res, array, sort, symbol);
+#endif
+  return BTOR_EXPORT_BOOLECTOR_NODE (res);
+}
+
 BoolectorNode *
 boolector_uf (Btor *btor, BoolectorSort sort, const char *symbol)
 {

src/boolector.h

@@ -867,6 +867,36 @@ BoolectorNode *boolector_array (Btor *btor,
                                 BoolectorSort sort,
                                 const char *symbol);
 
+/*!
+  Create a one-dimensional bit-vector array with sort ``sort`` initialized with
+  value ``value``.
+
+  An array variable's symbol is used as a simple means of identification,
+  either when printing a model via boolector_print_model, or generating file
+  dumps via boolector_dump_btor and boolector_dump_smt2.
+  A symbol must be unique but may be NULL in case that no symbol should be
+  assigned.
+
+  :param btor: Boolector instance.
+  :param sort: Array sort which maps bit-vectors to bit-vectors.
+  :param value: Value to initialize array.
+  :param symbol: Name of array variable.
+  :return: Bit-vector array of sort ``sort`` and with symbol ``symbol``.
+
+  .. note::
+    In contrast to composite expressions, which are maintained uniquely w.r.t.
+    to their kind, inputs (and consequently, bit width), array variables are
+    not.  Hence, each call to boolector_const_array with the same arguments
+    will return a fresh array variable.
+
+  .. seealso::
+    boolector_array
+ */
+BoolectorNode *boolector_const_array (Btor *btor,
+                                      BoolectorSort sort,
+                                      BoolectorNode *value,
+                                      const char *symbol);
+
 /*!
   Create an uninterpreted function with sort ``sort`` and with symbol
   ``symbol``.

src/btorbv.c

@@ -1911,12 +1911,10 @@ BtorBitVectorTuple *
 btor_bv_new_tuple (BtorMemMgr *mm, uint32_t arity)
 {
   assert (mm);
-  assert (arity > 0);
-
   BtorBitVectorTuple *res;
 
   BTOR_CNEW (mm, res);
-  BTOR_CNEWN (mm, res->bv, arity);
+  if (arity) BTOR_CNEWN (mm, res->bv, arity);
   res->arity = arity;
   return res;
 }
@@ -1942,9 +1940,12 @@ btor_bv_free_tuple (BtorMemMgr *mm, BtorBitVectorTuple *t)
   assert (t);
 
   uint32_t i;
-  for (i = 0; i < t->arity; i++) btor_bv_free (mm, t->bv[i]);
 
-  btor_mem_free (mm, t->bv, sizeof (BtorBitVectorTuple *) * t->arity);
+  if (t->arity)
+  {
+    for (i = 0; i < t->arity; i++) btor_bv_free (mm, t->bv[i]);
+    btor_mem_free (mm, t->bv, sizeof (BtorBitVectorTuple *) * t->arity);
+  }
   btor_mem_free (mm, t, sizeof (BtorBitVectorTuple));
 }
 

src/btorcore.c

@@ -4301,6 +4301,8 @@ check_model (Btor *btor, Btor *clone, BtorPtrHashTable *inputs)
         value      = (BtorBitVector *) it.bucket->data.as_ptr;
         args_tuple = btor_iter_hashptr_next (&it);
 
+        if (args_tuple->arity == 0) continue;
+
         /* create condition */
         assert (BTOR_EMPTY_STACK (consts));
         for (i = 0; i < args_tuple->arity; i++)

src/btorexp.c

@@ -115,6 +115,33 @@ btor_exp_array (Btor *btor, BtorSortId sort, const char *symbol)
   return exp;
 }
 
+BtorNode *
+btor_exp_const_array (Btor *btor, BtorSortId sort, BtorNode *value)
+{
+  assert (btor);
+  assert (sort);
+  assert (btor_sort_is_fun (btor, sort));
+  assert (
+      btor_sort_tuple_get_arity (btor, btor_sort_fun_get_domain (btor, sort))
+      == 1);
+  assert (btor_sort_array_get_element (btor, sort)
+          == btor_node_get_sort_id (value));
+  assert (value);
+  assert (btor_sort_is_bv (btor, btor_node_get_sort_id (value)));
+
+  BtorNode *exp, *param;
+  BtorSortId idxsort;
+
+  idxsort       = btor_sort_array_get_index (btor, sort);
+  param         = btor_exp_param (btor, idxsort, 0);
+  exp           = btor_exp_lambda (btor, param, value);
+  exp->is_array = 1;
+
+  btor_node_release (btor, param);
+
+  return exp;
+}
+
 BtorNode *
 btor_exp_uf (Btor *btor, BtorSortId sort, const char *symbol)
 {

src/btorexp.h

@@ -32,6 +32,8 @@ BtorNode *btor_exp_param (Btor *btor, BtorSortId sort, const char *symbol);
 /* Create an array variable of given sort. */
 BtorNode *btor_exp_array (Btor *btor, BtorSortId sort, const char *symbol);
 
+BtorNode *btor_exp_const_array (Btor *btor, BtorSortId sort, BtorNode *value);
+
 /* Create an uninterpreted function of given sort. */
 BtorNode *btor_exp_uf (Btor *btor, BtorSortId sort, const char *symbol);
 

src/btormodel.c

@@ -273,6 +273,7 @@ recursively_compute_function_model (Btor *btor,
   assert (btor_node_is_regular (fun));
   assert (btor_node_is_fun (fun));
 
+  bool has_default_value = false;
   int32_t i;
   BtorNode *value, *cur_fun, *cur;
   BtorPtrHashTable *static_rho;
@@ -317,6 +318,19 @@ recursively_compute_function_model (Btor *btor,
         }
         BTOR_RELEASE_STACK (stack);
       }
+      else if (btor_node_is_const_array (cur_fun))
+      {
+        /* Default value for model. Note, we add a 0-arity tuple to the
+         * function model to indicate a default value for all indices. */
+        t        = btor_bv_new_tuple (btor->mm, 0);
+        bv_value = btor_model_recursively_compute_assignment (
+            btor, bv_model, fun_model, cur_fun->e[1]);
+        add_to_fun_model (btor, fun_model, fun, t, bv_value);
+        btor_bv_free (mm, bv_value);
+        btor_bv_free_tuple (mm, t);
+        has_default_value = true;
+        cur_fun           = 0;
+      }
       else
       {
         /* only compute models for array lambdas */
@@ -364,6 +378,49 @@ recursively_compute_function_model (Btor *btor,
       cur_fun = 0;
     }
   }
+
+  /* Remove all model entries that are the same as the default value. */
+  if (has_default_value)
+  {
+    BtorBitVector *default_value;
+    BtorBitVectorTuple *args;
+    BtorPtrHashBucket *b;
+    BtorPtrHashTable *cur_model, *new_model;
+    BtorPtrHashTableIterator it;
+
+    t = btor_bv_new_tuple (mm, 0);
+    assert (btor_hashint_map_contains (fun_model, fun->id));
+    cur_model = btor_hashint_map_get (fun_model, fun->id)->as_ptr;
+    assert (cur_model);
+    b = btor_hashptr_table_get (cur_model, t);
+    assert (b);
+    default_value = b->data.as_ptr;
+
+    new_model = btor_hashptr_table_new (mm, cur_model->hash, cur_model->cmp);
+    btor_iter_hashptr_init (&it, cur_model);
+    while (btor_iter_hashptr_has_next (&it))
+    {
+      bv_value = it.bucket->data.as_ptr;
+      args     = btor_iter_hashptr_next (&it);
+
+      if (btor_bv_compare (bv_value, default_value) || args->arity == 0)
+      {
+        btor_hashptr_table_add (new_model, args)->data.as_ptr = bv_value;
+      }
+      /* Skip values that are same as 'default_value'. */
+      else
+      {
+        btor_bv_free (mm, bv_value);
+        btor_bv_free_tuple (mm, args);
+      }
+    }
+    /* Replace model of 'fun' with new cleaned up model. */
+    btor_hashptr_table_delete (cur_model);
+    btor_hashint_map_remove (fun_model, fun->id, 0);
+    btor_hashint_map_add (fun_model, fun->id)->as_ptr = new_model;
+
+    btor_bv_free_tuple (mm, t);
+  }
 }
 
 const BtorPtrHashTable *

src/btornode.h

@@ -431,6 +431,15 @@ btor_node_is_array (const BtorNode *exp)
   return btor_node_real_addr (exp)->is_array == 1;
 }
 
+static inline bool
+btor_node_is_const_array (const BtorNode *exp)
+{
+  assert (exp);
+  exp = btor_node_real_addr (exp);
+  return btor_node_is_array (exp) && exp->kind == BTOR_LAMBDA_NODE
+         && !btor_node_real_addr (exp->e[1])->parameterized;
+}
+
 static inline bool
 btor_node_is_forall (const BtorNode *exp)
 {