214 lines · plain
1// RUN: mlir-translate --export-smtlib %s | FileCheck %s2// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED3 4smt.solver () : () -> () {5 %c0_bv32 = smt.bv.constant #smt.bv<0> : !smt.bv<32>6 7 // CHECK: (assert (let (([[V0:.+]] (bvneg #x00000000)))8 // CHECK: (let (([[V1:.+]] (= [[V0]] #x00000000)))9 // CHECK: [[V1]])))10 11 // CHECK-INLINED: (assert (= (bvneg #x00000000) #x00000000))12 %0 = smt.bv.neg %c0_bv32 : !smt.bv<32>13 %a0 = smt.eq %0, %c0_bv32 : !smt.bv<32>14 smt.assert %a015 16 // CHECK: (assert (let (([[V2:.+]] (bvadd #x00000000 #x00000000)))17 // CHECK: (let (([[V3:.+]] (= [[V2]] #x00000000)))18 // CHECK: [[V3]])))19 20 // CHECK-INLINED: (assert (= (bvadd #x00000000 #x00000000) #x00000000))21 %1 = smt.bv.add %c0_bv32, %c0_bv32 : !smt.bv<32>22 %a1 = smt.eq %1, %c0_bv32 : !smt.bv<32>23 smt.assert %a124 25 // CHECK: (assert (let (([[V4:.+]] (bvmul #x00000000 #x00000000)))26 // CHECK: (let (([[V5:.+]] (= [[V4]] #x00000000)))27 // CHECK: [[V5]])))28 29 // CHECK-INLINED: (assert (= (bvmul #x00000000 #x00000000) #x00000000))30 %3 = smt.bv.mul %c0_bv32, %c0_bv32 : !smt.bv<32>31 %a3 = smt.eq %3, %c0_bv32 : !smt.bv<32>32 smt.assert %a333 34 // CHECK: (assert (let (([[V6:.+]] (bvurem #x00000000 #x00000000)))35 // CHECK: (let (([[V7:.+]] (= [[V6]] #x00000000)))36 // CHECK: [[V7]])))37 38 // CHECK-INLINED: (assert (= (bvurem #x00000000 #x00000000) #x00000000))39 %4 = smt.bv.urem %c0_bv32, %c0_bv32 : !smt.bv<32>40 %a4 = smt.eq %4, %c0_bv32 : !smt.bv<32>41 smt.assert %a442 43 // CHECK: (assert (let (([[V8:.+]] (bvsrem #x00000000 #x00000000)))44 // CHECK: (let (([[V9:.+]] (= [[V8]] #x00000000)))45 // CHECK: [[V9]])))46 47 // CHECK-INLINED: (assert (= (bvsrem #x00000000 #x00000000) #x00000000))48 %5 = smt.bv.srem %c0_bv32, %c0_bv32 : !smt.bv<32>49 %a5 = smt.eq %5, %c0_bv32 : !smt.bv<32>50 smt.assert %a551 52 // CHECK: (assert (let (([[V10:.+]] (bvsmod #x00000000 #x00000000)))53 // CHECK: (let (([[V11:.+]] (= [[V10]] #x00000000)))54 // CHECK: [[V11]])))55 56 // CHECK-INLINED: (assert (= (bvsmod #x00000000 #x00000000) #x00000000))57 %7 = smt.bv.smod %c0_bv32, %c0_bv32 : !smt.bv<32>58 %a7 = smt.eq %7, %c0_bv32 : !smt.bv<32>59 smt.assert %a760 61 // CHECK: (assert (let (([[V12:.+]] (bvshl #x00000000 #x00000000)))62 // CHECK: (let (([[V13:.+]] (= [[V12]] #x00000000)))63 // CHECK: [[V13]])))64 65 // CHECK-INLINED: (assert (= (bvshl #x00000000 #x00000000) #x00000000))66 %8 = smt.bv.shl %c0_bv32, %c0_bv32 : !smt.bv<32>67 %a8 = smt.eq %8, %c0_bv32 : !smt.bv<32>68 smt.assert %a869 70 // CHECK: (assert (let (([[V14:.+]] (bvlshr #x00000000 #x00000000)))71 // CHECK: (let (([[V15:.+]] (= [[V14]] #x00000000)))72 // CHECK: [[V15]])))73 74 // CHECK-INLINED: (assert (= (bvlshr #x00000000 #x00000000) #x00000000))75 %9 = smt.bv.lshr %c0_bv32, %c0_bv32 : !smt.bv<32>76 %a9 = smt.eq %9, %c0_bv32 : !smt.bv<32>77 smt.assert %a978 79 // CHECK: (assert (let (([[V16:.+]] (bvashr #x00000000 #x00000000)))80 // CHECK: (let (([[V17:.+]] (= [[V16]] #x00000000)))81 // CHECK: [[V17]])))82 83 // CHECK-INLINED: (assert (= (bvashr #x00000000 #x00000000) #x00000000))84 %10 = smt.bv.ashr %c0_bv32, %c0_bv32 : !smt.bv<32>85 %a10 = smt.eq %10, %c0_bv32 : !smt.bv<32>86 smt.assert %a1087 88 // CHECK: (assert (let (([[V18:.+]] (bvudiv #x00000000 #x00000000)))89 // CHECK: (let (([[V19:.+]] (= [[V18]] #x00000000)))90 // CHECK: [[V19]])))91 92 // CHECK-INLINED: (assert (= (bvudiv #x00000000 #x00000000) #x00000000))93 %11 = smt.bv.udiv %c0_bv32, %c0_bv32 : !smt.bv<32>94 %a11 = smt.eq %11, %c0_bv32 : !smt.bv<32>95 smt.assert %a1196 97 // CHECK: (assert (let (([[V20:.+]] (bvsdiv #x00000000 #x00000000)))98 // CHECK: (let (([[V21:.+]] (= [[V20]] #x00000000)))99 // CHECK: [[V21]])))100 101 // CHECK-INLINED: (assert (= (bvsdiv #x00000000 #x00000000) #x00000000))102 %12 = smt.bv.sdiv %c0_bv32, %c0_bv32 : !smt.bv<32>103 %a12 = smt.eq %12, %c0_bv32 : !smt.bv<32>104 smt.assert %a12105 106 // CHECK: (assert (let (([[V22:.+]] (bvnot #x00000000)))107 // CHECK: (let (([[V23:.+]] (= [[V22]] #x00000000)))108 // CHECK: [[V23]])))109 110 // CHECK-INLINED: (assert (= (bvnot #x00000000) #x00000000))111 %13 = smt.bv.not %c0_bv32 : !smt.bv<32>112 %a13 = smt.eq %13, %c0_bv32 : !smt.bv<32>113 smt.assert %a13114 115 // CHECK: (assert (let (([[V24:.+]] (bvand #x00000000 #x00000000)))116 // CHECK: (let (([[V25:.+]] (= [[V24]] #x00000000)))117 // CHECK: [[V25]])))118 119 // CHECK-INLINED: (assert (= (bvand #x00000000 #x00000000) #x00000000))120 %14 = smt.bv.and %c0_bv32, %c0_bv32 : !smt.bv<32>121 %a14 = smt.eq %14, %c0_bv32 : !smt.bv<32>122 smt.assert %a14123 124 // CHECK: (assert (let (([[V26:.+]] (bvor #x00000000 #x00000000)))125 // CHECK: (let (([[V27:.+]] (= [[V26]] #x00000000)))126 // CHECK: [[V27]])))127 128 // CHECK-INLINED: (assert (= (bvor #x00000000 #x00000000) #x00000000))129 %15 = smt.bv.or %c0_bv32, %c0_bv32 : !smt.bv<32>130 %a15 = smt.eq %15, %c0_bv32 : !smt.bv<32>131 smt.assert %a15132 133 // CHECK: (assert (let (([[V28:.+]] (bvxor #x00000000 #x00000000)))134 // CHECK: (let (([[V29:.+]] (= [[V28]] #x00000000)))135 // CHECK: [[V29]])))136 137 // CHECK-INLINED: (assert (= (bvxor #x00000000 #x00000000) #x00000000))138 %16 = smt.bv.xor %c0_bv32, %c0_bv32 : !smt.bv<32>139 %a16 = smt.eq %16, %c0_bv32 : !smt.bv<32>140 smt.assert %a16141 142 // CHECK: (assert (let (([[V30:.+]] (bvslt #x00000000 #x00000000)))143 // CHECK: [[V30]]))144 145 // CHECK-INLINED: (assert (bvslt #x00000000 #x00000000))146 %27 = smt.bv.cmp slt %c0_bv32, %c0_bv32 : !smt.bv<32>147 smt.assert %27148 149 // CHECK: (assert (let (([[V31:.+]] (bvsle #x00000000 #x00000000)))150 // CHECK: [[V31]]))151 152 // CHECK-INLINED: (assert (bvsle #x00000000 #x00000000))153 %28 = smt.bv.cmp sle %c0_bv32, %c0_bv32 : !smt.bv<32>154 smt.assert %28155 156 // CHECK: (assert (let (([[V32:.+]] (bvsgt #x00000000 #x00000000)))157 // CHECK: [[V32]]))158 159 // CHECK-INLINED: (assert (bvsgt #x00000000 #x00000000))160 %29 = smt.bv.cmp sgt %c0_bv32, %c0_bv32 : !smt.bv<32>161 smt.assert %29162 163 // CHECK: (assert (let (([[V33:.+]] (bvsge #x00000000 #x00000000)))164 // CHECK: [[V33]]))165 166 // CHECK-INLINED: (assert (bvsge #x00000000 #x00000000))167 %30 = smt.bv.cmp sge %c0_bv32, %c0_bv32 : !smt.bv<32>168 smt.assert %30169 170 // CHECK: (assert (let (([[V34:.+]] (bvult #x00000000 #x00000000)))171 // CHECK: [[V34]]))172 173 // CHECK-INLINED: (assert (bvult #x00000000 #x00000000))174 %31 = smt.bv.cmp ult %c0_bv32, %c0_bv32 : !smt.bv<32>175 smt.assert %31176 177 // CHECK: (assert (let (([[V35:.+]] (bvule #x00000000 #x00000000)))178 // CHECK: [[V35]]))179 180 // CHECK-INLINED: (assert (bvule #x00000000 #x00000000))181 %32 = smt.bv.cmp ule %c0_bv32, %c0_bv32 : !smt.bv<32>182 smt.assert %32183 184 // CHECK: (assert (let (([[V36:.+]] (bvugt #x00000000 #x00000000)))185 // CHECK: [[V36]]))186 187 // CHECK-INLINED: (assert (bvugt #x00000000 #x00000000))188 %33 = smt.bv.cmp ugt %c0_bv32, %c0_bv32 : !smt.bv<32>189 smt.assert %33190 191 // CHECK: (assert (let (([[V37:.+]] (bvuge #x00000000 #x00000000)))192 // CHECK: [[V37]]))193 194 // CHECK-INLINED: (assert (bvuge #x00000000 #x00000000))195 %34 = smt.bv.cmp uge %c0_bv32, %c0_bv32 : !smt.bv<32>196 smt.assert %34197 198 // CHECK: (assert (let (([[V38:.+]] (concat #x00000000 #x00000000)))199 // CHECK: (let (([[V39:.+]] ((_ extract 23 8) [[V38]])))200 // CHECK: (let (([[V40:.+]] ((_ repeat 2) [[V39]])))201 // CHECK: (let (([[V41:.+]] (= [[V40]] #x00000000)))202 // CHECK: [[V41]])))))203 204 // CHECK-INLINED: (assert (= ((_ repeat 2) ((_ extract 23 8) (concat #x00000000 #x00000000))) #x00000000))205 %35 = smt.bv.concat %c0_bv32, %c0_bv32 : !smt.bv<32>, !smt.bv<32>206 %36 = smt.bv.extract %35 from 8 : (!smt.bv<64>) -> !smt.bv<16>207 %37 = smt.bv.repeat 2 times %36 : !smt.bv<16>208 %a37 = smt.eq %37, %c0_bv32 : !smt.bv<32>209 smt.assert %a37210 211 // CHECK: (reset)212 // CHECK-INLINED: (reset)213}214