feat: array operations with custom types

[jetafese]

Given the circuit below:

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 can now generate the equivalent program in Btor Dialect:

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

And the final llvm ir is as expected:

declare void @__VERIFIER_error()
declare void @__VERIFIER_assert(i1, i64)
define void @main() !dbg !3 {
  br label %1, !dbg !7
1:                                                ; preds = %8, %0
  %2 = phi <16 x i4> [ %5, %8 ], [ <i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1, i4 1>, %0 ]
  %3 = extractelement <16 x i4> %2, i4 -8, !dbg !9
  %4 = add i4 %3, 1, !dbg !10
  %5 = insertelement <16 x i4> %2, i4 %4, i4 -8, !dbg !11
  %6 = icmp eq i4 %3, -1, !dbg !12
  %7 = xor i1 %6, true, !dbg !13
  br i1 %7, label %8, label %9, !dbg !14
8:                                                ; preds = %1
  br label %1, !dbg !15
9:                                                ; preds = %1
  call void @__VERIFIER_assert(i1 %7, i64 0), !dbg !16
  call void @__VERIFIER_error(), !dbg !17
  unreachable, !dbg !18
}