[YICES-HELP] Summation within forall

[Michael Sartin-Tarm]

Hello,

I am using Yices as an instruction scheduler, in which I need to find the
total number of instructions scheduled on a tile. To do this, I need to use
a summation. I'm using the 'forall' expression, since there may be a
variable amount of instruction 'chunks' on the tile. However, I'm running
into issues when I try to access array indexes that are dependent on the
current value of i.

In pseudo code, I'm trying to do something like the following (the eventual
sum would lie in array[4]):
array[1] = 0;
for (int i = 2; i =< 4; i++)
    array[i] = array[i-1] + 1;

Here is my attempt to do the same within Yices:

(define-type page (subrange 1 4))
(define array :: (-> int int))

(assert (forall (i :: page)
    (if (<= i 1)
    (= (array i) 0)
    (= (array i) (+ (array (- i 1)) 1 ))
)))

(check)

Using the 'set-evidence!' flag, I would hope to see output like the
following:

unknown
(= (array 1) 0)
(= (array 2) 1)
(= (array 3) 2)
(= (array 4) 3)

However, what I see instead is a bunch of capital I's and periods, as Yices
stalls indefinitely. There's something about the '(array (- i 1))' directive
it doesn't like. This happens with any nonzero value integer in (array (- i
x)) within this loop.

Is there another way I can accomplish a summation using a 'forall' loop that
I'm missing, or will I have to do this manually?

Thank you for your help!
Michael Sartin-Tarm
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/yices-help/attachments/20110603/4b6c5de7/attachment.html