How to use array and set values

[barbaro...@gmail.com]

Hi,
I'm trying to understand how array works with boolector but for now it is not all clear. Can anyone create an example for me in C that would create an array of 10 elements where the value at position x is equal to x? So e.g. at position 3 I'd have the value 3? In the end I would like to see the model showing the values.

I followed the examples provided with the documentation[1] but I can solve my problem

Thanks

[1] https://boolector.github.io/docs/cboolector.html

[Mathias Preiner]

Hi Alberto,

The number of elements of an array is bound by the bit-width of the index sort of the arrary. If you want to restrict the number of elements you need to restrict the value range of the indices you use to access the array.

In your example, you just have to assert specific values for elements on specific indices. You can do something like this (code not tested) as follows.

#include "boolector/boolector.h"

#include <stdio.h>

int
main (void)
{
  Btor *btor       = boolector_new ();

  boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1);


  BoolectorSort si = boolector_bitvec_sort (btor, 16);
  BoolectorSort se = boolector_bitvec_sort (btor, 16);
  BoolectorSort sa = boolector_array_sort (btor, si, se);

  BoolectorNode *a = boolector_array (btor, sa, "a");

  // Assert a[i] = i for i < 10
  BoolectorNode *ci, *ri, *ei;
  for (unsigned i = 0; i < 10; i++)
  {
    ci = boolector_int (btor, i, si);

    // Read from array 'a' at position 'i'
    ri = boolector_read (btor, a, ci);

    // a[i] = i
    ei = boolector_eq (btor, ri, ci);

   

    // assert a[i] = i

    boolector_assert(btor, ei);

    boolector_release (btor, ci);
    boolector_release (btor, ri);
    boolector_release (btor, ei);
  }

  unsigned res = boolector_sat (btor);

  // Satisfiable?
  if (res == 10)
  {
    unsigned size;
    char **indices, **values;

    boolector_array_assignment (btor, a, &indices, &values, &size);

    // Print model
    for (unsigned i = 0; i < size; i++)
    {
      printf ("a[%s] = %s\n", indices[i], values[i]);
    }
    boolector_free_array_assignment (btor, indices, values, size);
  }

  boolector_release(btor, a);
  boolector_release_sort(btor, si);
  boolector_release_sort(btor, se);
  boolector_release_sort(btor, sa);

  return 0;
}

HTH

Mathias