lib/smt/src/sat/store.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! Fixed memory for the learned clauses a solver may remove under a cap, sized before a search and
2 //! reused slot by slot. A solver with a cap on learned clauses adds and removes clauses throughout
3 //! a search, and a caller that bounds memory wants that churn to stay inside memory whose size is
4 //! known before the search starts.
5 //!
6 //! Learned clauses differ in length, and each holds at most one literal per variable. The solver
7 //! keeps a clause that justifies a current value even when the cap asks for a removal, and it keeps
8 //! 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 decision
11 //! levels (*replaceable learned clauses*), and the other learned clauses stay in the solver's heap
12 //! memory, as every learned clause does while the cap is null. The store gives each clause one slot
13 //! as wide as the variable count, all in one block of literals (a slab), and keeps the numbers of
14 //! the free slots on a stack, so taking or returning a slot is constant work with no allocator
15 //! 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 most
17 //! recently and one more. Taking a slot from a full store trips an assertion, because the slot
18 //! count is meant to rule that case out. When the cap or the variable count grows, the solver
19 //! builds a larger store and moves the stored clauses into it, and when the cap is removed it moves
20 //! them back to its heap. A compile-time record of this memory (`Store.claim`) states the size
21 //! equation and the overload behavior, and the shape check at the end of the file validates it.
22 const std = @import("std");
23 const alloc_phase = @import("alloc_phase");
24 const types = @import("types.zig");
25
26 const assert = std.debug.assert;
27 const Allocator = std.mem.Allocator;
28 const Literal = types.Literal;
29
30 /// Fixed memory for the replaceable learned clauses of one solver: equal slots in one slab of
31 /// literals, one clause per slot, with a stack of free slot numbers. The solver keeps one while
32 /// `Solver.max_learned_clauses` is set, and it moves each replaceable learned clause into it as the
33 /// clause is learned. `init` allocates the slab and the stack, `activate` moves the store from
34 /// `.initialization` to `.steady`, and `deinit` moves it to `.teardown` and frees both. In
35 /// `.steady`, taking and returning a slot is constant work and calls no allocator.
36 pub const Store = struct {
37 /// A compile-time record of the store's memory: what the slab and the stack cover, what stays
38 /// outside them, the equation that sizes them from `Limits`, the overload behavior, and the
39 /// tests that witness each obligation. The shape check at the end of the file validates the
40 /// record and the store's shape at compile time. The equation gives the slot count times the
41 /// variable count in literals, plus one 32-bit stack entry per slot, with the slot count that
42 /// `Capacity.derive` computes. The record states that an overflow is refused before any storage
43 /// 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 of
45 /// 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 with
146 /// the sizes a solve needs.
147 capacity: Capacity,
148 slab: []Literal,
149 free_slots: []u32,
150 free_count: usize,
151
152 /// The inputs that size a store: the cap on replaceable learned clauses and the solver's
153 /// variable count. The solver builds one from its cap and its variable count at the start of
154 /// 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,
160
161 /// Returns the limits for `replaceable_clauses` and `variables`. The solver builds its
162 /// 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 };
170
171 /// The sizes of one store: its slot count, its slot width in literals and its total literal
172 /// count. The solver derives the sizes a solve needs and asks its current store whether it
173 /// `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 than
176 /// the variable count, plus 2. The count covers the clauses kept because they justify
177 /// 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,
183
184 /// Returns the sizes a store needs for `limits`. The solver and `init` size a store from it
185 /// before anything is allocated. The call returns `error.CapacityOverflow` when the slot
186 /// count, the literal count or the slab's byte size overflows `usize`, or when the slot
187 /// 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) catch
190 return error.CapacityOverflow;
191 const retained_peak = @max(limits.replaceable_clauses, locked_floor);
192 const slots = std.math.add(usize, retained_peak, 2) catch
193 return error.CapacityOverflow;
194 if (slots > std.math.maxInt(u32)) return error.CapacityOverflow;
195 const literal_count = std.math.mul(usize, slots, limits.variables) catch
196 return error.CapacityOverflow;
197 _ = std.math.mul(usize, literal_count, @sizeOf(Literal)) catch
198 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 };
208
209 /// Returns a store in `.initialization` whose slab and stack come from `allocator`, with every
210 /// slot free. The solver builds its store with it at the start of a capped solve that needs
211 /// more room than its current store has. The call returns `error.CapacityOverflow` from
212 /// `Capacity.derive` and `error.OutOfMemory` from the allocator, and it frees the slab when the
213 /// 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 }
230
231 /// Moves the store from `.initialization` to `.steady`, after which the store calls no
232 /// allocator until `deinit`. The solver calls it once, right after `init`. The call asserts
233 /// 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 }
241
242 /// Returns true when the store has at least `required.slots` slots, each at least
243 /// `required.slot_width` literals wide. The solver keeps its store across solves while the
244 /// 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 }
250
251 /// Returns the number of free slots. A caller checks how many slots remain free, for example to
252 /// 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 }
258
259 /// Returns true when `literals` starts inside the slab. The solver checks which memory holds a
260 /// 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 }
268
269 /// Copies `literals` into a free slot and returns the copy. The solver stores each replaceable
270 /// learned clause through it and keeps the returned slice in its clause list. The slot taken is
271 /// 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 }
288
289 /// Returns the slot that holds `literals` to the free stack. The solver calls it when it
290 /// removes a learned clause or moves the clause back to its heap. The next `acquire` reuses
291 /// that slot. The call asserts that the store is `.steady` and that `literals` starts at a slot
292 /// 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 }
307
308 /// Frees the slab and the stack with `allocator` and leaves the store undefined. The solver
309 /// calls it when it replaces its store, when it drops the store after the cap is removed, and
310 /// when it is freed itself. `allocator` has to be the one given to `init`. Every slice the
311 /// 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 };
320
321 comptime {
322 alloc_phase.capacity.requireAllocatorExactOwnerShape(Store);
323 }
324
325 test "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 }
348
349 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);
355
356 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);
359
360 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 }
373
374 fn 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 }
379
380 test "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 }
392
393 const limits = Store.Limits.inspect(4, 6);
394 try std.testing.checkAllAllocationFailures(
395 std.testing.allocator,
396 checkStoreInitFailures,
397 .{limits},
398 );
399
400 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 }
405
406 test "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 }
429
430 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);
436
437 failing.fail_index = failing.alloc_index;
438 failing.resize_fail_index = failing.resize_index;
439
440 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 }
450
451 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());
457
458 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 }