lib/smt/src/smtlib/write.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! Prints a script or a single term as SMT-LIB text. A caller hands a formula it built to another
2 //! solver, or stores it, and needs text any SMT-LIB reader accepts.
3 //!
4 //! Each term kind prints as its SMT-LIB operator applied to its operands, and bit-vector constants
5 //! print as `(_ bvV W)`. A list operator with one operand prints as the operand alone, and an `and`
6 //! with none prints as `true` and an `or` with none as `false`. The same rule changes the meaning
7 //! of `distinct` with one operand, which prints as its operand, and of `+` and `*` with none, which
8 //! print as `false`. A negative integer prints as `-5`, which standard SMT-LIB readers refuse,
9 //! since SMT-LIB writes it `(- 5)`. The writer recurses once per level of the term, with no depth
10 //! bound.
11 const std = @import("std");
12 const smt = @import("../root.zig");
13
14 const term = smt.term;
15
16 /// Writes `(set-logic L)` with the script's logic, then one `declare-const` per named constant of
17 /// the `Context`, one `declare-fun` per function declaration, one `assert` per assertion of the
18 /// script, and `(check-sat)`, so code can hand a whole formula to another solver or read it back.
19 /// Declarations follow the order in which the `Context` built them. The call declares every
20 /// constant and function of the `Context`, including those no assertion uses. Two constants that
21 /// share a name print two `declare-const` lines with that name, which a reader refuses. The
22 /// function returns only the writer's errors.
23 pub fn writeScript(writer: *std.Io.Writer, script: *const term.Script) std.Io.Writer.Error!void {
24 try writer.print("(set-logic {s})\n", .{script.logic});
25 for (script.ctx.nodes.items) |node| {
26 switch (node) {
27 .symbol => |symbol| {
28 try writer.print("(declare-const {s} ", .{symbol.name});
29 try symbol.sort.write(writer);
30 try writer.writeAll(")\n");
31 },
32 else => {},
33 }
34 }
35 for (script.ctx.functions.items) |decl| {
36 try writer.print("(declare-fun {s} (", .{decl.name});
37 for (decl.params, 0..) |param, index| {
38 if (index > 0) try writer.writeAll(" ");
39 try param.write(writer);
40 }
41 try writer.writeAll(") ");
42 try decl.result.write(writer);
43 try writer.writeAll(")\n");
44 }
45 for (script.assertions.items) |assertion| {
46 try writer.writeAll("(assert ");
47 try writeTerm(writer, script.ctx, assertion);
48 try writer.writeAll(")\n");
49 }
50 try writer.writeAll("(check-sat)\n");
51 }
52
53 /// Writes the term `id` of `ctx` in SMT-LIB syntax, so code can print a single term for a message
54 /// or a log, and `writeScript` calls it for every assertion. A constant prints as its name, and an
55 /// application of a function with no arguments as the function's name alone. An `and` with no
56 /// operands prints as `true` and an `or` with none as `false`, and a list operator with one operand
57 /// prints the operand alone. `distinct` with one operand prints as its operand, `+` and `*` with no
58 /// operands print as `false`, and a negative integer prints as `-5`: each reads back as a different
59 /// term or fails in standard readers. An `id` past the terms of `ctx` makes the call panic. The
60 /// function returns only the writer's errors.
61 pub fn writeTerm(writer: *std.Io.Writer, ctx: *const term.Context, id: term.Term) std.Io.Writer.Error!void {
62 const node = ctx.nodes.items[id];
63 switch (node) {
64 .symbol => |symbol| try writer.writeAll(symbol.name),
65 .apply => |item| try writeApply(writer, ctx, item.function, item.args),
66 .bool => |value| try writer.writeAll(if (value) "true" else "false"),
67 .int => |value| try writer.print("{d}", .{value}),
68 .bitvec => |value| try writer.print("(_ bv{d} {d})", .{ value.value, value.width }),
69 .not => |operand| try writeUnary(writer, ctx, "not", operand),
70 .and_ => |operands| try writeNary(writer, ctx, "and", operands),
71 .or_ => |operands| try writeNary(writer, ctx, "or", operands),
72 .implies => |pair| try writeBinary(writer, ctx, "=>", pair.lhs, pair.rhs),
73 .eq => |pair| try writeBinary(writer, ctx, "=", pair.lhs, pair.rhs),
74 .distinct => |operands| try writeNary(writer, ctx, "distinct", operands),
75 .add => |operands| try writeNary(writer, ctx, "+", operands),
76 .mul => |operands| try writeNary(writer, ctx, "*", operands),
77 .le => |pair| try writeBinary(writer, ctx, "<=", pair.lhs, pair.rhs),
78 .lt => |pair| try writeBinary(writer, ctx, "<", pair.lhs, pair.rhs),
79 .ge => |pair| try writeBinary(writer, ctx, ">=", pair.lhs, pair.rhs),
80 .gt => |pair| try writeBinary(writer, ctx, ">", pair.lhs, pair.rhs),
81 .bvule => |pair| try writeBinary(writer, ctx, "bvule", pair.lhs, pair.rhs),
82 .bvult => |pair| try writeBinary(writer, ctx, "bvult", pair.lhs, pair.rhs),
83 .bvsle => |pair| try writeBinary(writer, ctx, "bvsle", pair.lhs, pair.rhs),
84 .bvslt => |pair| try writeBinary(writer, ctx, "bvslt", pair.lhs, pair.rhs),
85 .bvuaddo => |pair| try writeBinary(writer, ctx, "bvuaddo", pair.lhs, pair.rhs),
86 .bvsaddo => |pair| try writeBinary(writer, ctx, "bvsaddo", pair.lhs, pair.rhs),
87 .bvssubo => |pair| try writeBinary(writer, ctx, "bvssubo", pair.lhs, pair.rhs),
88 .bvumulo => |pair| try writeBinary(writer, ctx, "bvumulo", pair.lhs, pair.rhs),
89 .bvsmulo => |pair| try writeBinary(writer, ctx, "bvsmulo", pair.lhs, pair.rhs),
90 .bvnot => |operand| try writeUnary(writer, ctx, "bvnot", operand),
91 .bvand => |pair| try writeBinary(writer, ctx, "bvand", pair.lhs, pair.rhs),
92 .bvor => |pair| try writeBinary(writer, ctx, "bvor", pair.lhs, pair.rhs),
93 .bvxor => |pair| try writeBinary(writer, ctx, "bvxor", pair.lhs, pair.rhs),
94 .bvshl => |pair| try writeBinary(writer, ctx, "bvshl", pair.lhs, pair.rhs),
95 .bvlshr => |pair| try writeBinary(writer, ctx, "bvlshr", pair.lhs, pair.rhs),
96 .bvashr => |pair| try writeBinary(writer, ctx, "bvashr", pair.lhs, pair.rhs),
97 .bvudiv => |pair| try writeBinary(writer, ctx, "bvudiv", pair.lhs, pair.rhs),
98 .bvurem => |pair| try writeBinary(writer, ctx, "bvurem", pair.lhs, pair.rhs),
99 .bvsdiv => |pair| try writeBinary(writer, ctx, "bvsdiv", pair.lhs, pair.rhs),
100 .bvsrem => |pair| try writeBinary(writer, ctx, "bvsrem", pair.lhs, pair.rhs),
101 .bvsmod => |pair| try writeBinary(writer, ctx, "bvsmod", pair.lhs, pair.rhs),
102 .array_select => |item| try writeBinary(writer, ctx, "select", item.array, item.index),
103 .array_store => |item| try writeTernary(writer, ctx, "store", item.array, item.index, item.value),
104 .bvconcat => |pair| try writeBinary(writer, ctx, "concat", pair.lhs, pair.rhs),
105 .bvextract => |item| try writeExtract(writer, ctx, item.operand, item.high, item.low),
106 .bvzeroext => |item| try writeExtension(writer, ctx, "zero_extend", item.operand, item.extra),
107 .bvsignext => |item| try writeExtension(writer, ctx, "sign_extend", item.operand, item.extra),
108 .bvrotl => |item| try writeExtension(writer, ctx, "rotate_left", item.operand, item.amount),
109 .bvrotr => |item| try writeExtension(writer, ctx, "rotate_right", item.operand, item.amount),
110 .bvadd => |pair| try writeBinary(writer, ctx, "bvadd", pair.lhs, pair.rhs),
111 .bvsub => |pair| try writeBinary(writer, ctx, "bvsub", pair.lhs, pair.rhs),
112 .bvmul => |pair| try writeBinary(writer, ctx, "bvmul", pair.lhs, pair.rhs),
113 }
114 }
115
116 fn writeApply(writer: *std.Io.Writer, ctx: *const term.Context, function_id: term.Function, args: []const term.Term) std.Io.Writer.Error!void {
117 const decl = ctx.functions.items[function_id];
118 if (args.len == 0) {
119 try writer.writeAll(decl.name);
120 return;
121 }
122 try writer.print("({s}", .{decl.name});
123 for (args) |arg| {
124 try writer.writeAll(" ");
125 try writeTerm(writer, ctx, arg);
126 }
127 try writer.writeAll(")");
128 }
129
130 fn writeUnary(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, operand: term.Term) std.Io.Writer.Error!void {
131 try writer.print("({s} ", .{name});
132 try writeTerm(writer, ctx, operand);
133 try writer.writeAll(")");
134 }
135
136 fn writeBinary(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, lhs: term.Term, rhs: term.Term) std.Io.Writer.Error!void {
137 try writer.print("({s} ", .{name});
138 try writeTerm(writer, ctx, lhs);
139 try writer.writeAll(" ");
140 try writeTerm(writer, ctx, rhs);
141 try writer.writeAll(")");
142 }
143
144 fn writeTernary(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, first: term.Term, second: term.Term, third: term.Term) std.Io.Writer.Error!void {
145 try writer.print("({s} ", .{name});
146 try writeTerm(writer, ctx, first);
147 try writer.writeAll(" ");
148 try writeTerm(writer, ctx, second);
149 try writer.writeAll(" ");
150 try writeTerm(writer, ctx, third);
151 try writer.writeAll(")");
152 }
153
154 fn writeExtract(writer: *std.Io.Writer, ctx: *const term.Context, operand: term.Term, high: u32, low: u32) std.Io.Writer.Error!void {
155 try writer.print("((_ extract {d} {d}) ", .{ high, low });
156 try writeTerm(writer, ctx, operand);
157 try writer.writeAll(")");
158 }
159
160 fn writeExtension(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, operand: term.Term, extra: u32) std.Io.Writer.Error!void {
161 try writer.print("((_ {s} {d}) ", .{ name, extra });
162 try writeTerm(writer, ctx, operand);
163 try writer.writeAll(")");
164 }
165
166 fn writeNary(writer: *std.Io.Writer, ctx: *const term.Context, name: []const u8, operands: []const term.Term) std.Io.Writer.Error!void {
167 if (operands.len == 0) {
168 try writer.writeAll(if (std.mem.eql(u8, name, "and")) "true" else "false");
169 return;
170 }
171 if (operands.len == 1) {
172 try writeTerm(writer, ctx, operands[0]);
173 return;
174 }
175 try writer.print("({s}", .{name});
176 for (operands) |operand| {
177 try writer.writeAll(" ");
178 try writeTerm(writer, ctx, operand);
179 }
180 try writer.writeAll(")");
181 }
182
183 test "SMT-LIB writer emits declarations and assertions" {
184 var ctx = term.Context.init(std.testing.allocator);
185 defer ctx.deinit();
186 var script = term.Script.init(&ctx, "QF_LIA");
187 defer script.deinit();
188 const x = try ctx.symbol("x", .int);
189 const zero = try ctx.intValue(0);
190 try script.assertTerm(try ctx.ge(x, zero));
191 var buffer: [512]u8 = undefined;
192 var stream = std.Io.Writer.fixed(&buffer);
193 try writeScript(&stream, &script);
194 const text = stream.buffered();
195 try std.testing.expect(std.mem.indexOf(u8, text, "(set-logic QF_LIA)\n") != null);
196 try std.testing.expect(std.mem.indexOf(u8, text, "(declare-const x Int)\n") != null);
197 try std.testing.expect(std.mem.indexOf(u8, text, "(assert (>= x 0))\n") != null);
198 }