tiny.smt.ProofArtifact

1/// The clauses, assumptions and steps behind one unsatisfiable answer, copied out of the solver and2/// owned by the caller. A caller keeps it as the evidence of an unsatisfiable answer after the3/// solver moves on, checks it with `valid`, and writes it out as text. A proof reader and tests4/// also build artifacts by hand with `init` and the append functions. The artifact allocates every5/// copy with the allocator given to `init` and frees them in `deinit`. The artifact shares no6/// memory with the solver, so it stays usable after the solver changes or is freed.7pub const ProofArtifact = struct {8    allocator: std.mem.Allocator,9    /// The number of variables the artifact covers. Every literal has to name a variable below it,10    /// or `valid` returns false. `Solver.lastProofArtifact` sets it to the solver's variable count.11    variable_count: usize,12    /// The starting clauses, in order. From `Solver.lastProofArtifact` they are every clause the13    /// solver held when the solve began, learned clauses it kept included, then an empty clause14    /// when the caller had added one. `appendClause` adds one at the end.15    clauses: std.ArrayList(ProofClause) = .empty,16    /// The literals assumed true for the refutation. From `Solver.lastProofArtifact` they are the17    /// solve's assumptions, cut down to the smaller set that core minimization certified when it18    /// finished. They can be more than `Solver.lastUnsatCore` reports, because the artifact keeps19    /// every assumption of the solve unless core minimization certified a smaller set. When the20    /// clauses were refuted before the search began, as by two opposite unit clauses, the core is21    /// empty and the artifact keeps every assumption. When a conflict comes while the solver22    /// assigns the first of two or more assumptions, the core holds that one assumption, core23    /// minimization leaves it as it is, and the artifact keeps every assumption. When a conflict24    /// limit runs out during the certifying solve of core minimization, the core is empty and the25    /// artifact keeps every assumption.26    assumptions: std.ArrayList(Literal) = .empty,27    /// The proof steps in order, each checked against the starting clauses, the assumptions and the28    /// steps before it. `appendStep` adds one at the end.29    steps: std.ArrayList(ProofStep) = .empty,3031    /// Returns an empty artifact over `variable_count` variables that allocates with `allocator`.32    /// Code that builds an artifact by hand, such as a proof reader, starts from it. The call33    /// allocates nothing.34    pub fn init(allocator: std.mem.Allocator, variable_count: usize) ProofArtifact {35        return .{ .allocator = allocator, .variable_count = variable_count };36    }3738    /// Frees every clause and step copy and the three lists with the artifact's allocator. The39    /// owner of an artifact calls it once, when it is done with the evidence. The artifact is40    /// undefined afterward.41    pub fn deinit(self: *ProofArtifact) void {42        for (self.clauses.items) |clause| {43            self.allocator.free(clause.literals);44        }45        self.clauses.deinit(self.allocator);46        self.assumptions.deinit(self.allocator);47        for (self.steps.items) |step| {48            self.allocator.free(step.literals);49        }50        self.steps.deinit(self.allocator);51        self.* = undefined;52    }5354    /// Copies `literals` and adds the copy as the last starting clause. A proof reader calls it55    /// once per starting clause, in file order. The caller keeps `literals`. The call returns56    /// `error.OutOfMemory` when the copy or the list growth fails, and then the artifact is as it57    /// was.58    pub fn appendClause(self: *ProofArtifact, literals: []const Literal) !void {59        const owned = try self.allocator.dupe(Literal, literals);60        errdefer self.allocator.free(owned);61        try self.clauses.append(self.allocator, .{ .literals = owned });62    }6364    /// Appends `literals` to the assumption list. A proof reader calls it for the assumption65    /// record, and `Solver.lastProofArtifact` calls it once with the solve's assumptions. Calls66    /// accumulate: each one appends after what earlier calls added. The call returns67    /// `error.OutOfMemory` when the list growth fails.68    pub fn appendAssumptions(self: *ProofArtifact, literals: []const Literal) !void {69        try self.assumptions.appendSlice(self.allocator, literals);70    }7172    /// Copies `literals` and adds the copy as the last proof step. A proof reader calls it once per73    /// step, in file order, and `Solver.lastProofArtifact` calls it once per step of the trace. The74    /// caller keeps `literals`. The call returns `error.OutOfMemory` when the copy or the list75    /// growth fails, and then the artifact is as it was.76    pub fn appendStep(self: *ProofArtifact, literals: []const Literal) !void {77        const owned = try self.allocator.dupe(Literal, literals);78        errdefer self.allocator.free(owned);79        try self.steps.append(self.allocator, .{ .literals = owned });80    }8182    /// Returns true when every step follows by unit propagation from the starting clauses, the83    /// assumptions and the steps before it, and the last step is the empty clause. A caller runs it84    /// to confirm an unsatisfiable answer independently of the solver that gave it. To check one85    /// step, the call assumes the assumptions true and the step's literals false, then propagates86    /// unit clauses over the starting clauses and the earlier steps until a clause becomes false87    /// (Reverse Unit Propagation). The step passes when a clause becomes false, and also when the88    /// assumptions clash with the negated step. The call returns false when the step list is empty,89    /// or when any literal names a variable at or above `variable_count`. A step may use only the90    /// steps before it, so a step that only a later step supports fails. Each step repeats the91    /// propagation over every starting clause and earlier step until a pass leaves every value as92    /// it was. The call allocates one truth value per variable with the artifact's allocator for93    /// its own duration, and `error.OutOfMemory` is its only error.94    pub fn valid(self: *const ProofArtifact) !bool {95        if (self.steps.items.len == 0) return false;96        if (!proofClausesUseKnownVariables(97            ProofClause,98            self.variable_count,99            self.clauses.items,100        )) return false;101        if (!proofLiteralsUseKnownVariables(102            self.variable_count,103            self.assumptions.items,104        )) return false;105        for (self.steps.items) |step| {106            if (!proofLiteralsUseKnownVariables(self.variable_count, step.literals)) return false;107        }108        const assignment = try self.allocator.alloc(BoolValue, self.variable_count);109        defer self.allocator.free(assignment);110        for (self.steps.items, 0..) |step, index| {111            if (!rupCheckKnownVariablesWithClauses(112                assignment,113                ProofClause,114                self.clauses.items,115                self.assumptions.items,116                self.steps.items,117                step.literals,118                index,119            )) return false;120        }121        return self.steps.items[self.steps.items.len - 1].literals.len == 0;122    }123};

1pub const ProofArtifact = sat.ProofArtifact;