lib/smt/src/smtlib/test.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const smt = @import("../root.zig");
3 const smtlib = @import("root.zig");
4
5 const term = smt.term;
6
7 test {
8 _ = @import("parse/test.zig");
9 std.testing.refAllDecls(smtlib.parse);
10 std.testing.refAllDecls(smtlib.write);
11 }
12
13 test "SMT-LIB parser rereads emitted QF_BV script" {
14 var ctx = term.Context.init(std.testing.allocator);
15 defer ctx.deinit();
16 var script = term.Script.init(&ctx, "QF_BV");
17 defer script.deinit();
18 const x = try ctx.symbol("x", .{ .bitvec = 4 });
19 const one = try ctx.bitvecValue(1, 4);
20 try script.assertTerm(try ctx.bvult(x, try ctx.bvadd(x, one)));
21 var buffer: [1024]u8 = undefined;
22 var stream = std.Io.Writer.fixed(&buffer);
23 try smtlib.writeScript(&stream, &script);
24 const text = stream.buffered();
25
26 var parsed_ctx = term.Context.init(std.testing.allocator);
27 defer parsed_ctx.deinit();
28 var parsed = try smtlib.parseScript(&parsed_ctx, text);
29 defer parsed.deinit();
30 try std.testing.expectEqualStrings("QF_BV", parsed.logic);
31 try std.testing.expectEqual(@as(usize, 1), parsed.assertions.items.len);
32 var out_buffer: [1024]u8 = undefined;
33 var out_stream = std.Io.Writer.fixed(&out_buffer);
34 try smtlib.writeScript(&out_stream, &parsed);
35 try std.testing.expect(std.mem.indexOf(u8, out_stream.buffered(), "(declare-const x (_ BitVec 4))") != null);
36 try std.testing.expect(std.mem.indexOf(u8, out_stream.buffered(), "(assert (bvult x (bvadd x (_ bv1 4))))") != null);
37 }
38
39 test "SMT-LIB parser rereads signed bit-vector comparisons" {
40 var ctx = term.Context.init(std.testing.allocator);
41 defer ctx.deinit();
42 var script = term.Script.init(&ctx, "QF_BV");
43 defer script.deinit();
44 const lhs = try ctx.symbol("lhs", .{ .bitvec = 4 });
45 const rhs = try ctx.symbol("rhs", .{ .bitvec = 4 });
46 try script.assertTerm(try ctx.bvslt(lhs, rhs));
47 try script.assertTerm(try ctx.bvsle(lhs, rhs));
48 var buffer: [2048]u8 = undefined;
49 var stream = std.Io.Writer.fixed(&buffer);
50 try smtlib.writeScript(&stream, &script);
51
52 var parsed_ctx = term.Context.init(std.testing.allocator);
53 defer parsed_ctx.deinit();
54 var parsed = try smtlib.parseScript(&parsed_ctx, stream.buffered());
55 defer parsed.deinit();
56 var out_buffer: [2048]u8 = undefined;
57 var out_stream = std.Io.Writer.fixed(&out_buffer);
58 try smtlib.writeScript(&out_stream, &parsed);
59 const out = out_stream.buffered();
60 try std.testing.expect(std.mem.indexOf(u8, out, "(assert (bvslt lhs rhs))") != null);
61 try std.testing.expect(std.mem.indexOf(u8, out, "(assert (bvsle lhs rhs))") != null);
62 }
63
64 test "SMT-LIB parser rereads overflow predicates" {
65 var ctx = term.Context.init(std.testing.allocator);
66 defer ctx.deinit();
67 var script = term.Script.init(&ctx, "QF_BV");
68 defer script.deinit();
69 const x = try ctx.symbol("x", .{ .bitvec = 8 });
70 const y = try ctx.symbol("y", .{ .bitvec = 8 });
71 try script.assertTerm(try ctx.not(try ctx.bvuaddo(x, y)));
72 try script.assertTerm(try ctx.bvsaddo(x, y));
73 try script.assertTerm(try ctx.bvssubo(x, y));
74 try script.assertTerm(try ctx.bvumulo(x, y));
75 try script.assertTerm(try ctx.bvsmulo(x, y));
76 var buffer: [2048]u8 = undefined;
77 var stream = std.Io.Writer.fixed(&buffer);
78 try smtlib.writeScript(&stream, &script);
79 const text = stream.buffered();
80
81 var parsed_ctx = term.Context.init(std.testing.allocator);
82 defer parsed_ctx.deinit();
83 var parsed = try smtlib.parseScript(&parsed_ctx, text);
84 defer parsed.deinit();
85 var out_buffer: [2048]u8 = undefined;
86 var out_stream = std.Io.Writer.fixed(&out_buffer);
87 try smtlib.writeScript(&out_stream, &parsed);
88 try std.testing.expect(std.mem.indexOf(u8, out_stream.buffered(), "(assert (not (bvuaddo x y)))") != null);
89 try std.testing.expect(std.mem.indexOf(u8, out_stream.buffered(), "(assert (bvsaddo x y))") != null);
90 try std.testing.expect(std.mem.indexOf(u8, out_stream.buffered(), "(assert (bvssubo x y))") != null);
91 try std.testing.expect(std.mem.indexOf(u8, out_stream.buffered(), "(assert (bvumulo x y))") != null);
92 try std.testing.expect(std.mem.indexOf(u8, out_stream.buffered(), "(assert (bvsmulo x y))") != null);
93 }
94
95 test "SMT-LIB parser rereads bit-vector subtraction" {
96 var ctx = term.Context.init(std.testing.allocator);
97 defer ctx.deinit();
98 var script = term.Script.init(&ctx, "QF_BV");
99 defer script.deinit();
100 const x = try ctx.symbol("x", .{ .bitvec = 4 });
101 const y = try ctx.symbol("y", .{ .bitvec = 4 });
102 const one = try ctx.bitvecValue(1, 4);
103 try script.assertTerm(try ctx.eq(try ctx.bvsub(x, y), one));
104 var buffer: [1024]u8 = undefined;
105 var stream = std.Io.Writer.fixed(&buffer);
106 try smtlib.writeScript(&stream, &script);
107 const text = stream.buffered();
108
109 var parsed_ctx = term.Context.init(std.testing.allocator);
110 defer parsed_ctx.deinit();
111 var parsed = try smtlib.parseScript(&parsed_ctx, text);
112 defer parsed.deinit();
113 var out_buffer: [1024]u8 = undefined;
114 var out_stream = std.Io.Writer.fixed(&out_buffer);
115 try smtlib.writeScript(&out_stream, &parsed);
116 try std.testing.expect(std.mem.indexOf(u8, out_stream.buffered(), "(assert (= (bvsub x y) (_ bv1 4)))") != null);
117 }
118
119 test "SMT-LIB parser rereads bitwise bit-vector terms" {
120 var ctx = term.Context.init(std.testing.allocator);
121 defer ctx.deinit();
122 var script = term.Script.init(&ctx, "QF_BV");
123 defer script.deinit();
124 const x = try ctx.symbol("x", .{ .bitvec = 4 });
125 const y = try ctx.symbol("y", .{ .bitvec = 4 });
126 const masked = try ctx.bvand(x, y);
127 const either = try ctx.bvor(x, y);
128 try script.assertTerm(try ctx.eq(try ctx.bvxor(masked, either), try ctx.bvnot(x)));
129 var buffer: [1024]u8 = undefined;
130 var stream = std.Io.Writer.fixed(&buffer);
131 try smtlib.writeScript(&stream, &script);
132 const text = stream.buffered();
133
134 var parsed_ctx = term.Context.init(std.testing.allocator);
135 defer parsed_ctx.deinit();
136 var parsed = try smtlib.parseScript(&parsed_ctx, text);
137 defer parsed.deinit();
138 var out_buffer: [1024]u8 = undefined;
139 var out_stream = std.Io.Writer.fixed(&out_buffer);
140 try smtlib.writeScript(&out_stream, &parsed);
141 const out = out_stream.buffered();
142 try std.testing.expect(std.mem.indexOf(u8, out, "(bvand x y)") != null);
143 try std.testing.expect(std.mem.indexOf(u8, out, "(bvor x y)") != null);
144 try std.testing.expect(std.mem.indexOf(u8, out, "(bvxor") != null);
145 try std.testing.expect(std.mem.indexOf(u8, out, "(bvnot x)") != null);
146 }
147
148 test "SMT-LIB parser rereads bit-vector shifts" {
149 var ctx = term.Context.init(std.testing.allocator);
150 defer ctx.deinit();
151 var script = term.Script.init(&ctx, "QF_BV");
152 defer script.deinit();
153 const x = try ctx.symbol("x", .{ .bitvec = 4 });
154 const amount = try ctx.symbol("amount", .{ .bitvec = 4 });
155 try script.assertTerm(try ctx.eq(try ctx.bvlshr(try ctx.bvshl(x, amount), amount), x));
156 try script.assertTerm(try ctx.eq(try ctx.bvashr(x, amount), x));
157 try script.assertTerm(try ctx.eq(try ctx.bvurem(x, amount), try ctx.bvudiv(x, amount)));
158 try script.assertTerm(try ctx.eq(try ctx.bvsrem(x, amount), try ctx.bvsdiv(x, amount)));
159 try script.assertTerm(try ctx.eq(try ctx.bvsmod(x, amount), x));
160 var buffer: [1024]u8 = undefined;
161 var stream = std.Io.Writer.fixed(&buffer);
162 try smtlib.writeScript(&stream, &script);
163 const text = stream.buffered();
164
165 var parsed_ctx = term.Context.init(std.testing.allocator);
166 defer parsed_ctx.deinit();
167 var parsed = try smtlib.parseScript(&parsed_ctx, text);
168 defer parsed.deinit();
169 var out_buffer: [1024]u8 = undefined;
170 var out_stream = std.Io.Writer.fixed(&out_buffer);
171 try smtlib.writeScript(&out_stream, &parsed);
172 const out = out_stream.buffered();
173 try std.testing.expect(std.mem.indexOf(u8, out, "(bvshl x amount)") != null);
174 try std.testing.expect(std.mem.indexOf(u8, out, "(bvlshr (bvshl x amount) amount)") != null);
175 try std.testing.expect(std.mem.indexOf(u8, out, "(bvashr x amount)") != null);
176 try std.testing.expect(std.mem.indexOf(u8, out, "(bvurem x amount)") != null);
177 try std.testing.expect(std.mem.indexOf(u8, out, "(bvudiv x amount)") != null);
178 try std.testing.expect(std.mem.indexOf(u8, out, "(bvsrem x amount)") != null);
179 try std.testing.expect(std.mem.indexOf(u8, out, "(bvsdiv x amount)") != null);
180 try std.testing.expect(std.mem.indexOf(u8, out, "(bvsmod x amount)") != null);
181 }
182
183 test "SMT-LIB parser rereads bit-vector concat and extract" {
184 var ctx = term.Context.init(std.testing.allocator);
185 defer ctx.deinit();
186 var script = term.Script.init(&ctx, "QF_BV");
187 defer script.deinit();
188 const high = try ctx.symbol("high", .{ .bitvec = 4 });
189 const low = try ctx.symbol("low", .{ .bitvec = 4 });
190 const word = try ctx.bvconcat(high, low);
191 try script.assertTerm(try ctx.eq(try ctx.bvextract(word, 7, 4), high));
192 try script.assertTerm(try ctx.eq(try ctx.bvextract(word, 3, 0), low));
193 var buffer: [2048]u8 = undefined;
194 var stream = std.Io.Writer.fixed(&buffer);
195 try smtlib.writeScript(&stream, &script);
196 const text = stream.buffered();
197
198 var parsed_ctx = term.Context.init(std.testing.allocator);
199 defer parsed_ctx.deinit();
200 var parsed = try smtlib.parseScript(&parsed_ctx, text);
201 defer parsed.deinit();
202 var out_buffer: [2048]u8 = undefined;
203 var out_stream = std.Io.Writer.fixed(&out_buffer);
204 try smtlib.writeScript(&out_stream, &parsed);
205 const out = out_stream.buffered();
206 try std.testing.expect(std.mem.indexOf(u8, out, "(concat high low)") != null);
207 try std.testing.expect(std.mem.indexOf(u8, out, "((_ extract 7 4) (concat high low))") != null);
208 try std.testing.expect(std.mem.indexOf(u8, out, "((_ extract 3 0) (concat high low))") != null);
209 }
210
211 test "SMT-LIB parser rereads bit-vector extensions" {
212 var ctx = term.Context.init(std.testing.allocator);
213 defer ctx.deinit();
214 var script = term.Script.init(&ctx, "QF_BV");
215 defer script.deinit();
216 const signed = try ctx.symbol("signed", .{ .bitvec = 4 });
217 const unsigned = try ctx.symbol("unsigned", .{ .bitvec = 4 });
218 try script.assertTerm(try ctx.eq(try ctx.bvzeroext(unsigned, 4), try ctx.bitvecValue(0x05, 8)));
219 try script.assertTerm(try ctx.eq(try ctx.bvsignext(signed, 4), try ctx.bitvecValue(0xfa, 8)));
220 var buffer: [2048]u8 = undefined;
221 var stream = std.Io.Writer.fixed(&buffer);
222 try smtlib.writeScript(&stream, &script);
223 const text = stream.buffered();
224
225 var parsed_ctx = term.Context.init(std.testing.allocator);
226 defer parsed_ctx.deinit();
227 var parsed = try smtlib.parseScript(&parsed_ctx, text);
228 defer parsed.deinit();
229 var out_buffer: [2048]u8 = undefined;
230 var out_stream = std.Io.Writer.fixed(&out_buffer);
231 try smtlib.writeScript(&out_stream, &parsed);
232 const out = out_stream.buffered();
233 try std.testing.expect(std.mem.indexOf(u8, out, "((_ zero_extend 4) unsigned)") != null);
234 try std.testing.expect(std.mem.indexOf(u8, out, "((_ sign_extend 4) signed)") != null);
235 }
236
237 test "SMT-LIB parser rereads bit-vector rotations" {
238 var ctx = term.Context.init(std.testing.allocator);
239 defer ctx.deinit();
240 var script = term.Script.init(&ctx, "QF_BV");
241 defer script.deinit();
242 const x = try ctx.symbol("x", .{ .bitvec = 4 });
243 try script.assertTerm(try ctx.eq(try ctx.bvrotl(x, 1), try ctx.bitvecValue(0x3, 4)));
244 try script.assertTerm(try ctx.eq(try ctx.bvrotr(x, 1), try ctx.bitvecValue(0xc, 4)));
245 var buffer: [2048]u8 = undefined;
246 var stream = std.Io.Writer.fixed(&buffer);
247 try smtlib.writeScript(&stream, &script);
248 const text = stream.buffered();
249
250 var parsed_ctx = term.Context.init(std.testing.allocator);
251 defer parsed_ctx.deinit();
252 var parsed = try smtlib.parseScript(&parsed_ctx, text);
253 defer parsed.deinit();
254 var out_buffer: [2048]u8 = undefined;
255 var out_stream = std.Io.Writer.fixed(&out_buffer);
256 try smtlib.writeScript(&out_stream, &parsed);
257 const out = out_stream.buffered();
258 try std.testing.expect(std.mem.indexOf(u8, out, "((_ rotate_left 1) x)") != null);
259 try std.testing.expect(std.mem.indexOf(u8, out, "((_ rotate_right 1) x)") != null);
260 }
261
262 test "SMT-LIB parser rereads bit-vector array select store terms" {
263 var ctx = term.Context.init(std.testing.allocator);
264 defer ctx.deinit();
265 var script = term.Script.init(&ctx, "QF_ABV");
266 defer script.deinit();
267 const memory = try ctx.symbol("memory", .{ .array = .{ .index_width = 2, .element_width = 4 } });
268 const index = try ctx.symbol("index", .{ .bitvec = 2 });
269 const value = try ctx.symbol("value", .{ .bitvec = 4 });
270 const written = try ctx.arrayStore(memory, index, value);
271 try script.assertTerm(try ctx.eq(try ctx.arraySelect(written, index), value));
272 var buffer: [2048]u8 = undefined;
273 var stream = std.Io.Writer.fixed(&buffer);
274 try smtlib.writeScript(&stream, &script);
275 const text = stream.buffered();
276
277 var parsed_ctx = term.Context.init(std.testing.allocator);
278 defer parsed_ctx.deinit();
279 var parsed = try smtlib.parseScript(&parsed_ctx, text);
280 defer parsed.deinit();
281 var out_buffer: [2048]u8 = undefined;
282 var out_stream = std.Io.Writer.fixed(&out_buffer);
283 try smtlib.writeScript(&out_stream, &parsed);
284 const out = out_stream.buffered();
285 try std.testing.expect(std.mem.indexOf(u8, out, "(set-logic QF_ABV)") != null);
286 try std.testing.expect(std.mem.indexOf(u8, out, "(declare-const memory (Array (_ BitVec 2) (_ BitVec 4)))") != null);
287 try std.testing.expect(std.mem.indexOf(u8, out, "(assert (= (select (store memory index value) index) value))") != null);
288 }
289
290 test "SMT-LIB parser rereads uninterpreted function applications" {
291 var ctx = term.Context.init(std.testing.allocator);
292 defer ctx.deinit();
293 var script = term.Script.init(&ctx, "QF_UFBV");
294 defer script.deinit();
295 const bv4 = term.Sort{ .bitvec = 4 };
296 const x = try ctx.symbol("x", bv4);
297 const y = try ctx.symbol("y", bv4);
298 const f = try ctx.function("f", &.{bv4}, bv4);
299 const p = try ctx.function("p", &.{bv4}, .bool);
300 try script.assertTerm(try ctx.eq(try ctx.apply(f, &.{x}), try ctx.apply(f, &.{y})));
301 try script.assertTerm(try ctx.apply(p, &.{x}));
302 var buffer: [2048]u8 = undefined;
303 var stream = std.Io.Writer.fixed(&buffer);
304 try smtlib.writeScript(&stream, &script);
305 const text = stream.buffered();
306
307 var parsed_ctx = term.Context.init(std.testing.allocator);
308 defer parsed_ctx.deinit();
309 var parsed = try smtlib.parseScript(&parsed_ctx, text);
310 defer parsed.deinit();
311 var out_buffer: [2048]u8 = undefined;
312 var out_stream = std.Io.Writer.fixed(&out_buffer);
313 try smtlib.writeScript(&out_stream, &parsed);
314 const out = out_stream.buffered();
315 try std.testing.expect(std.mem.indexOf(u8, out, "(set-logic QF_UFBV)") != null);
316 try std.testing.expect(std.mem.indexOf(u8, out, "(declare-fun f ((_ BitVec 4)) (_ BitVec 4))") != null);
317 try std.testing.expect(std.mem.indexOf(u8, out, "(declare-fun p ((_ BitVec 4)) Bool)") != null);
318 try std.testing.expect(std.mem.indexOf(u8, out, "(assert (= (f x) (f y)))") != null);
319 try std.testing.expect(std.mem.indexOf(u8, out, "(assert (p x))") != null);
320 }
321
322 test "SMT-LIB parser rejects ill-sorted function applications" {
323 const source =
324 \\(set-logic QF_UFBV)
325 \\(declare-const x Bool)
326 \\(declare-fun f ((_ BitVec 4)) (_ BitVec 4))
327 \\(assert (= (f x) (_ bv0 4)))
328 \\(check-sat)
329 \\
330 ;
331 var ctx = term.Context.init(std.testing.allocator);
332 defer ctx.deinit();
333 try std.testing.expectError(error.FunctionArgumentSortMismatch, smtlib.parseScript(&ctx, source));
334 }