feat: use vector types for ops

[jetafese]

Unblocking work so that we can generate the rest of our pipeline

Having custom types makes conversion between dialects harder. I implemented what we've learnt about customizing operations to get a vector type that doesn't need an index type yet. This should make converting operations easier since the type will remain constant

Thus, given the following btor2 input, that uses arrays:

1 sort bitvec 4
2 sort array 1 1
3 one 1
4 constd 1 8
5 state 2
6 init 2 5 3
7 read 1 5 4
8 one 1
9 add 1 7 8
10 write 2 5 4 9
11 next 2 5 10
12 ones 1
13 sort bitvec 1
14 eq 13 7 12
15 bad 14

we take 2^{bitvec width} as the size of our vector. This gives us the mlir representation below:

module {
  func.func @main() {
    %0 = btor.constant 1 : i4
    %1 = btor.array %0 : vector<16xi4>
    cf.br ^bb1(%1 : vector<16xi4>)
  ^bb1(%2: vector<16xi4>):  // 2 preds: ^bb0, ^bb1
    %3 = btor.constant 1 : i4
    %4 = btor.constant -8 : i4
    %5 = btor.read %2[%4] : vector<16xi4>, i4
    %6 = btor.add %5, %3 : i4
    %7 = btor.write %6, %2[%4] : vector<16xi4>
    %8 = btor.constant -1 : i4
    %9 = btor.cmp eq, %5, %8 : i4
    btor.assert_not(%9)
    cf.br ^bb1(%7 : vector<16xi4>)
  }
}