[models] Add support for printing arrays

[bclement-ocp]

This patch adds the support for printing arrays in the models output.
Rather than printing default values, we print smtlib abstract values
(@xxx) for the unknown elements, because we don't have a default value
available easily otherwise.

The example model in #555 now displays as:

(
  (define-fun x () Int 0)
  (define-fun y () Int 0)
  (define-fun a1 () (Array Int Int) (store (as @A1 (Array Int Int)) 0 0))
)

This also removes the "Functions" / "Constants" / "Arrays" sections
because they were now wrong (some arrays were in constants, other in
arrays) and hence somewhat confusing. Instead, the "values" section is
added then printing with --model-type constraints.

Uses of Printer.print_fmt have also been replaced with Format.fprintf
because they were causing weird looking outputs with some combinations
of options. Only the final value is printer with print_fmt, which
should do the appropriate (actually, I don't think it is needed here,
but better safe than sorry) cleanup dance only once.

Fixes #555

(Note that this includes #658 but it is only for the tests with --produce-models)

[Halbaroth]

I'm not sure to understand this comment. If the constant is present in the arrays map, then it is present in arrays_symbols and ignored by the function output_constants_counterexample.

[Halbaroth]

I am not sure to understand why some arrays will be printed as constant and other by output_arrays_counterexample.

[bclement-ocp]

If I remember correctly, this is because arrays for which there has been no get/set are not added to the array_symbols.

I didn't think it was very important to keep this distinction, but it should not be too hard to iterate over the constant array symbols in output_arrays_counterexample instead.

[bclement-ocp]

I have a version that does what I described above, but it's not very pretty because:

• There are arrays that only appear in the constants portion. This is the case where an array is defined to be equal to another array.
• There are also arrays that only appear in the arrays portion. This is the case of an array that is defined (i.e. has get/set on them) but does not appear in the original problem and was synthesized by the solver.

Here is a (slightly overcomplicated) example:

(set-logic ALL)
(declare-const x Int)
(declare-const y Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const a4 (Array Int Int))
(assert (= a4 a2))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(assert (= (store a1 y y) a1))
(assert (= (store a2 7 3) a2))
(assert (= (store a2 19 4) a2))

(declare-const a3 (Array Int Int))

(declare-fun f (Bool) (Array Int Int))
(assert (= (f true) a2))
(assert (= (store (f false) 7 3) (f false)))

(check-sat)
(get-model)

A model is:

unknown
(
  ; Functions
  (define-fun f ((arg_0 Bool)) (Array Int Int) (ite (= arg_0 true) a4 !k2))
  ; Constants
  (define-fun x () Int 0)
  (define-fun y () Int 0)
  ; Arrays
  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
  (define-fun a2 () (Array Int Int) a4)
  (define-fun a4 () (Array Int Int)
   (store (store (as @a4 (Array Int Int)) 7 3) 19 4))
  (define-fun !k2 () (Array Int Int) (store (as @!k2 (Array Int Int)) 7 3))
)

In this example, a1 and a4 are in both constants and arrays; a2 is only in constants; and !k2 is only in arrays.

[bclement-ocp]

(I will push the code but am waiting on the merge of #703 to include tests)

[bclement-ocp]

That said I am not convinced that keeping the separation while printing is worth the added code complexity.

[Halbaroth]

I agree. All the values are functions. We should remove the difference. I suggest to keep the code as simple as possible and remove the pointless SMTLIB comments in the output model. We will produce a better code for the next release.

[bclement-ocp]

@Halbaroth should we merge the version with the separation or without? I forgot what was the conclusion of the discussion earlier, I think it was to use the version without separation?

[Halbaroth]

@Halbaroth should we merge the version with the separation or without? I forgot what was the conclusion of the discussion earlier, I think it was to use the version without separation?

Without the separation in the printing please ;) Keep the code as simple as possible to be sure we don't forget any value.

[bclement-ocp]

OK, then this is the original code that you reviewed, I just pushed it again with some tests.

Note that the models are not "correct" wrt #706 (in that they don't print values but can refer to other constants), but that is a separate issue.