tiny.smt.proof

1//! A plain-text format for the evidence behind one unsatisfiable answer, with a writer and a2//! reader. The text writes each literal as a signed variable number counted from 1, as the DIMACS3//! CNF clause format does.4//!5//! A caller that reports an unsatisfiable answer needs to keep its evidence after the solver is6//! gone, and to hand it to a checker that does not trust the solver. A reader of such a text needs7//! every count and literal checked before a checker walks it. Each proof step is a clause that8//! follows from the clauses before it by unit propagation, so the evidence has to carry the9//! starting clauses, the assumptions and the steps in order.10//!11//! The text holds the clauses, assumptions and steps behind one unsatisfiable answer (*proof12//! artifact*, `sat.ProofArtifact`). The first line names the format and its version, 1. The header13//! line `p rup V C A S` gives the variable count and the numbers of starting clauses, assumptions14//! 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, and18//! `sat.ProofArtifact.valid` checks the steps.19const std = @import("std");20const sat = @import("sat/root.zig");2122/// Errors `parse` returns for a malformed text, besides the allocator's, so code that reports why a23/// proof text was refused switches on them.24pub 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, or28    /// 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 token35    /// 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};5051const magic = "tiny-smt-proof";52const version = "1";5354/// Writes `artifact` in the proof format: the format line, the header, one `b` record per starting55/// clause, one `a` record, and one `r` record per step. Code keeps with it the evidence of an56/// unsatisfiable answer, after reading the artifact from the solver's `lastProofArtifact`. The call57/// always writes the `a` record, as `a 0` when there are no assumptions. The call returns only the58/// writer's errors.59pub 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}7576/// Returns a `sat.ProofArtifact` that allocates with `allocator` and holds the records of the proof77/// text `source`, so code reads stored evidence and then checks the result with `valid`. The caller78/// owns the artifact and frees it with `deinit`. Lines are trimmed of spaces, tabs and carriage79/// returns, and blank lines are skipped. A record is one line: it cannot span lines, and the format80/// has no comment lines. The `a` record is optional, and a text without it has no assumptions. The81/// call returns each `ParseError` tag as that tag describes. The literal -2147483648 makes it82/// panic. The parser checks the format and the counts, and it does not check that the steps follow.83pub 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}150151fn 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}158159fn parseHeaderCount(token: []const u8) !usize {160    return std.fmt.parseInt(usize, token, 10) catch ParseError.InvalidHeader;161}162163fn 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}181182test "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}205206test "proof artifact parser rejects mismatched counts" {207    try std.testing.expectError(ParseError.ClauseCountMismatch, parse(std.testing.allocator,208        \\tiny-smt-proof 1209        \\p rup 1 1 0 1210        \\r 0211        \\212    ));213}214215test "proof artifact parser rejects unknown variables" {216    try std.testing.expectError(ParseError.InvalidVariable, parse(std.testing.allocator,217        \\tiny-smt-proof 1218        \\p rup 1 0 0 1219        \\r 2 0220        \\221    ));222}

1pub const proof = @import("proof.zig");