1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
// RUN: mlir-translate --export-smtlib %s | FileCheck %s
smt.solver () : () -> () {
%0 = smt.int.constant 5
%1 = smt.int.constant 10
// CHECK: (assert (let (([[V0:.+]] (+ 5 5 5)))
// CHECK: (let (([[V1:.+]] (= [[V0]] 10)))
// CHECK: [[V1]])))
// CHECK-INLINED: (assert (= (+ 5 5 5) 10))
%2 = smt.int.add %0, %0, %0
%a2 = smt.eq %2, %1 : !smt.int
smt.assert %a2
// CHECK: (assert (let (([[V2:.+]] (* 5 5 5)))
// CHECK: (let (([[V3:.+]] (= [[V2]] 10)))
// CHECK: [[V3]])))
// CHECK-INLINED: (assert (= (* 5 5 5) 10))
%3 = smt.int.mul %0, %0, %0
%a3 = smt.eq %3, %1 : !smt.int
smt.assert %a3
// CHECK: (assert (let (([[V4:.+]] (- 5 5)))
// CHECK: (let (([[V5:.+]] (= [[V4]] 10)))
// CHECK: [[V5]])))
// CHECK-INLINED: (assert (= (- 5 5) 10))
%4 = smt.int.sub %0, %0
%a4 = smt.eq %4, %1 : !smt.int
smt.assert %a4
// CHECK: (assert (let (([[V6:.+]] (div 5 5)))
// CHECK: (let (([[V7:.+]] (= [[V6]] 10)))
// CHECK: [[V7]])))
// CHECK-INLINED: (assert (= (div 5 5) 10))
%5 = smt.int.div %0, %0
%a5 = smt.eq %5, %1 : !smt.int
smt.assert %a5
// CHECK: (assert (let (([[V8:.+]] (mod 5 5)))
// CHECK: (let (([[V9:.+]] (= [[V8]] 10)))
// CHECK: [[V9]])))
// CHECK-INLINED: (assert (= (mod 5 5) 10))
%6 = smt.int.mod %0, %0
%a6 = smt.eq %6, %1 : !smt.int
smt.assert %a6
// CHECK: (assert (let (([[V10:.+]] (<= 5 5)))
// CHECK: [[V10]]))
// CHECK-INLINED: (assert (<= 5 5))
%9 = smt.int.cmp le %0, %0
smt.assert %9
// CHECK: (assert (let (([[V11:.+]] (< 5 5)))
// CHECK: [[V11]]))
// CHECK-INLINED: (assert (< 5 5))
%10 = smt.int.cmp lt %0, %0
smt.assert %10
// CHECK: (assert (let (([[V12:.+]] (>= 5 5)))
// CHECK: [[V12]]))
// CHECK-INLINED: (assert (>= 5 5))
%11 = smt.int.cmp ge %0, %0
smt.assert %11
// CHECK: (assert (let (([[V13:.+]] (> 5 5)))
// CHECK: [[V13]]))
// CHECK-INLINED: (assert (> 5 5))
%12 = smt.int.cmp gt %0, %0
smt.assert %12
// CHECK: (reset)
// CHECK-INLINED: (reset)
}
|
