Spacer: Timeout with simple array example

[mmsbrggr]

Hi everyone,

I am trying to use Spacer to verify programs that contain arrays/maps, when I noticed for some seemingly simple benchmarks Spacer gets stuck in a loop. Using different parameters for spacer and z3 did not help. I distilled a minimal simple benchmark that Spacer struggles with. Is there anything I can do get an answer for this and similar benchmarks (like combination of special parameters, different encoding, custom invariants, ...)?

(set-logic HORN)
(set-option :fp.spacer.q3.use_qgen true)
(set-option :fp.spacer.ground_pobs false)
(declare-fun INV ((Array Int Bool) Int) Bool)

; initial state
(assert (forall ((set (Array Int Bool))
         (element Int))
  (=> (and (= ((as const (Array Int Bool)) false) set)
           (= 0 element))
      (INV set element))))

; transition: set stays the same; inc element
(assert (forall ((set (Array Int Bool))
         (element Int)
         (set_ (Array Int Bool))
         (element_ Int))
  (=> (and (INV set element)
           (= set_ set)
           (= element_ (+ 1 element))
           )
      (INV set_ element_))))

; property: element not in set
(assert (forall ((set (Array Int Bool))
         (element Int))
  (=> (and (INV set element))
      (not (select set element)))))

(check-sat)

The benchmark encodes the following transition system: The state consists of an array (called set) and integer (called element). set is initialized to be an array mapping every integer to false, and element to 0. There is a single (symbolic) transition incrementing element (set remains the same). The query is given by the property that select set element is false, which must hold as set is always the array mapping every integer to false.

Any help is appreciated!

[blishko]

Looks like Eldarica 2.1 can solve this example (~12 seconds wall clock time on my machine).

[mmsbrggr]

@blishko. Thanks for the hint. That is true. Also on my machine Eldarica is able to solve the benchmark. However, originally I was aiming for a slight modification of the benchmark above: element gets added to set and element is incremented. This variation is still sat as the variable element can never be in set (as it is increment right after its current value is added). For this variation, which is arguably not much more complex, both Z3 and Eldarica don't provide an answer.

FYI. Here is the mentioned variation of the benchmark:

(set-logic HORN)
(set-option :fp.spacer.q3.use_qgen true)
(set-option :fp.spacer.ground_pobs false)
(declare-fun INV ((Array Int Bool) Int) Bool)

; initial state
(assert (forall ((set (Array Int Bool))
         (element Int))
  (=> (and (= ((as const (Array Int Bool)) false) set)
           (= 0 element))
      (INV set element))))

; transition: set stays the same; inc element
(assert (forall ((set (Array Int Bool))
         (element Int)
         (set_ (Array Int Bool))
         (element_ Int))
  (=> (and (INV set element)
           (= set_ (store set element true))
           (= element_ (+ 1 element))
           )
      (INV set_ element_))))

; property: element not in set
(assert (forall ((set (Array Int Bool))
         (element Int))
  (=> (and (INV set element))
      (not (select set element)))))

(check-sat)

[blishko]

It seems to me you need a quantified invariant here in order to be inductive.
Something like $\forall i : i \geq element \implies \neg set[i]$.
You may try FreqHorn for computing quantified invariants (here is one reference I found).
Maybe @grigoryfedyukovich can help?

[mmsbrggr]

@blishko. Thanks a lot for your pointers. I really appreciate it! I will give FreqHorn a try.
In general, you are correct, the benchmark definitely needs quantified invariants. As far as I know Spacer does support (some?) quantified invariants through q3 (I think it was previously called quicc or something like that). But I have to admit I am not familiar with the internals of q3.

[mmsbrggr]

FYI: I tried freqhorn. It manages to solve the first benchmark almost instantly. However, for the second, only slightly more complex benchmark, it returns unknown.