tiny.smt.sat.store

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

1//! Fixed memory for the learned clauses a solver may remove under a cap, sized before a search and2//! reused slot by slot. A solver with a cap on learned clauses adds and removes clauses throughout3//! a search, and a caller that bounds memory wants that churn to stay inside memory whose size is4//! known before the search starts.5//!6//! Learned clauses differ in length, and each holds at most one literal per variable. The solver7//! keeps a clause that justifies a current value even when the cap asks for a removal, and it keeps8//! the clause learned most recently, so the count it holds can pass the cap.9//!10//! The store (`Store`) holds only the learned clauses whose literals span more than two decision11//! levels (*replaceable learned clauses*), and the other learned clauses stay in the solver's heap12//! memory, as every learned clause does while the cap is null. The store gives each clause one slot13//! as wide as the variable count, all in one block of literals (a slab), and keeps the numbers of14//! the free slots on a stack, so taking or returning a slot is constant work with no allocator15//! call. The slot count is the larger of the cap and one more than the variable count, plus 2,16//! which covers the clauses kept because they justify current values, the clause learned most17//! recently and one more. Taking a slot from a full store trips an assertion, because the slot18//! count is meant to rule that case out. When the cap or the variable count grows, the solver19//! builds a larger store and moves the stored clauses into it, and when the cap is removed it moves20//! them back to its heap. A compile-time record of this memory (`Store.claim`) states the size21//! equation and the overload behavior, and the shape check at the end of the file validates it.22const std = @import("std");23const alloc_phase = @import("alloc_phase");24const types = @import("types.zig");2526const assert = std.debug.assert;27const Allocator = std.mem.Allocator;28const Literal = types.Literal;2930/// Fixed memory for the replaceable learned clauses of one solver: equal slots in one slab of31/// literals, one clause per slot, with a stack of free slot numbers. The solver keeps one while32/// `Solver.max_learned_clauses` is set, and it moves each replaceable learned clause into it as the33/// clause is learned. `init` allocates the slab and the stack, `activate` moves the store from34/// `.initialization` to `.steady`, and `deinit` moves it to `.teardown` and frees both. In35/// `.steady`, taking and returning a slot is constant work and calls no allocator.36pub const Store = struct {37    /// A compile-time record of the store's memory: what the slab and the stack cover, what stays38    /// outside them, the equation that sizes them from `Limits`, the overload behavior, and the39    /// tests that witness each obligation. The shape check at the end of the file validates the40    /// record and the store's shape at compile time. The equation gives the slot count times the41    /// variable count in literals, plus one 32-bit stack entry per slot, with the slot count that42    /// `Capacity.derive` computes. The record states that an overflow is refused before any storage43    /// exists, and that taking a slot from a full store is a sizing bug that trips an assertion.44    /// Learned clauses whose literals span at most two decision levels, and the learned clauses of45    /// a solver whose cap is null, stay outside the store in the solver's heap memory.46    pub const claim: alloc_phase.capacity.Declaration = .{47        .source = .{48            .id = "smt.learned_store",49            .kind = .phase_static,50            .limit_source = .caller,51            .storage = .{52                .covered = &.{53                    .{54                        .id = "replaceable_learned_clause_literal_slab_of_slots_x_fc9c9a108360",55                        .lifetime = .steady,56                        .detail = "replaceable learned-clause literal slab of slots x variableCount literals",57                    },58                    .{59                        .id = "slot_free_list_stack",60                        .lifetime = .steady,61                        .detail = "slot free-list stack",62                    },63                },64                .excluded = &.{65                    "glue learned clauses (lbd <= 2): the monotone termination set stays heap-owned by design",66                    "original clauses, clause headers, watch lists, trail, and search state in solver-owned dynamic containers",67                    "proof assumptions and unbudgeted proof steps; budgeted step literal storage is owned by smt.proof_trace",68                    "learned clauses on solvers without max_learned_clauses, which keep stage-three heap semantics",69                },70            },71            .capacity = .{72                .inputs = &.{73                    alloc_phase.capacity.bindInput(Limits, "replaceable_clauses", "replaceable_clauses"),74                    alloc_phase.capacity.bindInput(Limits, "variables", "variables"),75                },76                .type_selectors = &.{77                    alloc_phase.capacity.bindType(Literal, "literal"),78                    alloc_phase.capacity.bindType(u32, "u32"),79                },80                .nodes = &.{81                    .{ .input = 0 },82                    .{ .input = 1 },83                    .{ .constant = 1 },84                    .{ .add = .{ .left = 1, .right = 2 } },85                    .{ .maximum = .{ .left = 0, .right = 3 } },86                    .{ .constant = 2 },87                    .{ .add = .{ .left = 4, .right = 5 } },88                    .{ .product = .{ .left = 6, .right = 1 } },89                    .{ .scale = .{ .node = 2, .coefficient = .{ .size_of_concrete_type = 0 } } },90                    .{ .product = .{ .left = 7, .right = 8 } },91                    .{ .scale = .{ .node = 6, .coefficient = .{ .size_of_concrete_type = 1 } } },92                    .{ .add = .{ .left = 9, .right = 10 } },93                },94                .assertions = &.{.{95                    .scope = .closure_total,96                    .measure = .retained,97                    .relation = .exact,98                    .expression = 11,99                }},100            },101            .overload = .{102                .kind = .reject_before_seal,103                .detail = "Limits and Capacity.derive reject arithmetic overflow before any storage is acquired; steady acquire asserts a free slot because the slot equation covers locked clauses plus the protected just-learned clause plus one admission, so steady exhaustion is a capacity-model bug and crashes",104            },105            .risks = .{106                .transitive = .{107                    .status = .open,108                    .detail = "clause headers, watch lists, and proof steps referencing pool literals live in solver-owned dynamic containers, pool versus heap freeing is routed by a per-clause storage tag, BoundedStoreExerciseProperty forces pooled eviction and checks retained-clause entailment against a satisfiable truth-table model, and BoundedStoreProperty checks bounded status, cores, and artifacts through the smt-pbt lane",109                },110                .foreign = .{111                    .status = .excluded,112                    .detail = "the slab and free list are process-local memory from the caller allocator with no operating-system or foreign-runtime edge",113                },114            },115            .obligations = &.{116                .{ .key = "smt_capacity_capacity_model", .role = .capacity_model },117                .{ .key = "smt_capacity_overload", .role = .overload },118                .{ .key = "smt_oom_retry", .role = .foreign_risk },119                .{ .key = "smt_sealed_fill_overload", .role = .overload },120                .{ .key = "smt_sealed_fill_foreign_risk", .role = .foreign_risk },121                .{ .key = "smt_victim_order", .role = .transitive_risk },122                .{ .key = "smt_bounded_solve", .role = .transitive_risk },123                .{ .key = "smt_pool_lifecycle", .role = .transitive_risk },124            },125        },126        .bindings = .{127            .owner = @This(),128            .seal = .{129                .family = alloc_phase.capacity.selector(@This().activate),130                .premise = .{131                    .class = .checked_semantic_fact,132                    .authority = .checker,133                },134            },135            .teardown = .{136                .family = alloc_phase.capacity.selector(@This().deinit),137                .premise = .{138                    .class = .checked_semantic_fact,139                    .authority = .checker,140                },141            },142        },143    };144    phase: alloc_phase.capacity.Phase,145    /// The sizes that `Capacity.derive` gave when the store was built. `admits` compares them with146    /// the sizes a solve needs.147    capacity: Capacity,148    slab: []Literal,149    free_slots: []u32,150    free_count: usize,151152    /// The inputs that size a store: the cap on replaceable learned clauses and the solver's153    /// variable count. The solver builds one from its cap and its variable count at the start of154    /// each capped solve.155    pub const Limits = struct {156        /// The cap on replaceable learned clauses, taken from `Solver.max_learned_clauses`.157        replaceable_clauses: usize,158        /// The solver's variable count, which is the most literals a learned clause holds.159        variables: usize,160161        /// Returns the limits for `replaceable_clauses` and `variables`. The solver builds its162        /// store limits through it.163        pub fn inspect(replaceable_clauses: usize, variables: usize) Limits {164            return .{165                .replaceable_clauses = replaceable_clauses,166                .variables = variables,167            };168        }169    };170171    /// The sizes of one store: its slot count, its slot width in literals and its total literal172    /// count. The solver derives the sizes a solve needs and asks its current store whether it173    /// `admits` them before it builds a new one.174    pub const Capacity = struct {175        /// The number of clauses the store holds at once: the larger of the cap and one more than176        /// the variable count, plus 2. The count covers the clauses kept because they justify177        /// current values, the clause learned most recently and one more.178        slots: usize,179        /// Literals per slot, equal to the variable count.180        slot_width: usize,181        /// Literals in the slab: the slot count times the slot width.182        literal_count: usize,183184        /// Returns the sizes a store needs for `limits`. The solver and `init` size a store from it185        /// before anything is allocated. The call returns `error.CapacityOverflow` when the slot186        /// count, the literal count or the slab's byte size overflows `usize`, or when the slot187        /// count passes the largest `u32`.188        pub fn derive(limits: Limits) error{CapacityOverflow}!Capacity {189            const locked_floor = std.math.add(usize, limits.variables, 1) catch190                return error.CapacityOverflow;191            const retained_peak = @max(limits.replaceable_clauses, locked_floor);192            const slots = std.math.add(usize, retained_peak, 2) catch193                return error.CapacityOverflow;194            if (slots > std.math.maxInt(u32)) return error.CapacityOverflow;195            const literal_count = std.math.mul(usize, slots, limits.variables) catch196                return error.CapacityOverflow;197            _ = std.math.mul(usize, literal_count, @sizeOf(Literal)) catch198                return error.CapacityOverflow;199            assert(slots > limits.replaceable_clauses);200            assert(slots > limits.variables);201            return .{202                .slots = slots,203                .slot_width = limits.variables,204                .literal_count = literal_count,205            };206        }207    };208209    /// Returns a store in `.initialization` whose slab and stack come from `allocator`, with every210    /// slot free. The solver builds its store with it at the start of a capped solve that needs211    /// more room than its current store has. The call returns `error.CapacityOverflow` from212    /// `Capacity.derive` and `error.OutOfMemory` from the allocator, and it frees the slab when the213    /// stack allocation fails. The caller passes the same allocator to `deinit`.214    pub fn init(allocator: Allocator, limits: Limits) !Store {215        const capacity = try Capacity.derive(limits);216        const slab = try allocator.alloc(Literal, capacity.literal_count);217        errdefer allocator.free(slab);218        const free_slots = try allocator.alloc(u32, capacity.slots);219        for (free_slots, 0..) |*slot, index| {220            slot.* = @intCast(capacity.slots - 1 - index);221        }222        return .{223            .phase = .initialization,224            .capacity = capacity,225            .slab = slab,226            .free_slots = free_slots,227            .free_count = capacity.slots,228        };229    }230231    /// Moves the store from `.initialization` to `.steady`, after which the store calls no232    /// allocator until `deinit`. The solver calls it once, right after `init`. The call asserts233    /// that the store is as `init` left it.234    pub fn activate(self: *Store) void {235        assert(self.phase == .initialization);236        assert(self.slab.len == self.capacity.literal_count);237        assert(self.free_slots.len == self.capacity.slots);238        assert(self.free_count == self.capacity.slots);239        self.phase = .steady;240    }241242    /// Returns true when the store has at least `required.slots` slots, each at least243    /// `required.slot_width` literals wide. The solver keeps its store across solves while the244    /// store admits what the next solve needs. The call asserts that the store is `.steady`.245    pub fn admits(self: *const Store, required: Capacity) bool {246        assert(self.phase == .steady);247        if (self.capacity.slots < required.slots) return false;248        return self.capacity.slot_width >= required.slot_width;249    }250251    /// Returns the number of free slots. A caller checks how many slots remain free, for example to252    /// confirm that every slot is either free or holds a stored clause.253    pub fn freeSlots(self: *const Store) usize {254        assert(self.phase == .steady);255        assert(self.free_count <= self.capacity.slots);256        return self.free_count;257    }258259    /// Returns true when `literals` starts inside the slab. The solver checks which memory holds a260    /// clause before it moves or frees the clause. The call works in any phase before `.teardown`.261    pub fn owns(self: *const Store, literals: []const Literal) bool {262        assert(self.phase != .teardown);263        const base = @intFromPtr(self.slab.ptr);264        const address = @intFromPtr(literals.ptr);265        if (address < base) return false;266        return address < base + self.slab.len * @sizeOf(Literal);267    }268269    /// Copies `literals` into a free slot and returns the copy. The solver stores each replaceable270    /// learned clause through it and keeps the returned slice in its clause list. The slot taken is271    /// the one freed most recently. The call asserts that the store is `.steady`, that `literals`272    /// holds from 1 to `slot_width` literals and lies outside the slab, and that a slot is free,273    /// because a full store is a sizing bug.274    pub fn acquire(self: *Store, literals: []const Literal) []Literal {275        assert(self.phase == .steady);276        assert(literals.len >= 1);277        assert(literals.len <= self.capacity.slot_width);278        assert(self.free_count > 0);279        assert(!self.owns(literals));280        self.free_count -= 1;281        const slot = self.free_slots[self.free_count];282        assert(slot < self.capacity.slots);283        const base = @as(usize, slot) * self.capacity.slot_width;284        const target = self.slab[base .. base + literals.len];285        @memcpy(target, literals);286        return target;287    }288289    /// Returns the slot that holds `literals` to the free stack. The solver calls it when it290    /// removes a learned clause or moves the clause back to its heap. The next `acquire` reuses291    /// that slot. The call asserts that the store is `.steady` and that `literals` starts at a slot292    /// boundary inside the slab.293    pub fn release(self: *Store, literals: []Literal) void {294        assert(self.phase == .steady);295        assert(self.owns(literals));296        assert(self.capacity.slot_width > 0);297        const offset = @intFromPtr(literals.ptr) - @intFromPtr(self.slab.ptr);298        const slot_bytes = self.capacity.slot_width * @sizeOf(Literal);299        assert(offset % slot_bytes == 0);300        const slot = offset / slot_bytes;301        assert(slot < self.capacity.slots);302        assert(literals.len <= self.capacity.slot_width);303        assert(self.free_count < self.capacity.slots);304        self.free_slots[self.free_count] = @intCast(slot);305        self.free_count += 1;306    }307308    /// Frees the slab and the stack with `allocator` and leaves the store undefined. The solver309    /// calls it when it replaces its store, when it drops the store after the cap is removed, and310    /// when it is freed itself. `allocator` has to be the one given to `init`. Every slice the311    /// store handed out becomes invalid.312    pub fn deinit(self: *Store, allocator: Allocator) void {313        assert(self.phase != .teardown);314        self.phase = .teardown;315        allocator.free(self.free_slots);316        allocator.free(self.slab);317        self.* = undefined;318    }319};320321comptime {322    alloc_phase.capacity.requireAllocatorExactOwnerShape(Store);323}324325test "learned store capacity matches an independent typed-byte model" {326    comptime {327        @stardustClaim(328            @import("alloc_phase").capacity.witness(Store, "smt_capacity_capacity_model"),329            null,330            null,331            null,332            null,333            null,334            null,335        );336    }337    comptime {338        @stardustClaim(339            @import("alloc_phase").capacity.witness(Store, "smt_capacity_overload"),340            null,341            null,342            null,343            null,344            null,345            null,346        );347    }348349    const limits = Store.Limits.inspect(256, 96);350    const capacity = try Store.Capacity.derive(limits);351    const expected_slots = 256 + 2;352    try std.testing.expectEqual(@as(usize, expected_slots), capacity.slots);353    try std.testing.expectEqual(@as(usize, 96), capacity.slot_width);354    try std.testing.expectEqual(@as(usize, expected_slots * 96), capacity.literal_count);355356    const locked_dominated = try Store.Capacity.derive(Store.Limits.inspect(4, 20));357    try std.testing.expectEqual(@as(usize, 20 + 1 + 2), locked_dominated.slots);358    try std.testing.expectEqual(@as(usize, 20), locked_dominated.slot_width);359360    try std.testing.expectError(361        error.CapacityOverflow,362        Store.Capacity.derive(Store.Limits.inspect(std.math.maxInt(usize) - 1, 8)),363    );364    try std.testing.expectError(365        error.CapacityOverflow,366        Store.Capacity.derive(Store.Limits.inspect(8, std.math.maxInt(usize) - 1)),367    );368    try std.testing.expectError(369        error.CapacityOverflow,370        Store.Capacity.derive(Store.Limits.inspect(std.math.maxInt(u32), 4)),371    );372}373374fn checkStoreInitFailures(allocator: Allocator, limits: Store.Limits) !void {375    var store = try Store.init(allocator, limits);376    defer store.deinit(allocator);377    try std.testing.expectEqual(alloc_phase.capacity.Phase.initialization, store.phase);378}379380test "learned store init cleans every allocation failure and retries" {381    comptime {382        @stardustClaim(383            @import("alloc_phase").capacity.witness(Store, "smt_oom_retry"),384            null,385            null,386            null,387            null,388            null,389            null,390        );391    }392393    const limits = Store.Limits.inspect(4, 6);394    try std.testing.checkAllAllocationFailures(395        std.testing.allocator,396        checkStoreInitFailures,397        .{limits},398    );399400    var store = try Store.init(std.testing.allocator, limits);401    defer store.deinit(std.testing.allocator);402    store.activate();403    try std.testing.expectEqual(@as(usize, 9), store.freeSlots());404}405406test "learned store fills to capacity with stable slots and zero steady operations" {407    comptime {408        @stardustClaim(409            @import("alloc_phase").capacity.witness(Store, "smt_sealed_fill_overload"),410            null,411            null,412            null,413            null,414            null,415            null,416        );417    }418    comptime {419        @stardustClaim(420            @import("alloc_phase").capacity.witness(Store, "smt_sealed_fill_foreign_risk"),421            null,422            null,423            null,424            null,425            null,426            null,427        );428    }429430    var failing = std.testing.FailingAllocator.init(std.testing.allocator, .{});431    var store = try Store.init(failing.allocator(), Store.Limits.inspect(2, 3));432    defer store.deinit(failing.allocator());433    store.activate();434    const slot_count = store.capacity.slots;435    try std.testing.expectEqual(@as(usize, 6), slot_count);436437    failing.fail_index = failing.alloc_index;438    failing.resize_fail_index = failing.resize_index;439440    const pattern = [_]Literal{ Literal.positive(0), Literal.negative(1), Literal.positive(2) };441    var held: [8][]Literal = undefined;442    for (0..slot_count) |index| {443        held[index] = store.acquire(pattern[0 .. 1 + index % 3]);444    }445    try std.testing.expectEqual(@as(usize, 0), store.freeSlots());446    for (0..slot_count) |index| {447        try std.testing.expect(store.owns(held[index]));448        try std.testing.expectEqual(@as(u32, Literal.positive(0).raw), held[index][0].raw);449    }450451    const first_pointer = held[0].ptr;452    store.release(held[0]);453    try std.testing.expectEqual(@as(usize, 1), store.freeSlots());454    const reacquired = store.acquire(&.{Literal.negative(2)});455    try std.testing.expectEqual(first_pointer, reacquired.ptr);456    try std.testing.expectEqual(@as(usize, 0), store.freeSlots());457458    for (held[1..slot_count]) |slice| store.release(slice);459    store.release(reacquired);460    try std.testing.expectEqual(slot_count, store.freeSlots());461    try std.testing.expect(!failing.has_induced_failure);462}