Skip to content

Commit 2cdb240

Browse files
maksleventalTaoBi22maerhartmikeurbachdtzSiFive
committed
[mlir][SMT] add missing ExportSMTLIB tests
Co-authored-by: Bea Healy <[email protected]> Co-authored-by: Martin Erhart <[email protected]> Co-authored-by: Mike Urbach <[email protected]> Co-authored-by: Will Dietz <[email protected]> Co-authored-by: fzi-hielscher <[email protected]> Co-authored-by: Fehr Mathieu <[email protected]> Co-authored-by: Clo91eaf <[email protected]>
1 parent b07fc0f commit 2cdb240

File tree

3 files changed

+338
-0
lines changed

3 files changed

+338
-0
lines changed

‎mlir/test/Target/ExportSMTLIB/attributes.mlir

Lines changed: 143 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
// RUN: mlir-translate --export-smtlib %s | z3 -in 2>&1 | FileCheck %s
2+
// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | z3 -in 2>&1 | FileCheck %s
3+
// REQUIRES: z3
4+
5+
// Quantifiers Attributes
6+
smt.solver () : () -> () {
7+
8+
%true = smt.constant true
9+
10+
%7 = smt.exists weight 2 {
11+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
12+
%4 = smt.eq %arg2, %arg3 : !smt.int
13+
%5 = smt.implies %4, %true
14+
smt.yield %5 : !smt.bool
15+
}
16+
smt.assert %7
17+
18+
smt.check sat {} unknown {} unsat {}
19+
}
20+
21+
// CHECK-NOT: WARNING
22+
// CHECK-NOT: warning
23+
// CHECK-NOT: ERROR
24+
// CHECK-NOT: error
25+
// CHECK-NOT: unsat
26+
// CHECK: sat
27+
28+
// Quantifiers Attributes
29+
smt.solver () : () -> () {
30+
31+
%true = smt.constant true
32+
33+
%7 = smt.exists weight 2 {
34+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
35+
%4 = smt.eq %arg2, %arg3 : !smt.int
36+
%5 = smt.implies %4, %true
37+
smt.yield %5 : !smt.bool
38+
} patterns {
39+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
40+
%4 = smt.eq %arg2, %arg3 : !smt.int
41+
smt.yield %4: !smt.bool
42+
}
43+
smt.assert %7
44+
45+
smt.check sat {} unknown {} unsat {}
46+
}
47+
48+
// CHECK-NOT: WARNING
49+
// CHECK-NOT: warning
50+
// CHECK-NOT: ERROR
51+
// CHECK-NOT: error
52+
// CHECK-NOT: unsat
53+
// CHECK: sat
54+
55+
// Quantifiers Attributes
56+
smt.solver () : () -> () {
57+
58+
%true = smt.constant true
59+
60+
%7 = smt.exists {
61+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
62+
%4 = smt.eq %arg2, %arg3 : !smt.int
63+
%5 = smt.implies %4, %true
64+
smt.yield %5 : !smt.bool
65+
} patterns {
66+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
67+
%4 = smt.eq %arg2, %arg3 : !smt.int
68+
smt.yield %4: !smt.bool
69+
}
70+
smt.assert %7
71+
72+
smt.check sat {} unknown {} unsat {}
73+
}
74+
75+
// CHECK-NOT: WARNING
76+
// CHECK-NOT: warning
77+
// CHECK-NOT: ERROR
78+
// CHECK-NOT: error
79+
// CHECK-NOT: unsat
80+
// CHECK: sat
81+
82+
smt.solver () : () -> () {
83+
84+
%true = smt.constant true
85+
%three = smt.int.constant 3
86+
%four = smt.int.constant 4
87+
88+
%7 = smt.exists {
89+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
90+
%4 = smt.eq %arg2, %three: !smt.int
91+
%5 = smt.eq %arg3, %four: !smt.int
92+
%6 = smt.eq %4, %5: !smt.bool
93+
smt.yield %6 : !smt.bool
94+
} patterns {
95+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
96+
%4 = smt.eq %arg2, %three: !smt.int
97+
smt.yield %4: !smt.bool}, {
98+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
99+
%5 = smt.eq %arg3, %four: !smt.int
100+
smt.yield %5: !smt.bool
101+
}
102+
smt.assert %7
103+
104+
smt.check sat {} unknown {} unsat {}
105+
}
106+
107+
// CHECK-NOT: WARNING
108+
// CHECK-NOT: warning
109+
// CHECK-NOT: ERROR
110+
// CHECK-NOT: error
111+
// CHECK-NOT: unsat
112+
// CHECK: sat
113+
114+
smt.solver () : () -> () {
115+
116+
%true = smt.constant true
117+
%three = smt.int.constant 3
118+
%four = smt.int.constant 4
119+
120+
%10 = smt.exists {
121+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
122+
%4 = smt.eq %arg2, %three: !smt.int
123+
%5 = smt.eq %arg3, %four: !smt.int
124+
%9 = smt.eq %4, %5: !smt.bool
125+
smt.yield %9 : !smt.bool
126+
} patterns {
127+
^bb0(%arg2: !smt.int, %arg3: !smt.int):
128+
%4 = smt.eq %arg2, %three: !smt.int
129+
%5 = smt.eq %arg3, %four: !smt.int
130+
smt.yield %4, %5: !smt.bool, !smt.bool
131+
}
132+
smt.assert %10
133+
134+
smt.check sat {} unknown {} unsat {}
135+
136+
}
137+
138+
// CHECK-NOT: WARNING
139+
// CHECK-NOT: warning
140+
// CHECK-NOT: ERROR
141+
// CHECK-NOT: error
142+
// CHECK-NOT: unsat
143+
// CHECK: sat

