Vectors vs Sequences in Boogie

Question

Looking through the tests that come with Boogie, I noticed there are two collection types: Seq T and Vec T. Examples are:

type {:builtin "Seq"} Seq _;
function {:builtin "seq.empty"} empty(): Seq int;
function {:builtin "seq.len"} len(a: Seq int): int;
function {:builtin "seq.++"} append(a: Seq int, b: Seq int): Seq int;
function {:builtin "seq.unit"} unit(v: int): Seq int;
function {:builtin "seq.nth"} nth(a: Seq int, i: int): int;

procedure test()
{
  var s: Seq int;

  s ≔  append(unit(1),unit(2));
  assert nth(s,0) == 1;
  assert nth(s,1) == 2;
  assert len(s) == 2;
}

The above illustrates use of sequences, whilst for vectors it would be:

procedure test()
{
  var s: Vec int;

  s ≔  Vec_Append(Vec_Empty(),1);
  s ≔  Vec_Append(s,2);
  assert Vec_Nth(s,0) == 1;
  assert Vec_Nth(s,1) == 2;
  assert Vec_Len(s) == 2;
}

(This has to be compiled with -lib)

Looking within the file Core/LibraryDefinitions.bpl I see Vec is not defined in the same way as Seq.

My question: What's the difference here?

score 1 · Accepted Answer · answered Jun 18 '22 at 14:05

1

Seq targets the native sequence theory supported by SMT solvers Z3 and CVC5. Vec, on the other hand, is implemented in Boogie atop the generalized array theory supported only by Z3. As far as I remember, the supported operations have similar meanings. You might see differences in performance and completeness.

answered Jun 18 '22 at 14:05

Shaz Qadeer

26
1

So, it comes down to portability then really? – redjamjar Jun 19 '22 at 20:52
1

Yes, Seq is more portable since it is supported natively in SMT. But your mileage may vary depending on your problems. For some of the problems I was interested in, the implementation in Z3 was inadequate. CVC5 has done more work on the Seq theory recently so it may work better now. I suggest trying the various options on a few examples. – Shaz Qadeer Jun 20 '22 at 21:50

Vectors vs Sequences in Boogie

1 Answers1