lib/pluck/src/bdd.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const pretty = @import("pretty");
3 const time = @import("time.zig");
4 const Allocator = std.mem.Allocator;
5 const pretty_json = pretty.json;
6
7 pub const VarLabel = u32;
8
9 pub const NO_VAR: VarLabel = std.math.maxInt(VarLabel);
10
11 pub const VarLabelHashContext = struct {
12 const K: u64 = 0x517cc1b727220a95;
13
14 pub fn hash(_: VarLabelHashContext, key: VarLabel) u64 {
15 var x = @as(u64, key) *% K;
16 x ^= x >> 33;
17 x *%= K;
18 x ^= x >> 29;
19 return x;
20 }
21
22 pub fn eql(_: VarLabelHashContext, a: VarLabel, b: VarLabel) bool {
23 return a == b;
24 }
25 };
26
27 pub const VarLabelSet = std.HashMapUnmanaged(VarLabel, void, VarLabelHashContext, 80);
28
29 pub const NodeIndex = u32;
30
31 pub const Bdd = packed struct {
32 index: u31,
33 complement: bool,
34
35 pub const TRUE = Bdd{ .index = 0, .complement = false };
36 pub const FALSE = Bdd{ .index = 0, .complement = true };
37
38 pub fn fromRaw(raw: u32) Bdd {
39 return @bitCast(raw);
40 }
41
42 pub fn toRaw(self: Bdd) u32 {
43 return @bitCast(self);
44 }
45
46 pub fn neg(self: Bdd) Bdd {
47 return Bdd{
48 .index = self.index,
49 .complement = !self.complement,
50 };
51 }
52
53 pub fn isTrue(self: Bdd) bool {
54 return self.index == 0 and !self.complement;
55 }
56
57 pub fn isFalse(self: Bdd) bool {
58 return self.index == 0 and self.complement;
59 }
60
61 pub fn isConst(self: Bdd) bool {
62 return self.index == 0;
63 }
64
65 pub fn toReg(self: Bdd) Bdd {
66 return Bdd{ .index = self.index, .complement = false };
67 }
68
69 pub fn format(
70 self: Bdd,
71 comptime fmt: []const u8,
72 options: std.fmt.Options,
73 writer: anytype,
74 ) !void {
75 _ = fmt;
76 _ = options;
77 if (self.isTrue()) {
78 try writer.writeAll("T");
79 } else if (self.isFalse()) {
80 try writer.writeAll("F");
81 } else {
82 if (self.complement) {
83 try writer.print("!{d}", .{self.index});
84 } else {
85 try writer.print("{d}", .{self.index});
86 }
87 }
88 }
89 };
90
91 pub const Node = struct {
92 var_label: VarLabel,
93 low: Bdd,
94 high: Bdd,
95
96 pub fn init(var_label: VarLabel, low: Bdd, high: Bdd) Node {
97 return Node{
98 .var_label = var_label,
99 .low = low,
100 .high = high,
101 };
102 }
103 };
104
105 const NodeHashContext = struct {
106 const K: u64 = 0x517cc1b727220a95;
107
108 inline fn fxHashWord(h: u64, word: u64) u64 {
109 return (std.math.rotl(u64, h, 5) ^ word) *% K;
110 }
111
112 pub fn hash(self: @This(), node: Node) u64 {
113 _ = self;
114 var h: u64 = 0;
115 h = fxHashWord(h, @as(u64, node.var_label));
116 h = fxHashWord(h, @as(u64, node.low.toRaw()));
117 h = fxHashWord(h, @as(u64, node.high.toRaw()));
118 return h;
119 }
120
121 pub fn eql(self: @This(), a: Node, b: Node) bool {
122 _ = self;
123 return a.var_label == b.var_label and
124 a.low.toRaw() == b.low.toRaw() and
125 a.high.toRaw() == b.high.toRaw();
126 }
127 };
128
129 const IteKey = struct {
130 f: u32,
131 g: u32,
132 h: u32,
133
134 pub fn init(f: Bdd, g: Bdd, h: Bdd) IteKey {
135 return IteKey{
136 .f = f.toRaw(),
137 .g = g.toRaw(),
138 .h = h.toRaw(),
139 };
140 }
141 };
142
143 const IteKeyHashContext = struct {
144 const K: u64 = 0x517cc1b727220a95;
145
146 inline fn fxHashWord(h: u64, word: u64) u64 {
147 return (std.math.rotl(u64, h, 5) ^ word) *% K;
148 }
149
150 pub fn hash(self: @This(), key: IteKey) u64 {
151 _ = self;
152 var h: u64 = 0;
153 h = fxHashWord(h, @as(u64, key.f));
154 h = fxHashWord(h, @as(u64, key.g));
155 h = fxHashWord(h, @as(u64, key.h));
156 return h;
157 }
158
159 pub fn eql(self: @This(), a: IteKey, b: IteKey) bool {
160 _ = self;
161 return a.f == b.f and a.g == b.g and a.h == b.h;
162 }
163 };
164
165 const NormalizedIte = struct {
166 key: IteKey,
167 complement_result: bool,
168 is_const: bool,
169 const_result: Bdd,
170
171 pub fn normalize(f: Bdd, g: Bdd, h: Bdd, lessThan: anytype) NormalizedIte {
172 var nf = f;
173 var ng = g;
174 var nh = h;
175
176 if (nf.toRaw() == ng.toRaw()) {
177 ng = Bdd.TRUE;
178 }
179 if (nf.toRaw() == nh.toRaw()) {
180 nh = Bdd.FALSE;
181 }
182 if (nf.neg().toRaw() == nh.toRaw()) {
183 nh = Bdd.TRUE;
184 }
185 if (nf.neg().toRaw() == ng.toRaw()) {
186 ng = Bdd.FALSE;
187 }
188
189 if (nf.isTrue()) {
190 return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = ng };
191 }
192 if (nf.isFalse()) {
193 return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = nh };
194 }
195 if (ng.isTrue() and nh.isFalse()) {
196 return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = nf };
197 }
198 if (ng.isFalse() and nh.isTrue()) {
199 return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = nf.neg() };
200 }
201 if (ng.toRaw() == nh.toRaw()) {
202 return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = ng };
203 }
204
205 if (ng.isTrue() and !nh.isConst() and lessThan.call(nh, nf)) {
206 const tmp = nf;
207 nf = nh;
208 nh = tmp;
209 } else if (nh.isFalse() and !ng.isConst() and lessThan.call(ng, nf)) {
210 const tmp = nf;
211 nf = ng;
212 ng = tmp;
213 } else if (nh.isTrue() and !ng.isConst() and lessThan.call(ng, nf)) {
214 const old_f = nf;
215 nf = ng.neg();
216 ng = old_f.neg();
217 } else if (ng.isFalse() and !nh.isConst() and lessThan.call(nh, nf)) {
218 const old_f = nf;
219 nf = nh.neg();
220 nh = old_f.neg();
221 } else if (ng.toRaw() == nh.neg().toRaw() and !ng.isConst() and lessThan.call(ng, nf)) {
222 const tmp = nf;
223 nf = ng;
224 ng = tmp;
225 nh = tmp.neg();
226 }
227
228 var complement = false;
229 if (nf.complement and !nh.complement) {
230 nf = nf.neg();
231 const tmp = ng;
232 ng = nh;
233 nh = tmp;
234 } else if (!nf.complement and ng.complement) {
235 ng = ng.neg();
236 nh = nh.neg();
237 complement = true;
238 } else if (nf.complement and nh.complement) {
239 nf = nf.neg();
240 const tmp = ng;
241 ng = nh.neg();
242 nh = tmp.neg();
243 complement = true;
244 }
245
246 return NormalizedIte{
247 .key = IteKey.init(nf, ng, nh),
248 .complement_result = complement,
249 .is_const = false,
250 .const_result = Bdd.FALSE,
251 };
252 }
253 };
254
255 const LessThanHelper = struct {
256 manager: *const Manager,
257
258 pub inline fn call(self: LessThanHelper, a: Bdd, b: Bdd) bool {
259 const va = self.manager.topVar(a);
260 const vb = self.manager.topVar(b);
261 return self.manager.lessThan(va, vb);
262 }
263 };
264
265 const ConditionKey = struct {
266 f: u32,
267 variable: VarLabel,
268 value: bool,
269
270 pub fn init(f: Bdd, variable: VarLabel, value: bool) ConditionKey {
271 return ConditionKey{
272 .f = f.toRaw(),
273 .variable = variable,
274 .value = value,
275 };
276 }
277 };
278
279 pub const LimitConfig = struct {
280 time_limit: ?f64,
281 ite_limit: ?u64,
282 start_time: ?i64,
283 start_ite_count: u64,
284 start_node_count: usize,
285 start_ite_cache_count: usize,
286 ite_cache_reservations: usize,
287 time_limit_exceeded: bool,
288 ite_limit_exceeded: bool,
289
290 pub fn init() LimitConfig {
291 return LimitConfig{
292 .time_limit = null,
293 .ite_limit = null,
294 .start_time = null,
295 .start_ite_count = 0,
296 .start_node_count = 0,
297 .start_ite_cache_count = 0,
298 .ite_cache_reservations = 0,
299 .time_limit_exceeded = false,
300 .ite_limit_exceeded = false,
301 };
302 }
303
304 pub fn startTimeLimit(self: *LimitConfig, limit: f64) void {
305 self.time_limit = limit;
306 self.start_time = time.milliTimestamp();
307 self.time_limit_exceeded = false;
308 }
309
310 pub fn stopTimeLimit(self: *LimitConfig) void {
311 self.time_limit = null;
312 self.start_time = null;
313 }
314
315 pub fn startIteLimit(
316 self: *LimitConfig,
317 limit: u64,
318 current_count: u64,
319 node_count: usize,
320 ite_cache_count: usize,
321 ) void {
322 std.debug.assert(self.ite_cache_reservations == 0);
323 self.ite_limit = limit;
324 self.start_ite_count = current_count;
325 self.start_node_count = node_count;
326 self.start_ite_cache_count = ite_cache_count;
327 self.ite_cache_reservations = 0;
328 self.ite_limit_exceeded = false;
329 }
330
331 pub fn stopIteLimit(self: *LimitConfig) void {
332 std.debug.assert(self.ite_cache_reservations == 0);
333 self.ite_limit = null;
334 }
335
336 pub fn checkTimeLimit(self: *LimitConfig) bool {
337 if (self.time_limit) |limit| {
338 if (self.start_time) |start| {
339 const now = time.milliTimestamp();
340 const elapsed_seconds = @as(f64, @floatFromInt(now - start)) / 1000.0;
341 if (elapsed_seconds >= limit) {
342 self.time_limit_exceeded = true;
343 return true;
344 }
345 }
346 }
347 return false;
348 }
349
350 pub fn checkIteLimit(self: *LimitConfig, current_count: u64) bool {
351 if (self.ite_limit) |limit| {
352 if (current_count -| self.start_ite_count >= limit) {
353 self.ite_limit_exceeded = true;
354 return true;
355 }
356 }
357 return false;
358 }
359
360 pub fn checkNodeGrowth(self: *LimitConfig, current_count: usize) bool {
361 if (self.ite_limit) |limit| {
362 const growth: u64 = @intCast(current_count -| self.start_node_count);
363 if (growth >= limit) {
364 self.ite_limit_exceeded = true;
365 return true;
366 }
367 }
368 return false;
369 }
370
371 pub fn reserveIteCacheGrowth(self: *LimitConfig, current_count: usize) bool {
372 if (self.ite_limit) |limit| {
373 const growth: u64 = @intCast(current_count -| self.start_ite_cache_count);
374 const reserved: u64 = @intCast(self.ite_cache_reservations);
375 if (growth +| reserved >= limit) {
376 self.ite_limit_exceeded = true;
377 return true;
378 }
379 if (self.ite_cache_reservations == std.math.maxInt(usize)) {
380 self.ite_limit_exceeded = true;
381 return true;
382 }
383 self.ite_cache_reservations += 1;
384 }
385 return false;
386 }
387
388 pub fn releaseIteCacheGrowth(self: *LimitConfig) void {
389 if (self.ite_limit == null) return;
390 std.debug.assert(self.ite_cache_reservations > 0);
391 self.ite_cache_reservations -= 1;
392 }
393
394 pub fn boundedAllocationFailed(self: *LimitConfig) bool {
395 if (self.ite_limit == null) return false;
396 self.ite_limit_exceeded = true;
397 return true;
398 }
399 };
400
401 pub const SiftConfig = struct {
402 max_distance: u32 = 5,
403 max_blowup: f64 = 2.0,
404 time_limit_ms: u64 = 10,
405 };
406
407 pub const SiftResult = struct {
408 original_pos: u32,
409 final_pos: u32,
410 size_delta: i64,
411 aborted: bool,
412 };
413
414 pub const GlobalSiftResult = struct {
415 total_size_delta: i64,
416 vars_sifted: u32,
417 vars_improved: u32,
418 original_size: usize,
419 final_size: usize,
420 };
421
422 pub const Manager = struct {
423 const TABLE_MAX_LOAD_PERCENTAGE = 80;
424
425 allocator: Allocator,
426
427 nodes: std.ArrayListUnmanaged(Node),
428
429 unique_table: std.HashMapUnmanaged(Node, NodeIndex, NodeHashContext, TABLE_MAX_LOAD_PERCENTAGE),
430
431 unique_table_grow_at: usize,
432
433 ite_cache: std.HashMapUnmanaged(IteKey, Bdd, IteKeyHashContext, TABLE_MAX_LOAD_PERCENTAGE),
434
435 ite_cache_grow_at: usize,
436
437 condition_cache: std.AutoHashMapUnmanaged(ConditionKey, Bdd),
438
439 var_order: std.ArrayListUnmanaged(u32),
440
441 min_vars: std.ArrayListUnmanaged(VarLabel),
442
443 max_vars: std.ArrayListUnmanaged(VarLabel),
444
445 num_recursive_calls: u64,
446
447 ite_cache_hits: u64,
448
449 ite_cache_misses: u64,
450
451 unique_table_grows: u64,
452
453 ite_cache_grows: u64,
454
455 limits: LimitConfig,
456
457 const INITIAL_MANAGER_CAPACITY = 4096;
458 const INITIAL_CONDITION_CACHE_CAPACITY = 256;
459
460 fn tableLoadThreshold(capacity: usize) usize {
461 return (capacity * TABLE_MAX_LOAD_PERCENTAGE) / 100;
462 }
463
464 pub fn init(allocator: Allocator) !Manager {
465 var nodes = std.ArrayListUnmanaged(Node).empty;
466 errdefer nodes.deinit(allocator);
467
468 var min_vars = std.ArrayListUnmanaged(VarLabel).empty;
469 errdefer min_vars.deinit(allocator);
470
471 var max_vars = std.ArrayListUnmanaged(VarLabel).empty;
472 errdefer max_vars.deinit(allocator);
473
474 try nodes.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);
475 try min_vars.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);
476 try max_vars.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);
477
478 try nodes.append(allocator, Node.init(NO_VAR, Bdd.TRUE, Bdd.TRUE));
479 try min_vars.append(allocator, NO_VAR);
480 try max_vars.append(allocator, NO_VAR);
481
482 var unique_table = std.HashMapUnmanaged(Node, NodeIndex, NodeHashContext, TABLE_MAX_LOAD_PERCENTAGE){};
483 errdefer unique_table.deinit(allocator);
484 try unique_table.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);
485
486 var ite_cache = std.HashMapUnmanaged(IteKey, Bdd, IteKeyHashContext, TABLE_MAX_LOAD_PERCENTAGE){};
487 errdefer ite_cache.deinit(allocator);
488 try ite_cache.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);
489
490 var condition_cache = std.AutoHashMapUnmanaged(ConditionKey, Bdd){};
491 errdefer condition_cache.deinit(allocator);
492 try condition_cache.ensureTotalCapacity(allocator, INITIAL_CONDITION_CACHE_CAPACITY);
493
494 return Manager{
495 .allocator = allocator,
496 .nodes = nodes,
497 .unique_table = unique_table,
498 .unique_table_grow_at = tableLoadThreshold(unique_table.capacity()),
499 .ite_cache = ite_cache,
500 .ite_cache_grow_at = tableLoadThreshold(ite_cache.capacity()),
501 .condition_cache = condition_cache,
502 .var_order = std.ArrayListUnmanaged(u32).empty,
503 .min_vars = min_vars,
504 .max_vars = max_vars,
505 .num_recursive_calls = 0,
506 .ite_cache_hits = 0,
507 .ite_cache_misses = 0,
508 .unique_table_grows = 0,
509 .ite_cache_grows = 0,
510 .limits = LimitConfig.init(),
511 };
512 }
513
514 pub fn deinit(self: *Manager) void {
515 self.nodes.deinit(self.allocator);
516 self.unique_table.deinit(self.allocator);
517 self.ite_cache.deinit(self.allocator);
518 self.condition_cache.deinit(self.allocator);
519 self.var_order.deinit(self.allocator);
520 self.min_vars.deinit(self.allocator);
521 self.max_vars.deinit(self.allocator);
522 }
523
524 pub fn numVars(self: *const Manager) usize {
525 return self.var_order.items.len;
526 }
527
528 pub fn newVar(self: *Manager, polarity: bool) Allocator.Error!Bdd {
529 const label: VarLabel = @intCast(self.var_order.items.len);
530 const node = Node.init(label, Bdd.FALSE, Bdd.TRUE);
531
532 if (!try self.prepareVariableInsert(node)) return Bdd.FALSE;
533
534 self.var_order.appendAssumeCapacity(label);
535 const bdd = self.insertCanonicalAssumeCapacity(node);
536
537 return if (polarity) bdd else bdd.neg();
538 }
539
540 pub fn newVarAtPosition(self: *Manager, position: u32, polarity: bool) Allocator.Error!Bdd {
541 const label: VarLabel = @intCast(self.var_order.items.len);
542 const node = Node.init(label, Bdd.FALSE, Bdd.TRUE);
543
544 if (!try self.prepareVariableInsert(node)) return Bdd.FALSE;
545
546 for (self.var_order.items) |*pos| {
547 if (pos.* >= position) {
548 pos.* += 1;
549 }
550 }
551 self.var_order.appendAssumeCapacity(position);
552
553 const bdd = self.insertCanonicalAssumeCapacity(node);
554
555 return if (polarity) bdd else bdd.neg();
556 }
557
558 fn prepareVariableInsert(self: *Manager, node: Node) Allocator.Error!bool {
559 std.debug.assert(self.unique_table.getContext(node, NodeHashContext{}) == null);
560 if (self.limits.checkNodeGrowth(self.nodes.items.len)) return false;
561 self.ensureCanonicalInsertCapacity() catch |err| {
562 if (self.limits.boundedAllocationFailed()) return false;
563 return err;
564 };
565 self.var_order.ensureUnusedCapacity(self.allocator, 1) catch |err| {
566 if (self.limits.boundedAllocationFailed()) return false;
567 return err;
568 };
569 return true;
570 }
571
572 fn getOrInsert(self: *Manager, node: Node) Allocator.Error!Bdd {
573 if (node.low.toRaw() == node.high.toRaw()) {
574 return node.low;
575 }
576
577 if (node.high.complement) {
578 const canonical = Node.init(
579 node.var_label,
580 node.low.neg(),
581 node.high.neg(),
582 );
583 return (try self.insertCanonical(canonical)).neg();
584 } else {
585 return self.insertCanonical(node);
586 }
587 }
588
589 fn insertCanonical(self: *Manager, node: Node) Allocator.Error!Bdd {
590 if (self.unique_table.getContext(node, NodeHashContext{})) |index| {
591 return Bdd{ .index = @intCast(index), .complement = false };
592 }
593 if (self.limits.checkNodeGrowth(self.nodes.items.len)) return Bdd.FALSE;
594 self.ensureCanonicalInsertCapacity() catch |err| {
595 if (self.limits.boundedAllocationFailed()) return Bdd.FALSE;
596 return err;
597 };
598
599 return self.insertCanonicalAssumeCapacity(node);
600 }
601
602 fn insertCanonicalAssumeCapacity(self: *Manager, node: Node) Bdd {
603 const entry = self.unique_table.getOrPutAssumeCapacityContext(node, NodeHashContext{});
604 std.debug.assert(!entry.found_existing);
605
606 const idx: u31 = @intCast(self.nodes.items.len);
607 self.nodes.appendAssumeCapacity(node);
608
609 const low_min = self.min_vars.items[node.low.index];
610 const low_max = self.max_vars.items[node.low.index];
611 const high_min = self.min_vars.items[node.high.index];
612 const high_max = self.max_vars.items[node.high.index];
613
614 var min_var = node.var_label;
615 if (low_min != NO_VAR and low_min < min_var) min_var = low_min;
616 if (high_min != NO_VAR and high_min < min_var) min_var = high_min;
617
618 var max_var = node.var_label;
619 if (low_max != NO_VAR and low_max > max_var) max_var = low_max;
620 if (high_max != NO_VAR and high_max > max_var) max_var = high_max;
621
622 self.min_vars.appendAssumeCapacity(min_var);
623 self.max_vars.appendAssumeCapacity(max_var);
624 entry.value_ptr.* = idx;
625
626 return Bdd{ .index = idx, .complement = false };
627 }
628
629 fn ensureCanonicalInsertCapacity(self: *Manager) Allocator.Error!void {
630 if (self.nodes.items.len >= self.nodes.capacity) {
631 const reserve = @max(self.nodes.capacity, INITIAL_MANAGER_CAPACITY);
632 const target = self.nodes.items.len + reserve;
633 try self.nodes.ensureTotalCapacity(self.allocator, target);
634 try self.min_vars.ensureTotalCapacity(self.allocator, target);
635 try self.max_vars.ensureTotalCapacity(self.allocator, target);
636 }
637
638 const count = self.unique_table.count();
639 if (count < self.unique_table_grow_at) return;
640
641 const capacity = self.unique_table.capacity();
642 const reserve = @max(capacity, INITIAL_MANAGER_CAPACITY);
643 try self.unique_table.ensureTotalCapacity(self.allocator, count + reserve);
644 self.unique_table_grows += 1;
645 self.unique_table_grow_at = tableLoadThreshold(self.unique_table.capacity());
646 }
647
648 pub inline fn getNode(self: *const Manager, bdd: Bdd) Node {
649 return self.nodes.items[bdd.index];
650 }
651
652 pub inline fn topVar(self: *const Manager, bdd: Bdd) VarLabel {
653 if (bdd.isConst()) return NO_VAR;
654 return self.getNode(bdd).var_label;
655 }
656
657 pub fn getMinVar(self: *const Manager, bdd: Bdd) VarLabel {
658 return self.min_vars.items[bdd.index];
659 }
660
661 pub fn getMaxVar(self: *const Manager, bdd: Bdd) VarLabel {
662 return self.max_vars.items[bdd.index];
663 }
664
665 pub fn low(self: *const Manager, bdd: Bdd) Bdd {
666 if (bdd.isConst()) return Bdd.FALSE;
667 const node = self.getNode(bdd);
668 return if (bdd.complement) node.low.neg() else node.low;
669 }
670
671 pub fn high(self: *const Manager, bdd: Bdd) Bdd {
672 if (bdd.isConst()) return Bdd.FALSE;
673 const node = self.getNode(bdd);
674 return if (bdd.complement) node.high.neg() else node.high;
675 }
676
677 inline fn lessThan(self: *const Manager, a: VarLabel, b: VarLabel) bool {
678 if (a == NO_VAR) return false;
679 if (b == NO_VAR) return true;
680 return self.var_order.items[a] < self.var_order.items[b];
681 }
682
683 inline fn firstEssential(self: *const Manager, f: Bdd, g: Bdd, h: Bdd) VarLabel {
684 const vf = self.topVar(f);
685 const vg = self.topVar(g);
686 const vh = self.topVar(h);
687
688 var result = vf;
689 if (self.lessThan(vg, result)) result = vg;
690 if (self.lessThan(vh, result)) result = vh;
691 return result;
692 }
693
694 inline fn conditionEssential(self: *const Manager, f: Bdd, lbl: VarLabel, value: bool) Bdd {
695 if (f.isConst()) return f;
696 const node = self.getNode(f);
697 if (node.var_label != lbl) return f;
698
699 const result = if (value) node.high else node.low;
700 return if (f.complement) result.neg() else result;
701 }
702
703 pub fn checkLimits(self: *Manager) bool {
704 if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) return true;
705 if (self.limits.checkIteLimit(self.num_recursive_calls)) {
706 return true;
707 }
708 if (self.num_recursive_calls % 1000 == 0) {
709 if (self.limits.checkTimeLimit()) {
710 return true;
711 }
712 }
713 return false;
714 }
715
716 pub fn iteLimitExceeded(self: *const Manager) bool {
717 return self.limits.ite_limit_exceeded;
718 }
719
720 pub fn timeLimitExceeded(self: *const Manager) bool {
721 return self.limits.time_limit_exceeded;
722 }
723
724 pub fn setTimeLimit(self: *Manager, limit_seconds: f64) void {
725 self.limits.time_limit = limit_seconds;
726 self.limits.time_limit_exceeded = false;
727 }
728
729 pub fn startTimeLimit(self: *Manager, limit_seconds: f64) void {
730 self.limits.startTimeLimit(limit_seconds);
731 }
732
733 pub fn stopTimeLimit(self: *Manager) void {
734 self.limits.stopTimeLimit();
735 }
736
737 pub fn resetLimitFlags(self: *Manager) void {
738 self.limits.time_limit_exceeded = false;
739 self.limits.ite_limit_exceeded = false;
740 }
741
742 pub fn startIteLimit(self: *Manager, limit: u64) void {
743 self.limits.startIteLimit(
744 limit,
745 self.num_recursive_calls,
746 self.nodes.items.len,
747 self.ite_cache.count(),
748 );
749 }
750
751 pub fn stopIteLimit(self: *Manager) void {
752 self.limits.stopIteLimit();
753 }
754
755 pub fn ite(self: *Manager, f: Bdd, g: Bdd, h: Bdd) Allocator.Error!Bdd {
756 self.num_recursive_calls += 1;
757
758 if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {
759 return Bdd.FALSE;
760 }
761
762 if (self.num_recursive_calls % 1000 == 0) {
763 if (self.checkLimits()) return Bdd.FALSE;
764 }
765
766 const helper = LessThanHelper{ .manager = self };
767 const normalized = NormalizedIte.normalize(f, g, h, helper);
768
769 if (normalized.is_const) {
770 return normalized.const_result;
771 }
772
773 if (self.ite_cache.get(normalized.key)) |cached| {
774 self.ite_cache_hits += 1;
775 return if (normalized.complement_result) cached.neg() else cached;
776 }
777 self.ite_cache_misses += 1;
778
779 if (self.limits.reserveIteCacheGrowth(self.ite_cache.count())) return Bdd.FALSE;
780 defer self.limits.releaseIteCacheGrowth();
781
782 const top_var = self.firstEssential(f, g, h);
783
784 const fx_t = self.conditionEssential(f, top_var, true);
785 const gx_t = self.conditionEssential(g, top_var, true);
786 const hx_t = self.conditionEssential(h, top_var, true);
787 const fx_f = self.conditionEssential(f, top_var, false);
788 const gx_f = self.conditionEssential(g, top_var, false);
789 const hx_f = self.conditionEssential(h, top_var, false);
790
791 const t = try self.ite(fx_t, gx_t, hx_t);
792 if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {
793 return Bdd.FALSE;
794 }
795 const e = try self.ite(fx_f, gx_f, hx_f);
796
797 if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {
798 return Bdd.FALSE;
799 }
800
801 if (t.toRaw() == e.toRaw()) {
802 const cache_result = if (normalized.complement_result) t.neg() else t;
803 if (!try self.putIteCacheNoClobber(normalized.key, cache_result)) return Bdd.FALSE;
804 return t;
805 }
806
807 const result = try self.getOrInsert(Node.init(top_var, e, t));
808 if (self.limits.ite_limit_exceeded) return Bdd.FALSE;
809
810 const cache_result = if (normalized.complement_result) result.neg() else result;
811 if (!try self.putIteCacheNoClobber(normalized.key, cache_result)) return Bdd.FALSE;
812
813 return result;
814 }
815
816 fn putIteCacheNoClobber(self: *Manager, key: IteKey, value: Bdd) Allocator.Error!bool {
817 if (!try self.ensureReservedIteCacheCapacity()) return false;
818 self.ite_cache.putAssumeCapacityNoClobber(key, value);
819 return true;
820 }
821
822 fn ensureReservedIteCacheCapacity(self: *Manager) Allocator.Error!bool {
823 const reservations = @max(self.limits.ite_cache_reservations, 1);
824 std.debug.assert(reservations <= std.math.maxInt(u32));
825 const projected = self.ite_cache.count() +| reservations;
826 if (projected <= self.ite_cache_grow_at) return true;
827
828 const capacity = self.ite_cache.capacity();
829 const reserve = @max(capacity, INITIAL_MANAGER_CAPACITY);
830 const target = @max(projected, self.ite_cache.count() +| reserve);
831 const target_size = std.math.cast(u32, target) orelse {
832 if (self.limits.boundedAllocationFailed()) return false;
833 return error.OutOfMemory;
834 };
835 self.ite_cache.ensureTotalCapacity(self.allocator, target_size) catch |err| {
836 if (self.limits.boundedAllocationFailed()) return false;
837 return err;
838 };
839 self.ite_cache_grows += 1;
840 self.ite_cache_grow_at = tableLoadThreshold(self.ite_cache.capacity());
841 return true;
842 }
843
844 pub fn bddAnd(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {
845 if (a.isFalse() or b.isFalse()) return Bdd.FALSE;
846 if (a.isTrue()) return b;
847 if (b.isTrue()) return a;
848 if (a.toRaw() == b.toRaw()) return a;
849 if (a.neg().toRaw() == b.toRaw()) return Bdd.FALSE;
850
851 var left = a;
852 var right = b;
853 if (right.toRaw() < left.toRaw()) {
854 const tmp = left;
855 left = right;
856 right = tmp;
857 }
858 return self.ite(left, right, Bdd.FALSE);
859 }
860
861 pub fn bddOr(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {
862 if (a.isTrue() or b.isTrue()) return Bdd.TRUE;
863 if (a.isFalse()) return b;
864 if (b.isFalse()) return a;
865 if (a.toRaw() == b.toRaw()) return a;
866 if (a.neg().toRaw() == b.toRaw()) return Bdd.TRUE;
867
868 var left = a;
869 var right = b;
870 if (right.toRaw() < left.toRaw()) {
871 const tmp = left;
872 left = right;
873 right = tmp;
874 }
875 return self.ite(left, Bdd.TRUE, right);
876 }
877
878 pub fn bddNot(_: *Manager, a: Bdd) Bdd {
879 return a.neg();
880 }
881
882 pub fn bddXor(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {
883 if (a.isFalse()) return b;
884 if (b.isFalse()) return a;
885 if (a.isTrue()) return b.neg();
886 if (b.isTrue()) return a.neg();
887 if (a.toRaw() == b.toRaw()) return Bdd.FALSE;
888 if (a.neg().toRaw() == b.toRaw()) return Bdd.TRUE;
889
890 var left = a;
891 var right = b;
892 if (right.toRaw() < left.toRaw()) {
893 const tmp = left;
894 left = right;
895 right = tmp;
896 }
897 return self.ite(left, right.neg(), right);
898 }
899
900 pub fn bddIff(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {
901 if (a.isFalse()) return b.neg();
902 if (b.isFalse()) return a.neg();
903 if (a.isTrue()) return b;
904 if (b.isTrue()) return a;
905 if (a.toRaw() == b.toRaw()) return Bdd.TRUE;
906 if (a.neg().toRaw() == b.toRaw()) return Bdd.FALSE;
907
908 var left = a;
909 var right = b;
910 if (right.toRaw() < left.toRaw()) {
911 const tmp = left;
912 left = right;
913 right = tmp;
914 }
915 return self.ite(left, right, right.neg());
916 }
917
918 pub fn bddImplies(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {
919 if (a.isFalse() or b.isTrue()) return Bdd.TRUE;
920 if (a.isTrue()) return b;
921 if (b.isFalse()) return a.neg();
922 if (a.toRaw() == b.toRaw()) return Bdd.TRUE;
923 if (a.neg().toRaw() == b.toRaw()) return b;
924 return self.bddOr(a.neg(), b);
925 }
926
927 pub fn eq(self: *const Manager, a: Bdd, b: Bdd) bool {
928 _ = self;
929 return a.toRaw() == b.toRaw();
930 }
931
932 pub fn exists(self: *Manager, f: Bdd, variable: VarLabel) Allocator.Error!Bdd {
933 const f_true = try self.condition(f, variable, true);
934 const f_false = try self.condition(f, variable, false);
935 return self.bddOr(f_true, f_false);
936 }
937
938 pub fn condition(self: *Manager, f: Bdd, variable: VarLabel, value: bool) Allocator.Error!Bdd {
939 return self.conditionHelper(f, variable, value);
940 }
941
942 fn conditionHelper(self: *Manager, f: Bdd, variable: VarLabel, value: bool) Allocator.Error!Bdd {
943 if (f.isConst()) return f;
944
945 const node = self.getNode(f);
946
947 if (self.lessThan(variable, node.var_label)) {
948 return f;
949 }
950
951 if (node.var_label == variable) {
952 const result = if (value) node.high else node.low;
953 return if (f.complement) result.neg() else result;
954 }
955
956 const key = ConditionKey.init(f, variable, value);
957 if (self.condition_cache.get(key)) |cached| {
958 return cached;
959 }
960
961 const low_result = try self.conditionHelper(
962 if (f.complement) node.low.neg() else node.low,
963 variable,
964 value,
965 );
966 const high_result = try self.conditionHelper(
967 if (f.complement) node.high.neg() else node.high,
968 variable,
969 value,
970 );
971
972 if (low_result.toRaw() == high_result.toRaw()) {
973 if (!try self.putConditionCache(key, low_result)) return Bdd.FALSE;
974 return low_result;
975 }
976
977 const result = try self.getOrInsert(Node.init(node.var_label, low_result, high_result));
978 if (self.limits.ite_limit_exceeded) return Bdd.FALSE;
979
980 if (!try self.putConditionCache(key, result)) return Bdd.FALSE;
981
982 return result;
983 }
984
985 fn putConditionCache(self: *Manager, key: ConditionKey, value: Bdd) Allocator.Error!bool {
986 self.condition_cache.put(self.allocator, key, value) catch |err| {
987 if (self.limits.boundedAllocationFailed()) return false;
988 return err;
989 };
990 return true;
991 }
992
993 pub fn compose(self: *Manager, f: Bdd, variable: VarLabel, g: Bdd) Allocator.Error!Bdd {
994 if (f.isConst()) return f;
995
996 const node = self.getNode(f);
997
998 if (self.lessThan(variable, node.var_label)) {
999 return f;
1000 }
1001
1002 const f_low = if (f.complement) node.low.neg() else node.low;
1003 const f_high = if (f.complement) node.high.neg() else node.high;
1004
1005 if (node.var_label == variable) {
1006 return self.ite(g, f_high, f_low);
1007 }
1008
1009 const low_result = try self.compose(f_low, variable, g);
1010 const high_result = try self.compose(f_high, variable, g);
1011
1012 if (low_result.toRaw() == high_result.toRaw()) {
1013 return low_result;
1014 }
1015
1016 return self.getOrInsert(Node.init(node.var_label, low_result, high_result));
1017 }
1018
1019 pub fn sequentialCompose(
1020 self: *Manager,
1021 f: Bdd,
1022 variables: []const VarLabel,
1023 replacements: []const Bdd,
1024 ) Allocator.Error!Bdd {
1025 var result = f;
1026 for (variables, replacements) |variable, replacement| {
1027 result = try self.compose(result, variable, replacement);
1028 }
1029 return result;
1030 }
1031
1032 pub fn isVar(self: *const Manager, bdd: Bdd) bool {
1033 if (bdd.isConst()) return false;
1034 const node = self.getNode(bdd);
1035 const low_raw = if (bdd.complement) node.low.neg() else node.low;
1036 const high_raw = if (bdd.complement) node.high.neg() else node.high;
1037 return low_raw.isFalse() and high_raw.isTrue();
1038 }
1039
1040 pub fn hasVariable(self: *const Manager, bdd: Bdd, variable: VarLabel) bool {
1041 if (bdd.isConst()) return false;
1042
1043 const node = self.getNode(bdd);
1044 if (node.var_label == variable) return true;
1045
1046 return self.hasVariable(node.low.toReg(), variable) or
1047 self.hasVariable(node.high.toReg(), variable);
1048 }
1049
1050 pub fn size(self: *const Manager, bdd: Bdd) usize {
1051 if (bdd.isConst()) return 0;
1052
1053 var visited = std.AutoHashMap(u31, void).init(self.allocator);
1054 defer visited.deinit();
1055
1056 return self.sizeHelper(bdd, &visited);
1057 }
1058
1059 fn sizeHelper(self: *const Manager, bdd: Bdd, visited: *std.AutoHashMap(u31, void)) usize {
1060 if (bdd.isConst()) return 0;
1061 if (visited.contains(bdd.index)) return 0;
1062
1063 visited.put(bdd.index, {}) catch return 0;
1064
1065 const node = self.getNode(bdd);
1066 return 1 + self.sizeHelper(node.low.toReg(), visited) +
1067 self.sizeHelper(node.high.toReg(), visited);
1068 }
1069
1070 pub fn numRecursiveCalls(self: *const Manager) u64 {
1071 return self.num_recursive_calls;
1072 }
1073
1074 pub fn resetStats(self: *Manager) void {
1075 self.num_recursive_calls = 0;
1076 }
1077
1078 pub fn clearCache(self: *Manager) void {
1079 self.ite_cache.clearRetainingCapacity();
1080 self.ite_cache_grow_at = tableLoadThreshold(self.ite_cache.capacity());
1081 self.condition_cache.clearRetainingCapacity();
1082 }
1083
1084 pub fn getVarPosition(self: *const Manager, var_label: VarLabel) u32 {
1085 if (var_label >= self.var_order.items.len) return @intCast(self.var_order.items.len);
1086 return self.var_order.items[var_label];
1087 }
1088
1089 pub fn totalNodeCount(self: *const Manager) usize {
1090 return if (self.nodes.items.len > 0) self.nodes.items.len - 1 else 0;
1091 }
1092
1093 pub fn getVarAtPosition(self: *const Manager, position: u32) ?VarLabel {
1094 for (self.var_order.items, 0..) |pos, label| {
1095 if (pos == position) return @intCast(label);
1096 }
1097 return null;
1098 }
1099
1100 pub fn nodesAtLevel(self: *const Manager, var_label: VarLabel) usize {
1101 var count: usize = 0;
1102 for (self.nodes.items[1..]) |node| {
1103 if (node.var_label == var_label) count += 1;
1104 }
1105 return count;
1106 }
1107
1108 pub fn swapAdjacentVars(self: *Manager, upper_pos: u32, allocator: Allocator) !i64 {
1109 const lower_pos = upper_pos + 1;
1110
1111 const var_upper = self.getVarAtPosition(upper_pos) orelse return 0;
1112 const var_lower = self.getVarAtPosition(lower_pos) orelse return 0;
1113
1114 const size_before = self.totalNodeCount();
1115
1116 var nodes_to_process: std.ArrayList(u31) = .empty;
1117 defer nodes_to_process.deinit(allocator);
1118
1119 for (self.nodes.items[1..], 1..) |node, idx| {
1120 if (node.var_label == var_upper) {
1121 try nodes_to_process.append(allocator, @intCast(idx));
1122 }
1123 }
1124
1125 for (nodes_to_process.items) |idx| {
1126 const node = self.nodes.items[idx];
1127 const high_child = node.high;
1128 const low_child = node.low;
1129
1130 var f11: Bdd = undefined;
1131 var f10: Bdd = undefined;
1132 var f01: Bdd = undefined;
1133 var f00: Bdd = undefined;
1134
1135 if (!high_child.isConst() and self.getNode(high_child).var_label == var_lower) {
1136 const high_node = self.getNode(high_child);
1137 f11 = if (high_child.complement) high_node.high.neg() else high_node.high;
1138 f10 = if (high_child.complement) high_node.low.neg() else high_node.low;
1139 } else {
1140 f11 = high_child;
1141 f10 = high_child;
1142 }
1143
1144 if (!low_child.isConst() and self.getNode(low_child).var_label == var_lower) {
1145 const low_node = self.getNode(low_child);
1146 f01 = if (low_child.complement) low_node.high.neg() else low_node.high;
1147 f00 = if (low_child.complement) low_node.low.neg() else low_node.low;
1148 } else {
1149 f01 = low_child;
1150 f00 = low_child;
1151 }
1152
1153 const new_high = try self.getOrInsert(Node.init(var_upper, f01, f11));
1154 const new_low = try self.getOrInsert(Node.init(var_upper, f00, f10));
1155
1156 _ = try self.getOrInsert(Node.init(var_lower, new_low, new_high));
1157 }
1158
1159 self.var_order.items[var_upper] = lower_pos;
1160 self.var_order.items[var_lower] = upper_pos;
1161
1162 self.clearCache();
1163
1164 const size_after = self.totalNodeCount();
1165 return @as(i64, @intCast(size_after)) - @as(i64, @intCast(size_before));
1166 }
1167
1168 pub fn localSift(self: *Manager, var_label: VarLabel, config: SiftConfig, allocator: Allocator) !SiftResult {
1169 const original_pos = self.getVarPosition(var_label);
1170 const num_vars = self.numVars();
1171
1172 if (num_vars <= 1) {
1173 return SiftResult{
1174 .original_pos = original_pos,
1175 .final_pos = original_pos,
1176 .size_delta = 0,
1177 .aborted = false,
1178 };
1179 }
1180
1181 const original_size = self.totalNodeCount();
1182 var best_pos = original_pos;
1183 var best_size = original_size;
1184 var current_pos = original_pos;
1185 var aborted = false;
1186
1187 var moves_down: u32 = 0;
1188 while (moves_down < config.max_distance and current_pos + 1 < num_vars) {
1189 const delta = try self.swapAdjacentVars(current_pos, allocator);
1190 current_pos += 1;
1191 moves_down += 1;
1192
1193 const current_size = self.totalNodeCount();
1194 if (current_size < best_size) {
1195 best_size = current_size;
1196 best_pos = current_pos;
1197 }
1198
1199 if (original_size > 0) {
1200 const blowup = @as(f64, @floatFromInt(current_size)) / @as(f64, @floatFromInt(original_size));
1201 if (blowup > config.max_blowup) {
1202 aborted = true;
1203 break;
1204 }
1205 }
1206 _ = delta;
1207 }
1208
1209 while (current_pos > original_pos) {
1210 _ = try self.swapAdjacentVars(current_pos - 1, allocator);
1211 current_pos -= 1;
1212 }
1213
1214 if (!aborted) {
1215 var moves_up: u32 = 0;
1216 while (moves_up < config.max_distance and current_pos > 0) {
1217 _ = try self.swapAdjacentVars(current_pos - 1, allocator);
1218 current_pos -= 1;
1219 moves_up += 1;
1220
1221 const current_size = self.totalNodeCount();
1222 if (current_size < best_size) {
1223 best_size = current_size;
1224 best_pos = current_pos;
1225 }
1226
1227 if (original_size > 0) {
1228 const blowup = @as(f64, @floatFromInt(current_size)) / @as(f64, @floatFromInt(original_size));
1229 if (blowup > config.max_blowup) {
1230 aborted = true;
1231 break;
1232 }
1233 }
1234 }
1235 }
1236
1237 while (current_pos < best_pos) {
1238 _ = try self.swapAdjacentVars(current_pos, allocator);
1239 current_pos += 1;
1240 }
1241 while (current_pos > best_pos) {
1242 _ = try self.swapAdjacentVars(current_pos - 1, allocator);
1243 current_pos -= 1;
1244 }
1245
1246 const final_size = self.totalNodeCount();
1247 return SiftResult{
1248 .original_pos = original_pos,
1249 .final_pos = best_pos,
1250 .size_delta = @as(i64, @intCast(final_size)) - @as(i64, @intCast(original_size)),
1251 .aborted = aborted,
1252 };
1253 }
1254
1255 pub fn globalSift(self: *Manager, config: SiftConfig, allocator: Allocator, max_passes: u32) !GlobalSiftResult {
1256 const num_vars = self.numVars();
1257 if (num_vars <= 1) {
1258 const node_count = self.totalNodeCount();
1259 return GlobalSiftResult{
1260 .total_size_delta = 0,
1261 .vars_sifted = 0,
1262 .vars_improved = 0,
1263 .original_size = node_count,
1264 .final_size = node_count,
1265 };
1266 }
1267
1268 const original_size = self.totalNodeCount();
1269 var total_delta: i64 = 0;
1270 var vars_sifted: u32 = 0;
1271 var vars_improved: u32 = 0;
1272
1273 var pass: u32 = 0;
1274 while (pass < max_passes) : (pass += 1) {
1275 var improved_this_pass = false;
1276
1277 var var_idx: VarLabel = 0;
1278 while (var_idx < num_vars) : (var_idx += 1) {
1279 const result = try self.localSift(var_idx, config, allocator);
1280 vars_sifted += 1;
1281
1282 if (result.size_delta < 0) {
1283 vars_improved += 1;
1284 improved_this_pass = true;
1285 }
1286 total_delta += result.size_delta;
1287 }
1288
1289 if (!improved_this_pass) break;
1290 }
1291
1292 const final_size = self.totalNodeCount();
1293 return GlobalSiftResult{
1294 .total_size_delta = total_delta,
1295 .vars_sifted = vars_sifted,
1296 .vars_improved = vars_improved,
1297 .original_size = original_size,
1298 .final_size = final_size,
1299 };
1300 }
1301
1302 pub fn toString(self: *const Manager, bdd: Bdd, allocator: Allocator) ![]u8 {
1303 var buffer = std.Io.Writer.Allocating.init(allocator);
1304 errdefer buffer.deinit();
1305
1306 try self.toStringHelper(bdd, &buffer.writer);
1307 return try buffer.toOwnedSlice();
1308 }
1309
1310 fn toStringHelper(self: *const Manager, bdd: Bdd, writer: anytype) !void {
1311 if (bdd.isTrue()) {
1312 try writer.writeAll("T");
1313 } else if (bdd.isFalse()) {
1314 try writer.writeAll("F");
1315 } else {
1316 const node = self.getNode(bdd);
1317 if (bdd.complement) {
1318 try writer.writeAll("!");
1319 }
1320 try writer.print("({d}, ", .{node.var_label});
1321 try self.toStringHelper(node.high, writer);
1322 try writer.writeAll(", ");
1323 try self.toStringHelper(node.low, writer);
1324 try writer.writeAll(")");
1325 }
1326 }
1327
1328 pub fn toJson(self: *const Manager, bdd: Bdd, allocator: Allocator) ![]u8 {
1329 return writeBddJson(allocator, bdd, self.nodes.items);
1330 }
1331
1332 pub fn printStats(self: *const Manager, allocator: Allocator) ![]u8 {
1333 var buffer = std.Io.Writer.Allocating.init(allocator);
1334 errdefer buffer.deinit();
1335 const writer = &buffer.writer;
1336
1337 try writer.print("BDD Manager Stats:\n", .{});
1338 try writer.print(" Variables: {d}\n", .{self.var_order.items.len});
1339 try writer.print(" Nodes: {d}\n", .{self.nodes.items.len});
1340 try writer.print(" Unique table entries: {d}\n", .{self.unique_table.count()});
1341 try writer.print(" ITE cache entries: {d}\n", .{self.ite_cache.count()});
1342 try writer.print(" Condition cache entries: {d}\n", .{self.condition_cache.count()});
1343 try writer.print(" Recursive calls: {d}\n", .{self.num_recursive_calls});
1344 try writer.print(" ITE cache hits: {d}\n", .{self.ite_cache_hits});
1345 try writer.print(" ITE cache misses: {d}\n", .{self.ite_cache_misses});
1346 try writer.print(" Unique table grows: {d}\n", .{self.unique_table_grows});
1347 try writer.print(" ITE cache grows: {d}\n", .{self.ite_cache_grows});
1348 const total = self.ite_cache_hits + self.ite_cache_misses;
1349 if (total > 0) {
1350 const hit_ratio = @as(f64, @floatFromInt(self.ite_cache_hits)) / @as(f64, @floatFromInt(total)) * 100.0;
1351 try writer.print(" ITE cache hit ratio: {d:.1}%\n", .{hit_ratio});
1352 }
1353
1354 return try buffer.toOwnedSlice();
1355 }
1356 };
1357
1358 pub const BddCopy = struct {
1359 root: Bdd,
1360 nodes: []Node,
1361 var_order: []u32,
1362 allocator: Allocator,
1363
1364 pub fn deinit(self: *BddCopy) void {
1365 self.allocator.free(self.nodes);
1366 self.allocator.free(self.var_order);
1367 }
1368
1369 pub fn isConst(self: *const BddCopy) bool {
1370 return self.root.isConst();
1371 }
1372
1373 pub fn isTrue(self: *const BddCopy) bool {
1374 return self.root.isTrue();
1375 }
1376
1377 pub fn isFalse(self: *const BddCopy) bool {
1378 return self.root.isFalse();
1379 }
1380
1381 pub fn getNode(self: *const BddCopy, bdd: Bdd) Node {
1382 return self.nodes[bdd.index];
1383 }
1384
1385 pub fn toJson(self: *const BddCopy, allocator: Allocator) ![]u8 {
1386 return writeBddJson(allocator, self.root, self.nodes);
1387 }
1388 };
1389
1390 fn writeBddJson(allocator: Allocator, root: Bdd, nodes: []const Node) ![]u8 {
1391 var visited = std.AutoHashMap(u32, void).init(allocator);
1392 defer visited.deinit();
1393 try collectJsonNodes(root, nodes, &visited);
1394
1395 const indices = try allocator.alloc(u32, visited.count());
1396 defer allocator.free(indices);
1397 var index_count: usize = 0;
1398 var iterator = visited.keyIterator();
1399 while (iterator.next()) |index| {
1400 indices[index_count] = index.*;
1401 index_count += 1;
1402 }
1403 std.debug.assert(index_count == indices.len);
1404 std.mem.sort(u32, indices, {}, std.sort.asc(u32));
1405
1406 var output = std.Io.Writer.Allocating.init(allocator);
1407 errdefer output.deinit();
1408 var stream = pretty_json.Writer.init(&output.writer, .minified);
1409 const object = try stream.object();
1410 try writeNodeRef(object, "root", root);
1411 const node_objects = try object.object("nodes");
1412 for (indices) |index| {
1413 const node_object = try node_objects.formattedObject(16, "n{d}", .{index});
1414 const node = nodes[index];
1415 try node_object.field("var", node.var_label);
1416 try writeNodeRef(node_object, "high", node.high);
1417 try writeNodeRef(node_object, "low", node.low);
1418 try node_object.end();
1419 }
1420 try node_objects.end();
1421 try object.end();
1422 return try output.toOwnedSlice();
1423 }
1424
1425 fn collectJsonNodes(
1426 bdd: Bdd,
1427 nodes: []const Node,
1428 visited: *std.AutoHashMap(u32, void),
1429 ) !void {
1430 if (bdd.isConst()) return;
1431 const index = bdd.index;
1432 if (visited.contains(index)) return;
1433 try visited.put(index, {});
1434 const node = nodes[index];
1435 try collectJsonNodes(node.high, nodes, visited);
1436 try collectJsonNodes(node.low, nodes, visited);
1437 }
1438
1439 fn writeNodeRef(object: pretty_json.Object, name: []const u8, bdd: Bdd) !void {
1440 if (bdd.isTrue()) {
1441 try object.field(name, "true");
1442 } else if (bdd.isFalse()) {
1443 try object.field(name, "false");
1444 } else if (bdd.complement) {
1445 try object.formattedString(name, 16, "!n{d}", .{bdd.index});
1446 } else {
1447 try object.formattedString(name, 16, "n{d}", .{bdd.index});
1448 }
1449 }
1450
1451 pub fn deepCopy(manager: *const Manager, bdd: Bdd, allocator: Allocator) !BddCopy {
1452 const nodes = try allocator.dupe(Node, manager.nodes.items);
1453 errdefer allocator.free(nodes);
1454
1455 const var_order = try allocator.dupe(u32, manager.var_order.items);
1456
1457 return BddCopy{
1458 .root = bdd,
1459 .nodes = nodes,
1460 .var_order = var_order,
1461 .allocator = allocator,
1462 };
1463 }
1464
1465 test "manager initialization releases each failed allocation" {
1466 try std.testing.checkAllAllocationFailures(std.testing.allocator, initializeManager, .{});
1467 }
1468
1469 fn initializeManager(allocator: Allocator) !void {
1470 var manager = try Manager.init(allocator);
1471 defer manager.deinit();
1472 try std.testing.expectEqual(@as(usize, 1), manager.nodes.items.len);
1473 }
1474
1475 test "basic constants" {
1476 const allocator = std.testing.allocator;
1477 var manager = try Manager.init(allocator);
1478 defer manager.deinit();
1479
1480 try std.testing.expect(Bdd.TRUE.isTrue());
1481 try std.testing.expect(!Bdd.TRUE.isFalse());
1482 try std.testing.expect(Bdd.FALSE.isFalse());
1483 try std.testing.expect(!Bdd.FALSE.isTrue());
1484 try std.testing.expect(Bdd.TRUE.isConst());
1485 try std.testing.expect(Bdd.FALSE.isConst());
1486 }
1487
1488 test "variable creation" {
1489 const allocator = std.testing.allocator;
1490 var manager = try Manager.init(allocator);
1491 defer manager.deinit();
1492
1493 const x = try manager.newVar(true);
1494 const y = try manager.newVar(true);
1495
1496 try std.testing.expect(!x.isConst());
1497 try std.testing.expect(!y.isConst());
1498 try std.testing.expect(x.toRaw() != y.toRaw());
1499 try std.testing.expect(manager.isVar(x));
1500 try std.testing.expect(manager.isVar(y));
1501 }
1502
1503 test "negation" {
1504 const allocator = std.testing.allocator;
1505 var manager = try Manager.init(allocator);
1506 defer manager.deinit();
1507
1508 const x = try manager.newVar(true);
1509 const not_x = manager.bddNot(x);
1510
1511 try std.testing.expect(x.neg().toRaw() == not_x.toRaw());
1512 try std.testing.expect(not_x.neg().toRaw() == x.toRaw());
1513 try std.testing.expect(Bdd.TRUE.neg().toRaw() == Bdd.FALSE.toRaw());
1514 try std.testing.expect(Bdd.FALSE.neg().toRaw() == Bdd.TRUE.toRaw());
1515 }
1516
1517 test "and operation" {
1518 const allocator = std.testing.allocator;
1519 var manager = try Manager.init(allocator);
1520 defer manager.deinit();
1521
1522 const x = try manager.newVar(true);
1523 const y = try manager.newVar(true);
1524
1525 try std.testing.expect(manager.eq(try manager.bddAnd(x, Bdd.TRUE), x));
1526
1527 try std.testing.expect(manager.eq(try manager.bddAnd(x, Bdd.FALSE), Bdd.FALSE));
1528
1529 try std.testing.expect(manager.eq(try manager.bddAnd(x, x), x));
1530
1531 const x_neg = x.neg();
1532 const result = try manager.bddAnd(x, x_neg);
1533 try std.testing.expectEqual(Bdd.FALSE.toRaw(), result.toRaw());
1534
1535 const x_and_y = try manager.bddAnd(x, y);
1536 try std.testing.expect(!x_and_y.isConst());
1537 }
1538
1539 test "or operation" {
1540 const allocator = std.testing.allocator;
1541 var manager = try Manager.init(allocator);
1542 defer manager.deinit();
1543
1544 const x = try manager.newVar(true);
1545 const y = try manager.newVar(true);
1546
1547 try std.testing.expect(manager.eq(try manager.bddOr(x, Bdd.FALSE), x));
1548
1549 try std.testing.expect(manager.eq(try manager.bddOr(x, Bdd.TRUE), Bdd.TRUE));
1550
1551 try std.testing.expect(manager.eq(try manager.bddOr(x, x), x));
1552
1553 try std.testing.expect(manager.eq(try manager.bddOr(x, x.neg()), Bdd.TRUE));
1554
1555 const x_or_y = try manager.bddOr(x, y);
1556 try std.testing.expect(!x_or_y.isConst());
1557 }
1558
1559 test "iff and xor" {
1560 const allocator = std.testing.allocator;
1561 var manager = try Manager.init(allocator);
1562 defer manager.deinit();
1563
1564 const x = try manager.newVar(true);
1565 const y = try manager.newVar(true);
1566
1567 try std.testing.expect(manager.eq(try manager.bddIff(x, x), Bdd.TRUE));
1568
1569 try std.testing.expect(manager.eq(try manager.bddIff(x, x.neg()), Bdd.FALSE));
1570
1571 try std.testing.expect(manager.eq(try manager.bddXor(x, x), Bdd.FALSE));
1572
1573 try std.testing.expect(manager.eq(try manager.bddXor(x, x.neg()), Bdd.TRUE));
1574
1575 const iff = try manager.bddIff(x, y);
1576 const xor = try manager.bddXor(x, y);
1577 try std.testing.expect(manager.eq(iff, xor.neg()));
1578 }
1579
1580 test "binary boolean fast paths avoid trivial ite work" {
1581 const allocator = std.testing.allocator;
1582 var manager = try Manager.init(allocator);
1583 defer manager.deinit();
1584
1585 const x = try manager.newVar(true);
1586 const y = try manager.newVar(true);
1587
1588 manager.resetStats();
1589 try std.testing.expectEqual(Bdd.FALSE.toRaw(), (try manager.bddAnd(x, Bdd.FALSE)).toRaw());
1590 try std.testing.expectEqual(x.toRaw(), (try manager.bddAnd(x, Bdd.TRUE)).toRaw());
1591 try std.testing.expectEqual(x.toRaw(), (try manager.bddAnd(x, x)).toRaw());
1592 try std.testing.expectEqual(Bdd.FALSE.toRaw(), (try manager.bddAnd(x, x.neg())).toRaw());
1593 try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddOr(x, Bdd.TRUE)).toRaw());
1594 try std.testing.expectEqual(x.toRaw(), (try manager.bddOr(x, Bdd.FALSE)).toRaw());
1595 try std.testing.expectEqual(x.toRaw(), (try manager.bddOr(x, x)).toRaw());
1596 try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddOr(x, x.neg())).toRaw());
1597 try std.testing.expectEqual(x.toRaw(), (try manager.bddXor(x, Bdd.FALSE)).toRaw());
1598 try std.testing.expectEqual(x.neg().toRaw(), (try manager.bddXor(x, Bdd.TRUE)).toRaw());
1599 try std.testing.expectEqual(Bdd.FALSE.toRaw(), (try manager.bddXor(x, x)).toRaw());
1600 try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddXor(x, x.neg())).toRaw());
1601 try std.testing.expectEqual(x.toRaw(), (try manager.bddIff(x, Bdd.TRUE)).toRaw());
1602 try std.testing.expectEqual(x.neg().toRaw(), (try manager.bddIff(x, Bdd.FALSE)).toRaw());
1603 try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddIff(x, x)).toRaw());
1604 try std.testing.expectEqual(Bdd.FALSE.toRaw(), (try manager.bddIff(x, x.neg())).toRaw());
1605 try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddImplies(x, x)).toRaw());
1606 try std.testing.expectEqual(x.neg().toRaw(), (try manager.bddImplies(x, Bdd.FALSE)).toRaw());
1607 try std.testing.expectEqual(@as(u64, 0), manager.numRecursiveCalls());
1608
1609 const xy = try manager.bddAnd(x, y);
1610 const hits_before = manager.ite_cache_hits;
1611 const yx = try manager.bddAnd(y, x);
1612
1613 try std.testing.expectEqual(xy.toRaw(), yx.toRaw());
1614 try std.testing.expect(manager.ite_cache_hits > hits_before);
1615 }
1616
1617 test "ite cache reserves bulk capacity after startup" {
1618 const allocator = std.testing.allocator;
1619 var manager = try Manager.init(allocator);
1620 defer manager.deinit();
1621
1622 const initial_capacity = manager.ite_cache.capacity();
1623 const max_load = (initial_capacity * Manager.TABLE_MAX_LOAD_PERCENTAGE) / 100;
1624 try std.testing.expectEqual(max_load, manager.ite_cache_grow_at);
1625
1626 for (0..max_load) |i| {
1627 const f = Bdd{ .index = @intCast(i + 1), .complement = false };
1628 try std.testing.expect(try manager.putIteCacheNoClobber(IteKey.init(f, Bdd.TRUE, Bdd.FALSE), Bdd.TRUE));
1629 }
1630
1631 try std.testing.expectEqual(initial_capacity, manager.ite_cache.capacity());
1632 try std.testing.expectEqual(max_load, manager.ite_cache_grow_at);
1633
1634 const f = Bdd{ .index = @intCast(max_load + 1), .complement = false };
1635 try std.testing.expect(try manager.putIteCacheNoClobber(IteKey.init(f, Bdd.TRUE, Bdd.FALSE), Bdd.TRUE));
1636
1637 try std.testing.expect(manager.ite_cache.capacity() >= initial_capacity * 4);
1638 try std.testing.expectEqual(
1639 Manager.tableLoadThreshold(manager.ite_cache.capacity()),
1640 manager.ite_cache_grow_at,
1641 );
1642 }
1643
1644 test "canonical table reserves bulk capacity after startup" {
1645 const allocator = std.testing.allocator;
1646 var manager = try Manager.init(allocator);
1647 defer manager.deinit();
1648
1649 const initial_capacity = manager.unique_table.capacity();
1650 const max_load = (initial_capacity * Manager.TABLE_MAX_LOAD_PERCENTAGE) / 100;
1651 try std.testing.expectEqual(max_load, manager.unique_table_grow_at);
1652
1653 for (0..max_load) |_| {
1654 _ = try manager.newVar(true);
1655 }
1656
1657 try std.testing.expectEqual(initial_capacity, manager.unique_table.capacity());
1658 try std.testing.expectEqual(max_load, manager.unique_table_grow_at);
1659
1660 _ = try manager.newVar(true);
1661
1662 try std.testing.expect(manager.unique_table.capacity() >= initial_capacity * 4);
1663 try std.testing.expectEqual(
1664 Manager.tableLoadThreshold(manager.unique_table.capacity()),
1665 manager.unique_table_grow_at,
1666 );
1667 }
1668
1669 test "simple equality: (a OR b) AND a = a" {
1670 const allocator = std.testing.allocator;
1671 var manager = try Manager.init(allocator);
1672 defer manager.deinit();
1673
1674 const a = try manager.newVar(true);
1675 const b = try manager.newVar(true);
1676
1677 const a_or_b = try manager.bddOr(a, b);
1678 const result = try manager.bddAnd(a_or_b, a);
1679
1680 try std.testing.expect(manager.eq(result, a));
1681 }
1682
1683 test "condition (restrict)" {
1684 const allocator = std.testing.allocator;
1685 var manager = try Manager.init(allocator);
1686 defer manager.deinit();
1687
1688 const x = try manager.newVar(true);
1689 const y = try manager.newVar(true);
1690
1691 const x_or_y = try manager.bddOr(x, y);
1692 const restricted = try manager.condition(x_or_y, 1, false);
1693 try std.testing.expect(manager.eq(restricted, x));
1694
1695 const x_and_y = try manager.bddAnd(x, y);
1696 const restricted2 = try manager.condition(x_and_y, 0, true);
1697 try std.testing.expect(manager.eq(restricted2, y));
1698 }
1699
1700 test "condition cache with shared subgraphs" {
1701 const allocator = std.testing.allocator;
1702 var manager = try Manager.init(allocator);
1703 defer manager.deinit();
1704
1705 try std.testing.expect(manager.condition_cache.capacity() < Manager.INITIAL_MANAGER_CAPACITY);
1706 try std.testing.expect(manager.condition_cache.capacity() >= Manager.INITIAL_CONDITION_CACHE_CAPACITY);
1707
1708 const num_vars = 25;
1709 var vars: [num_vars]Bdd = undefined;
1710 for (0..num_vars) |i| {
1711 vars[i] = try manager.newVar(true);
1712 }
1713
1714 var result = vars[0];
1715 for (1..num_vars) |i| {
1716 result = try manager.bddXor(result, vars[i]);
1717 }
1718
1719 const middle = num_vars / 2;
1720 var others: ?Bdd = null;
1721 for (0..num_vars) |i| {
1722 if (i == middle) continue;
1723 others = if (others) |acc| try manager.bddXor(acc, vars[i]) else vars[i];
1724 }
1725
1726 const middle_var: VarLabel = @intCast(middle);
1727 const restricted_true = try manager.condition(result, middle_var, true);
1728 const restricted_false = try manager.condition(result, middle_var, false);
1729
1730 try std.testing.expect(manager.eq(restricted_true, manager.bddNot(others.?)));
1731 try std.testing.expect(manager.eq(restricted_false, others.?));
1732
1733 try std.testing.expect(manager.condition_cache.count() > 0);
1734 try std.testing.expect(manager.condition_cache.capacity() > 0);
1735 }
1736
1737 test "existential quantification" {
1738 const allocator = std.testing.allocator;
1739 var manager = try Manager.init(allocator);
1740 defer manager.deinit();
1741
1742 const x = try manager.newVar(true);
1743 const y = try manager.newVar(true);
1744 const z = try manager.newVar(true);
1745
1746 const x_and_y = try manager.bddAnd(x, y);
1747 const x_and_y_and_z = try manager.bddAnd(x_and_y, z);
1748 const result = try manager.exists(x_and_y_and_z, 1);
1749 const expected = try manager.bddAnd(x, z);
1750
1751 try std.testing.expect(manager.eq(result, expected));
1752 }
1753
1754 test "compose" {
1755 const allocator = std.testing.allocator;
1756 var manager = try Manager.init(allocator);
1757 defer manager.deinit();
1758
1759 const x = try manager.newVar(true);
1760 const y = try manager.newVar(true);
1761 const z = try manager.newVar(true);
1762
1763 const x_and_y = try manager.bddAnd(x, y);
1764 const result = try manager.compose(x_and_y, 1, z);
1765 const expected = try manager.bddAnd(x, z);
1766
1767 try std.testing.expect(manager.eq(result, expected));
1768 }
1769
1770 test "has variable" {
1771 const allocator = std.testing.allocator;
1772 var manager = try Manager.init(allocator);
1773 defer manager.deinit();
1774
1775 const x = try manager.newVar(true);
1776 const y = try manager.newVar(true);
1777 _ = try manager.newVar(true);
1778
1779 const x_and_y = try manager.bddAnd(x, y);
1780
1781 try std.testing.expect(manager.hasVariable(x_and_y, 0));
1782 try std.testing.expect(manager.hasVariable(x_and_y, 1));
1783 try std.testing.expect(!manager.hasVariable(x_and_y, 2));
1784 try std.testing.expect(!manager.hasVariable(Bdd.TRUE, 0));
1785 }
1786
1787 test "size" {
1788 const allocator = std.testing.allocator;
1789 var manager = try Manager.init(allocator);
1790 defer manager.deinit();
1791
1792 try std.testing.expectEqual(@as(usize, 0), manager.size(Bdd.TRUE));
1793 try std.testing.expectEqual(@as(usize, 0), manager.size(Bdd.FALSE));
1794
1795 const x = try manager.newVar(true);
1796 try std.testing.expectEqual(@as(usize, 1), manager.size(x));
1797
1798 const y = try manager.newVar(true);
1799 const x_and_y = try manager.bddAnd(x, y);
1800 try std.testing.expectEqual(@as(usize, 2), manager.size(x_and_y));
1801 }
1802
1803 test "getVarPosition and getVarAtPosition" {
1804 const allocator = std.testing.allocator;
1805 var manager = try Manager.init(allocator);
1806 defer manager.deinit();
1807
1808 _ = try manager.newVar(true);
1809 _ = try manager.newVar(true);
1810 _ = try manager.newVar(true);
1811
1812 try std.testing.expectEqual(@as(u32, 0), manager.getVarPosition(0));
1813 try std.testing.expectEqual(@as(u32, 1), manager.getVarPosition(1));
1814 try std.testing.expectEqual(@as(u32, 2), manager.getVarPosition(2));
1815
1816 try std.testing.expectEqual(@as(?VarLabel, 0), manager.getVarAtPosition(0));
1817 try std.testing.expectEqual(@as(?VarLabel, 1), manager.getVarAtPosition(1));
1818 try std.testing.expectEqual(@as(?VarLabel, 2), manager.getVarAtPosition(2));
1819 try std.testing.expectEqual(@as(?VarLabel, null), manager.getVarAtPosition(3));
1820 }
1821
1822 test "totalNodeCount" {
1823 const allocator = std.testing.allocator;
1824 var manager = try Manager.init(allocator);
1825 defer manager.deinit();
1826
1827 try std.testing.expectEqual(@as(usize, 0), manager.totalNodeCount());
1828
1829 _ = try manager.newVar(true);
1830 try std.testing.expectEqual(@as(usize, 1), manager.totalNodeCount());
1831
1832 const y = try manager.newVar(true);
1833 try std.testing.expectEqual(@as(usize, 2), manager.totalNodeCount());
1834
1835 const x = try manager.newVar(true);
1836 _ = try manager.bddAnd(x, y);
1837 try std.testing.expect(manager.totalNodeCount() >= 3);
1838 }
1839
1840 test "nodesAtLevel" {
1841 const allocator = std.testing.allocator;
1842 var manager = try Manager.init(allocator);
1843 defer manager.deinit();
1844
1845 const x = try manager.newVar(true);
1846 const y = try manager.newVar(true);
1847
1848 try std.testing.expectEqual(@as(usize, 1), manager.nodesAtLevel(0));
1849 try std.testing.expectEqual(@as(usize, 1), manager.nodesAtLevel(1));
1850
1851 _ = try manager.bddAnd(x, y);
1852 try std.testing.expect(manager.nodesAtLevel(0) >= 1);
1853 }
1854
1855 test "swapAdjacentVars basic" {
1856 const allocator = std.testing.allocator;
1857 var manager = try Manager.init(allocator);
1858 defer manager.deinit();
1859
1860 const x = try manager.newVar(true);
1861 const y = try manager.newVar(true);
1862 _ = try manager.bddAnd(x, y);
1863
1864 try std.testing.expectEqual(@as(u32, 0), manager.getVarPosition(0));
1865 try std.testing.expectEqual(@as(u32, 1), manager.getVarPosition(1));
1866
1867 _ = try manager.swapAdjacentVars(0, allocator);
1868
1869 try std.testing.expectEqual(@as(u32, 1), manager.getVarPosition(0));
1870 try std.testing.expectEqual(@as(u32, 0), manager.getVarPosition(1));
1871 }
1872
1873 test "localSift single variable" {
1874 const allocator = std.testing.allocator;
1875 var manager = try Manager.init(allocator);
1876 defer manager.deinit();
1877
1878 _ = try manager.newVar(true);
1879
1880 const result = try manager.localSift(0, SiftConfig{}, allocator);
1881 try std.testing.expectEqual(@as(u32, 0), result.original_pos);
1882 try std.testing.expectEqual(@as(u32, 0), result.final_pos);
1883 try std.testing.expectEqual(@as(i64, 0), result.size_delta);
1884 try std.testing.expect(!result.aborted);
1885 }
1886
1887 test "localSift returns to best position" {
1888 const allocator = std.testing.allocator;
1889 var manager = try Manager.init(allocator);
1890 defer manager.deinit();
1891
1892 _ = try manager.newVar(true);
1893 _ = try manager.newVar(true);
1894 _ = try manager.newVar(true);
1895
1896 const initial_pos = manager.getVarPosition(0);
1897 const result = try manager.localSift(0, SiftConfig{ .max_distance = 2 }, allocator);
1898
1899 try std.testing.expect(result.original_pos == initial_pos);
1900 try std.testing.expect(result.final_pos <= 2);
1901 try std.testing.expect(!result.aborted);
1902 }
1903
1904 test "min/max variable tracking" {
1905 const allocator = std.testing.allocator;
1906 var manager = try Manager.init(allocator);
1907 defer manager.deinit();
1908
1909 try std.testing.expectEqual(NO_VAR, manager.getMinVar(Bdd.TRUE));
1910 try std.testing.expectEqual(NO_VAR, manager.getMaxVar(Bdd.TRUE));
1911 try std.testing.expectEqual(NO_VAR, manager.getMinVar(Bdd.FALSE));
1912 try std.testing.expectEqual(NO_VAR, manager.getMaxVar(Bdd.FALSE));
1913
1914 const x = try manager.newVar(true);
1915 try std.testing.expectEqual(@as(VarLabel, 0), manager.getMinVar(x));
1916 try std.testing.expectEqual(@as(VarLabel, 0), manager.getMaxVar(x));
1917
1918 const y = try manager.newVar(true);
1919 const x_and_y = try manager.bddAnd(x, y);
1920 try std.testing.expectEqual(@as(VarLabel, 0), manager.getMinVar(x_and_y));
1921 try std.testing.expectEqual(@as(VarLabel, 1), manager.getMaxVar(x_and_y));
1922
1923 const z = try manager.newVar(true);
1924 const y_and_z = try manager.bddAnd(y, z);
1925 try std.testing.expectEqual(@as(VarLabel, 1), manager.getMinVar(y_and_z));
1926 try std.testing.expectEqual(@as(VarLabel, 2), manager.getMaxVar(y_and_z));
1927
1928 const combined = try manager.bddOr(x_and_y, y_and_z);
1929 try std.testing.expectEqual(@as(VarLabel, 0), manager.getMinVar(combined));
1930 try std.testing.expectEqual(@as(VarLabel, 2), manager.getMaxVar(combined));
1931 }
1932
1933 test "complemented edge preservation" {
1934 const allocator = std.testing.allocator;
1935 var manager = try Manager.init(allocator);
1936 defer manager.deinit();
1937
1938 const x = try manager.newVar(true);
1939 const y = try manager.newVar(true);
1940
1941 const x_and_y = try manager.bddAnd(x, y);
1942 const not_x_and_y = manager.bddNot(x_and_y);
1943
1944 const not_x = manager.bddNot(x);
1945 const not_y = manager.bddNot(y);
1946 const not_x_or_not_y = try manager.bddOr(not_x, not_y);
1947
1948 try std.testing.expect(manager.eq(not_x_and_y, not_x_or_not_y));
1949 }
1950
1951 test "de morgan's laws" {
1952 const allocator = std.testing.allocator;
1953 var manager = try Manager.init(allocator);
1954 defer manager.deinit();
1955
1956 const a = try manager.newVar(true);
1957 const b = try manager.newVar(true);
1958
1959 const lhs1 = manager.bddNot(try manager.bddAnd(a, b));
1960 const rhs1 = try manager.bddOr(manager.bddNot(a), manager.bddNot(b));
1961 try std.testing.expect(manager.eq(lhs1, rhs1));
1962
1963 const lhs2 = manager.bddNot(try manager.bddOr(a, b));
1964 const rhs2 = try manager.bddAnd(manager.bddNot(a), manager.bddNot(b));
1965 try std.testing.expect(manager.eq(lhs2, rhs2));
1966 }
1967
1968 test "three variable formula" {
1969 const allocator = std.testing.allocator;
1970 var manager = try Manager.init(allocator);
1971 defer manager.deinit();
1972
1973 const x = try manager.newVar(true);
1974 const y = try manager.newVar(true);
1975 const z = try manager.newVar(true);
1976
1977 const x_and_y = try manager.bddAnd(x, y);
1978 const formula = try manager.bddOr(x_and_y, z);
1979
1980 const cond_z_true = try manager.condition(formula, 2, true);
1981 try std.testing.expect(manager.eq(cond_z_true, Bdd.TRUE));
1982
1983 const cond_z_false = try manager.condition(formula, 2, false);
1984 try std.testing.expect(manager.eq(cond_z_false, x_and_y));
1985 }
1986
1987 test "implies operation" {
1988 const allocator = std.testing.allocator;
1989 var manager = try Manager.init(allocator);
1990 defer manager.deinit();
1991
1992 const a = try manager.newVar(true);
1993 const b = try manager.newVar(true);
1994
1995 try std.testing.expect(manager.eq(try manager.bddImplies(a, a), Bdd.TRUE));
1996
1997 try std.testing.expect(manager.eq(try manager.bddImplies(Bdd.FALSE, a), Bdd.TRUE));
1998
1999 try std.testing.expect(manager.eq(try manager.bddImplies(a, Bdd.TRUE), Bdd.TRUE));
2000
2001 try std.testing.expect(manager.eq(try manager.bddImplies(Bdd.TRUE, a), a));
2002
2003 try std.testing.expect(manager.eq(try manager.bddImplies(a, Bdd.FALSE), a.neg()));
2004
2005 const implies = try manager.bddImplies(a, b);
2006 const or_form = try manager.bddOr(a.neg(), b);
2007 try std.testing.expect(manager.eq(implies, or_form));
2008 }
2009
2010 test "recursive call counting" {
2011 const allocator = std.testing.allocator;
2012 var manager = try Manager.init(allocator);
2013 defer manager.deinit();
2014
2015 const initial_calls = manager.numRecursiveCalls();
2016
2017 const x = try manager.newVar(true);
2018 const y = try manager.newVar(true);
2019 _ = try manager.bddAnd(x, y);
2020
2021 try std.testing.expect(manager.numRecursiveCalls() > initial_calls);
2022
2023 manager.resetStats();
2024 try std.testing.expectEqual(@as(u64, 0), manager.numRecursiveCalls());
2025 }
2026
2027 test "newVarAtPosition" {
2028 const allocator = std.testing.allocator;
2029 var manager = try Manager.init(allocator);
2030 defer manager.deinit();
2031
2032 const x = try manager.newVar(true);
2033 const y = try manager.newVar(true);
2034
2035 const z = try manager.newVarAtPosition(0, true);
2036
2037 const z_and_x = try manager.bddAnd(z, x);
2038
2039 try std.testing.expectEqual(@as(VarLabel, 2), manager.topVar(z_and_x));
2040
2041 const x_and_y = try manager.bddAnd(x, y);
2042 try std.testing.expect(!x_and_y.isConst());
2043 }
2044
2045 test "sequentialCompose behavior" {
2046 const allocator = std.testing.allocator;
2047 var manager = try Manager.init(allocator);
2048 defer manager.deinit();
2049
2050 const x = try manager.newVar(true);
2051 const y = try manager.newVar(true);
2052 const z = try manager.newVar(true);
2053
2054 const x_and_y = try manager.bddAnd(x, y);
2055 const result1 = try manager.sequentialCompose(
2056 x_and_y,
2057 &[_]VarLabel{ 0, 1 },
2058 &[_]Bdd{ z, z },
2059 );
2060 try std.testing.expect(manager.eq(result1, z));
2061
2062 const result2 = try manager.sequentialCompose(
2063 x,
2064 &[_]VarLabel{ 0, 1 },
2065 &[_]Bdd{ y, x },
2066 );
2067 try std.testing.expect(manager.eq(result2, x));
2068
2069 const single_result = try manager.sequentialCompose(
2070 x_and_y,
2071 &[_]VarLabel{1},
2072 &[_]Bdd{z},
2073 );
2074 const compose_result = try manager.compose(x_and_y, 1, z);
2075 try std.testing.expect(manager.eq(single_result, compose_result));
2076 }
2077
2078 test "newVarAtPosition preserves existing BDDs" {
2079 const allocator = std.testing.allocator;
2080 var manager = try Manager.init(allocator);
2081 defer manager.deinit();
2082
2083 const x = try manager.newVar(true);
2084 const y = try manager.newVar(true);
2085
2086 const x_or_y = try manager.bddOr(x, y);
2087
2088 _ = try manager.newVarAtPosition(0, true);
2089
2090 const cond_x_true = try manager.condition(x_or_y, 0, true);
2091 try std.testing.expect(manager.eq(cond_x_true, Bdd.TRUE));
2092
2093 const cond_x_false = try manager.condition(x_or_y, 0, false);
2094 try std.testing.expect(manager.eq(cond_x_false, y));
2095 }
2096
2097 const DualNumber = struct {
2098 primal: f64,
2099 partials: []f64,
2100 allocator: Allocator,
2101
2102 pub fn init(allocator: Allocator, primal: f64, num_partials: usize) !DualNumber {
2103 const partials = try allocator.alloc(f64, num_partials);
2104 @memset(partials, 0.0);
2105 return DualNumber{
2106 .primal = primal,
2107 .partials = partials,
2108 .allocator = allocator,
2109 };
2110 }
2111
2112 pub fn initWithPartials(allocator: Allocator, primal: f64, partials: []const f64) !DualNumber {
2113 const owned_partials = try allocator.alloc(f64, partials.len);
2114 @memcpy(owned_partials, partials);
2115 return DualNumber{
2116 .primal = primal,
2117 .partials = owned_partials,
2118 .allocator = allocator,
2119 };
2120 }
2121
2122 pub fn constant(allocator: Allocator, value: f64, num_partials: usize) !DualNumber {
2123 return init(allocator, value, num_partials);
2124 }
2125
2126 pub fn deinit(self: *DualNumber) void {
2127 self.allocator.free(self.partials);
2128 }
2129
2130 pub fn add(self: DualNumber, other: DualNumber) DualNumber {
2131 for (self.partials, other.partials) |*sp, op| {
2132 sp.* += op;
2133 }
2134 return DualNumber{
2135 .primal = self.primal + other.primal,
2136 .partials = self.partials,
2137 .allocator = self.allocator,
2138 };
2139 }
2140
2141 pub fn mul(self: DualNumber, other: DualNumber) DualNumber {
2142 for (self.partials, other.partials) |*sp, op| {
2143 sp.* = self.primal * op + other.primal * sp.*;
2144 }
2145 return DualNumber{
2146 .primal = self.primal * other.primal,
2147 .partials = self.partials,
2148 .allocator = self.allocator,
2149 };
2150 }
2151
2152 pub fn clone(self: DualNumber) !DualNumber {
2153 return initWithPartials(self.allocator, self.primal, self.partials);
2154 }
2155 };
2156
2157 pub const VarWeight = struct {
2158 low: f64,
2159 high: f64,
2160 };
2161
2162 const VarWeightDual = struct {
2163 low: f64,
2164 low_partials: []f64,
2165 high: f64,
2166 high_partials: []f64,
2167 };
2168
2169 pub const WmcParams = struct {
2170 allocator: Allocator,
2171
2172 num_partials: usize,
2173
2174 weights: std.ArrayListUnmanaged(VarWeight),
2175
2176 dual_weights: std.ArrayListUnmanaged(VarWeightDual),
2177
2178 is_dual: bool,
2179
2180 pub fn init(allocator: Allocator) WmcParams {
2181 return WmcParams{
2182 .allocator = allocator,
2183 .num_partials = 0,
2184 .weights = std.ArrayListUnmanaged(VarWeight).empty,
2185 .dual_weights = std.ArrayListUnmanaged(VarWeightDual).empty,
2186 .is_dual = false,
2187 };
2188 }
2189
2190 pub fn initDual(allocator: Allocator, num_partials: usize) WmcParams {
2191 return WmcParams{
2192 .allocator = allocator,
2193 .num_partials = num_partials,
2194 .weights = std.ArrayListUnmanaged(VarWeight).empty,
2195 .dual_weights = std.ArrayListUnmanaged(VarWeightDual).empty,
2196 .is_dual = true,
2197 };
2198 }
2199
2200 pub fn deinit(self: *WmcParams) void {
2201 self.weights.deinit(self.allocator);
2202 for (self.dual_weights.items) |*dw| {
2203 self.allocator.free(dw.low_partials);
2204 self.allocator.free(dw.high_partials);
2205 }
2206 self.dual_weights.deinit(self.allocator);
2207 }
2208
2209 fn ensureCapacity(self: *WmcParams, variable: VarLabel) !void {
2210 const needed = variable + 1;
2211 while (self.weights.items.len < needed) {
2212 try self.weights.append(self.allocator, VarWeight{ .low = 1.0, .high = 1.0 });
2213 }
2214 }
2215
2216 fn ensureCapacityDual(self: *WmcParams, variable: VarLabel) !void {
2217 const needed = variable + 1;
2218 while (self.dual_weights.items.len < needed) {
2219 const low_partials = try self.allocator.alloc(f64, self.num_partials);
2220 @memset(low_partials, 0.0);
2221 const high_partials = try self.allocator.alloc(f64, self.num_partials);
2222 @memset(high_partials, 0.0);
2223 try self.dual_weights.append(self.allocator, VarWeightDual{
2224 .low = 1.0,
2225 .low_partials = low_partials,
2226 .high = 1.0,
2227 .high_partials = high_partials,
2228 });
2229 }
2230 }
2231
2232 pub fn setWeight(self: *WmcParams, variable: VarLabel, low: f64, high: f64) !void {
2233 try self.ensureCapacity(variable);
2234 self.weights.items[variable] = VarWeight{ .low = low, .high = high };
2235
2236 if (self.is_dual) {
2237 try self.ensureCapacityDual(variable);
2238 self.dual_weights.items[variable].low = low;
2239 self.dual_weights.items[variable].high = high;
2240 @memset(self.dual_weights.items[variable].low_partials, 0.0);
2241 @memset(self.dual_weights.items[variable].high_partials, 0.0);
2242 }
2243 }
2244
2245 pub fn setWeightDeriv(
2246 self: *WmcParams,
2247 variable: VarLabel,
2248 low: f64,
2249 low_partials: []const f64,
2250 high: f64,
2251 high_partials: []const f64,
2252 ) !void {
2253 std.debug.assert(self.is_dual);
2254 std.debug.assert(low_partials.len == self.num_partials);
2255 std.debug.assert(high_partials.len == self.num_partials);
2256
2257 try self.ensureCapacity(variable);
2258 self.weights.items[variable] = VarWeight{ .low = low, .high = high };
2259
2260 try self.ensureCapacityDual(variable);
2261 self.dual_weights.items[variable].low = low;
2262 self.dual_weights.items[variable].high = high;
2263 @memcpy(self.dual_weights.items[variable].low_partials, low_partials);
2264 @memcpy(self.dual_weights.items[variable].high_partials, high_partials);
2265 }
2266
2267 pub fn getWeight(self: *const WmcParams, variable: VarLabel) VarWeight {
2268 if (variable >= self.weights.items.len) {
2269 return VarWeight{ .low = 1.0, .high = 1.0 };
2270 }
2271 return self.weights.items[variable];
2272 }
2273
2274 fn getDualWeight(self: *const WmcParams, variable: VarLabel) ?VarWeightDual {
2275 if (!self.is_dual or variable >= self.dual_weights.items.len) {
2276 return null;
2277 }
2278 return self.dual_weights.items[variable];
2279 }
2280 };
2281
2282 pub const WmcDualResult = struct {
2283 primal: f64,
2284 partials: []f64,
2285 allocator: Allocator,
2286
2287 pub fn deinit(self: *WmcDualResult) void {
2288 self.allocator.free(self.partials);
2289 }
2290
2291 pub fn varPartial(self: *const WmcDualResult, index: usize) f64 {
2292 if (index >= self.partials.len) return 0.0;
2293 return self.partials[index];
2294 }
2295
2296 pub fn numPartials(self: *const WmcDualResult) usize {
2297 return self.partials.len;
2298 }
2299 };
2300
2301 pub fn wmc(manager: *const Manager, bdd: Bdd, params: *const WmcParams) f64 {
2302 return wmcWithAllocator(manager, bdd, params, manager.allocator);
2303 }
2304
2305 pub fn wmcWithAllocator(manager: *const Manager, bdd: Bdd, params: *const WmcParams, allocator: Allocator) f64 {
2306 var cache = WmcDenseCache.init(allocator, manager.nodes.items.len) catch {
2307 var hash_cache = std.AutoHashMap(u32, f64).init(allocator);
2308 defer hash_cache.deinit();
2309
2310 return wmcHelperHash(manager, bdd, params, &hash_cache);
2311 };
2312 defer cache.deinit();
2313
2314 return wmcHelper(manager, bdd, params, &cache);
2315 }
2316
2317 const WmcDenseCache = struct {
2318 const bits_per_valid_word = @bitSizeOf(usize);
2319
2320 allocator: Allocator,
2321 values: []f64,
2322 valid_words: []usize,
2323
2324 fn init(allocator: Allocator, node_count: usize) Allocator.Error!WmcDenseCache {
2325 const entry_count = node_count * 2;
2326 const values = try allocator.alloc(f64, entry_count);
2327 errdefer allocator.free(values);
2328 const valid_words = try allocator.alloc(usize, validWordCount(entry_count));
2329 @memset(valid_words, 0);
2330 return WmcDenseCache{
2331 .allocator = allocator,
2332 .values = values,
2333 .valid_words = valid_words,
2334 };
2335 }
2336
2337 fn deinit(self: *WmcDenseCache) void {
2338 self.allocator.free(self.valid_words);
2339 self.allocator.free(self.values);
2340 }
2341
2342 fn get(self: *const WmcDenseCache, bdd: Bdd) ?f64 {
2343 const index = cacheIndex(bdd);
2344 if (index >= self.values.len) return null;
2345 if (!self.isValid(index)) return null;
2346 return self.values[index];
2347 }
2348
2349 fn put(self: *WmcDenseCache, bdd: Bdd, value: f64) void {
2350 const index = cacheIndex(bdd);
2351 if (index < self.values.len) {
2352 self.values[index] = value;
2353 self.markValid(index);
2354 }
2355 }
2356
2357 fn cacheIndex(bdd: Bdd) usize {
2358 return @as(usize, bdd.index) * 2 + @intFromBool(bdd.complement);
2359 }
2360
2361 fn validWordCount(entry_count: usize) usize {
2362 return (entry_count + bits_per_valid_word - 1) / bits_per_valid_word;
2363 }
2364
2365 fn validMask(index: usize) usize {
2366 const shift: std.math.Log2Int(usize) = @intCast(index % bits_per_valid_word);
2367 return @as(usize, 1) << shift;
2368 }
2369
2370 fn isValid(self: *const WmcDenseCache, index: usize) bool {
2371 const word_index = index / bits_per_valid_word;
2372 return self.valid_words[word_index] & validMask(index) != 0;
2373 }
2374
2375 fn markValid(self: *WmcDenseCache, index: usize) void {
2376 const word_index = index / bits_per_valid_word;
2377 self.valid_words[word_index] |= validMask(index);
2378 }
2379 };
2380
2381 fn wmcHelper(
2382 manager: *const Manager,
2383 bdd: Bdd,
2384 params: *const WmcParams,
2385 cache: *WmcDenseCache,
2386 ) f64 {
2387 if (bdd.isTrue()) return 1.0;
2388 if (bdd.isFalse()) return 0.0;
2389
2390 if (cache.get(bdd)) |cached| {
2391 return cached;
2392 }
2393
2394 const node = manager.getNode(bdd);
2395 const weight = params.getWeight(node.var_label);
2396
2397 const low_child = if (bdd.complement) node.low.neg() else node.low;
2398 const high_child = if (bdd.complement) node.high.neg() else node.high;
2399
2400 const low_result = wmcHelper(manager, low_child, params, cache);
2401 const high_result = wmcHelper(manager, high_child, params, cache);
2402
2403 const result = weight.low * low_result + weight.high * high_result;
2404
2405 cache.put(bdd, result);
2406
2407 return result;
2408 }
2409
2410 fn wmcHelperHash(
2411 manager: *const Manager,
2412 bdd: Bdd,
2413 params: *const WmcParams,
2414 cache: *std.AutoHashMap(u32, f64),
2415 ) f64 {
2416 if (bdd.isTrue()) return 1.0;
2417 if (bdd.isFalse()) return 0.0;
2418
2419 const cache_key = bdd.toRaw();
2420 if (cache.get(cache_key)) |cached| {
2421 return cached;
2422 }
2423
2424 const node = manager.getNode(bdd);
2425 const weight = params.getWeight(node.var_label);
2426
2427 const low_child = if (bdd.complement) node.low.neg() else node.low;
2428 const high_child = if (bdd.complement) node.high.neg() else node.high;
2429
2430 const low_result = wmcHelperHash(manager, low_child, params, cache);
2431 const high_result = wmcHelperHash(manager, high_child, params, cache);
2432
2433 const result = weight.low * low_result + weight.high * high_result;
2434
2435 cache.put(cache_key, result) catch {};
2436
2437 return result;
2438 }
2439
2440 pub fn wmcDual(
2441 manager: *const Manager,
2442 bdd: Bdd,
2443 params: *const WmcParams,
2444 allocator: Allocator,
2445 ) !WmcDualResult {
2446 std.debug.assert(params.is_dual);
2447
2448 var cache = std.AutoHashMap(u32, DualNumber).init(allocator);
2449 defer {
2450 var it = cache.valueIterator();
2451 while (it.next()) |val| {
2452 var v = val.*;
2453 v.deinit();
2454 }
2455 cache.deinit();
2456 }
2457
2458 var result = try wmcDualHelper(manager, bdd, params, allocator, &cache);
2459
2460 const partials = result.partials;
2461 result.partials = &[_]f64{};
2462
2463 return WmcDualResult{
2464 .primal = result.primal,
2465 .partials = partials,
2466 .allocator = allocator,
2467 };
2468 }
2469
2470 fn wmcDualHelper(
2471 manager: *const Manager,
2472 bdd: Bdd,
2473 params: *const WmcParams,
2474 allocator: Allocator,
2475 cache: *std.AutoHashMap(u32, DualNumber),
2476 ) !DualNumber {
2477 if (bdd.isTrue()) {
2478 return DualNumber.constant(allocator, 1.0, params.num_partials);
2479 }
2480 if (bdd.isFalse()) {
2481 return DualNumber.constant(allocator, 0.0, params.num_partials);
2482 }
2483
2484 const cache_key = bdd.toRaw();
2485 if (cache.get(cache_key)) |cached| {
2486 return cached.clone();
2487 }
2488
2489 const node = manager.getNode(bdd);
2490
2491 const maybe_dual_weight = params.getDualWeight(node.var_label);
2492
2493 const low_child = if (bdd.complement) node.low.neg() else node.low;
2494 const high_child = if (bdd.complement) node.high.neg() else node.high;
2495
2496 var result = result: {
2497 var low_result = try wmcDualHelper(manager, low_child, params, allocator, cache);
2498 defer low_result.deinit();
2499
2500 var high_result = try wmcDualHelper(manager, high_child, params, allocator, cache);
2501 defer high_result.deinit();
2502
2503 var low_weight_dual: DualNumber = undefined;
2504 var high_weight_dual: DualNumber = undefined;
2505
2506 if (maybe_dual_weight) |dual_weight| {
2507 low_weight_dual = try DualNumber.initWithPartials(
2508 allocator,
2509 dual_weight.low,
2510 dual_weight.low_partials,
2511 );
2512 errdefer low_weight_dual.deinit();
2513 high_weight_dual = try DualNumber.initWithPartials(
2514 allocator,
2515 dual_weight.high,
2516 dual_weight.high_partials,
2517 );
2518 } else {
2519 low_weight_dual = try DualNumber.constant(allocator, 1.0, params.num_partials);
2520 errdefer low_weight_dual.deinit();
2521 high_weight_dual = try DualNumber.constant(allocator, 1.0, params.num_partials);
2522 }
2523
2524 var low_term = low_weight_dual.mul(low_result);
2525 var high_term = high_weight_dual.mul(high_result);
2526 defer high_term.deinit();
2527
2528 break :result low_term.add(high_term);
2529 };
2530 errdefer result.deinit();
2531
2532 const cached = try result.clone();
2533 cache.put(cache_key, cached) catch {
2534 var mutable_cached = cached;
2535 mutable_cached.deinit();
2536 };
2537
2538 return result;
2539 }
2540
2541 const WmcCacheEntry = struct {
2542 value: f64 = 0.0,
2543 generation: u64 = 0,
2544 };
2545
2546 pub const WmcCacheStats = struct {
2547 hits: u64 = 0,
2548 misses: u64 = 0,
2549 invalidations: u64 = 0,
2550 evictions: u64 = 0,
2551
2552 pub fn hitRate(self: WmcCacheStats) f64 {
2553 const total = self.hits + self.misses;
2554 if (total == 0) return 0.0;
2555 return @as(f64, @floatFromInt(self.hits)) / @as(f64, @floatFromInt(total));
2556 }
2557 };
2558
2559 pub const WmcContext = struct {
2560 cache: std.ArrayListUnmanaged(WmcCacheEntry),
2561
2562 entry_count: usize,
2563
2564 params_version: u64,
2565
2566 structure_version: u64,
2567
2568 cache_generation: u64,
2569
2570 stats: WmcCacheStats,
2571
2572 allocator: Allocator,
2573
2574 manager: ?*const Manager,
2575
2576 pub fn init(allocator: Allocator) WmcContext {
2577 return WmcContext{
2578 .cache = .empty,
2579 .entry_count = 0,
2580 .params_version = 0,
2581 .structure_version = 0,
2582 .cache_generation = 1,
2583 .stats = .{},
2584 .allocator = allocator,
2585 .manager = null,
2586 };
2587 }
2588
2589 pub fn deinit(self: *WmcContext) void {
2590 self.cache.deinit(self.allocator);
2591 }
2592
2593 pub fn wmcCached(
2594 self: *WmcContext,
2595 manager: *const Manager,
2596 bdd: Bdd,
2597 params: *const WmcParams,
2598 ) f64 {
2599 if (bdd.isTrue()) return 1.0;
2600 if (bdd.isFalse()) return 0.0;
2601 self.bindManager(manager);
2602 if (!self.ensureCapacity(manager.nodes.items.len)) {
2603 self.stats.misses += 1;
2604 return wmcWithAllocator(manager, bdd, params, self.allocator);
2605 }
2606
2607 if (self.getCached(bdd)) |cached| {
2608 self.stats.hits += 1;
2609 return cached;
2610 }
2611
2612 self.stats.misses += 1;
2613 return self.wmcHelperCached(manager, bdd, params);
2614 }
2615
2616 fn wmcHelperCached(
2617 self: *WmcContext,
2618 manager: *const Manager,
2619 bdd: Bdd,
2620 params: *const WmcParams,
2621 ) f64 {
2622 if (bdd.isTrue()) return 1.0;
2623 if (bdd.isFalse()) return 0.0;
2624
2625 if (self.getCached(bdd)) |cached| {
2626 return cached;
2627 }
2628
2629 const node = manager.getNode(bdd);
2630 const weight = params.getWeight(node.var_label);
2631
2632 const low_child = if (bdd.complement) node.low.neg() else node.low;
2633 const high_child = if (bdd.complement) node.high.neg() else node.high;
2634
2635 const low_result = self.wmcHelperCached(manager, low_child, params);
2636 const high_result = self.wmcHelperCached(manager, high_child, params);
2637
2638 const result = weight.low * low_result + weight.high * high_result;
2639
2640 self.putCached(bdd, result);
2641
2642 return result;
2643 }
2644
2645 fn ensureCapacity(self: *WmcContext, node_count: usize) bool {
2646 const required = node_count * 2;
2647 if (self.cache.items.len >= required) return true;
2648
2649 const old_len = self.cache.items.len;
2650 self.cache.ensureTotalCapacity(self.allocator, required) catch return false;
2651 self.cache.items.len = required;
2652 @memset(self.cache.items[old_len..], .{});
2653 return true;
2654 }
2655
2656 fn bindManager(self: *WmcContext, manager: *const Manager) void {
2657 if (self.manager) |bound| {
2658 if (bound == manager) return;
2659 self.clearEntries();
2660 }
2661 self.manager = manager;
2662 }
2663
2664 fn clearEntries(self: *WmcContext) void {
2665 @memset(self.cache.items, .{});
2666 self.entry_count = 0;
2667 }
2668
2669 fn getCached(self: *const WmcContext, bdd: Bdd) ?f64 {
2670 const index = cacheIndex(bdd);
2671 if (index >= self.cache.items.len) return null;
2672 const entry = self.cache.items[index];
2673 if (entry.generation != self.cache_generation) return null;
2674 return entry.value;
2675 }
2676
2677 fn putCached(self: *WmcContext, bdd: Bdd, value: f64) void {
2678 const index = cacheIndex(bdd);
2679 if (index >= self.cache.items.len) return;
2680 const was_occupied = self.cache.items[index].generation != 0;
2681 self.cache.items[index] = .{
2682 .value = value,
2683 .generation = self.cache_generation,
2684 };
2685 if (!was_occupied) {
2686 self.entry_count += 1;
2687 }
2688 }
2689
2690 pub fn invalidateAll(self: *WmcContext) void {
2691 self.structure_version += 1;
2692 self.advanceGeneration();
2693 self.stats.invalidations += 1;
2694 }
2695
2696 pub fn invalidateWeights(self: *WmcContext) void {
2697 self.params_version += 1;
2698 self.advanceGeneration();
2699 self.stats.invalidations += 1;
2700 }
2701
2702 fn advanceGeneration(self: *WmcContext) void {
2703 self.cache_generation +%= 1;
2704 if (self.cache_generation == 0) {
2705 self.clearEntries();
2706 self.cache_generation = 1;
2707 }
2708 }
2709
2710 pub fn invalidateForVars(
2711 self: *WmcContext,
2712 manager: *const Manager,
2713 vars: []const VarLabel,
2714 ) void {
2715 self.stats.invalidations += 1;
2716
2717 var removed: usize = 0;
2718 for (self.cache.items, 0..) |*entry, index| {
2719 if (entry.generation == 0) continue;
2720 const bdd = bddFromCacheIndex(index);
2721 for (vars) |var_label| {
2722 if (manager.hasVariable(bdd, var_label)) {
2723 entry.* = .{};
2724 removed += 1;
2725 self.entry_count -= 1;
2726 break;
2727 }
2728 }
2729 }
2730
2731 self.stats.evictions += removed;
2732 }
2733
2734 pub fn trimToSize(self: *WmcContext, max_entries: usize) usize {
2735 const current = self.entry_count;
2736 if (current <= max_entries) return 0;
2737
2738 const to_evict = current - max_entries;
2739 var evicted: usize = 0;
2740
2741 for (self.cache.items) |*entry| {
2742 if (evicted >= to_evict) break;
2743 if (entry.generation != 0) {
2744 entry.* = .{};
2745 evicted += 1;
2746 }
2747 }
2748
2749 self.entry_count -= evicted;
2750 self.stats.evictions += evicted;
2751 return evicted;
2752 }
2753
2754 pub fn clear(self: *WmcContext) void {
2755 self.clearEntries();
2756 self.stats = .{};
2757 self.params_version = 0;
2758 self.structure_version = 0;
2759 self.cache_generation = 1;
2760 self.manager = null;
2761 }
2762
2763 pub fn cacheSize(self: *const WmcContext) usize {
2764 return self.entry_count;
2765 }
2766
2767 pub fn getStats(self: *const WmcContext) WmcCacheStats {
2768 return self.stats;
2769 }
2770
2771 fn cacheIndex(bdd: Bdd) usize {
2772 return @as(usize, bdd.index) * 2 + @intFromBool(bdd.complement);
2773 }
2774
2775 fn bddFromCacheIndex(index: usize) Bdd {
2776 return Bdd{
2777 .index = @intCast(index / 2),
2778 .complement = index % 2 == 1,
2779 };
2780 }
2781 };
2782
2783 test "wmc scalar - constant BDDs" {
2784 const allocator = std.testing.allocator;
2785 var manager = try Manager.init(allocator);
2786 defer manager.deinit();
2787
2788 var params = WmcParams.init(allocator);
2789 defer params.deinit();
2790
2791 try std.testing.expectApproxEqAbs(@as(f64, 1.0), wmc(&manager, Bdd.TRUE, ¶ms), 1e-10);
2792
2793 try std.testing.expectApproxEqAbs(@as(f64, 0.0), wmc(&manager, Bdd.FALSE, ¶ms), 1e-10);
2794 }
2795
2796 test "wmc scalar - single variable" {
2797 const allocator = std.testing.allocator;
2798 var manager = try Manager.init(allocator);
2799 defer manager.deinit();
2800
2801 var params = WmcParams.init(allocator);
2802 defer params.deinit();
2803
2804 const x = try manager.newVar(true);
2805
2806 try std.testing.expectApproxEqAbs(@as(f64, 1.0), wmc(&manager, x, ¶ms), 1e-10);
2807
2808 try params.setWeight(0, 0.3, 0.7);
2809
2810 try std.testing.expectApproxEqAbs(@as(f64, 0.7), wmc(&manager, x, ¶ms), 1e-10);
2811
2812 try std.testing.expectApproxEqAbs(@as(f64, 0.3), wmc(&manager, x.neg(), ¶ms), 1e-10);
2813 }
2814
2815 test "wmc scalar - two variables AND" {
2816 const allocator = std.testing.allocator;
2817 var manager = try Manager.init(allocator);
2818 defer manager.deinit();
2819
2820 var params = WmcParams.init(allocator);
2821 defer params.deinit();
2822
2823 try params.setWeight(0, 0.3, 0.7);
2824 try params.setWeight(1, 0.4, 0.6);
2825
2826 const x = try manager.newVar(true);
2827 const y = try manager.newVar(true);
2828 const x_and_y = try manager.bddAnd(x, y);
2829
2830 try std.testing.expectApproxEqAbs(@as(f64, 0.42), wmc(&manager, x_and_y, ¶ms), 1e-10);
2831 }
2832
2833 test "wmc scalar - two variables OR" {
2834 const allocator = std.testing.allocator;
2835 var manager = try Manager.init(allocator);
2836 defer manager.deinit();
2837
2838 var params = WmcParams.init(allocator);
2839 defer params.deinit();
2840
2841 try params.setWeight(0, 0.3, 0.7);
2842 try params.setWeight(1, 0.4, 0.6);
2843
2844 const x = try manager.newVar(true);
2845 const y = try manager.newVar(true);
2846 const x_or_y = try manager.bddOr(x, y);
2847
2848 try std.testing.expectApproxEqAbs(@as(f64, 0.88), wmc(&manager, x_or_y, ¶ms), 1e-10);
2849 }
2850
2851 test "WmcDenseCache - valid bits are independent" {
2852 const allocator = std.testing.allocator;
2853 var cache = try WmcDenseCache.init(allocator, 2);
2854 defer cache.deinit();
2855
2856 const positive = Bdd{ .index = 1, .complement = false };
2857 const negative = Bdd{ .index = 1, .complement = true };
2858
2859 try std.testing.expect(cache.get(positive) == null);
2860 try std.testing.expect(cache.get(negative) == null);
2861
2862 cache.put(positive, 0.75);
2863 try std.testing.expectApproxEqAbs(@as(f64, 0.75), cache.get(positive).?, 1e-10);
2864 try std.testing.expect(cache.get(negative) == null);
2865
2866 cache.put(negative, 0.25);
2867 try std.testing.expectApproxEqAbs(@as(f64, 0.75), cache.get(positive).?, 1e-10);
2868 try std.testing.expectApproxEqAbs(@as(f64, 0.25), cache.get(negative).?, 1e-10);
2869 }
2870
2871 test "wmc scalar - sum to one" {
2872 const allocator = std.testing.allocator;
2873 var manager = try Manager.init(allocator);
2874 defer manager.deinit();
2875
2876 var params = WmcParams.init(allocator);
2877 defer params.deinit();
2878
2879 try params.setWeight(0, 0.3, 0.7);
2880 try params.setWeight(1, 0.4, 0.6);
2881
2882 const x = try manager.newVar(true);
2883 const y = try manager.newVar(true);
2884
2885 const formula = try manager.bddXor(x, y);
2886 const wmc_formula = wmc(&manager, formula, ¶ms);
2887 const wmc_neg = wmc(&manager, formula.neg(), ¶ms);
2888
2889 try std.testing.expectApproxEqAbs(@as(f64, 1.0), wmc_formula + wmc_neg, 1e-10);
2890 }
2891
2892 test "wmc dual - basic gradient" {
2893 const allocator = std.testing.allocator;
2894 var manager = try Manager.init(allocator);
2895 defer manager.deinit();
2896
2897 var params = WmcParams.initDual(allocator, 2);
2898 defer params.deinit();
2899
2900 var x_low_partials = [_]f64{ 0.0, 0.0 };
2901 var x_high_partials = [_]f64{ 1.0, 0.0 };
2902 try params.setWeightDeriv(0, 0.3, &x_low_partials, 0.7, &x_high_partials);
2903
2904 var y_low_partials = [_]f64{ 0.0, 0.0 };
2905 var y_high_partials = [_]f64{ 0.0, 1.0 };
2906 try params.setWeightDeriv(1, 0.4, &y_low_partials, 0.6, &y_high_partials);
2907
2908 const x = try manager.newVar(true);
2909 const y = try manager.newVar(true);
2910 const x_and_y = try manager.bddAnd(x, y);
2911
2912 var result = try wmcDual(&manager, x_and_y, ¶ms, allocator);
2913 defer result.deinit();
2914
2915 try std.testing.expectApproxEqAbs(@as(f64, 0.42), result.primal, 1e-10);
2916
2917 try std.testing.expectApproxEqAbs(@as(f64, 0.6), result.partials[0], 1e-10);
2918
2919 try std.testing.expectApproxEqAbs(@as(f64, 0.7), result.partials[1], 1e-10);
2920 }
2921
2922 test "wmc dual releases temporaries once on allocation failure" {
2923 const allocator = std.testing.allocator;
2924 var manager = try Manager.init(allocator);
2925 defer manager.deinit();
2926
2927 var params = WmcParams.initDual(allocator, 1);
2928 defer params.deinit();
2929
2930 var zero_partials = [_]f64{0.0};
2931 var one_partials = [_]f64{1.0};
2932 try params.setWeightDeriv(0, 0.3, &zero_partials, 0.7, &one_partials);
2933 const x = try manager.newVar(true);
2934
2935 for (0..8) |fail_index| {
2936 var failing = std.testing.FailingAllocator.init(allocator, .{
2937 .fail_index = fail_index,
2938 });
2939 if (wmcDual(&manager, x, ¶ms, failing.allocator())) |value| {
2940 var result = value;
2941 result.deinit();
2942 } else |err| {
2943 try std.testing.expect(err == error.OutOfMemory);
2944 }
2945 }
2946 }
2947
2948 test "wmc dual - three variables with chain rule" {
2949 const allocator = std.testing.allocator;
2950 var manager = try Manager.init(allocator);
2951 defer manager.deinit();
2952
2953 var params = WmcParams.initDual(allocator, 3);
2954 defer params.deinit();
2955
2956 var zero_partials = [_]f64{ 0.0, 0.0, 0.0 };
2957 var x_high_partials = [_]f64{ 1.0, 0.0, 0.0 };
2958 var y_high_partials = [_]f64{ 0.0, 1.0, 0.0 };
2959 var z_high_partials = [_]f64{ 0.0, 0.0, 1.0 };
2960
2961 try params.setWeightDeriv(0, 0.8, &zero_partials, 0.2, &x_high_partials);
2962 try params.setWeightDeriv(1, 0.7, &zero_partials, 0.3, &y_high_partials);
2963 try params.setWeightDeriv(2, 0.5, &zero_partials, 0.5, &z_high_partials);
2964
2965 const x = try manager.newVar(true);
2966 const y = try manager.newVar(true);
2967 const z = try manager.newVar(true);
2968
2969 const x_and_y = try manager.bddAnd(x, y);
2970 const formula = try manager.bddOr(x_and_y, z);
2971
2972 var result = try wmcDual(&manager, formula, ¶ms, allocator);
2973 defer result.deinit();
2974
2975 try std.testing.expectApproxEqAbs(@as(f64, 0.53), result.primal, 1e-10);
2976
2977 try std.testing.expectApproxEqAbs(@as(f64, 0.65), result.partials[0], 1e-10);
2978
2979 try std.testing.expectApproxEqAbs(@as(f64, 0.2), result.partials[1], 1e-10);
2980
2981 try std.testing.expectApproxEqAbs(@as(f64, 0.94), result.partials[2], 1e-10);
2982 }
2983
2984 test "wmc dual - negation" {
2985 const allocator = std.testing.allocator;
2986 var manager = try Manager.init(allocator);
2987 defer manager.deinit();
2988
2989 var params = WmcParams.initDual(allocator, 1);
2990 defer params.deinit();
2991
2992 var zero_partials = [_]f64{0.0};
2993 var one_partials = [_]f64{1.0};
2994 try params.setWeightDeriv(0, 0.3, &zero_partials, 0.7, &one_partials);
2995
2996 const x = try manager.newVar(true);
2997
2998 var result_x = try wmcDual(&manager, x, ¶ms, allocator);
2999 defer result_x.deinit();
3000
3001 var result_not_x = try wmcDual(&manager, x.neg(), ¶ms, allocator);
3002 defer result_not_x.deinit();
3003
3004 try std.testing.expectApproxEqAbs(@as(f64, 1.0), result_x.primal + result_not_x.primal, 1e-10);
3005
3006 try std.testing.expectApproxEqAbs(@as(f64, 1.0), result_x.partials[0], 1e-10);
3007
3008 try std.testing.expectApproxEqAbs(@as(f64, 0.0), result_not_x.partials[0], 1e-10);
3009 }
3010
3011 test "wmc params - varPartial helper" {
3012 const allocator = std.testing.allocator;
3013
3014 var params = WmcParams.initDual(allocator, 3);
3015 defer params.deinit();
3016
3017 var low_partials = [_]f64{ 0.1, 0.2, 0.3 };
3018 var high_partials = [_]f64{ 0.4, 0.5, 0.6 };
3019 try params.setWeightDeriv(0, 0.3, &low_partials, 0.7, &high_partials);
3020
3021 const dw = params.getDualWeight(0).?;
3022
3023 try std.testing.expectApproxEqAbs(@as(f64, 0.1), dw.low_partials[0], 1e-10);
3024 try std.testing.expectApproxEqAbs(@as(f64, 0.2), dw.low_partials[1], 1e-10);
3025 try std.testing.expectApproxEqAbs(@as(f64, 0.3), dw.low_partials[2], 1e-10);
3026 try std.testing.expectApproxEqAbs(@as(f64, 0.4), dw.high_partials[0], 1e-10);
3027 try std.testing.expectApproxEqAbs(@as(f64, 0.5), dw.high_partials[1], 1e-10);
3028 try std.testing.expectApproxEqAbs(@as(f64, 0.6), dw.high_partials[2], 1e-10);
3029 }
3030
3031 test "wmc scalar - larger formula" {
3032 const allocator = std.testing.allocator;
3033 var manager = try Manager.init(allocator);
3034 defer manager.deinit();
3035
3036 var params = WmcParams.init(allocator);
3037 defer params.deinit();
3038
3039 try params.setWeight(0, 0.5, 0.5);
3040 try params.setWeight(1, 0.5, 0.5);
3041 try params.setWeight(2, 0.5, 0.5);
3042
3043 const x = try manager.newVar(true);
3044 const y = try manager.newVar(true);
3045 const z = try manager.newVar(true);
3046
3047 const x_xor_y = try manager.bddXor(x, y);
3048 const formula = try manager.bddXor(x_xor_y, z);
3049
3050 const result = wmc(&manager, formula, ¶ms);
3051 try std.testing.expectApproxEqAbs(@as(f64, 0.5), result, 1e-10);
3052 }
3053
3054 pub const WeightedSampleResult = struct {
3055 sample: Bdd,
3056 probability: f64,
3057 };
3058
3059 pub const WeightedSampler = struct {
3060 allocator: Allocator,
3061 manager: *Manager,
3062 bdd: Bdd,
3063 params: *const WmcParams,
3064 cache: WmcDenseCache,
3065 var_bdds: []Bdd,
3066 total_wmc: f64,
3067
3068 pub fn init(
3069 allocator: Allocator,
3070 manager: *Manager,
3071 bdd: Bdd,
3072 params: *const WmcParams,
3073 ) !WeightedSampler {
3074 const var_bdds = try allocator.alloc(Bdd, manager.numVars());
3075 errdefer allocator.free(var_bdds);
3076 for (var_bdds, 0..) |*var_bdd, label| {
3077 var_bdd.* = try manager.getOrInsert(Node.init(@intCast(label), Bdd.FALSE, Bdd.TRUE));
3078 }
3079
3080 var cache = try WmcDenseCache.init(allocator, manager.nodes.items.len);
3081 errdefer cache.deinit();
3082 const total_wmc = wmcHelper(manager, bdd, params, &cache);
3083 return WeightedSampler{
3084 .allocator = allocator,
3085 .manager = manager,
3086 .bdd = bdd,
3087 .params = params,
3088 .cache = cache,
3089 .var_bdds = var_bdds,
3090 .total_wmc = total_wmc,
3091 };
3092 }
3093
3094 pub fn deinit(self: *WeightedSampler) void {
3095 self.cache.deinit();
3096 self.allocator.free(self.var_bdds);
3097 }
3098
3099 pub fn sample(self: *WeightedSampler, rng: std.Random) Allocator.Error!WeightedSampleResult {
3100 if (self.bdd.isTrue()) {
3101 return WeightedSampleResult{
3102 .sample = Bdd.TRUE,
3103 .probability = 1.0,
3104 };
3105 }
3106 if (self.bdd.isFalse() or self.total_wmc == 0.0) {
3107 return WeightedSampleResult{
3108 .sample = Bdd.FALSE,
3109 .probability = 0.0,
3110 };
3111 }
3112
3113 return try weightedSampleFromCache(self.manager, self.bdd, self.params, rng, 1.0, &self.cache, self.var_bdds);
3114 }
3115 };
3116
3117 fn weightedSampleLiteral(manager: *const Manager, bdd: Bdd, params: *const WmcParams) ?WeightedSampleResult {
3118 if (bdd.isConst()) return null;
3119
3120 const node = manager.getNode(bdd);
3121 const low_child = if (bdd.complement) node.low.neg() else node.low;
3122 const high_child = if (bdd.complement) node.high.neg() else node.high;
3123 const weight = params.getWeight(node.var_label);
3124
3125 if (low_child.isFalse() and high_child.isTrue()) {
3126 return .{ .sample = bdd, .probability = weight.high };
3127 }
3128 if (low_child.isTrue() and high_child.isFalse()) {
3129 return .{ .sample = bdd, .probability = weight.low };
3130 }
3131 return null;
3132 }
3133
3134 pub fn weightedSample(
3135 manager: *Manager,
3136 bdd: Bdd,
3137 params: *const WmcParams,
3138 rng: std.Random,
3139 ) Allocator.Error!WeightedSampleResult {
3140 if (bdd.isTrue()) {
3141 return WeightedSampleResult{
3142 .sample = Bdd.TRUE,
3143 .probability = 1.0,
3144 };
3145 }
3146 if (bdd.isFalse()) {
3147 return WeightedSampleResult{
3148 .sample = Bdd.FALSE,
3149 .probability = 0.0,
3150 };
3151 }
3152 if (weightedSampleLiteral(manager, bdd, params)) |sample| {
3153 return sample;
3154 }
3155
3156 var cache = try WmcDenseCache.init(manager.allocator, manager.nodes.items.len);
3157 defer cache.deinit();
3158
3159 const total_wmc = wmcHelper(manager, bdd, params, &cache);
3160 if (total_wmc == 0.0) {
3161 return WeightedSampleResult{
3162 .sample = Bdd.FALSE,
3163 .probability = 0.0,
3164 };
3165 }
3166
3167 return try weightedSampleFromCache(manager, bdd, params, rng, 1.0, &cache, &.{});
3168 }
3169
3170 fn cachedWmc(
3171 manager: *const Manager,
3172 bdd: Bdd,
3173 params: *const WmcParams,
3174 cache: *WmcDenseCache,
3175 ) f64 {
3176 if (bdd.isTrue()) return 1.0;
3177 if (bdd.isFalse()) return 0.0;
3178
3179 if (cache.get(bdd)) |cached| {
3180 return cached;
3181 }
3182
3183 return wmcHelper(manager, bdd, params, cache);
3184 }
3185
3186 fn sampleVarBdd(manager: *Manager, var_bdds: []const Bdd, label: VarLabel) Allocator.Error!Bdd {
3187 const index: usize = @intCast(label);
3188 if (index < var_bdds.len) return var_bdds[index];
3189 return manager.getOrInsert(Node.init(label, Bdd.FALSE, Bdd.TRUE));
3190 }
3191
3192 fn weightedSampleFromCache(
3193 manager: *Manager,
3194 bdd: Bdd,
3195 params: *const WmcParams,
3196 rng: std.Random,
3197 accumulated_weight: f64,
3198 cache: *WmcDenseCache,
3199 var_bdds: []const Bdd,
3200 ) Allocator.Error!WeightedSampleResult {
3201 if (bdd.isTrue()) {
3202 return WeightedSampleResult{
3203 .sample = Bdd.TRUE,
3204 .probability = accumulated_weight,
3205 };
3206 }
3207 if (bdd.isFalse()) {
3208 return WeightedSampleResult{
3209 .sample = Bdd.FALSE,
3210 .probability = 0.0,
3211 };
3212 }
3213
3214 const node = manager.getNode(bdd);
3215 const weight = params.getWeight(node.var_label);
3216
3217 const low_child = if (bdd.complement) node.low.neg() else node.low;
3218 const high_child = if (bdd.complement) node.high.neg() else node.high;
3219
3220 const wmc_low = cachedWmc(manager, low_child, params, cache);
3221 const wmc_high = cachedWmc(manager, high_child, params, cache);
3222
3223 const weighted_low = weight.low * wmc_low;
3224 const weighted_high = weight.high * wmc_high;
3225 const total = weighted_low + weighted_high;
3226
3227 if (total == 0.0) {
3228 return WeightedSampleResult{
3229 .sample = Bdd.FALSE,
3230 .probability = 0.0,
3231 };
3232 }
3233
3234 const prob_high = weighted_high / total;
3235
3236 const r = rng.float(f64);
3237
3238 const var_bdd = try sampleVarBdd(manager, var_bdds, node.var_label);
3239
3240 if (r < prob_high) {
3241 const sub_result = try weightedSampleFromCache(
3242 manager,
3243 high_child,
3244 params,
3245 rng,
3246 accumulated_weight * weight.high,
3247 cache,
3248 var_bdds,
3249 );
3250 if (sub_result.sample.isFalse()) {
3251 return sub_result;
3252 }
3253 const sample_bdd = try manager.bddAnd(var_bdd, sub_result.sample);
3254 return WeightedSampleResult{
3255 .sample = sample_bdd,
3256 .probability = sub_result.probability,
3257 };
3258 } else {
3259 const sub_result = try weightedSampleFromCache(
3260 manager,
3261 low_child,
3262 params,
3263 rng,
3264 accumulated_weight * weight.low,
3265 cache,
3266 var_bdds,
3267 );
3268 if (sub_result.sample.isFalse()) {
3269 return sub_result;
3270 }
3271 const sample_bdd = try manager.bddAnd(var_bdd.neg(), sub_result.sample);
3272 return WeightedSampleResult{
3273 .sample = sample_bdd,
3274 .probability = sub_result.probability,
3275 };
3276 }
3277 }
3278
3279 const BddPath = struct {
3280 bdd: Bdd,
3281 probability: f64,
3282 };
3283
3284 fn bdd_path_more_probable(_: void, a: BddPath, b: BddPath) bool {
3285 return a.probability > b.probability;
3286 }
3287
3288 pub fn topKPaths(
3289 manager: *Manager,
3290 bdd: Bdd,
3291 k: usize,
3292 params: *const WmcParams,
3293 allocator: Allocator,
3294 ) !Bdd {
3295 if (bdd.isFalse() or k == 0) {
3296 return Bdd.FALSE;
3297 }
3298 if (bdd.isTrue()) {
3299 return Bdd.TRUE;
3300 }
3301
3302 var paths: std.ArrayList(BddPath) = .empty;
3303 defer paths.deinit(allocator);
3304
3305 try enumeratePaths(manager, bdd, Bdd.TRUE, params, 1.0, &paths, allocator);
3306
3307 std.mem.sort(BddPath, paths.items, {}, bdd_path_more_probable);
3308
3309 var result = Bdd.FALSE;
3310 const limit = @min(k, paths.items.len);
3311 for (paths.items[0..limit]) |path| {
3312 result = try manager.bddOr(result, path.bdd);
3313 }
3314
3315 return result;
3316 }
3317
3318 fn enumeratePaths(
3319 manager: *Manager,
3320 bdd: Bdd,
3321 current_path: Bdd,
3322 params: *const WmcParams,
3323 current_prob: f64,
3324 paths: *std.ArrayList(BddPath),
3325 allocator: Allocator,
3326 ) !void {
3327 if (bdd.isFalse()) {
3328 return;
3329 }
3330 if (bdd.isTrue()) {
3331 try paths.append(allocator, BddPath{
3332 .bdd = current_path,
3333 .probability = current_prob,
3334 });
3335 return;
3336 }
3337
3338 const node = manager.getNode(bdd);
3339 const weight = params.getWeight(node.var_label);
3340
3341 const low_child = if (bdd.complement) node.low.neg() else node.low;
3342 const high_child = if (bdd.complement) node.high.neg() else node.high;
3343
3344 const var_bdd = try manager.getOrInsert(Node.init(node.var_label, Bdd.FALSE, Bdd.TRUE));
3345
3346 if (!high_child.isFalse()) {
3347 const new_path = try manager.bddAnd(current_path, var_bdd);
3348 try enumeratePaths(manager, high_child, new_path, params, current_prob * weight.high, paths, allocator);
3349 }
3350
3351 if (!low_child.isFalse()) {
3352 const new_path = try manager.bddAnd(current_path, var_bdd.neg());
3353 try enumeratePaths(manager, low_child, new_path, params, current_prob * weight.low, paths, allocator);
3354 }
3355 }
3356
3357 test "weighted sample - single variable" {
3358 const allocator = std.testing.allocator;
3359 var manager = try Manager.init(allocator);
3360 defer manager.deinit();
3361
3362 var params = WmcParams.init(allocator);
3363 defer params.deinit();
3364
3365 try params.setWeight(0, 0.3, 0.7);
3366
3367 const x = try manager.newVar(true);
3368
3369 var prng = std.Random.DefaultPrng.init(12345);
3370 const rng = prng.random();
3371
3372 for (0..10) |_| {
3373 const result = try weightedSample(&manager, x, ¶ms, rng);
3374 try std.testing.expect(manager.eq(result.sample, x));
3375 try std.testing.expectApproxEqAbs(@as(f64, 0.7), result.probability, 1e-10);
3376 }
3377 }
3378
3379 test "weighted sample - literal guard avoids allocation" {
3380 const allocator = std.testing.allocator;
3381 var manager = try Manager.init(allocator);
3382 defer manager.deinit();
3383
3384 var params = WmcParams.init(allocator);
3385 defer params.deinit();
3386
3387 try params.setWeight(0, 0.25, 0.75);
3388
3389 const x = try manager.newVar(true);
3390
3391 var empty: [0]u8 = .{};
3392 var fixed = std.heap.FixedBufferAllocator.init(&empty);
3393 const original_allocator = manager.allocator;
3394 manager.allocator = fixed.allocator();
3395 defer manager.allocator = original_allocator;
3396
3397 var prng = std.Random.DefaultPrng.init(20260608);
3398 const rng = prng.random();
3399
3400 const positive = try weightedSample(&manager, x, ¶ms, rng);
3401 try std.testing.expect(manager.eq(positive.sample, x));
3402 try std.testing.expectApproxEqAbs(@as(f64, 0.75), positive.probability, 1e-10);
3403
3404 const negative = try weightedSample(&manager, x.neg(), ¶ms, rng);
3405 try std.testing.expect(manager.eq(negative.sample, x.neg()));
3406 try std.testing.expectApproxEqAbs(@as(f64, 0.25), negative.probability, 1e-10);
3407 }
3408
3409 test "weighted sample - two variable AND" {
3410 const allocator = std.testing.allocator;
3411 var manager = try Manager.init(allocator);
3412 defer manager.deinit();
3413
3414 var params = WmcParams.init(allocator);
3415 defer params.deinit();
3416
3417 try params.setWeight(0, 0.5, 0.5);
3418 try params.setWeight(1, 0.5, 0.5);
3419
3420 const x = try manager.newVar(true);
3421 const y = try manager.newVar(true);
3422 const x_and_y = try manager.bddAnd(x, y);
3423
3424 var prng = std.Random.DefaultPrng.init(54321);
3425 const rng = prng.random();
3426
3427 for (0..20) |_| {
3428 const result = try weightedSample(&manager, x_and_y, ¶ms, rng);
3429 try std.testing.expect(!result.sample.isFalse());
3430 const check = try manager.bddImplies(result.sample, x_and_y);
3431 try std.testing.expect(check.isTrue());
3432 }
3433 }
3434
3435 test "weighted sampler - deterministic sequence" {
3436 const allocator = std.testing.allocator;
3437 var manager = try Manager.init(allocator);
3438 defer manager.deinit();
3439
3440 var params = WmcParams.init(allocator);
3441 defer params.deinit();
3442
3443 try params.setWeight(0, 0.2, 0.8);
3444 try params.setWeight(1, 0.4, 0.6);
3445
3446 const x = try manager.newVar(true);
3447 const y = try manager.newVar(true);
3448 const x_or_y = try manager.bddOr(x, y);
3449
3450 var sampler = try WeightedSampler.init(allocator, &manager, x_or_y, ¶ms);
3451 defer sampler.deinit();
3452
3453 const num_samples: usize = 32;
3454 var expected: [num_samples]Bdd = undefined;
3455
3456 var prng_a = std.Random.DefaultPrng.init(2026);
3457 const rng_a = prng_a.random();
3458 for (0..num_samples) |idx| {
3459 const result = try sampler.sample(rng_a);
3460 expected[idx] = result.sample;
3461 }
3462
3463 var prng_b = std.Random.DefaultPrng.init(2026);
3464 const rng_b = prng_b.random();
3465 for (0..num_samples) |idx| {
3466 const result = try sampler.sample(rng_b);
3467 try std.testing.expect(manager.eq(result.sample, expected[idx]));
3468 }
3469 }
3470
3471 test "weighted sampler - frequency matches exact WMC" {
3472 const allocator = std.testing.allocator;
3473 var manager = try Manager.init(allocator);
3474 defer manager.deinit();
3475
3476 var params = WmcParams.init(allocator);
3477 defer params.deinit();
3478
3479 const x_low: f64 = 0.25;
3480 const x_high: f64 = 0.75;
3481 const y_low: f64 = 0.35;
3482 const y_high: f64 = 0.65;
3483
3484 try params.setWeight(0, x_low, x_high);
3485 try params.setWeight(1, y_low, y_high);
3486
3487 const x = try manager.newVar(true);
3488 const y = try manager.newVar(true);
3489 const x_or_y = try manager.bddOr(x, y);
3490
3491 var sampler = try WeightedSampler.init(allocator, &manager, x_or_y, ¶ms);
3492 defer sampler.deinit();
3493
3494 const not_x_and_y = try manager.bddAnd(x.neg(), y);
3495
3496 var prng = std.Random.DefaultPrng.init(4242);
3497 const rng = prng.random();
3498
3499 var count_x: usize = 0;
3500 var count_not_x_and_y: usize = 0;
3501
3502 const num_samples: usize = 20000;
3503 for (0..num_samples) |_| {
3504 const result = try sampler.sample(rng);
3505 if (manager.eq(result.sample, x)) {
3506 count_x += 1;
3507 } else if (manager.eq(result.sample, not_x_and_y)) {
3508 count_not_x_and_y += 1;
3509 } else {
3510 try std.testing.expect(false);
3511 }
3512 }
3513
3514 const total_mass = x_high + x_low * y_high;
3515 const expected_x = x_high / total_mass;
3516 const observed_x = @as(f64, @floatFromInt(count_x)) / @as(f64, @floatFromInt(num_samples));
3517
3518 try std.testing.expectApproxEqAbs(expected_x, observed_x, 0.02);
3519 try std.testing.expectEqual(num_samples, count_x + count_not_x_and_y);
3520 }
3521
3522 test "top_k_paths - simple BDD" {
3523 const allocator = std.testing.allocator;
3524 var manager = try Manager.init(allocator);
3525 defer manager.deinit();
3526
3527 var params = WmcParams.init(allocator);
3528 defer params.deinit();
3529
3530 try params.setWeight(0, 0.2, 0.8);
3531 try params.setWeight(1, 0.3, 0.7);
3532
3533 const x = try manager.newVar(true);
3534 const y = try manager.newVar(true);
3535 const x_or_y = try manager.bddOr(x, y);
3536
3537 const top1 = try topKPaths(&manager, x_or_y, 1, ¶ms, allocator);
3538 try std.testing.expect(manager.eq(top1, x));
3539
3540 const top2 = try topKPaths(&manager, x_or_y, 2, ¶ms, allocator);
3541 try std.testing.expect(manager.eq(top2, x_or_y));
3542 }
3543
3544 test "top_k_paths - AND formula" {
3545 const allocator = std.testing.allocator;
3546 var manager = try Manager.init(allocator);
3547 defer manager.deinit();
3548
3549 var params = WmcParams.init(allocator);
3550 defer params.deinit();
3551
3552 try params.setWeight(0, 0.3, 0.7);
3553 try params.setWeight(1, 0.4, 0.6);
3554
3555 const x = try manager.newVar(true);
3556 const y = try manager.newVar(true);
3557 const x_and_y = try manager.bddAnd(x, y);
3558
3559 const top1 = try topKPaths(&manager, x_and_y, 1, ¶ms, allocator);
3560 try std.testing.expect(manager.eq(top1, x_and_y));
3561 }
3562
3563 test "limit config - ITE limit" {
3564 var config = LimitConfig.init();
3565
3566 config.startIteLimit(100, 0, 0, 0);
3567 try std.testing.expect(!config.checkIteLimit(50));
3568 try std.testing.expect(!config.ite_limit_exceeded);
3569
3570 try std.testing.expect(config.checkIteLimit(100));
3571 try std.testing.expect(config.ite_limit_exceeded);
3572
3573 config.stopIteLimit();
3574 try std.testing.expect(config.ite_limit == null);
3575 }
3576
3577 test "manager limits integration" {
3578 const allocator = std.testing.allocator;
3579 var manager = try Manager.init(allocator);
3580 defer manager.deinit();
3581
3582 manager.startIteLimit(5);
3583
3584 const x = try manager.newVar(true);
3585 const y = try manager.newVar(true);
3586 _ = try manager.bddAnd(x, y);
3587
3588 try std.testing.expect(manager.num_recursive_calls > 0);
3589
3590 _ = manager.checkLimits();
3591
3592 manager.stopIteLimit();
3593 }
3594
3595 test "manager ITE limit enforcement" {
3596 const allocator = std.testing.allocator;
3597 var manager = try Manager.init(allocator);
3598 defer manager.deinit();
3599
3600 manager.startIteLimit(3);
3601
3602 const x = try manager.newVar(true);
3603 const y = try manager.newVar(true);
3604 const z = try manager.newVar(true);
3605
3606 const xy = try manager.bddAnd(x, y);
3607 const xyz = try manager.bddAnd(xy, z);
3608 _ = xyz;
3609
3610 _ = manager.checkLimits();
3611
3612 try std.testing.expect(manager.iteLimitExceeded());
3613
3614 manager.stopIteLimit();
3615 }
3616
3617 test "manager ITE operation ceiling rejects later work" {
3618 const allocator = std.testing.allocator;
3619 var manager = try Manager.init(allocator);
3620 defer manager.deinit();
3621
3622 const variable = try manager.newVar(true);
3623 const node_count = manager.nodes.items.len;
3624 const cache_count = manager.ite_cache.count();
3625 manager.startIteLimit(1);
3626
3627 const admitted = try manager.ite(variable, Bdd.TRUE, Bdd.FALSE);
3628 try std.testing.expectEqual(variable.toRaw(), admitted.toRaw());
3629 try std.testing.expect(manager.checkLimits());
3630 try std.testing.expect(manager.iteLimitExceeded());
3631
3632 const rejected = try manager.ite(variable, Bdd.TRUE, Bdd.FALSE);
3633 try std.testing.expect(rejected.isFalse());
3634 try std.testing.expect(manager.iteLimitExceeded());
3635 try std.testing.expectEqual(node_count, manager.nodes.items.len);
3636 try std.testing.expectEqual(cache_count, manager.ite_cache.count());
3637 manager.stopIteLimit();
3638 }
3639
3640 test "manager node growth quota admits the exact maximum without partial variables" {
3641 const allocator = std.testing.allocator;
3642 var manager = try Manager.init(allocator);
3643 defer manager.deinit();
3644
3645 const node_baseline = manager.nodes.items.len;
3646 manager.startIteLimit(2);
3647
3648 const first = try manager.newVar(true);
3649 const second = try manager.newVar(true);
3650 try std.testing.expect(!first.isFalse());
3651 try std.testing.expect(!second.isFalse());
3652 try std.testing.expectEqual(node_baseline + 2, manager.nodes.items.len);
3653 try std.testing.expectEqual(@as(usize, 2), manager.var_order.items.len);
3654
3655 const rejected = try manager.newVar(true);
3656 try std.testing.expect(rejected.isFalse());
3657 try std.testing.expect(manager.iteLimitExceeded());
3658 try std.testing.expectEqual(node_baseline + 2, manager.nodes.items.len);
3659 try std.testing.expectEqual(@as(usize, 2), manager.var_order.items.len);
3660
3661 manager.stopIteLimit();
3662 manager.startIteLimit(1);
3663 const next = try manager.newVar(true);
3664 try std.testing.expect(!next.isFalse());
3665 try std.testing.expectEqual(node_baseline + 3, manager.nodes.items.len);
3666 try std.testing.expectEqual(@as(usize, 3), manager.var_order.items.len);
3667 manager.stopIteLimit();
3668 }
3669
3670 test "manager ITE cache growth quota admits the exact maximum" {
3671 const allocator = std.testing.allocator;
3672 var manager = try Manager.init(allocator);
3673 defer manager.deinit();
3674
3675 manager.startIteLimit(2);
3676 const first = IteKey.init(.{ .index = 1, .complement = false }, Bdd.TRUE, Bdd.FALSE);
3677 const second = IteKey.init(.{ .index = 2, .complement = false }, Bdd.TRUE, Bdd.FALSE);
3678 const rejected = IteKey.init(.{ .index = 3, .complement = false }, Bdd.TRUE, Bdd.FALSE);
3679
3680 try std.testing.expect(!manager.limits.reserveIteCacheGrowth(manager.ite_cache.count()));
3681 try std.testing.expect(try manager.putIteCacheNoClobber(first, Bdd.TRUE));
3682 manager.limits.releaseIteCacheGrowth();
3683 try std.testing.expect(!manager.limits.reserveIteCacheGrowth(manager.ite_cache.count()));
3684 try std.testing.expect(try manager.putIteCacheNoClobber(second, Bdd.TRUE));
3685 manager.limits.releaseIteCacheGrowth();
3686 try std.testing.expectEqual(@as(u32, 2), manager.ite_cache.count());
3687 try std.testing.expect(manager.limits.reserveIteCacheGrowth(manager.ite_cache.count()));
3688 try std.testing.expect(manager.iteLimitExceeded());
3689 try std.testing.expectEqual(@as(u32, 2), manager.ite_cache.count());
3690 try std.testing.expect(!manager.ite_cache.contains(rejected));
3691 manager.stopIteLimit();
3692 }
3693
3694 test "unbounded manager reports allocation failure" {
3695 const allocator = std.testing.allocator;
3696 var manager = try Manager.init(allocator);
3697 defer manager.deinit();
3698
3699 var failing = std.testing.FailingAllocator.init(allocator, .{ .fail_index = 0 });
3700 manager.allocator = failing.allocator();
3701 defer manager.allocator = allocator;
3702
3703 try std.testing.expectError(error.OutOfMemory, manager.newVar(true));
3704 try std.testing.expect(!manager.iteLimitExceeded());
3705 try std.testing.expectEqual(@as(usize, 1), manager.nodes.items.len);
3706 try std.testing.expectEqual(@as(usize, 0), manager.var_order.items.len);
3707 }
3708
3709 test "bounded manager maps allocation failure to its quota surface" {
3710 const allocator = std.testing.allocator;
3711 var manager = try Manager.init(allocator);
3712 defer manager.deinit();
3713
3714 manager.startIteLimit(1);
3715 var failing = std.testing.FailingAllocator.init(allocator, .{ .fail_index = 0 });
3716 manager.allocator = failing.allocator();
3717 defer manager.allocator = allocator;
3718
3719 const rejected = try manager.newVar(true);
3720 try std.testing.expect(rejected.isFalse());
3721 try std.testing.expect(manager.iteLimitExceeded());
3722 try std.testing.expectEqual(@as(usize, 1), manager.nodes.items.len);
3723 try std.testing.expectEqual(@as(usize, 0), manager.var_order.items.len);
3724 manager.stopIteLimit();
3725 }
3726
3727 test "condition cache allocation failure is observable" {
3728 const allocator = std.testing.allocator;
3729 var manager = try Manager.init(allocator);
3730 defer manager.deinit();
3731
3732 manager.condition_cache.deinit(allocator);
3733 manager.condition_cache = .{};
3734 var failing = std.testing.FailingAllocator.init(allocator, .{ .fail_index = 0 });
3735 manager.allocator = failing.allocator();
3736 defer manager.allocator = allocator;
3737
3738 const key = ConditionKey.init(Bdd.TRUE, 0, true);
3739 try std.testing.expectError(error.OutOfMemory, manager.putConditionCache(key, Bdd.TRUE));
3740 try std.testing.expect(!manager.iteLimitExceeded());
3741
3742 manager.startIteLimit(1);
3743 failing.fail_index = failing.alloc_index;
3744 try std.testing.expect(!try manager.putConditionCache(key, Bdd.TRUE));
3745 try std.testing.expect(manager.iteLimitExceeded());
3746 manager.stopIteLimit();
3747 }
3748
3749 test "time limit API" {
3750 const allocator = std.testing.allocator;
3751 var manager = try Manager.init(allocator);
3752 defer manager.deinit();
3753
3754 manager.setTimeLimit(10.0);
3755 try std.testing.expect(manager.limits.time_limit.? == 10.0);
3756 try std.testing.expect(!manager.timeLimitExceeded());
3757
3758 manager.startTimeLimit(5.0);
3759 try std.testing.expect(manager.limits.time_limit.? == 5.0);
3760
3761 manager.stopTimeLimit();
3762 try std.testing.expect(manager.limits.time_limit == null);
3763
3764 manager.limits.time_limit_exceeded = true;
3765 manager.limits.ite_limit_exceeded = true;
3766 manager.resetLimitFlags();
3767 try std.testing.expect(!manager.timeLimitExceeded());
3768 try std.testing.expect(!manager.iteLimitExceeded());
3769
3770 manager.startTimeLimit(0.001);
3771
3772 const x = try manager.newVar(true);
3773 const y = try manager.newVar(true);
3774 const z = try manager.newVar(true);
3775
3776 var formula = try manager.bddAnd(x, y);
3777 for (0..100) |_| {
3778 formula = try manager.bddOr(formula, try manager.bddAnd(y, z));
3779 formula = try manager.bddAnd(formula, try manager.bddOr(x, z));
3780 }
3781
3782 manager.stopTimeLimit();
3783 }
3784
3785 test "toJson - constants" {
3786 const allocator = std.testing.allocator;
3787 var manager = try Manager.init(allocator);
3788 defer manager.deinit();
3789
3790 const true_json = try manager.toJson(Bdd.TRUE, allocator);
3791 defer allocator.free(true_json);
3792 try std.testing.expectEqualStrings("{\"root\":\"true\",\"nodes\":{}}", true_json);
3793
3794 const false_json = try manager.toJson(Bdd.FALSE, allocator);
3795 defer allocator.free(false_json);
3796 try std.testing.expectEqualStrings("{\"root\":\"false\",\"nodes\":{}}", false_json);
3797 }
3798
3799 test "toJson - variable" {
3800 const allocator = std.testing.allocator;
3801 var manager = try Manager.init(allocator);
3802 defer manager.deinit();
3803
3804 const x = try manager.newVar(true);
3805 const json = try manager.toJson(x, allocator);
3806 defer allocator.free(json);
3807
3808 try std.testing.expect(std.mem.indexOf(u8, json, "\"root\":") != null);
3809 try std.testing.expect(std.mem.indexOf(u8, json, "\"nodes\":") != null);
3810 try std.testing.expect(std.mem.indexOf(u8, json, "\"var\":0") != null);
3811 try std.testing.expect(std.mem.indexOf(u8, json, "\"high\":\"true\"") != null);
3812 try std.testing.expect(std.mem.indexOf(u8, json, "\"low\":\"false\"") != null);
3813 }
3814
3815 test "toJson - compound formula" {
3816 const allocator = std.testing.allocator;
3817 var manager = try Manager.init(allocator);
3818 defer manager.deinit();
3819
3820 const x = try manager.newVar(true);
3821 const y = try manager.newVar(true);
3822 const x_and_y = try manager.bddAnd(x, y);
3823
3824 const json = try manager.toJson(x_and_y, allocator);
3825 defer allocator.free(json);
3826 var parsed = try std.json.parseFromSlice(std.json.Value, allocator, json, .{});
3827 defer parsed.deinit();
3828
3829 try std.testing.expect(std.mem.indexOf(u8, json, "\"root\":") != null);
3830 try std.testing.expect(std.mem.indexOf(u8, json, "\"nodes\":") != null);
3831 try std.testing.expect(std.mem.indexOf(u8, json, "\"var\":0") != null);
3832 try std.testing.expect(std.mem.indexOf(u8, json, "\"var\":1") != null);
3833 try std.testing.expect(parsed.value.object.get("nodes") != null);
3834 }
3835
3836 test "printStats" {
3837 const allocator = std.testing.allocator;
3838 var manager = try Manager.init(allocator);
3839 defer manager.deinit();
3840
3841 _ = try manager.newVar(true);
3842 _ = try manager.newVar(true);
3843
3844 const stats = try manager.printStats(allocator);
3845 defer allocator.free(stats);
3846
3847 try std.testing.expect(std.mem.indexOf(u8, stats, "Variables: 2") != null);
3848 try std.testing.expect(std.mem.indexOf(u8, stats, "Nodes:") != null);
3849 try std.testing.expect(std.mem.indexOf(u8, stats, "Recursive calls:") != null);
3850 }
3851
3852 test "deepCopy - basic" {
3853 const allocator = std.testing.allocator;
3854 var manager = try Manager.init(allocator);
3855 defer manager.deinit();
3856
3857 const x = try manager.newVar(true);
3858 const y = try manager.newVar(true);
3859 const x_and_y = try manager.bddAnd(x, y);
3860
3861 var copy = try deepCopy(&manager, x_and_y, allocator);
3862 defer copy.deinit();
3863
3864 try std.testing.expect(!copy.isConst());
3865 try std.testing.expect(!copy.isTrue());
3866 try std.testing.expect(!copy.isFalse());
3867
3868 const json = try copy.toJson(allocator);
3869 defer allocator.free(json);
3870 try std.testing.expect(std.mem.indexOf(u8, json, "\"root\":") != null);
3871 try std.testing.expect(std.mem.indexOf(u8, json, "\"nodes\":") != null);
3872 }
3873
3874 test "deepCopy - constants" {
3875 const allocator = std.testing.allocator;
3876 var manager = try Manager.init(allocator);
3877 defer manager.deinit();
3878
3879 var true_copy = try deepCopy(&manager, Bdd.TRUE, allocator);
3880 defer true_copy.deinit();
3881 try std.testing.expect(true_copy.isTrue());
3882
3883 var false_copy = try deepCopy(&manager, Bdd.FALSE, allocator);
3884 defer false_copy.deinit();
3885 try std.testing.expect(false_copy.isFalse());
3886 }
3887
3888 test "finite difference derivative validation - single variable" {
3889 const allocator = std.testing.allocator;
3890 var manager = try Manager.init(allocator);
3891 defer manager.deinit();
3892
3893 const x = try manager.newVar(true);
3894 const epsilon: f64 = 1e-6;
3895
3896 const test_probs = [_]f64{ 0.1, 0.3, 0.5, 0.7, 0.9 };
3897
3898 for (test_probs) |p| {
3899 var params_dual = WmcParams.initDual(allocator, 1);
3900 defer params_dual.deinit();
3901 var zero_partials = [_]f64{0.0};
3902 var one_partials = [_]f64{1.0};
3903 try params_dual.setWeightDeriv(0, 1.0 - p, &zero_partials, p, &one_partials);
3904
3905 var dual_result = try wmcDual(&manager, x, ¶ms_dual, allocator);
3906 defer dual_result.deinit();
3907 const analytic_grad = dual_result.partials[0];
3908
3909 var params_plus = WmcParams.init(allocator);
3910 defer params_plus.deinit();
3911 try params_plus.setWeight(0, 1.0 - (p + epsilon), p + epsilon);
3912
3913 var params_minus = WmcParams.init(allocator);
3914 defer params_minus.deinit();
3915 try params_minus.setWeight(0, 1.0 - (p - epsilon), p - epsilon);
3916
3917 const wmc_plus = wmc(&manager, x, ¶ms_plus);
3918 const wmc_minus = wmc(&manager, x, ¶ms_minus);
3919 const fd_grad = (wmc_plus - wmc_minus) / (2.0 * epsilon);
3920
3921 try std.testing.expectApproxEqAbs(analytic_grad, fd_grad, 1e-5);
3922 }
3923 }
3924
3925 test "finite difference derivative validation - two variable AND" {
3926 const allocator = std.testing.allocator;
3927 var manager = try Manager.init(allocator);
3928 defer manager.deinit();
3929
3930 const x = try manager.newVar(true);
3931 const y = try manager.newVar(true);
3932 const x_and_y = try manager.bddAnd(x, y);
3933
3934 const px: f64 = 0.6;
3935 const py: f64 = 0.7;
3936 const epsilon: f64 = 1e-6;
3937
3938 var params_dual = WmcParams.initDual(allocator, 2);
3939 defer params_dual.deinit();
3940 var zero_partials = [_]f64{ 0.0, 0.0 };
3941 var x_partials = [_]f64{ 1.0, 0.0 };
3942 var y_partials = [_]f64{ 0.0, 1.0 };
3943 try params_dual.setWeightDeriv(0, 1.0 - px, &zero_partials, px, &x_partials);
3944 try params_dual.setWeightDeriv(1, 1.0 - py, &zero_partials, py, &y_partials);
3945
3946 var dual_result = try wmcDual(&manager, x_and_y, ¶ms_dual, allocator);
3947 defer dual_result.deinit();
3948
3949 var params_plus = WmcParams.init(allocator);
3950 defer params_plus.deinit();
3951 try params_plus.setWeight(0, 1.0 - (px + epsilon), px + epsilon);
3952 try params_plus.setWeight(1, 1.0 - py, py);
3953
3954 var params_minus = WmcParams.init(allocator);
3955 defer params_minus.deinit();
3956 try params_minus.setWeight(0, 1.0 - (px - epsilon), px - epsilon);
3957 try params_minus.setWeight(1, 1.0 - py, py);
3958
3959 const fd_grad_x = (wmc(&manager, x_and_y, ¶ms_plus) - wmc(&manager, x_and_y, ¶ms_minus)) / (2.0 * epsilon);
3960 try std.testing.expectApproxEqAbs(dual_result.partials[0], fd_grad_x, 1e-5);
3961
3962 var params_plus_y = WmcParams.init(allocator);
3963 defer params_plus_y.deinit();
3964 try params_plus_y.setWeight(0, 1.0 - px, px);
3965 try params_plus_y.setWeight(1, 1.0 - (py + epsilon), py + epsilon);
3966
3967 var params_minus_y = WmcParams.init(allocator);
3968 defer params_minus_y.deinit();
3969 try params_minus_y.setWeight(0, 1.0 - px, px);
3970 try params_minus_y.setWeight(1, 1.0 - (py - epsilon), py - epsilon);
3971
3972 const fd_grad_y = (wmc(&manager, x_and_y, ¶ms_plus_y) - wmc(&manager, x_and_y, ¶ms_minus_y)) / (2.0 * epsilon);
3973 try std.testing.expectApproxEqAbs(dual_result.partials[1], fd_grad_y, 1e-5);
3974 }
3975
3976 test "finite difference derivative validation - XOR formula" {
3977 const allocator = std.testing.allocator;
3978 var manager = try Manager.init(allocator);
3979 defer manager.deinit();
3980
3981 const x = try manager.newVar(true);
3982 const y = try manager.newVar(true);
3983 const formula = try manager.bddXor(x, y);
3984
3985 const px: f64 = 0.4;
3986 const py: f64 = 0.6;
3987 const epsilon: f64 = 1e-6;
3988
3989 var params_dual = WmcParams.initDual(allocator, 4);
3990 defer params_dual.deinit();
3991 var x_high_partials = [_]f64{ 1.0, 0.0, 0.0, 0.0 };
3992 var x_low_partials = [_]f64{ 0.0, 1.0, 0.0, 0.0 };
3993 var y_high_partials = [_]f64{ 0.0, 0.0, 1.0, 0.0 };
3994 var y_low_partials = [_]f64{ 0.0, 0.0, 0.0, 1.0 };
3995 try params_dual.setWeightDeriv(0, 1.0 - px, &x_low_partials, px, &x_high_partials);
3996 try params_dual.setWeightDeriv(1, 1.0 - py, &y_low_partials, py, &y_high_partials);
3997
3998 var dual_result = try wmcDual(&manager, formula, ¶ms_dual, allocator);
3999 defer dual_result.deinit();
4000
4001 const grad_px = dual_result.partials[0] - dual_result.partials[1];
4002 const grad_py = dual_result.partials[2] - dual_result.partials[3];
4003
4004 var params_px_plus = WmcParams.init(allocator);
4005 defer params_px_plus.deinit();
4006 try params_px_plus.setWeight(0, 1.0 - (px + epsilon), px + epsilon);
4007 try params_px_plus.setWeight(1, 1.0 - py, py);
4008
4009 var params_px_minus = WmcParams.init(allocator);
4010 defer params_px_minus.deinit();
4011 try params_px_minus.setWeight(0, 1.0 - (px - epsilon), px - epsilon);
4012 try params_px_minus.setWeight(1, 1.0 - py, py);
4013
4014 const fd_grad_x = (wmc(&manager, formula, ¶ms_px_plus) - wmc(&manager, formula, ¶ms_px_minus)) / (2.0 * epsilon);
4015 try std.testing.expectApproxEqAbs(grad_px, fd_grad_x, 1e-4);
4016
4017 var params_py_plus = WmcParams.init(allocator);
4018 defer params_py_plus.deinit();
4019 try params_py_plus.setWeight(0, 1.0 - px, px);
4020 try params_py_plus.setWeight(1, 1.0 - (py + epsilon), py + epsilon);
4021
4022 var params_py_minus = WmcParams.init(allocator);
4023 defer params_py_minus.deinit();
4024 try params_py_minus.setWeight(0, 1.0 - px, px);
4025 try params_py_minus.setWeight(1, 1.0 - (py - epsilon), py - epsilon);
4026
4027 const fd_grad_y = (wmc(&manager, formula, ¶ms_py_plus) - wmc(&manager, formula, ¶ms_py_minus)) / (2.0 * epsilon);
4028 try std.testing.expectApproxEqAbs(grad_py, fd_grad_y, 1e-4);
4029 }
4030
4031 test "sampling distribution matches WMC - simple verification" {
4032 const allocator = std.testing.allocator;
4033 var manager = try Manager.init(allocator);
4034 defer manager.deinit();
4035
4036 var params = WmcParams.init(allocator);
4037 defer params.deinit();
4038
4039 try params.setWeight(0, 0.3, 0.7);
4040
4041 const x = try manager.newVar(true);
4042
4043 var prng = std.Random.DefaultPrng.init(42);
4044 const rng = prng.random();
4045
4046 var true_count: usize = 0;
4047 const num_samples: usize = 10000;
4048
4049 for (0..num_samples) |_| {
4050 const result = try weightedSample(&manager, x, ¶ms, rng);
4051 try std.testing.expect(manager.eq(result.sample, x));
4052 true_count += 1;
4053 }
4054
4055 try std.testing.expectEqual(num_samples, true_count);
4056 }
4057
4058 test "sampling coverage - all paths found for OR" {
4059 const allocator = std.testing.allocator;
4060 var manager = try Manager.init(allocator);
4061 defer manager.deinit();
4062
4063 var params = WmcParams.init(allocator);
4064 defer params.deinit();
4065
4066 try params.setWeight(0, 0.5, 0.5);
4067 try params.setWeight(1, 0.5, 0.5);
4068
4069 const x = try manager.newVar(true);
4070 const y = try manager.newVar(true);
4071 const x_or_y = try manager.bddOr(x, y);
4072
4073 var seen_x_true = false;
4074 var seen_x_false_y_true = false;
4075
4076 var prng = std.Random.DefaultPrng.init(12345);
4077 const rng = prng.random();
4078
4079 for (0..1000) |_| {
4080 const result = try weightedSample(&manager, x_or_y, ¶ms, rng);
4081 if (manager.eq(result.sample, x)) {
4082 seen_x_true = true;
4083 }
4084 const not_x_and_y = try manager.bddAnd(x.neg(), y);
4085 if (manager.eq(result.sample, not_x_and_y)) {
4086 seen_x_false_y_true = true;
4087 }
4088 }
4089
4090 try std.testing.expect(seen_x_true);
4091 try std.testing.expect(seen_x_false_y_true);
4092 }
4093
4094 test "top_k_paths covers exact WMC" {
4095 const allocator = std.testing.allocator;
4096 var manager = try Manager.init(allocator);
4097 defer manager.deinit();
4098
4099 var params = WmcParams.init(allocator);
4100 defer params.deinit();
4101
4102 try params.setWeight(0, 0.3, 0.7);
4103 try params.setWeight(1, 0.4, 0.6);
4104 try params.setWeight(2, 0.5, 0.5);
4105
4106 const x = try manager.newVar(true);
4107 const y = try manager.newVar(true);
4108 const z = try manager.newVar(true);
4109
4110 const xy = try manager.bddAnd(x, y);
4111 const formula = try manager.bddOr(xy, z);
4112
4113 const exact_wmc = wmc(&manager, formula, ¶ms);
4114
4115 const top_many = try topKPaths(&manager, formula, 100, ¶ms, allocator);
4116 const top_wmc = wmc(&manager, top_many, ¶ms);
4117
4118 try std.testing.expectApproxEqAbs(exact_wmc, top_wmc, 1e-10);
4119 }
4120
4121 test "CNF benchmark - 3-SAT clause" {
4122 const allocator = std.testing.allocator;
4123 var manager = try Manager.init(allocator);
4124 defer manager.deinit();
4125
4126 var params = WmcParams.init(allocator);
4127 defer params.deinit();
4128
4129 const x = try manager.newVar(true);
4130 const y = try manager.newVar(true);
4131 const z = try manager.newVar(true);
4132
4133 try params.setWeight(0, 0.5, 0.5);
4134 try params.setWeight(1, 0.5, 0.5);
4135 try params.setWeight(2, 0.5, 0.5);
4136
4137 const clause1 = try manager.bddOr(try manager.bddOr(x, y), z);
4138 const clause2 = try manager.bddOr(try manager.bddOr(x.neg(), y), z.neg());
4139 const clause3 = try manager.bddOr(try manager.bddOr(x, y.neg()), z);
4140
4141 const cnf = try manager.bddAnd(try manager.bddAnd(clause1, clause2), clause3);
4142
4143 const result = wmc(&manager, cnf, ¶ms);
4144 try std.testing.expectApproxEqAbs(@as(f64, 5.0 / 8.0), result, 1e-10);
4145 }
4146
4147 test "complement edge WMC correctness - complex formula" {
4148 const allocator = std.testing.allocator;
4149 var manager = try Manager.init(allocator);
4150 defer manager.deinit();
4151
4152 var params = WmcParams.init(allocator);
4153 defer params.deinit();
4154
4155 try params.setWeight(0, 0.3, 0.7);
4156 try params.setWeight(1, 0.4, 0.6);
4157
4158 const x = try manager.newVar(true);
4159 const y = try manager.newVar(true);
4160
4161 const formula = try manager.bddImplies(x, y);
4162 const neg_formula = manager.bddNot(formula);
4163
4164 const wmc_formula = wmc(&manager, formula, ¶ms);
4165 const wmc_neg = wmc(&manager, neg_formula, ¶ms);
4166 try std.testing.expectApproxEqAbs(@as(f64, 1.0), wmc_formula + wmc_neg, 1e-10);
4167
4168 try std.testing.expectApproxEqAbs(@as(f64, 0.72), wmc_formula, 1e-10);
4169 }
4170
4171 test "complement edge WMC - double negation" {
4172 const allocator = std.testing.allocator;
4173 var manager = try Manager.init(allocator);
4174 defer manager.deinit();
4175
4176 var params = WmcParams.init(allocator);
4177 defer params.deinit();
4178
4179 try params.setWeight(0, 0.25, 0.75);
4180
4181 const x = try manager.newVar(true);
4182 const not_x = manager.bddNot(x);
4183 const not_not_x = manager.bddNot(not_x);
4184
4185 try std.testing.expect(manager.eq(x, not_not_x));
4186
4187 const wmc_x = wmc(&manager, x, ¶ms);
4188 const wmc_nnx = wmc(&manager, not_not_x, ¶ms);
4189 try std.testing.expectApproxEqAbs(wmc_x, wmc_nnx, 1e-10);
4190 }
4191
4192 test "absorption law: a AND (a OR b) = a" {
4193 const allocator = std.testing.allocator;
4194 var manager = try Manager.init(allocator);
4195 defer manager.deinit();
4196
4197 const a = try manager.newVar(true);
4198 const b = try manager.newVar(true);
4199
4200 const a_or_b = try manager.bddOr(a, b);
4201 const result = try manager.bddAnd(a, a_or_b);
4202
4203 try std.testing.expect(manager.eq(result, a));
4204 }
4205
4206 test "absorption law: a OR (a AND b) = a" {
4207 const allocator = std.testing.allocator;
4208 var manager = try Manager.init(allocator);
4209 defer manager.deinit();
4210
4211 const a = try manager.newVar(true);
4212 const b = try manager.newVar(true);
4213
4214 const a_and_b = try manager.bddAnd(a, b);
4215 const result = try manager.bddOr(a, a_and_b);
4216
4217 try std.testing.expect(manager.eq(result, a));
4218 }
4219
4220 test "distributive law: a AND (b OR c) = (a AND b) OR (a AND c)" {
4221 const allocator = std.testing.allocator;
4222 var manager = try Manager.init(allocator);
4223 defer manager.deinit();
4224
4225 const a = try manager.newVar(true);
4226 const b = try manager.newVar(true);
4227 const c = try manager.newVar(true);
4228
4229 const b_or_c = try manager.bddOr(b, c);
4230 const lhs = try manager.bddAnd(a, b_or_c);
4231
4232 const a_and_b = try manager.bddAnd(a, b);
4233 const a_and_c = try manager.bddAnd(a, c);
4234 const rhs = try manager.bddOr(a_and_b, a_and_c);
4235
4236 try std.testing.expect(manager.eq(lhs, rhs));
4237 }
4238
4239 test "consensus theorem: (a AND b) OR (!a AND c) OR (b AND c) = (a AND b) OR (!a AND c)" {
4240 const allocator = std.testing.allocator;
4241 var manager = try Manager.init(allocator);
4242 defer manager.deinit();
4243
4244 const a = try manager.newVar(true);
4245 const b = try manager.newVar(true);
4246 const c = try manager.newVar(true);
4247
4248 const a_and_b = try manager.bddAnd(a, b);
4249 const not_a_and_c = try manager.bddAnd(a.neg(), c);
4250 const b_and_c = try manager.bddAnd(b, c);
4251
4252 const lhs = try manager.bddOr(try manager.bddOr(a_and_b, not_a_and_c), b_and_c);
4253 const rhs = try manager.bddOr(a_and_b, not_a_and_c);
4254
4255 try std.testing.expect(manager.eq(lhs, rhs));
4256 }
4257
4258 const AlarmFixture = struct {
4259 alarm: Bdd,
4260 earthquake: Bdd,
4261 burglary: Bdd,
4262 };
4263
4264 fn createAlarmFixture(manager: *Manager) Allocator.Error!AlarmFixture {
4265 const earthquake = try manager.newVar(true);
4266 const burglary = try manager.newVar(true);
4267 const alarm = try manager.bddOr(earthquake, burglary);
4268 return .{ .alarm = alarm, .earthquake = earthquake, .burglary = burglary };
4269 }
4270
4271 test "fixture - alarm model WMC" {
4272 const allocator = std.testing.allocator;
4273 var manager = try Manager.init(allocator);
4274 defer manager.deinit();
4275
4276 var params = WmcParams.init(allocator);
4277 defer params.deinit();
4278
4279 const fixture = try createAlarmFixture(&manager);
4280
4281 try params.setWeight(0, 0.9999, 0.0001);
4282 try params.setWeight(1, 0.999, 0.001);
4283
4284 const alarm_prob = wmc(&manager, fixture.alarm, ¶ms);
4285 try std.testing.expectApproxEqAbs(@as(f64, 0.0010999), alarm_prob, 1e-6);
4286 }
4287
4288 const ConditionalFixture = struct {
4289 result: Bdd,
4290 earthquake: Bdd,
4291 phone_bad: Bdd,
4292 phone_good: Bdd,
4293 };
4294
4295 fn createConditionalFixture(manager: *Manager) Allocator.Error!ConditionalFixture {
4296 const earthquake = try manager.newVar(true);
4297 const phone_bad = try manager.newVar(true);
4298 const phone_good = try manager.newVar(true);
4299
4300 const case_eq = try manager.bddAnd(earthquake, phone_bad);
4301 const case_normal = try manager.bddAnd(earthquake.neg(), phone_good);
4302 const result = try manager.bddOr(case_eq, case_normal);
4303
4304 return .{ .result = result, .earthquake = earthquake, .phone_bad = phone_bad, .phone_good = phone_good };
4305 }
4306
4307 test "fixture - conditional model WMC" {
4308 const allocator = std.testing.allocator;
4309 var manager = try Manager.init(allocator);
4310 defer manager.deinit();
4311
4312 var params = WmcParams.init(allocator);
4313 defer params.deinit();
4314
4315 const fixture = try createConditionalFixture(&manager);
4316
4317 try params.setWeight(0, 0.9999, 0.0001);
4318 try params.setWeight(1, 0.3, 0.7);
4319 try params.setWeight(2, 0.01, 0.99);
4320
4321 const phone_prob = wmc(&manager, fixture.result, ¶ms);
4322 try std.testing.expectApproxEqAbs(@as(f64, 0.989971), phone_prob, 1e-6);
4323 }
4324
4325 test "WmcContext - basic caching correctness" {
4326 const allocator = std.testing.allocator;
4327 var manager = try Manager.init(allocator);
4328 defer manager.deinit();
4329
4330 var params = WmcParams.init(allocator);
4331 defer params.deinit();
4332
4333 var ctx = WmcContext.init(allocator);
4334 defer ctx.deinit();
4335
4336 try params.setWeight(0, 0.3, 0.7);
4337 try params.setWeight(1, 0.4, 0.6);
4338
4339 const x = try manager.newVar(true);
4340 const y = try manager.newVar(true);
4341 const x_and_y = try manager.bddAnd(x, y);
4342
4343 const result1 = ctx.wmcCached(&manager, x_and_y, ¶ms);
4344
4345 const expected = wmc(&manager, x_and_y, ¶ms);
4346 try std.testing.expectApproxEqAbs(expected, result1, 1e-10);
4347
4348 const result2 = ctx.wmcCached(&manager, x_and_y, ¶ms);
4349 try std.testing.expectApproxEqAbs(result1, result2, 1e-10);
4350
4351 const stats = ctx.getStats();
4352 try std.testing.expect(stats.hits > 0);
4353 try std.testing.expect(stats.misses > 0);
4354 }
4355
4356 test "WmcContext - cache invalidation on weight change" {
4357 const allocator = std.testing.allocator;
4358 var manager = try Manager.init(allocator);
4359 defer manager.deinit();
4360
4361 var params = WmcParams.init(allocator);
4362 defer params.deinit();
4363
4364 var ctx = WmcContext.init(allocator);
4365 defer ctx.deinit();
4366
4367 try params.setWeight(0, 0.3, 0.7);
4368 const x = try manager.newVar(true);
4369
4370 const result1 = ctx.wmcCached(&manager, x, ¶ms);
4371 try std.testing.expectApproxEqAbs(@as(f64, 0.7), result1, 1e-10);
4372
4373 try params.setWeight(0, 0.2, 0.8);
4374
4375 ctx.invalidateWeights();
4376
4377 const result2 = ctx.wmcCached(&manager, x, ¶ms);
4378 try std.testing.expectApproxEqAbs(@as(f64, 0.8), result2, 1e-10);
4379 }
4380
4381 test "WmcContext - cache size and trimming" {
4382 const allocator = std.testing.allocator;
4383 var manager = try Manager.init(allocator);
4384 defer manager.deinit();
4385
4386 var params = WmcParams.init(allocator);
4387 defer params.deinit();
4388
4389 var ctx = WmcContext.init(allocator);
4390 defer ctx.deinit();
4391
4392 for (0..10) |i| {
4393 try params.setWeight(@intCast(i), 0.5, 0.5);
4394 const v = try manager.newVar(true);
4395 _ = ctx.wmcCached(&manager, v, ¶ms);
4396 }
4397
4398 const size_before = ctx.cacheSize();
4399 try std.testing.expect(size_before >= 10);
4400
4401 const evicted = ctx.trimToSize(5);
4402 try std.testing.expect(evicted > 0);
4403 try std.testing.expect(ctx.cacheSize() <= 5);
4404 }
4405
4406 test "WmcContext - structure version invalidation" {
4407 const allocator = std.testing.allocator;
4408 var manager = try Manager.init(allocator);
4409 defer manager.deinit();
4410
4411 var params = WmcParams.init(allocator);
4412 defer params.deinit();
4413
4414 var ctx = WmcContext.init(allocator);
4415 defer ctx.deinit();
4416
4417 try params.setWeight(0, 0.5, 0.5);
4418 const x = try manager.newVar(true);
4419
4420 _ = ctx.wmcCached(&manager, x, ¶ms);
4421
4422 ctx.invalidateAll();
4423
4424 _ = ctx.wmcCached(&manager, x, ¶ms);
4425 const stats_after = ctx.getStats();
4426
4427 try std.testing.expect(stats_after.invalidations == 1);
4428 }
4429
4430 test "WmcContext - hit rate calculation" {
4431 const allocator = std.testing.allocator;
4432 var manager = try Manager.init(allocator);
4433 defer manager.deinit();
4434
4435 var params = WmcParams.init(allocator);
4436 defer params.deinit();
4437
4438 var ctx = WmcContext.init(allocator);
4439 defer ctx.deinit();
4440
4441 try params.setWeight(0, 0.3, 0.7);
4442 const x = try manager.newVar(true);
4443
4444 _ = ctx.wmcCached(&manager, x, ¶ms);
4445
4446 _ = ctx.wmcCached(&manager, x, ¶ms);
4447
4448 const stats = ctx.getStats();
4449 const hit_rate = stats.hitRate();
4450
4451 try std.testing.expect(hit_rate > 0.0);
4452 try std.testing.expect(hit_rate <= 1.0);
4453 }
4454
4455 test "WmcContext - correctness on complex BDD" {
4456 const allocator = std.testing.allocator;
4457 var manager = try Manager.init(allocator);
4458 defer manager.deinit();
4459
4460 var params = WmcParams.init(allocator);
4461 defer params.deinit();
4462
4463 var ctx = WmcContext.init(allocator);
4464 defer ctx.deinit();
4465
4466 const fixture = try createAlarmFixture(&manager);
4467
4468 try params.setWeight(0, 0.9999, 0.0001);
4469 try params.setWeight(1, 0.999, 0.001);
4470
4471 const cached_result = ctx.wmcCached(&manager, fixture.alarm, ¶ms);
4472 const direct_result = wmc(&manager, fixture.alarm, ¶ms);
4473
4474 try std.testing.expectApproxEqAbs(direct_result, cached_result, 1e-10);
4475 }
4476
4477 test "WmcContext - manager change clears stale entries" {
4478 const allocator = std.testing.allocator;
4479 var manager_a = try Manager.init(allocator);
4480 defer manager_a.deinit();
4481
4482 var manager_b = try Manager.init(allocator);
4483 defer manager_b.deinit();
4484
4485 var params = WmcParams.init(allocator);
4486 defer params.deinit();
4487
4488 var ctx = WmcContext.init(allocator);
4489 defer ctx.deinit();
4490
4491 try params.setWeight(0, 0.3, 0.7);
4492 try params.setWeight(1, 0.4, 0.6);
4493
4494 const ax = try manager_a.newVar(true);
4495 const ay = try manager_a.newVar(true);
4496 const a_formula = try manager_a.bddAnd(ax, ay);
4497
4498 const bx = try manager_b.newVar(true);
4499 const by = try manager_b.newVar(true);
4500 const b_formula = try manager_b.bddOr(bx, by);
4501
4502 try std.testing.expectEqual(a_formula.toRaw(), b_formula.toRaw());
4503
4504 const first = ctx.wmcCached(&manager_a, a_formula, ¶ms);
4505 try std.testing.expectApproxEqAbs(@as(f64, 0.42), first, 1e-10);
4506
4507 const second = ctx.wmcCached(&manager_b, b_formula, ¶ms);
4508 try std.testing.expectApproxEqAbs(@as(f64, 0.88), second, 1e-10);
4509 }
4510
4511 test "WmcContext - multiple queries same BDD" {
4512 const allocator = std.testing.allocator;
4513 var manager = try Manager.init(allocator);
4514 defer manager.deinit();
4515
4516 var params = WmcParams.init(allocator);
4517 defer params.deinit();
4518
4519 var ctx = WmcContext.init(allocator);
4520 defer ctx.deinit();
4521
4522 try params.setWeight(0, 0.3, 0.7);
4523 try params.setWeight(1, 0.4, 0.6);
4524
4525 const x = try manager.newVar(true);
4526 const y = try manager.newVar(true);
4527 const x_and_y = try manager.bddAnd(x, y);
4528
4529 var sum: f64 = 0;
4530 for (0..100) |_| {
4531 sum += ctx.wmcCached(&manager, x_and_y, ¶ms);
4532 }
4533
4534 const expected = 0.7 * 0.6 * 100;
4535 try std.testing.expectApproxEqAbs(expected, sum, 1e-8);
4536
4537 const stats = ctx.getStats();
4538 try std.testing.expect(stats.hitRate() > 0.9);
4539 }
4540
4541 test "WmcContext - invalidateForVars correctness" {
4542 const allocator = std.testing.allocator;
4543 var manager = try Manager.init(allocator);
4544 defer manager.deinit();
4545
4546 var params = WmcParams.init(allocator);
4547 defer params.deinit();
4548
4549 var ctx = WmcContext.init(allocator);
4550 defer ctx.deinit();
4551
4552 try params.setWeight(0, 0.3, 0.7);
4553 try params.setWeight(1, 0.4, 0.6);
4554
4555 const x = try manager.newVar(true);
4556 const y = try manager.newVar(true);
4557 const x_and_y = try manager.bddAnd(x, y);
4558
4559 const result1 = ctx.wmcCached(&manager, x_and_y, ¶ms);
4560 try std.testing.expectApproxEqAbs(@as(f64, 0.42), result1, 1e-10);
4561
4562 try params.setWeight(0, 0.1, 0.9);
4563
4564 ctx.invalidateForVars(&manager, &[_]VarLabel{0});
4565
4566 const result2 = ctx.wmcCached(&manager, x_and_y, ¶ms);
4567
4568 const expected_new = wmc(&manager, x_and_y, ¶ms);
4569 try std.testing.expectApproxEqAbs(expected_new, result2, 1e-10);
4570 try std.testing.expectApproxEqAbs(@as(f64, 0.54), result2, 1e-10);
4571
4572 try std.testing.expect(@abs(result2 - result1) > 0.1);
4573 }
4574
4575 test "WmcContext - invalidateForVars preserves unrelated cache entries" {
4576 const allocator = std.testing.allocator;
4577 var manager = try Manager.init(allocator);
4578 defer manager.deinit();
4579
4580 var params = WmcParams.init(allocator);
4581 defer params.deinit();
4582
4583 var ctx = WmcContext.init(allocator);
4584 defer ctx.deinit();
4585
4586 try params.setWeight(0, 0.3, 0.7);
4587 try params.setWeight(1, 0.4, 0.6);
4588
4589 const x = try manager.newVar(true);
4590 const y = try manager.newVar(true);
4591
4592 _ = ctx.wmcCached(&manager, x, ¶ms);
4593 _ = ctx.wmcCached(&manager, y, ¶ms);
4594
4595 try std.testing.expectEqual(@as(usize, 2), ctx.cacheSize());
4596
4597 try params.setWeight(0, 0.1, 0.9);
4598 ctx.invalidateForVars(&manager, &[_]VarLabel{0});
4599
4600 try std.testing.expectEqual(@as(usize, 1), ctx.cacheSize());
4601
4602 const stats_before_y = ctx.getStats();
4603 const y_result = ctx.wmcCached(&manager, y, ¶ms);
4604 const stats_after_y = ctx.getStats();
4605
4606 try std.testing.expectApproxEqAbs(@as(f64, 0.6), y_result, 1e-10);
4607 try std.testing.expectEqual(stats_before_y.hits + 1, stats_after_y.hits);
4608
4609 const x_result = ctx.wmcCached(&manager, x, ¶ms);
4610 try std.testing.expectApproxEqAbs(@as(f64, 0.9), x_result, 1e-10);
4611 }
4612
4613 test "WmcContext - invalidateForVars removes recursive dependent entries" {
4614 const allocator = std.testing.allocator;
4615 var manager = try Manager.init(allocator);
4616 defer manager.deinit();
4617
4618 var params = WmcParams.init(allocator);
4619 defer params.deinit();
4620
4621 var ctx = WmcContext.init(allocator);
4622 defer ctx.deinit();
4623
4624 try params.setWeight(0, 0.3, 0.7);
4625 try params.setWeight(1, 0.4, 0.6);
4626
4627 const x = try manager.newVar(true);
4628 const y = try manager.newVar(true);
4629 const x_and_y = try manager.bddAnd(x, y);
4630
4631 const result1 = ctx.wmcCached(&manager, x_and_y, ¶ms);
4632 try std.testing.expectApproxEqAbs(@as(f64, 0.42), result1, 1e-10);
4633
4634 try params.setWeight(1, 0.2, 0.8);
4635 ctx.invalidateForVars(&manager, &[_]VarLabel{1});
4636
4637 const result2 = ctx.wmcCached(&manager, x_and_y, ¶ms);
4638 const expected_new = wmc(&manager, x_and_y, ¶ms);
4639
4640 try std.testing.expectApproxEqAbs(expected_new, result2, 1e-10);
4641 try std.testing.expectApproxEqAbs(@as(f64, 0.56), result2, 1e-10);
4642 }
4643
4644 test "WmcContext - invalidateForVars keeps cache version stable" {
4645 const allocator = std.testing.allocator;
4646 var manager = try Manager.init(allocator);
4647 defer manager.deinit();
4648
4649 var params = WmcParams.init(allocator);
4650 defer params.deinit();
4651
4652 var ctx = WmcContext.init(allocator);
4653 defer ctx.deinit();
4654
4655 try params.setWeight(0, 0.3, 0.7);
4656
4657 const x = try manager.newVar(true);
4658
4659 const result1 = ctx.wmcCached(&manager, x, ¶ms);
4660 try std.testing.expectApproxEqAbs(@as(f64, 0.7), result1, 1e-10);
4661
4662 try params.setWeight(0, 0.1, 0.9);
4663 ctx.invalidateForVars(&manager, &[_]VarLabel{0});
4664
4665 const result2 = ctx.wmcCached(&manager, x, ¶ms);
4666
4667 try std.testing.expectApproxEqAbs(@as(f64, 0.9), result2, 1e-10);
4668 try std.testing.expectEqual(@as(u64, 0), ctx.params_version);
4669 }
4670
4671 test "WmcContext - memory growth with lazy invalidation" {
4672 const allocator = std.testing.allocator;
4673 var manager = try Manager.init(allocator);
4674 defer manager.deinit();
4675
4676 var params = WmcParams.init(allocator);
4677 defer params.deinit();
4678
4679 var ctx = WmcContext.init(allocator);
4680 defer ctx.deinit();
4681
4682 try params.setWeight(0, 0.5, 0.5);
4683 const x = try manager.newVar(true);
4684
4685 for (0..10) |_| {
4686 _ = ctx.wmcCached(&manager, x, ¶ms);
4687 ctx.invalidateWeights();
4688 }
4689
4690 try std.testing.expect(ctx.cacheSize() >= 1);
4691
4692 _ = ctx.trimToSize(1);
4693 try std.testing.expect(ctx.cacheSize() <= 1);
4694 }
4695
4696 test "WmcContext - clear resets everything" {
4697 const allocator = std.testing.allocator;
4698 var manager = try Manager.init(allocator);
4699 defer manager.deinit();
4700
4701 var params = WmcParams.init(allocator);
4702 defer params.deinit();
4703
4704 var ctx = WmcContext.init(allocator);
4705 defer ctx.deinit();
4706
4707 try params.setWeight(0, 0.5, 0.5);
4708 const x = try manager.newVar(true);
4709
4710 _ = ctx.wmcCached(&manager, x, ¶ms);
4711 ctx.invalidateWeights();
4712 _ = ctx.wmcCached(&manager, x, ¶ms);
4713
4714 try std.testing.expect(ctx.cacheSize() > 0);
4715 try std.testing.expect(ctx.getStats().hits > 0 or ctx.getStats().misses > 0);
4716
4717 ctx.clear();
4718
4719 try std.testing.expectEqual(@as(usize, 0), ctx.cacheSize());
4720 try std.testing.expectEqual(@as(u64, 0), ctx.getStats().hits);
4721 try std.testing.expectEqual(@as(u64, 0), ctx.getStats().misses);
4722 try std.testing.expectEqual(@as(u64, 0), ctx.params_version);
4723 try std.testing.expectEqual(@as(u64, 0), ctx.structure_version);
4724 }