Support producing models for arrays

[daniel-raffler]

Hello, as mentioned in #614 I'm currently working on adding OpenSMT support to the JavaSMT framework. One of the issues I've run into is with the way OpenSMT represents array variables in its model. Most solvers will return a nested "store expression" that represents the value, but for OpenSMT only an abstract value is provided.

Here's a simple example:

(set-logic QF_AUFLIA)

(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))

(declare-const x Int)
(declare-const y Int)

(assert (distinct (select a1 x) y))
(assert (= (store a1 x y) a2))

(check-sat)
(get-model)

(exit)

Z3 will print this model:

(
  (define-fun a1 () (Array Int Int) ((as const (Array Int Int)) 0))
  (define-fun a2 () (Array Int Int) (store ((as const (Array Int Int)) 0) 0 1))
  (define-fun x () Int 0)
  (define-fun y () Int 1)
)

But for OpenSMT we only get abstract values:

(
  (define-fun a1 () (Array Int Int) (as @2 (Array Int Int)))
  (define-fun a2 () (Array Int Int) (as @6 (Array Int Int)))
  (define-fun x () Int 3)
  (define-fun y () Int 1)
)

Is there any way to "unwind" the abstract values into proper terms? This would probably also require support for "const" as a built-in function?

Thanks, Daniel

[blishko]

Hi Daniel, The functionality to compute models for arrays is not yet implemented in OpenSMT. Support for arrays has been added relatively recently and we have not tried computing models for theories with arrays, yet. This is yet another TODO.

[blishko]

What you see in the output is most likely some fallback mechanism. OpenSMT should probably report an error with an unsupported message instead.

[daniel-raffler]

Thanks for the quick reply! I'll then just disable model generation for array for now.