‎mlir/test/Target/ExportSMTLIB/basic.mlir

Lines changed: 192 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,192 @@
1+
// REQUIRES: z3-prover
2+
// RUN: mlir-translate --export-smtlib %s | z3 -in %t 2>&1 | FileCheck %s
3+
// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | z3 -in 2>&1 | FileCheck %s
4+
// REQUIRES: z3
5+
6+
// Function and constant symbol declarations, uninterpreted sorts
7+
smt.solver () : () -> () {
8+
%0 = smt.declare_fun "b" : !smt.bv<32>
9+
%1 = smt.declare_fun : !smt.int
10+
%2 = smt.declare_fun : !smt.func<(!smt.int, !smt.bv<32>) !smt.bool>
11+
%3 = smt.apply_func %2(%1, %0) : !smt.func<(!smt.int, !smt.bv<32>) !smt.bool>
12+
smt.assert %3
13+
14+
%4 = smt.declare_fun : !smt.sort<"uninterpreted">
15+
%5 = smt.declare_fun : !smt.sort<"other"[!smt.sort<"uninterpreted">]>
16+
%6 = smt.declare_fun : !smt.func<(!smt.sort<"other"[!smt.sort<"uninterpreted">]>, !smt.sort<"uninterpreted">) !smt.bool>
17+
%7 = smt.apply_func %6(%5, %4) : !smt.func<(!smt.sort<"other"[!smt.sort<"uninterpreted">]>, !smt.sort<"uninterpreted">) !smt.bool>
18+
smt.assert %7
19+
20+
smt.check sat {} unknown {} unsat {}
21+
}
22+
23+
// CHECK-NOT: WARNING
24+
// CHECK-NOT: warning
25+
// CHECK-NOT: ERROR
26+
// CHECK-NOT: error
27+
// CHECK-NOT: unsat
28+
// CHECK: sat
29+
30+
// Big expression
31+
smt.solver () : () -> () {
32+
%true = smt.constant true
33+
%false = smt.constant false
34+
%0 = smt.not %true
35+
%1 = smt.and %0, %true, %false
36+
%2 = smt.or %1, %0, %true
37+
%3 = smt.xor %0, %2
38+
%4 = smt.implies %3, %false
39+
%5 = smt.implies %4, %true
40+
smt.assert %5
41+
42+
smt.check sat {} unknown {} unsat {}
43+
}
44+
45+
// CHECK-NOT: WARNING
46+
// CHECK-NOT: warning
47+
// CHECK-NOT: ERROR
48+
// CHECK-NOT: error
49+
// CHECK-NOT: unsat
50+
// CHECK: sat
51+
52+
// Constant array
53+
smt.solver () : () -> () {
54+
%true = smt.constant true
55+
%false = smt.constant false
56+
%c = smt.int.constant 0
57+
%0 = smt.array.broadcast %true : !smt.array<[!smt.int -> !smt.bool]>
58+
%1 = smt.array.store %0[%c], %false : !smt.array<[!smt.int -> !smt.bool]>
59+
%2 = smt.array.select %1[%c] : !smt.array<[!smt.int -> !smt.bool]>
60+
smt.assert %2
61+
62+
smt.check sat {} unknown {} unsat {}
63+
}
64+
65+
// CHECK-NOT: WARNING
66+
// CHECK-NOT: warning
67+
// CHECK-NOT: ERROR
68+
// CHECK-NOT: error
69+
// CHECK: unsat
70+
71+
// BitVector extract and concat, and constants
72+
smt.solver () : () -> () {
73+
%xf = smt.bv.constant #smt.bv<0xf> : !smt.bv<4>
74+
%x0 = smt.bv.constant #smt.bv<0> : !smt.bv<4>
75+
%xff = smt.bv.constant #smt.bv<0xff> : !smt.bv<8>
76+
77+
%0 = smt.bv.concat %xf, %x0 : !smt.bv<4>, !smt.bv<4>
78+
%1 = smt.bv.extract %0 from 4 : (!smt.bv<8>) -> !smt.bv<4>
79+
%2 = smt.bv.repeat 2 times %1 : !smt.bv<4>
80+
%3 = smt.eq %2, %xff : !smt.bv<8>
81+
smt.assert %3
82+
83+
smt.check sat {} unknown {} unsat {}
84+
}
85+
86+
// CHECK-NOT: WARNING
87+
// CHECK-NOT: warning
88+
// CHECK-NOT: ERROR
89+
// CHECK-NOT: error
90+
// CHECK-NOT: unsat
91+
// CHECK: sat
92+
93+
// Quantifiers
94+
smt.solver () : () -> () {
95+
%1 = smt.forall ["a"] {
96+
^bb0(%arg2: !smt.int):
97+
%c2_1 = smt.int.constant 2
98+
%2 = smt.int.mul %arg2, %c2_1
99+
100+
%3 = smt.exists {
101+
^bb0(%arg1: !smt.int):
102+
%c2 = smt.int.constant 2
103+
%4 = smt.int.mul %c2, %arg1
104+
%5 = smt.eq %4, %2 : !smt.int
105+
smt.yield %5 : !smt.bool
106+
}
107+
108+
smt.yield %3 : !smt.bool
109+
}
110+
smt.assert %1
111+
112+
smt.check sat {} unknown {} unsat {}
113+
}
114+
115+
// CHECK-NOT: WARNING
116+
// CHECK-NOT: warning
117+
// CHECK-NOT: ERROR
118+
// CHECK-NOT: error
119+
// CHECK-NOT: unsat
120+
// CHECK: sat
121+
122+
// Push and pop
123+
smt.solver () : () -> () {
124+
%three = smt.int.constant 3
125+
%four = smt.int.constant 4
126+
%unsat_eq = smt.eq %three, %four : !smt.int
127+
%sat_eq = smt.eq %three, %three : !smt.int
128+
129+
smt.push 1
130+
smt.assert %unsat_eq
131+
smt.check sat {} unknown {} unsat {}
132+
smt.pop 1
133+
smt.assert %sat_eq
134+
smt.check sat {} unknown {} unsat {}
135+
}
136+
137+
// CHECK-NOT: WARNING
138+
// CHECK-NOT: warning
139+
// CHECK-NOT: ERROR
140+
// CHECK-NOT: error
141+
// CHECK-NOT: sat
142+
// CHECK: unsat
143+
// CHECK-NOT: WARNING
144+
// CHECK-NOT: warning
145+
// CHECK-NOT: ERROR
146+
// CHECK-NOT: error
147+
// CHECK-NOT: unsat
148+
// CHECK: sat
149+
150+
// Reset
151+
smt.solver () : () -> () {
152+
%three = smt.int.constant 3
153+
%four = smt.int.constant 4
154+
%unsat_eq = smt.eq %three, %four : !smt.int
155+
%sat_eq = smt.eq %three, %three : !smt.int
156+
157+
smt.assert %unsat_eq
158+
smt.check sat {} unknown {} unsat {}
159+
smt.reset
160+
smt.assert %sat_eq
161+
smt.check sat {} unknown {} unsat {}
162+
}
163+
164+
// CHECK-NOT: WARNING
165+
// CHECK-NOT: warning
166+
// CHECK-NOT: ERROR
167+
// CHECK-NOT: error
168+
// CHECK-NOT: sat
169+
// CHECK: unsat
170+
// CHECK-NOT: WARNING
171+
// CHECK-NOT: warning
172+
// CHECK-NOT: ERROR
173+
// CHECK-NOT: error
174+
// CHECK-NOT: unsat
175+
// CHECK: sat
176+
177+
smt.solver () : () -> () {
178+
smt.set_logic "HORN"
179+
%c = smt.declare_fun : !smt.int
180+
%c4 = smt.int.constant 4
181+
%eq = smt.eq %c, %c4 : !smt.int
182+
smt.assert %eq
183+
smt.check sat {} unknown {} unsat {}
184+
}
185+
186+
// CHECK-NOT: WARNING
187+
// CHECK-NOT: warning
188+
// CHECK-NOT: ERROR
189+
// CHECK-NOT: error
190+
// CHECK-NOT: unsat
191+
// CHECK-NOT: sat
192+
// CHECK: unknown

‎mlir/test/Target/ExportSMTLIB/lit.local.cfg

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
if lit.util.which("z3", config.environment["PATH"]):
2+
config.available_features.add("z3-prover")
3+

0 commit comments

Comments
 (0)