[YICES-HELP] Summation within forall
msartintarm at gmail.com
Fri Jun 3 12:53:22 PDT 2011
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):
array = 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 ))
Using the 'set-evidence!' flag, I would hope to see output like the
(= (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!
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the YICES-HELP