lib/smt/src/proof.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! A plain-text format for the evidence behind one unsatisfiable answer, with a writer and a
2 //! reader. The text writes each literal as a signed variable number counted from 1, as the DIMACS
3 //! CNF clause format does.
4 //!
5 //! A caller that reports an unsatisfiable answer needs to keep its evidence after the solver is
6 //! gone, and to hand it to a checker that does not trust the solver. A reader of such a text needs
7 //! every count and literal checked before a checker walks it. Each proof step is a clause that
8 //! follows from the clauses before it by unit propagation, so the evidence has to carry the
9 //! starting clauses, the assumptions and the steps in order.
10 //!
11 //! The text holds the clauses, assumptions and steps behind one unsatisfiable answer (*proof
12 //! artifact*, `sat.ProofArtifact`). The first line names the format and its version, 1. The header
13 //! line `p rup V C A S` gives the variable count and the numbers of starting clauses, assumptions
14 //! and steps. After the header, each line holds one letter, a list of literals, then 0 (*record*).
15 //! A `b` record is a starting clause, the single `a` record lists the assumptions, and each `r`
16 //! record is one step. The starting clauses are every clause the solver held when the solve began,
17 //! learned clauses it kept included. The reader checks the format and the counts, and
18 //! `sat.ProofArtifact.valid` checks the steps.
19 const std = @import("std");
20 const sat = @import("sat/root.zig");
21
22 /// Errors `parse` returns for a malformed text, besides the allocator's, so code that reports why a
23 /// proof text was refused switches on them.
24 pub const ParseError = error{
25 /// The first non-blank line does not name this format and version 1, or the text is empty.
26 InvalidMagic,
27 /// A `p` line whose kind differs from `rup`, whose counts are other than unsigned numbers, or
28 /// that holds other than four counts.
29 InvalidHeader,
30 /// A second `p` line.
31 DuplicateHeader,
32 /// A record comes before any header, or the text has no header.
33 MissingHeader,
34 /// A line that starts with a letter other than `b`, `a` or `r`, a second `a` record, or a token
35 /// after the closing 0 of a record.
36 InvalidRecord,
37 /// A record token other than a 32-bit signed integer.
38 InvalidLiteral,
39 /// A record with no closing 0.
40 UnterminatedRecord,
41 /// The number of `b` records differs from the header's clause count.
42 ClauseCountMismatch,
43 /// The number of literals in the `a` record differs from the header's assumption count.
44 AssumptionCountMismatch,
45 /// The number of `r` records differs from the header's step count.
46 StepCountMismatch,
47 /// A literal names a variable at or above the header's variable count.
48 InvalidVariable,
49 };
50
51 const magic = "tiny-smt-proof";
52 const version = "1";
53
54 /// Writes `artifact` in the proof format: the format line, the header, one `b` record per starting
55 /// clause, one `a` record, and one `r` record per step. Code keeps with it the evidence of an
56 /// unsatisfiable answer, after reading the artifact from the solver's `lastProofArtifact`. The call
57 /// always writes the `a` record, as `a 0` when there are no assumptions. The call returns only the
58 /// writer's errors.
59 pub fn write(writer: *std.Io.Writer, artifact: *const sat.ProofArtifact) std.Io.Writer.Error!void {
60 try writer.print("{s} {s}\n", .{ magic, version });
61 try writer.print("p rup {d} {d} {d} {d}\n", .{
62 artifact.variable_count,
63 artifact.clauses.items.len,
64 artifact.assumptions.items.len,
65 artifact.steps.items.len,
66 });
67 for (artifact.clauses.items) |clause| {
68 try writeLiteralRecord(writer, "b", clause.literals);
69 }
70 try writeLiteralRecord(writer, "a", artifact.assumptions.items);
71 for (artifact.steps.items) |step| {
72 try writeLiteralRecord(writer, "r", step.literals);
73 }
74 }
75
76 /// Returns a `sat.ProofArtifact` that allocates with `allocator` and holds the records of the proof
77 /// text `source`, so code reads stored evidence and then checks the result with `valid`. The caller
78 /// owns the artifact and frees it with `deinit`. Lines are trimmed of spaces, tabs and carriage
79 /// returns, and blank lines are skipped. A record is one line: it cannot span lines, and the format
80 /// has no comment lines. The `a` record is optional, and a text without it has no assumptions. The
81 /// call returns each `ParseError` tag as that tag describes. The literal -2147483648 makes it
82 /// panic. The parser checks the format and the counts, and it does not check that the steps follow.
83 pub fn parse(allocator: std.mem.Allocator, source: []const u8) !sat.ProofArtifact {
84 var artifact = sat.ProofArtifact.init(allocator, 0);
85 errdefer artifact.deinit();
86 var magic_seen = false;
87 var header_seen = false;
88 var expected_clauses: usize = 0;
89 var expected_assumptions: usize = 0;
90 var expected_steps: usize = 0;
91 var clauses_seen: usize = 0;
92 var assumptions_seen: usize = 0;
93 var steps_seen: usize = 0;
94 var assumption_record_seen = false;
95 var lines = std.mem.splitScalar(u8, source, '\n');
96 while (lines.next()) |raw_line| {
97 const line = std.mem.trim(u8, raw_line, " \t\r");
98 if (line.len == 0) continue;
99 var tokens = std.mem.tokenizeAny(u8, line, " \t\r");
100 const first = tokens.next() orelse continue;
101 if (!magic_seen) {
102 if (!std.mem.eql(u8, first, magic)) return ParseError.InvalidMagic;
103 const found_version = tokens.next() orelse return ParseError.InvalidMagic;
104 if (!std.mem.eql(u8, found_version, version)) return ParseError.InvalidMagic;
105 if (tokens.next() != null) return ParseError.InvalidMagic;
106 magic_seen = true;
107 continue;
108 }
109 if (std.mem.eql(u8, first, "p")) {
110 if (header_seen) return ParseError.DuplicateHeader;
111 const kind = tokens.next() orelse return ParseError.InvalidHeader;
112 if (!std.mem.eql(u8, kind, "rup")) return ParseError.InvalidHeader;
113 artifact.variable_count = try parseHeaderCount(tokens.next() orelse return ParseError.InvalidHeader);
114 expected_clauses = try parseHeaderCount(tokens.next() orelse return ParseError.InvalidHeader);
115 expected_assumptions = try parseHeaderCount(tokens.next() orelse return ParseError.InvalidHeader);
116 expected_steps = try parseHeaderCount(tokens.next() orelse return ParseError.InvalidHeader);
117 if (tokens.next() != null) return ParseError.InvalidHeader;
118 header_seen = true;
119 continue;
120 }
121 if (!header_seen) return ParseError.MissingHeader;
122 if (std.mem.eql(u8, first, "b")) {
123 const literals = try parseLiteralRecord(allocator, artifact.variable_count, &tokens);
124 defer allocator.free(literals);
125 try artifact.appendClause(literals);
126 clauses_seen += 1;
127 } else if (std.mem.eql(u8, first, "a")) {
128 if (assumption_record_seen) return ParseError.InvalidRecord;
129 const literals = try parseLiteralRecord(allocator, artifact.variable_count, &tokens);
130 defer allocator.free(literals);
131 try artifact.appendAssumptions(literals);
132 assumptions_seen += literals.len;
133 assumption_record_seen = true;
134 } else if (std.mem.eql(u8, first, "r")) {
135 const literals = try parseLiteralRecord(allocator, artifact.variable_count, &tokens);
136 defer allocator.free(literals);
137 try artifact.appendStep(literals);
138 steps_seen += 1;
139 } else {
140 return ParseError.InvalidRecord;
141 }
142 }
143 if (!magic_seen) return ParseError.InvalidMagic;
144 if (!header_seen) return ParseError.MissingHeader;
145 if (clauses_seen != expected_clauses) return ParseError.ClauseCountMismatch;
146 if (assumptions_seen != expected_assumptions) return ParseError.AssumptionCountMismatch;
147 if (steps_seen != expected_steps) return ParseError.StepCountMismatch;
148 return artifact;
149 }
150
151 fn writeLiteralRecord(writer: *std.Io.Writer, prefix: []const u8, literals: []const sat.Literal) std.Io.Writer.Error!void {
152 try writer.writeAll(prefix);
153 for (literals) |literal| {
154 try writer.print(" {d}", .{literal.toDimacs()});
155 }
156 try writer.writeAll(" 0\n");
157 }
158
159 fn parseHeaderCount(token: []const u8) !usize {
160 return std.fmt.parseInt(usize, token, 10) catch ParseError.InvalidHeader;
161 }
162
163 fn parseLiteralRecord(allocator: std.mem.Allocator, variable_count: usize, tokens: anytype) ![]sat.Literal {
164 var literals: std.ArrayList(sat.Literal) = .empty;
165 errdefer literals.deinit(allocator);
166 var terminated = false;
167 while (tokens.next()) |token| {
168 const value = std.fmt.parseInt(i32, token, 10) catch return ParseError.InvalidLiteral;
169 if (value == 0) {
170 terminated = true;
171 if (tokens.next() != null) return ParseError.InvalidRecord;
172 break;
173 }
174 const literal = sat.Literal.fromDimacs(value) catch return ParseError.InvalidLiteral;
175 if (literal.variable() >= variable_count) return ParseError.InvalidVariable;
176 try literals.append(allocator, literal);
177 }
178 if (!terminated) return ParseError.UnterminatedRecord;
179 return literals.toOwnedSlice(allocator);
180 }
181
182 test "proof artifact format roundtrips valid unsat evidence" {
183 var solver = sat.Solver.init(std.testing.allocator);
184 defer solver.deinit();
185 const a = try solver.addVariable();
186 const b = try solver.addVariable();
187 try solver.addClause(&.{ sat.Literal.positive(a), sat.Literal.positive(b) });
188 try solver.addClause(&.{ sat.Literal.negative(a), sat.Literal.positive(b) });
189 try solver.addClause(&.{ sat.Literal.positive(a), sat.Literal.negative(b) });
190 try solver.addClause(&.{ sat.Literal.negative(a), sat.Literal.negative(b) });
191 try std.testing.expectEqual(sat.Status.unsat, try solver.solve());
192 var artifact = (try solver.lastProofArtifact(std.testing.allocator)).?;
193 defer artifact.deinit();
194 var out: std.Io.Writer.Allocating = .init(std.testing.allocator);
195 defer out.deinit();
196 try write(&out.writer, &artifact);
197 var parsed = try parse(std.testing.allocator, out.written());
198 defer parsed.deinit();
199 try std.testing.expectEqual(artifact.variable_count, parsed.variable_count);
200 try std.testing.expectEqual(artifact.clauses.items.len, parsed.clauses.items.len);
201 try std.testing.expectEqual(artifact.assumptions.items.len, parsed.assumptions.items.len);
202 try std.testing.expectEqual(artifact.steps.items.len, parsed.steps.items.len);
203 try std.testing.expect(try parsed.valid());
204 }
205
206 test "proof artifact parser rejects mismatched counts" {
207 try std.testing.expectError(ParseError.ClauseCountMismatch, parse(std.testing.allocator,
208 \\tiny-smt-proof 1
209 \\p rup 1 1 0 1
210 \\r 0
211 \\
212 ));
213 }
214
215 test "proof artifact parser rejects unknown variables" {
216 try std.testing.expectError(ParseError.InvalidVariable, parse(std.testing.allocator,
217 \\tiny-smt-proof 1
218 \\p rup 1 0 0 1
219 \\r 2 0
220 \\
221 ));
222 }