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?

Answer 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.