Constant (e.g., zero-initialized) arrays

[cdisselkoen]

Hi,

Thanks so much for all your work maintaining this library! I was looking at the current C API documentation, and I don't see a way to create a constant array - that is, an array where all elements have a given concrete value, such as 0. I'm looking for a feature analogous to Z3's Z3_mk_const_array. Does an equivalent feature exist in Boolector?

[mpreiner]

Boolector currently does not have an API function for this, but can handle it internally. We can add this functionality.

[cdisselkoen]

I'm happy to assist on the implementation if that would be helpful. I haven't ever touched the Boolector codebase, but if you would give me a pointer for how this should be implemented I can give it a shot.

[mpreiner]

Thanks for the offer, but I already have an implementation for it, just need to test it. I'll probably merge it back to master early next week.

[mpreiner]

@cdisselkoen This is now implemented on master with commit a1b1408fde1076a8da08b04f47e99af711c8874f. However, we do not yet fully support equality over constant arrays. In this case, Boolector will abort with an error.

[cdisselkoen]

Awesome, thanks!

[cdisselkoen]

Hmm, is it possible this feature doesn't yet work in incremental solving mode? I have the following minimal example using the C API (omitting resource cleanup etc for brevity):

#include <stdio.h>
#include <stdlib.h>
#include "boolector.h"

int main() {
  Btor *btor = boolector_new();
  boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 2);
  boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1);
  BoolectorSort eight_bit = boolector_bitvec_sort(btor, 8);
  BoolectorSort array_sort = boolector_array_sort(btor, eight_bit, eight_bit);

  BoolectorNode *fortytwo = boolector_unsigned_int(btor, 42, eight_bit);
  BoolectorNode *const_array = boolector_const_array(btor, array_sort, fortytwo, 0);

  BoolectorNode *seven = boolector_unsigned_int(btor, 7, eight_bit);
  BoolectorNode *val = boolector_read(btor, const_array, seven);
  printf("val is %sconstant\n", boolector_is_const(btor, val) ? "" : "not ");
  // printf("val's bits are %s\n", boolector_get_bits(btor, val));

  if (boolector_sat(btor) != BOOLECTOR_SAT) abort();
  printf("assignment for val is %s\n", boolector_bv_assignment(btor, val));
}

If I comment out the BTOR_OPT_INCREMENTAL line, it works fine: it gives a value of 42 for val as expected. However, as written, with incremental mode, it gives a value of 0 for val.

I'm testing on macOS with Boolector commit dfce248e and the Lingeling solver.

[mpreiner]

Thanks for reporting! This was a bug in the model generation and was not directly related to constant arrays, but was uncovered by it. This is now fixed on master e69de24.

[copy]

@mpreiner Does this have a matching smt2 syntax? Z3 uses ((as const (Array Int Int)) 1)), which I believe is non-standard.

[mpreiner]

I haven't added support in the SMT2 parser yet. I's on my TODO list. I'll let you know as soon as this is supported.

[mpreiner]

It's not in the standard (yet), but at least CVC4 and Z3 support defining constant arrays like that.