83 lines · plain
1// RUN: mlir-translate --export-smtlib %s | FileCheck %s2 3smt.solver () : () -> () {4 %0 = smt.int.constant 55 %1 = smt.int.constant 106 7 // CHECK: (assert (let (([[V0:.+]] (+ 5 5 5)))8 // CHECK: (let (([[V1:.+]] (= [[V0]] 10)))9 // CHECK: [[V1]])))10 11 // CHECK-INLINED: (assert (= (+ 5 5 5) 10))12 %2 = smt.int.add %0, %0, %013 %a2 = smt.eq %2, %1 : !smt.int14 smt.assert %a215 16 // CHECK: (assert (let (([[V2:.+]] (* 5 5 5)))17 // CHECK: (let (([[V3:.+]] (= [[V2]] 10)))18 // CHECK: [[V3]])))19 20 // CHECK-INLINED: (assert (= (* 5 5 5) 10))21 %3 = smt.int.mul %0, %0, %022 %a3 = smt.eq %3, %1 : !smt.int23 smt.assert %a324 25 // CHECK: (assert (let (([[V4:.+]] (- 5 5)))26 // CHECK: (let (([[V5:.+]] (= [[V4]] 10)))27 // CHECK: [[V5]])))28 29 // CHECK-INLINED: (assert (= (- 5 5) 10))30 %4 = smt.int.sub %0, %031 %a4 = smt.eq %4, %1 : !smt.int32 smt.assert %a433 34 // CHECK: (assert (let (([[V6:.+]] (div 5 5)))35 // CHECK: (let (([[V7:.+]] (= [[V6]] 10)))36 // CHECK: [[V7]])))37 38 // CHECK-INLINED: (assert (= (div 5 5) 10))39 %5 = smt.int.div %0, %040 %a5 = smt.eq %5, %1 : !smt.int41 smt.assert %a542 43 // CHECK: (assert (let (([[V8:.+]] (mod 5 5)))44 // CHECK: (let (([[V9:.+]] (= [[V8]] 10)))45 // CHECK: [[V9]])))46 47 // CHECK-INLINED: (assert (= (mod 5 5) 10))48 %6 = smt.int.mod %0, %049 %a6 = smt.eq %6, %1 : !smt.int50 smt.assert %a651 52 // CHECK: (assert (let (([[V10:.+]] (<= 5 5)))53 // CHECK: [[V10]]))54 55 // CHECK-INLINED: (assert (<= 5 5))56 %9 = smt.int.cmp le %0, %057 smt.assert %958 59 // CHECK: (assert (let (([[V11:.+]] (< 5 5)))60 // CHECK: [[V11]]))61 62 // CHECK-INLINED: (assert (< 5 5))63 %10 = smt.int.cmp lt %0, %064 smt.assert %1065 66 // CHECK: (assert (let (([[V12:.+]] (>= 5 5)))67 // CHECK: [[V12]]))68 69 // CHECK-INLINED: (assert (>= 5 5))70 %11 = smt.int.cmp ge %0, %071 smt.assert %1172 73 // CHECK: (assert (let (([[V13:.+]] (> 5 5)))74 // CHECK: [[V13]]))75 76 // CHECK-INLINED: (assert (> 5 5))77 %12 = smt.int.cmp gt %0, %078 smt.assert %1279 80 // CHECK: (reset)81 // CHECK-INLINED: (reset)82}83