Use generic Z3 sequences from Boogie

[wrwg]

I'm trying to create a generic Seq T type in Boogie which uses Z3 sequences.

An intern at our team created non-generic sequence types a while ago using the following:

type {:datatype} {:builtin "(Seq T@Value)"} SeqOfValue;
function {:builtin "(as seq.empty (Seq T@Value))"} EmptySeq(): SeqOfValue;
function {:builtin "seq.nth"} IndexSeq(a: SeqOfValue, i: int): Value;
...

I'm not quite seeing how I could do the same for Seq T in presence of monomorphization. I would somehow need to refer to the type substitution in the string for :builtin.

@shazqadeer

[shazqadeer]

@wrwg : See

https://github.com/boogie-org/boogie/blob/master/Test/sequences/intseq_lib.bpl

and

https://github.com/boogie-org/boogie/blob/master/Test/sequences/intseq_datatype_lib.bpl

for appropriate usage.

You have to use -lib to get the definitions automatically.