Add input and constraint translation to MLIR

[jetafese]

Convert from the btor2 file below

1 sort bitvec 1
2 input 1 turn
3 state 1 state0
4 state 1 state1
5 ite 1 -2 -3 3
6 ite 1 2 -4 4
7 next 1 3 5
8 next 1 4 6
9 eq 1 3 4
10 one 1
11 state 1 initially
12 init 1 11 10
13 zero 1
14 next 1 11 13
15 implies 1 11 -9
16 constraint 15
17 bad 9

to the MLIR module:

module  {
  func @init() -> (i1, i1, i1) {
    %0 = btor.const true
    %1 = btor.undef : i1
    return %1, %1, %0 : i1, i1, i1
  }
  func @next(%arg0: i1, %arg1: i1, %arg2: i1) -> (i1, i1, i1) {
    %0 = btor.not %arg0 : i1
    %1 = btor.const false
    %2 = btor.input %1 : i1  {id = 0 : i64}
    %3 = btor.not %2 : i1
    %4 = btor.ite %3, %0, %arg0 : i1
    %5 = btor.not %arg1 : i1
    %6 = btor.ite %2, %5, %arg1 : i1
    %7 = btor.const false
    %8 = btor.cmp eq, %arg0, %arg1 : i1
    %9 = btor.not %8 : i1
    %10 = btor.implies %arg2, %9 : i1
    btor.assume(%10)
    btor.assert_not(%8)
    return %4, %6, %7 : i1, i1, i1
  }
}