[SMT-LIB] Question on Initializing Large Arrays in SMT

[Christopher L Conway]

Bill,

Chaining store operations in this way creates an intermediate array
value for every element of the array, which is likely to slow down
reasoning in the solver. I think you'd be better off generating a set
of assertions of the form
    (= (select A 0) bvhex11[8])
    (= (select A 1) bvhex22[8])
and so on.

-Chris

On Sun, Jan 23, 2011 at 12:19 PM, Bill Kimball <kimballwb at gmail.com> wrote:
> Hello all,
> Sorry if this is a dup... not sure if the first email went through before
> registering.
>
> ***
>
> I'm having trouble figuring out the proper way to initialize a large array
> in SMT.
>
> If I have an array (in c code) such as:
>
> char myArray[] = "\x11\x22\x33\x44 ... (where 11, 22, 33 etc are hex bytes)
>
> Using theory of Arrays in SMT I presume I could do:
> (store (store (store (store A 0 bvhex11[8]) 1 bvhex22[8]) 2 bvhex33[8]) 3
> bvhex44[8]) ...
>
> My question is ....Is this the "right" way to create an array in SMT with a
> very large number of initial values?  There would be thousands of stores and
> I'm not sure if this is "efficient".
>
> Thanks for any help,
> Bill Kimball
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>