tiny.smt.ConflictScratch

1/// Scratch memory for one conflict analysis at a time, in storage its caller hands over: a buffer2/// of up to one literal per variable and one mark bit per variable. The solver builds one over the3/// tail of its trail allocation at the start of each solve and takes a loan from it for each4/// conflict it analyzes. `init` takes the storage, `activate` moves the scratch from5/// `.initialization` to `.steady`, and `deinit` moves it to `.teardown` and returns the storage.6/// The scratch calls no allocator. One loan is out at a time, and every loan function refuses a7/// released or copied loan.8pub const ConflictScratch = struct {9    /// The errors that `acquire`, `release` and the loan functions return. The solver's conflict10    /// analysis passes them up with `try`, so they belong to the errors a solve can return. Each11    /// error is returned before any change to the scratch.12    pub const Exhaustion = error{13        /// `acquire` was called while a loan is out.14        ConflictScratchInUse,15        /// `acquire` asked for more variables than the scratch covers, or `Loan.append` or16        /// `Loan.recordResolution` went past the loan's variable count.17        ConflictScratchCapacityExceeded,18        /// `acquire` found the loan counter at the largest `u64`.19        ConflictScratchLoanEpochExhausted,20        /// A loan function or `release` got a loan that is released, a copy at another address,21        /// from a scratch outside `.steady`, or from another scratch.22        ConflictScratchStaleLoan,23    };2425    /// A compile-time record of the scratch's memory: what the storage covers, what stays outside26    /// it, the equation that sizes it from `Limits`, the refusal behavior, the work bound, and the27    /// tests that witness each obligation. The shape check at the end of the file validates the28    /// record and the scratch's shape at compile time. The equation gives the variable count times29    /// the size of a literal, plus the variable count divided by 8 and rounded up, in bytes. The30    /// record states that short storage, oversize use, an exhausted loan counter, copied loans and31    /// overlapping loans are refused before the caller's storage or the scratch changes. The record32    /// states the work bound: taking a loan clears at most one byte per 8 variables, and an33    /// analysis takes at most one resolution step per variable. The learned clauses the solver34    /// keeps, the trail's own entries, the clauses, the watch lists, the search state and the proof35    /// steps stay outside the storage.36    pub const claim: alloc_phase.capacity.Declaration = .{37        .source = .{38            .id = "smt.conflict_scratch",39            .kind = .phase_static,40            .limit_source = .caller,41            .storage = .{42                .covered = &.{43                    .{44                        .id = "conflict_analysis_learned_literal_scratch",45                        .lifetime = .transferred,46                        .detail = "one learned literal per admitted solver variable in the exact trail-tail storage transferred by the caller",47                    },48                    .{49                        .id = "conflict_analysis_seen_variable_scratch",50                        .lifetime = .transferred,51                        .detail = "one dense seen bit per admitted solver variable in the exact trail-tail storage transferred by the caller",52                    },53                },54                .excluded = &.{55                    "retained learned-clause literals copied by addLearnedClause",56                    "the primary trail prefix, rounded tail padding, original clauses, clause headers, watch lists, and search state",57                    "proof trace steps and reverse-unit-propagation assignment state",58                    "old plus new trail backing overlap while variable growth establishes a larger admitted solve workspace",59                },60            },61            .capacity = .{62                .inputs = &.{63                    alloc_phase.capacity.bindInput(Limits, "variables", "variables"),64                },65                .type_selectors = &.{66                    alloc_phase.capacity.bindType(Literal, "literal"),67                },68                .nodes = &.{69                    .{ .input = 0 },70                    .{ .scale = .{ .node = 0, .coefficient = .{ .size_of_concrete_type = 0 } } },71                    .{ .constant = 8 },72                    .{ .ceiling_division = .{ .left = 0, .right = 2 } },73                    .{ .add = .{ .left = 1, .right = 3 } },74                },75                .assertions = &.{.{76                    .scope = .closure_total,77                    .measure = .retained,78                    .relation = .exact,79                    .expression = 4,80                }},81            },82            .overload = .{83                .kind = .reject_before_mutation,84                .detail = "short storage, oversize use, epoch exhaustion, copied tokens, and overlapping address-bound affine loans fail before caller storage or ownership state changes",85            },86            .risks = .{87                .transitive = .{88                    .status = .open,89                    .detail = "learnFromConflict uses one address-bound epoch loan within stable token-storage and owner lifetimes and bounded SAT properties check status, proof, core, and learned-clause semantics; retained learned-clause copies remain a separate owner",90                },91                .foreign = .{92                    .status = .excluded,93                    .detail = "the exact transferred trail tail is process-local memory and conflict analysis crosses no operating-system or foreign-runtime edge",94                },95            },96            .work = .{97                .equation = "initialization <= 1, acquire clearing <= ceil(variables / 8), and resolution steps <= variables",98            },99            .obligations = &.{100                .{ .key = "smt_conflict_scratch_capacity", .role = .capacity_model },101                .{ .key = "smt_conflict_scratch_acquisition", .role = .custom },102                .{ .key = "smt_conflict_scratch_storage_identity", .role = .foreign_risk },103                .{ .key = "smt_conflict_scratch_overload", .role = .overload },104                .{ .key = "smt_conflict_scratch_reuse", .role = .overload },105                .{ .key = "smt_conflict_scratch_work_bound", .role = .work_bound },106                .{ .key = "smt_conflict_scratch_solver_admission", .role = .overload },107                .{ .key = "smt_conflict_scratch_solver_semantics", .role = .transitive_risk },108                .{ .key = "smt_conflict_scratch_foreign_risk", .role = .foreign_risk },109            },110        },111        .bindings = .{112            .owner = @This(),113            .seal = .{114                .family = alloc_phase.capacity.selector(@This().activate),115                .premise = .{116                    .class = .checked_semantic_fact,117                    .authority = .checker,118                },119            },120            .teardown = .{121                .family = alloc_phase.capacity.selector(@This().deinit),122                .premise = .{123                    .class = .checked_semantic_fact,124                    .authority = .checker,125                },126            },127        },128    };129130    /// The alignment the caller's storage needs, equal to the alignment of a literal. A caller131    /// aligns a buffer of its own to this value before it hands the buffer to `init`.132    pub const storage_alignment: usize = @alignOf(Literal);133    /// The byte slice a scratch takes from its caller, aligned for literals. A caller passes one to134    /// `init` and gets the same one back from `deinit`.135    pub const Storage = []align(storage_alignment) u8;136    /// The errors of `init`: `error.CapacityOverflow` from `Capacity.derive`, and137    /// `error.StorageLengthMismatch` when the storage length differs from `Capacity.storage_bytes`.138    /// The solver passes them up from the start of a solve.139    pub const InitError = Capacity.DeriveError || error{StorageLengthMismatch};140    /// Work bounds that the shape check reads: any number of setup steps, and zero cleanup steps141    /// per call. The shape check at the end of the file requires it beside the record in `claim`.142    pub const work_limits: alloc_phase.capacity.WorkLimits = .{143        .transition_steps_max = std.math.maxInt(usize),144        .cleanup_steps_per_call_max = 0,145        .cleanup_calls_at_capacity_max = 0,146    };147148    phase: alloc_phase.capacity.Phase,149    /// The sizes `Capacity.derive` gave for the limits passed to `init`. `admits` and `acquire`150    /// compare with its variable count, and the solver reads it to find the storage again at each151    /// analysis.152    capacity: Capacity,153    /// The storage passed to `init`, which `deinit` returns. The literal buffer starts at its first154    /// byte, and the mark bits start at `Capacity.seen_offset`. The solver checks at each analysis155    /// that it still matches the tail of the trail allocation.156    storage: Storage,157    literals: []Literal,158    seen: []u8,159    loaned: bool = false,160    loan_epoch: u64 = 0,161    loan_identity: usize = 0,162    loan_variables: usize = 0,163    loan_literal_count: usize = 0,164    loan_resolution_steps: usize = 0,165166    /// The input that sizes a scratch: its variable count. The solver builds one from the variable167    /// count a solve needs, counting every variable its assumptions name.168    pub const Limits = struct {169        /// The number of variables the scratch covers.170        variables: usize,171172        /// Returns the limits for `variables`. The solver builds its scratch limits through it.173        pub fn inspect(variables: usize) Limits {174            return .{ .variables = variables };175        }176    };177178    /// The sizes of one scratch and of the trail allocation that holds it, in bytes and in179    /// literals. The solver derives it at the start of each solve to size its trail allocation and180    /// to find the scratch storage inside it.181    pub const Capacity = struct {182        /// The variable count from the limits, which is the most literals and marks a loan uses.183        variables: usize,184        /// Bytes of the literal buffer: the variable count times the size of a literal.185        literal_bytes: usize,186        /// The byte offset of the mark bits in the storage, equal to `literal_bytes`.187        seen_offset: usize,188        /// Bytes of mark bits: the variable count divided by 8, rounded up.189        seen_bytes: usize,190        /// Bytes of storage: `literal_bytes` plus `seen_bytes`. `init` refuses storage of any other191        /// length.192        storage_bytes: usize,193        /// The storage size in literals, rounded up, which is the number of trail entries the194        /// solver sets aside for the scratch.195        backing_literals: usize,196        /// The trail allocation the solver needs, in literals: the variable count plus197        /// `backing_literals`.198        trail_capacity: usize,199200        /// The error of `derive`: `error.CapacityOverflow`. `init` and the solver pass it up before201        /// anything is allocated.202        pub const DeriveError = error{CapacityOverflow};203204        /// Returns the sizes for `limits`. The solver sizes its trail allocation from it before a205        /// solve, and `init` checks the storage length against it. The call returns206        /// `error.CapacityOverflow` when the literal bytes, the storage bytes or the trail207        /// allocation overflows `usize`.208        pub fn derive(limits: Limits) DeriveError!Capacity {209            const literal_bytes = std.math.mul(210                usize,211                limits.variables,212                @sizeOf(Literal),213            ) catch return error.CapacityOverflow;214            const seen_bytes = limits.variables / 8 +215                @intFromBool(limits.variables % 8 != 0);216            const storage_bytes = std.math.add(217                usize,218                literal_bytes,219                seen_bytes,220            ) catch return error.CapacityOverflow;221            const backing_literals = storage_bytes / @sizeOf(Literal) +222                @intFromBool(storage_bytes % @sizeOf(Literal) != 0);223            const trail_capacity = std.math.add(224                usize,225                limits.variables,226                backing_literals,227            ) catch return error.CapacityOverflow;228            assert(literal_bytes % @alignOf(Literal) == 0);229            return .{230                .variables = limits.variables,231                .literal_bytes = literal_bytes,232                .seen_offset = literal_bytes,233                .seen_bytes = seen_bytes,234                .storage_bytes = storage_bytes,235                .backing_literals = backing_literals,236                .trail_capacity = trail_capacity,237            };238        }239    };240241    /// A handle to the scratch memory for one conflict analysis, which reaches the scratch's242    /// literal buffer and marks and holds the scratch's address and the loan's number. The solver's243    /// conflict analysis takes one per conflict with `acquire`, marks the variables it meets,244    /// collects the learned clause's literals, and hands the loan back with `release`. Every loan245    /// function checks the loan first and returns `error.ConflictScratchStaleLoan` when the loan246    /// was released, when a later `acquire` replaced it, when it is a copy at another address, or247    /// when the scratch is outside `.steady`. The loan stays valid only at the address `acquire`248    /// filled, so the caller keeps it in place until `release`.249    pub const Loan = struct {250        const BitPosition = struct {251            byte: usize,252            mask: u8,253        };254255        owner: *ConflictScratch,256        epoch: u64,257258        /// Marks `variable_index` as met and returns true, or returns false when it was already259        /// marked. The analysis calls it on each literal of a clause it resolves on, and a false260        /// result skips a variable it has already counted. The call asserts that `variable_index`261        /// is below the loan's variable count. The call returns `error.ConflictScratchStaleLoan`262        /// for a stale loan.263        pub fn markSeen(self: *const Loan, variable_index: u32) Exhaustion!bool {264            const owner = try self.ownerFor();265            assert(variable_index < owner.loan_variables);266            const bit = bitPosition(variable_index);267            if (owner.seen[bit.byte] & bit.mask != 0) return false;268            owner.seen[bit.byte] |= bit.mask;269            return true;270        }271272        /// Removes the mark from `variable_index`. The analysis unmarks the variable it resolves on273        /// at each step. The call asserts that `variable_index` is below the loan's variable count274        /// and is marked. The call returns `error.ConflictScratchStaleLoan` for a stale loan.275        pub fn clearSeen(self: *const Loan, variable_index: u32) Exhaustion!void {276            const owner = try self.ownerFor();277            assert(variable_index < owner.loan_variables);278            const bit = bitPosition(variable_index);279            assert(owner.seen[bit.byte] & bit.mask != 0);280            owner.seen[bit.byte] &= ~bit.mask;281        }282283        /// Returns true when `variable_index` is marked. The analysis walks the trail backward and284        /// stops at the first marked variable. The call asserts that `variable_index` is below the285        /// loan's variable count. The call returns `error.ConflictScratchStaleLoan` for a stale286        /// loan.287        pub fn isSeen(self: *const Loan, variable_index: u32) Exhaustion!bool {288            const owner = try self.ownerFor();289            assert(variable_index < owner.loan_variables);290            const bit = bitPosition(variable_index);291            return owner.seen[bit.byte] & bit.mask != 0;292        }293294        /// Adds `literal` after the loan's earlier literals. The analysis adds each literal of the295        /// learned clause through it. The call returns `error.ConflictScratchCapacityExceeded` when296        /// the loan already holds its variable count of literals, and297        /// `error.ConflictScratchStaleLoan` for a stale loan, before any change.298        pub fn append(self: *const Loan, literal: Literal) Exhaustion!void {299            const owner = try self.ownerFor();300            if (owner.loan_literal_count == owner.loan_variables) {301                return error.ConflictScratchCapacityExceeded;302            }303            owner.literals[owner.loan_literal_count] = literal;304            owner.loan_literal_count += 1;305        }306307        /// Counts one resolution step. The analysis calls it at the start of each resolution step.308        /// The call returns `error.ConflictScratchCapacityExceeded` when the loan has already309        /// counted its variable count of steps, and `error.ConflictScratchStaleLoan` for a stale310        /// loan, before counting.311        pub fn recordResolution(self: *const Loan) Exhaustion!void {312            const owner = try self.ownerFor();313            if (owner.loan_resolution_steps == owner.loan_variables) {314                return error.ConflictScratchCapacityExceeded;315            }316            owner.loan_resolution_steps += 1;317        }318319        /// Returns the literals added since `acquire`, in order. The analysis reads the learned320        /// clause through it when the resolution ends. The slice points into the scratch storage,321        /// so literals added under a later loan overwrite it. The call returns322        /// `error.ConflictScratchStaleLoan` for a stale loan.323        pub fn literals(self: *const Loan) Exhaustion![]const Literal {324            const owner = try self.ownerFor();325            assert(owner.loan_literal_count <= owner.loan_variables);326            return owner.literals[0..owner.loan_literal_count];327        }328329        fn ownerFor(self: *const Loan) Exhaustion!*ConflictScratch {330            const owner = self.owner;331            if (owner.phase != .steady or332                !owner.loaned or333                owner.loan_epoch != self.epoch or334                owner.loan_identity != @intFromPtr(self))335            {336                return error.ConflictScratchStaleLoan;337            }338            return owner;339        }340341        fn bitPosition(variable_index: u32) BitPosition {342            return .{343                .byte = variable_index / 8,344                .mask = @as(u8, 1) << @intCast(variable_index % 8),345            };346        }347    };348349    /// Returns a scratch in `.initialization` over `storage`, sized for `limits`. The solver builds350    /// one over the tail of its trail allocation at the start of each solve that has at least one351    /// variable. The call returns `error.CapacityOverflow` from `Capacity.derive`, and352    /// `error.StorageLengthMismatch` when `storage` is shorter or longer than353    /// `Capacity.storage_bytes`. On either error, `storage` stays unchanged and stays with the354    /// caller. The scratch holds `storage` until `deinit` returns it.355    pub fn init(storage: Storage, limits: Limits) InitError!ConflictScratch {356        const capacity = try Capacity.derive(limits);357        if (storage.len != capacity.storage_bytes) {358            return error.StorageLengthMismatch;359        }360        const owned = storage;361        const literals = typedSlice(Literal, owned, 0, capacity.variables);362        const seen = owned[capacity.seen_offset..][0..capacity.seen_bytes];363        assert(literals.len * @sizeOf(Literal) == capacity.literal_bytes);364        assert(seen.len == capacity.seen_bytes);365        return .{366            .phase = .initialization,367            .capacity = capacity,368            .storage = owned,369            .literals = literals,370            .seen = seen,371        };372    }373374    /// Moves the scratch from `.initialization` to `.steady`, after which `acquire` can hand out375    /// loans. The solver calls it once, right after `init`. The call asserts that the scratch is as376    /// `init` left it.377    pub fn activate(self: *ConflictScratch) void {378        assert(self.phase == .initialization);379        assert(self.storage.len == self.capacity.storage_bytes);380        assert(!self.loaned);381        assert(self.loan_identity == 0);382        assert(self.loan_variables == 0);383        assert(self.loan_literal_count == 0);384        assert(self.loan_resolution_steps == 0);385        self.phase = .steady;386    }387388    /// Returns true when the scratch covers at least `required.variables` variables. A caller that389    /// holds a scratch checks with it whether the scratch covers a variable count before reusing390    /// the scratch for that count. The solver builds a new scratch at each solve, so the package391    /// itself makes no call to it. The call asserts that the scratch is `.steady`.392    pub fn admits(self: *const ConflictScratch, required: Capacity) bool {393        assert(self.phase == .steady);394        return self.capacity.variables >= required.variables;395    }396397    /// Clears the marks and fills `loan` as the one loan out, covering `variables` variables. The398    /// analysis takes a loan with it at the start of each conflict it analyzes. The call returns399    /// `error.ConflictScratchInUse` while another loan is out,400    /// `error.ConflictScratchCapacityExceeded` when `variables` passes the scratch's variable401    /// count, and `error.ConflictScratchLoanEpochExhausted` when the loan counter is at the largest402    /// `u64`. Each error leaves the scratch and its marks as they were. The call clears every mark403    /// byte, at most one byte per 8 variables of the scratch. The call records the address of404    /// `loan`, so the caller keeps `loan` in place until `release`. The call asserts that the405    /// scratch is `.steady`.406    pub fn acquire(407        self: *ConflictScratch,408        variables: usize,409        loan: *Loan,410    ) Exhaustion!void {411        assert(self.phase == .steady);412        if (self.loaned) return error.ConflictScratchInUse;413        if (variables > self.capacity.variables) {414            return error.ConflictScratchCapacityExceeded;415        }416        const epoch = std.math.add(u64, self.loan_epoch, 1) catch {417            return error.ConflictScratchLoanEpochExhausted;418        };419        @memset(self.seen, 0);420        loan.* = .{421            .owner = self,422            .epoch = epoch,423        };424        self.loaned = true;425        self.loan_epoch = epoch;426        self.loan_identity = @intFromPtr(loan);427        self.loan_variables = variables;428        self.loan_literal_count = 0;429        self.loan_resolution_steps = 0;430    }431432    /// Ends the current loan, so `acquire` can hand out the next one. The analysis releases its433    /// loan when it returns, whether it learned a clause or failed. The call returns434    /// `error.ConflictScratchStaleLoan` when `loan` is stale or comes from another scratch, and435    /// then the current loan stays out. Every loan function refuses `loan` after the call. The call436    /// asserts that the scratch is `.steady`.437    pub fn release(self: *ConflictScratch, loan: *const Loan) Exhaustion!void {438        assert(self.phase == .steady);439        const owner = try loan.ownerFor();440        if (owner != self) return error.ConflictScratchStaleLoan;441        assert(self.loan_literal_count <= self.loan_variables);442        assert(self.loan_resolution_steps <= self.loan_variables);443        self.loaned = false;444        self.loan_identity = 0;445        self.loan_variables = 0;446        self.loan_literal_count = 0;447        self.loan_resolution_steps = 0;448    }449450    /// Moves the scratch to `.teardown`, returns the storage passed to `init`, and leaves the451    /// scratch undefined. The solver calls it when a solve ends and checks that the storage came452    /// back with the same address and length. The call asserts that no loan is out. The call works453    /// from `.initialization` or `.steady`.454    pub fn deinit(self: *ConflictScratch) Storage {455        assert(self.phase != .teardown);456        assert(!self.loaned);457        assert(self.loan_identity == 0);458        assert(self.loan_variables == 0);459        assert(self.loan_literal_count == 0);460        assert(self.loan_resolution_steps == 0);461        assert(self.storage.len == self.capacity.storage_bytes);462        self.phase = .teardown;463        const storage = self.storage;464        self.* = undefined;465        return storage;466    }467};

1pub const ConflictScratch = sat.ConflictScratch;