Skip to content

Commit e016a90

Browse files
maksleventalTaoBi22maerhartmikeurbachdtzSiFive
authored
[mlir][SMT] add missing ExportSMTLIB tests (#136069)
Whoops forgot these -export-smtlib 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 bf7f602 commit e016a90

File tree

3 files changed

+339
-0
lines changed

3 files changed

+339
-0
lines changed

Diff for: ‎mlir/test/Target/ExportSMTLIB/attributes.mlir

+143
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
// REQUIRES: z3-prover
2+
// RUN: mlir-translate --export-smtlib %s | z3 -in 2>&1 | FileCheck %s
3+
// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | z3 -in 2>&1 | FileCheck %s
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

Diff for: ‎mlir/test/Target/ExportSMTLIB/basic.mlir

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

Diff for: ‎mlir/test/Target/ExportSMTLIB/lit.local.cfg

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
import lit.util
2+
3+
if lit.util.which("z3", config.environment["PATH"]):
4+
config.available_features.add("z3-prover")
5+

0 commit comments

Comments
 (0)