lib/pluck/src/profiling/internal/factor.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const Allocator = std.mem.Allocator;
3
4 const pluck = @import("pluck");
5 const bdd = pluck.bdd;
6 const Manager = bdd.Manager;
7 const Bdd = bdd.Bdd;
8
9 const pexpr = pluck.pexpr;
10 const evaluator = pluck.evaluator;
11 const state_module = pluck.state;
12 const toplevel = pluck.toplevel;
13 const runtime = pluck.runtime;
14 const weight_dd = pluck.weight_dd;
15 const WeightDD = weight_dd.WeightDD;
16 const GuardedWeight = weight_dd.GuardedWeight;
17
18 const LazyKCConfig = state_module.LazyKCConfig;
19 const LazyKCState = state_module.LazyKCState;
20 const LimitReason = state_module.LimitReason;
21 const bench_util = @import("util.zig");
22
23 const ExactMetrics = struct {
24 worlds: usize,
25 vars: usize,
26 nodes: usize,
27 compile_ns: u64,
28 wmc_ns: u64,
29 total_ns: u64,
30 limit_reason: ?LimitReason,
31 program_error: bool,
32 };
33
34 const LpsmcMetrics = struct {
35 outcomes: usize,
36 vars: usize,
37 nodes: usize,
38 lpsmc_ns: u64,
39 limit_reason: ?LimitReason,
40 program_error: bool,
41 };
42
43 const LpsmcAccuracyMetrics = struct {
44 prob_true: f64,
45 abs_error: f64,
46 total_k: usize,
47 avg_k: f64,
48 min_k: usize,
49 max_k: usize,
50 lpsmc_ns: u64,
51 limit_reason: ?LimitReason,
52 program_error: bool,
53 };
54
55 const FactorBenchMetrics = struct {
56 vars: usize,
57 nodes: usize,
58 weight_dd_nodes: usize,
59 guard_peak: usize,
60 compile_ns: u64,
61 wmc_ns: u64,
62 total_ns: u64,
63 limit_reason: ?LimitReason,
64 program_error: bool,
65 };
66
67 fn limitTag(reason: ?LimitReason) []const u8 {
68 return if (reason) |r| switch (r) {
69 .max_depth => "max_depth",
70 .time_limit => "time_limit",
71 .ite_limit => "ite_limit",
72 .factor_weight_too_complex => "factor_weight_too_complex",
73 } else "";
74 }
75
76 fn nsToMs(ns: u64) f64 {
77 return @as(f64, @floatFromInt(ns)) / 1_000_000.0;
78 }
79
80 fn loadDefs(ctx: *toplevel.ToplevelContext, defs: []const []const u8) !void {
81 for (defs) |src| {
82 _ = try ctx.processForm(src);
83 }
84 }
85
86 fn buildWeightedIntDistExpr(allocator: Allocator, bitwidth: usize) ![]u8 {
87 const num_values: usize = @as(usize, 1) << @intCast(bitwidth);
88 const prob: f64 = 1.0 / @as(f64, @floatFromInt(num_values));
89
90 var buf = std.Io.Writer.Allocating.init(allocator);
91 errdefer buf.deinit();
92
93 try buf.writer.print("(mk_int_weighted @{d} [", .{bitwidth});
94 for (0..num_values) |value| {
95 if (value != 0) try buf.writer.writeAll(" ");
96 try buf.writer.print("(Pair @{d} {d})", .{ value, prob });
97 }
98 try buf.writer.writeAll("])");
99
100 return try buf.toOwnedSlice();
101 }
102
103 fn buildNestedIfExpr(
104 allocator: Allocator,
105 names: []const []const u8,
106 index: usize,
107 base: f64,
108 step: f64,
109 ) ![]u8 {
110 if (index >= names.len) {
111 return std.fmt.allocPrint(allocator, "{d:.6}", .{base});
112 }
113
114 const remaining: usize = names.len - index - 1;
115 const offset: f64 = step * @as(f64, @floatFromInt(@as(usize, 1) << @intCast(remaining)));
116
117 const false_expr = try buildNestedIfExpr(allocator, names, index + 1, base, step);
118 defer allocator.free(false_expr);
119
120 const true_expr = try buildNestedIfExpr(allocator, names, index + 1, base + offset, step);
121 defer allocator.free(true_expr);
122
123 return std.fmt.allocPrint(allocator, "(if {s} {s} {s})", .{ names[index], true_expr, false_expr });
124 }
125
126 fn buildBooleanWeightExpr(allocator: Allocator, bits: usize) ![]u8 {
127 if (bits == 0) {
128 return allocator.dupe(u8, "0.1");
129 }
130
131 var names = try allocator.alloc([]const u8, bits);
132 defer allocator.free(names);
133 for (0..bits) |i| {
134 names[i] = try std.fmt.allocPrint(allocator, "b{d}", .{i});
135 }
136 defer {
137 for (names) |name| {
138 allocator.free(name);
139 }
140 }
141
142 const nested = try buildNestedIfExpr(allocator, names, 0, 0.1, 0.001);
143 defer allocator.free(nested);
144
145 var buf = std.Io.Writer.Allocating.init(allocator);
146 errdefer buf.deinit();
147 try buf.writer.writeAll("(let [");
148 for (names, 0..) |name, i| {
149 if (i != 0) try buf.writer.writeAll(" ");
150 try buf.writer.print("{s} (flip 0.5)", .{name});
151 }
152 try buf.writer.writeAll("] ");
153 try buf.writer.writeAll(nested);
154 try buf.writer.writeAll(")");
155
156 return try buf.toOwnedSlice();
157 }
158
159 fn buildIntDistEqWeightExpr(allocator: Allocator, bitwidth: usize) ![]u8 {
160 const int_dist = try buildWeightedIntDistExpr(allocator, bitwidth);
161 defer allocator.free(int_dist);
162
163 return std.fmt.allocPrint(
164 allocator,
165 "(let [x {s}] (if (int_dist_eq x (mk_int @{d} @0)) 0.2 0.8))",
166 .{ int_dist, bitwidth },
167 );
168 }
169
170 fn runExactWithConfig(
171 allocator: Allocator,
172 defs: []const []const u8,
173 expr_source: []const u8,
174 cfg_in: LazyKCConfig,
175 ) !ExactMetrics {
176 var ctx = try toplevel.ToplevelContext.init(allocator);
177 defer ctx.deinit();
178
179 try loadDefs(&ctx, defs);
180
181 var expr_arena = std.heap.ArenaAllocator.init(allocator);
182 defer expr_arena.deinit();
183
184 const expr = try pexpr.parseExpr(expr_arena.allocator(), expr_source, &ctx.types, &ctx.definitions);
185
186 return runExactParsed(allocator, &ctx.definitions, expr, cfg_in);
187 }
188
189 fn runExactParsed(
190 allocator: Allocator,
191 definitions: *const pexpr.Definitions,
192 expr: *pexpr.PExpr,
193 cfg_in: LazyKCConfig,
194 ) !ExactMetrics {
195 var run_arena = std.heap.ArenaAllocator.init(allocator);
196 defer run_arena.deinit();
197 const run_alloc = run_arena.allocator();
198
199 var manager = try Manager.init(run_alloc);
200 defer manager.deinit();
201
202 var cfg = cfg_in;
203 cfg.full_dist = true;
204
205 var state = try state_module.initChecked(run_alloc, &manager, definitions, cfg);
206 defer state_module.deinit(&state);
207 state.query = expr;
208 state_module.startTimeLimit(&state);
209 defer state_module.stopTimeLimit(&state);
210
211 const compile_start = bench_util.nowNs();
212 const worlds_result = evaluator.tracedCompileInner(expr, runtime.Env.empty, Bdd.TRUE, &state, 0) catch |err| switch (err) {
213 error.PluckError => {
214 const compile_ns: u64 = bench_util.elapsedNs(compile_start);
215 return ExactMetrics{
216 .worlds = 0,
217 .vars = manager.var_order.items.len,
218 .nodes = manager.nodes.items.len,
219 .compile_ns = compile_ns,
220 .wmc_ns = 0,
221 .total_ns = compile_ns,
222 .limit_reason = state.stats.limit_reason,
223 .program_error = true,
224 };
225 },
226 else => return err,
227 };
228
229 var worlds = worlds_result.worlds;
230
231 if (cfg.full_dist) {
232 const new_worlds = try evaluator.inferFullDistribution(run_alloc, worlds, &state);
233 evaluator.freeWorldsSlice(run_alloc, worlds);
234 worlds = new_worlds;
235 }
236
237 if (try evaluator.processIntDistWorlds(run_alloc, worlds, &manager)) |int_worlds| {
238 evaluator.freeWorldsSlice(run_alloc, worlds);
239 worlds = int_worlds;
240 }
241
242 const compile_ns: u64 = bench_util.elapsedNs(compile_start);
243
244 var wmc_ns: u64 = 0;
245 if (state.stats.limit_reason == null and !state.stats.program_error) {
246 const wmc_start = bench_util.nowNs();
247 const weighted_results = try evaluator.computeWmcSequential(
248 run_alloc,
249 worlds,
250 &state.wmc_params,
251 &state.weight_dd,
252 state.weight_dd_root,
253 );
254 wmc_ns = bench_util.elapsedNs(wmc_start);
255 run_alloc.free(weighted_results);
256 }
257
258 const metrics = ExactMetrics{
259 .worlds = worlds.len,
260 .vars = manager.var_order.items.len,
261 .nodes = manager.nodes.items.len,
262 .compile_ns = compile_ns,
263 .wmc_ns = wmc_ns,
264 .total_ns = compile_ns + wmc_ns,
265 .limit_reason = state.stats.limit_reason,
266 .program_error = state.stats.program_error,
267 };
268
269 evaluator.freeWorldsSlice(run_alloc, worlds);
270 return metrics;
271 }
272
273 fn runExact(
274 allocator: Allocator,
275 defs: []const []const u8,
276 expr_source: []const u8,
277 ) !ExactMetrics {
278 return runExactWithConfig(allocator, defs, expr_source, .{});
279 }
280
281 fn runExactFactorBenchParsed(
282 allocator: Allocator,
283 definitions: *const pexpr.Definitions,
284 expr: *pexpr.PExpr,
285 cfg: LazyKCConfig,
286 ) !FactorBenchMetrics {
287 var run_arena = std.heap.ArenaAllocator.init(allocator);
288 defer run_arena.deinit();
289 const run_alloc = run_arena.allocator();
290
291 var manager = try Manager.init(run_alloc);
292 defer manager.deinit();
293
294 var state = try state_module.initChecked(run_alloc, &manager, definitions, cfg);
295 defer state_module.deinit(&state);
296 state.query = expr;
297 state_module.startTimeLimit(&state);
298 defer state_module.stopTimeLimit(&state);
299
300 const compile_start = bench_util.nowNs();
301 const worlds_result = evaluator.tracedCompileInner(expr, runtime.Env.empty, Bdd.TRUE, &state, 0) catch |err| switch (err) {
302 error.PluckError => {
303 const compile_ns: u64 = bench_util.elapsedNs(compile_start);
304 return FactorBenchMetrics{
305 .vars = manager.var_order.items.len,
306 .nodes = manager.nodes.items.len,
307 .weight_dd_nodes = state.weight_dd.nodeCount(state.weight_dd_root),
308 .guard_peak = state.stats.max_factor_guard_branches,
309 .compile_ns = compile_ns,
310 .wmc_ns = 0,
311 .total_ns = compile_ns,
312 .limit_reason = state.stats.limit_reason,
313 .program_error = true,
314 };
315 },
316 else => return err,
317 };
318
319 var worlds = worlds_result.worlds;
320
321 if (cfg.full_dist) {
322 const new_worlds = try evaluator.inferFullDistribution(run_alloc, worlds, &state);
323 evaluator.freeWorldsSlice(run_alloc, worlds);
324 worlds = new_worlds;
325 }
326
327 if (try evaluator.processIntDistWorlds(run_alloc, worlds, &manager)) |int_worlds| {
328 evaluator.freeWorldsSlice(run_alloc, worlds);
329 worlds = int_worlds;
330 }
331
332 const compile_ns: u64 = bench_util.elapsedNs(compile_start);
333
334 var wmc_ns: u64 = 0;
335 if (state.stats.limit_reason == null and !state.stats.program_error) {
336 const wmc_start = bench_util.nowNs();
337 const weighted_results = try evaluator.computeWmcSequential(
338 run_alloc,
339 worlds,
340 &state.wmc_params,
341 &state.weight_dd,
342 state.weight_dd_root,
343 );
344 wmc_ns = bench_util.elapsedNs(wmc_start);
345 run_alloc.free(weighted_results);
346 }
347
348 const metrics = FactorBenchMetrics{
349 .vars = manager.var_order.items.len,
350 .nodes = manager.nodes.items.len,
351 .weight_dd_nodes = state.weight_dd.nodeCount(state.weight_dd_root),
352 .guard_peak = state.stats.max_factor_guard_branches,
353 .compile_ns = compile_ns,
354 .wmc_ns = wmc_ns,
355 .total_ns = compile_ns + wmc_ns,
356 .limit_reason = state.stats.limit_reason,
357 .program_error = state.stats.program_error,
358 };
359
360 evaluator.freeWorldsSlice(run_alloc, worlds);
361 return metrics;
362 }
363
364 fn runLpsmc(
365 allocator: Allocator,
366 defs: []const []const u8,
367 inner_query_source: []const u8,
368 k: usize,
369 ) !LpsmcMetrics {
370 var ctx = try toplevel.ToplevelContext.init(allocator);
371 defer ctx.deinit();
372 ctx.config.lpsmc_rng_seed = 4242;
373
374 try loadDefs(&ctx, defs);
375
376 var expr_arena = std.heap.ArenaAllocator.init(allocator);
377 defer expr_arena.deinit();
378 const expr = try buildInternalLpsmcExpr(expr_arena.allocator(), &ctx, inner_query_source, k);
379
380 var query_result = try ctx.runQueryExpr(expr);
381 defer query_result.deinit();
382
383 return LpsmcMetrics{
384 .outcomes = query_result.outcomes.len,
385 .vars = query_result.stats.variable_count,
386 .nodes = query_result.stats.node_count,
387 .lpsmc_ns = query_result.stats.time_ns,
388 .limit_reason = query_result.stats.limit_reason,
389 .program_error = query_result.program_error,
390 };
391 }
392
393 fn runLpsmcAccuracyParsed(
394 allocator: Allocator,
395 base_ctx: *const toplevel.ToplevelContext,
396 inner_query: *pexpr.PExpr,
397 k: usize,
398 exact_prob: f64,
399 adaptive: bool,
400 adaptive_max: usize,
401 ) !LpsmcAccuracyMetrics {
402 var ctx = try base_ctx.initWorker(allocator);
403 defer ctx.deinit();
404 ctx.config.lpsmc_rng_seed = 4242;
405 ctx.config.lpsmc_adaptive_k = adaptive;
406 ctx.config.lpsmc_adaptive_k_max = adaptive_max;
407 try ctx.enableIncrementalLPSMC();
408
409 var expr_arena = std.heap.ArenaAllocator.init(allocator);
410 defer expr_arena.deinit();
411 const expr = try buildInternalLpsmcExprParsed(expr_arena.allocator(), inner_query, k);
412
413 var query_result = try ctx.runQueryExpr(expr);
414 defer query_result.deinit();
415
416 var prob_true: f64 = 0.0;
417 for (query_result.outcomes) |outcome| {
418 if (std.mem.eql(u8, outcome.value_str, "True")) {
419 prob_true = outcome.probability;
420 break;
421 }
422 }
423
424 var run_stats = evaluator.LpsmcRunStats{};
425 if (ctx.getLpsmcRunStats()) |stats| {
426 run_stats = stats;
427 }
428
429 return LpsmcAccuracyMetrics{
430 .prob_true = prob_true,
431 .abs_error = @abs(prob_true - exact_prob),
432 .total_k = run_stats.total_k,
433 .avg_k = run_stats.avg_k,
434 .min_k = run_stats.min_k,
435 .max_k = run_stats.max_k,
436 .lpsmc_ns = query_result.stats.time_ns,
437 .limit_reason = query_result.limit_reason,
438 .program_error = query_result.program_error,
439 };
440 }
441
442 fn expectLpsmcAccuracy(metrics: LpsmcAccuracyMetrics, exact_prob: f64) !void {
443 try std.testing.expect(!metrics.program_error);
444 try std.testing.expect(metrics.limit_reason == null);
445 try std.testing.expect(metrics.total_k > 0);
446 try std.testing.expectApproxEqAbs(exact_prob, metrics.prob_true, 1e-12);
447 }
448
449 fn buildInternalLpsmcExpr(
450 allocator: Allocator,
451 ctx: *toplevel.ToplevelContext,
452 inner_query_source: []const u8,
453 k: usize,
454 ) !*pexpr.PExpr {
455 const inner_query = try pexpr.parseExpr(allocator, inner_query_source, &ctx.types, &ctx.definitions);
456 return buildInternalLpsmcExprParsed(allocator, inner_query, k);
457 }
458
459 fn buildInternalLpsmcExprParsed(
460 allocator: Allocator,
461 inner_query: *pexpr.PExpr,
462 k: usize,
463 ) !*pexpr.PExpr {
464 const k_expr = try toplevel.query.makeConstIntExpr(allocator, @intCast(k));
465 return toplevel.query.makeConstructExpr(
466 allocator,
467 "SubproblemMonteCarlo",
468 &[_]*pexpr.PExpr{ k_expr, inner_query },
469 );
470 }
471
472 test "BENCHMARK: factor nondeterministic weights (explicit branching)" {
473 const benchmark_latency = bench_util.benchmarkScope("factor nondeterministic weights (explicit branching)");
474 defer benchmark_latency.end();
475 const allocator = bench_util.allocator();
476 const bench = bench_util.BenchConfig.init();
477
478 bench_util.stdout("\n=== Benchmark: factor nondeterministic weights (explicit branching) ===\n", .{});
479 bench_util.stdout("benchmark,case,depth,worlds,vars,nodes,compile_ns,wmc_ns,total_ns,limit,program_error\n", .{});
480
481 const chain_def = "(define (chain n) (case n of O => True | S m => (weight_step (chain m))))";
482
483 const cases = [_]struct {
484 name: []const u8,
485 shared_gate: bool,
486 }{
487 .{ .name = "shared_gate", .shared_gate = true },
488 .{ .name = "independent_gate", .shared_gate = false },
489 };
490
491 const depths = [_]usize{ 2, 4 };
492 const case_len = bench.limit(cases.len, 1);
493 const depth_len = bench.limit(depths.len, 1);
494
495 for (cases[0..case_len]) |case| {
496 const cond_expr = if (case.shared_gate) "gate" else "(flip 0.5)";
497 const weight_step_def = try std.fmt.allocPrint(
498 allocator,
499 "(define (weight_step x) (if {s} (case (factor 0.2) of Unit => x) (case (factor 0.8) of Unit => x)))",
500 .{cond_expr},
501 );
502 defer allocator.free(weight_step_def);
503
504 if (case.shared_gate) {
505 const gate_def = "(define gate (flip 0.5))";
506 const defs = [_][]const u8{ gate_def, weight_step_def, chain_def };
507
508 for (depths[0..depth_len]) |depth| {
509 const expr = try std.fmt.allocPrint(allocator, "(chain {d})", .{depth});
510 defer allocator.free(expr);
511 const metrics = try runExact(allocator, &defs, expr);
512 bench_util.stdout("factor_branch,{s},{d},{d},{d},{d},{d},{d},{d},{s},{d}\n", .{
513 case.name,
514 depth,
515 metrics.worlds,
516 metrics.vars,
517 metrics.nodes,
518 metrics.compile_ns,
519 metrics.wmc_ns,
520 metrics.total_ns,
521 limitTag(metrics.limit_reason),
522 @intFromBool(metrics.program_error),
523 });
524 }
525 } else {
526 const defs = [_][]const u8{ weight_step_def, chain_def };
527
528 for (depths[0..depth_len]) |depth| {
529 const expr = try std.fmt.allocPrint(allocator, "(chain {d})", .{depth});
530 defer allocator.free(expr);
531 const metrics = try runExact(allocator, &defs, expr);
532 bench_util.stdout("factor_branch,{s},{d},{d},{d},{d},{d},{d},{d},{s},{d}\n", .{
533 case.name,
534 depth,
535 metrics.worlds,
536 metrics.vars,
537 metrics.nodes,
538 metrics.compile_ns,
539 metrics.wmc_ns,
540 metrics.total_ns,
541 limitTag(metrics.limit_reason),
542 @intFromBool(metrics.program_error),
543 });
544 }
545 }
546 }
547 }
548
549 test "BENCHMARK: factor WeightDD vs guard-list (boolean chain)" {
550 const benchmark_latency = bench_util.benchmarkScope("factor WeightDD vs guard-list (boolean chain)");
551 defer benchmark_latency.end();
552 const allocator = bench_util.allocator();
553 const bench = bench_util.BenchConfig.init();
554
555 bench_util.stdout("\n=== Benchmark: factor WeightDD vs guard-list (boolean chain) ===\n", .{});
556 bench_util.stdout("benchmark,mode,bits,vars,nodes,weightdd_nodes,guard_peak,compile_ns,wmc_ns,total_ns,limit,program_error\n", .{});
557
558 const modes = [_]struct {
559 name: []const u8,
560 cfg: LazyKCConfig,
561 }{
562 .{ .name = "guard_list", .cfg = .{ .full_dist = true, .factor_max_branches = 0 } },
563 .{ .name = "weightdd", .cfg = .{ .full_dist = true, .factor_max_branches = 1 } },
564 };
565
566 const bit_sizes = [_]usize{ 3, 4, 5, 6 };
567 const bit_len = bench.limit(bit_sizes.len, 1);
568
569 const SummaryRow = struct {
570 bits: usize,
571 mode: []const u8,
572 metrics: FactorBenchMetrics,
573 };
574
575 var summary: std.ArrayList(SummaryRow) = .empty;
576 defer summary.deinit(allocator);
577
578 var ctx = try toplevel.ToplevelContext.init(allocator);
579 defer ctx.deinit();
580
581 for (bit_sizes[0..bit_len]) |bits| {
582 const weight_expr = try buildBooleanWeightExpr(allocator, bits);
583 defer allocator.free(weight_expr);
584 const expr = try std.fmt.allocPrint(allocator, "(case (factor {s}) of Unit => True)", .{weight_expr});
585 defer allocator.free(expr);
586
587 var expr_arena = std.heap.ArenaAllocator.init(allocator);
588 defer expr_arena.deinit();
589 const parsed_expr = try pexpr.parseExpr(expr_arena.allocator(), expr, &ctx.types, &ctx.definitions);
590
591 for (modes) |mode| {
592 const metrics = try runExactFactorBenchParsed(allocator, &ctx.definitions, parsed_expr, mode.cfg);
593 bench_util.stdout("factor_weightdd_bool,{s},{d},{d},{d},{d},{d},{d},{d},{d},{s},{d}\n", .{
594 mode.name,
595 bits,
596 metrics.vars,
597 metrics.nodes,
598 metrics.weight_dd_nodes,
599 metrics.guard_peak,
600 metrics.compile_ns,
601 metrics.wmc_ns,
602 metrics.total_ns,
603 limitTag(metrics.limit_reason),
604 @intFromBool(metrics.program_error),
605 });
606 try summary.append(allocator, .{ .bits = bits, .mode = mode.name, .metrics = metrics });
607 }
608 }
609
610 bench_util.stdout("\nsummary_bool_chain,bits,mode,compile_ms,bdd_nodes,weightdd_nodes,guard_peak\n", .{});
611 for (summary.items) |row| {
612 bench_util.stdout("summary_bool_chain,{d},{s},{d:.3},{d},{d},{d}\n", .{
613 row.bits,
614 row.mode,
615 nsToMs(row.metrics.compile_ns),
616 row.metrics.nodes,
617 row.metrics.weight_dd_nodes,
618 row.metrics.guard_peak,
619 });
620 }
621 }
622
623 test "BENCHMARK: factor WeightDD vs guard-list (int_dist_eq)" {
624 const benchmark_latency = bench_util.benchmarkScope("factor WeightDD vs guard-list (int_dist_eq)");
625 defer benchmark_latency.end();
626 const allocator = bench_util.allocator();
627 const bench = bench_util.BenchConfig.init();
628
629 bench_util.stdout("\n=== Benchmark: factor WeightDD vs guard-list (int_dist_eq) ===\n", .{});
630 bench_util.stdout("benchmark,mode,bitwidth,vars,nodes,weightdd_nodes,guard_peak,compile_ns,wmc_ns,total_ns,limit,program_error\n", .{});
631
632 const modes = [_]struct {
633 name: []const u8,
634 cfg: LazyKCConfig,
635 }{
636 .{ .name = "guard_list", .cfg = .{ .full_dist = true, .factor_max_branches = 0 } },
637 .{ .name = "weightdd", .cfg = .{ .full_dist = true, .factor_max_branches = 1 } },
638 };
639
640 const bitwidths = [_]usize{ 2, 3, 4, 5 };
641 const bit_len = bench.limit(bitwidths.len, 1);
642
643 const SummaryRow = struct {
644 bitwidth: usize,
645 mode: []const u8,
646 metrics: FactorBenchMetrics,
647 };
648
649 var summary: std.ArrayList(SummaryRow) = .empty;
650 defer summary.deinit(allocator);
651
652 var ctx = try toplevel.ToplevelContext.init(allocator);
653 defer ctx.deinit();
654
655 for (bitwidths[0..bit_len]) |bitwidth| {
656 const weight_expr = try buildIntDistEqWeightExpr(allocator, bitwidth);
657 defer allocator.free(weight_expr);
658 const expr = try std.fmt.allocPrint(allocator, "(case (factor {s}) of Unit => True)", .{weight_expr});
659 defer allocator.free(expr);
660
661 var expr_arena = std.heap.ArenaAllocator.init(allocator);
662 defer expr_arena.deinit();
663 const parsed_expr = try pexpr.parseExpr(expr_arena.allocator(), expr, &ctx.types, &ctx.definitions);
664
665 for (modes) |mode| {
666 const metrics = try runExactFactorBenchParsed(allocator, &ctx.definitions, parsed_expr, mode.cfg);
667 bench_util.stdout("factor_weightdd_intdist,{s},{d},{d},{d},{d},{d},{d},{d},{d},{s},{d}\n", .{
668 mode.name,
669 bitwidth,
670 metrics.vars,
671 metrics.nodes,
672 metrics.weight_dd_nodes,
673 metrics.guard_peak,
674 metrics.compile_ns,
675 metrics.wmc_ns,
676 metrics.total_ns,
677 limitTag(metrics.limit_reason),
678 @intFromBool(metrics.program_error),
679 });
680 try summary.append(allocator, .{ .bitwidth = bitwidth, .mode = mode.name, .metrics = metrics });
681 }
682 }
683
684 bench_util.stdout("\nsummary_int_dist,bits,mode,compile_ms,bdd_nodes,weightdd_nodes,guard_peak\n", .{});
685 for (summary.items) |row| {
686 bench_util.stdout("summary_int_dist,{d},{s},{d:.3},{d},{d},{d}\n", .{
687 row.bitwidth,
688 row.mode,
689 nsToMs(row.metrics.compile_ns),
690 row.metrics.nodes,
691 row.metrics.weight_dd_nodes,
692 row.metrics.guard_peak,
693 });
694 }
695 }
696
697 test "BENCHMARK: WeightDD refinement budget" {
698 const benchmark_latency = bench_util.benchmarkScope("WeightDD refinement budget");
699 defer benchmark_latency.end();
700 const allocator = bench_util.allocator();
701 const bench = bench_util.BenchConfig.init();
702
703 bench_util.stdout("\n=== Benchmark: WeightDD refinement budget ===\n", .{});
704 bench_util.stdout("benchmark,vars,guards,eager_ns,refine_ns,unknown\n", .{});
705
706 const var_counts = [_]usize{ 4, 6 };
707 const var_len = bench.limit(var_counts.len, 1);
708
709 for (var_counts[0..var_len]) |var_count| {
710 var manager = try Manager.init(allocator);
711 defer manager.deinit();
712
713 const vars = try allocator.alloc(Bdd, var_count);
714 defer allocator.free(vars);
715 for (vars, 0..) |*slot, i| {
716 _ = i;
717 slot.* = try manager.newVar(true);
718 }
719
720 const guard_count = @as(usize, 1) << @intCast(var_count);
721 var guards = try allocator.alloc(GuardedWeight, guard_count);
722 defer allocator.free(guards);
723
724 for (0..guard_count) |mask| {
725 var guard = Bdd.TRUE;
726 for (vars, 0..) |var_bdd, bit| {
727 const lit = if (((mask >> @intCast(bit)) & 1) == 1)
728 var_bdd
729 else
730 manager.bddNot(var_bdd);
731 guard = try manager.bddAnd(guard, lit);
732 }
733 const weight = 0.5 + @as(f64, @floatFromInt(mask)) * 0.001;
734 guards[mask] = .{ .guard = guard, .weight = weight };
735 }
736
737 var dd_eager = try WeightDD.init(allocator, &manager);
738 defer dd_eager.deinit();
739
740 const eager_start = bench_util.nowNs();
741 const eager_root = try dd_eager.buildFromGuardList(guards);
742 _ = eager_root;
743 const eager_ns: u64 = bench_util.elapsedNs(eager_start);
744
745 var dd_refine = try WeightDD.init(allocator, &manager);
746 defer dd_refine.deinit();
747
748 const budget: usize = @max(@as(usize, 1), var_count);
749 const refine_start = bench_util.nowNs();
750 const refine_root = try dd_refine.refineWeight(guards, budget);
751 const refine_ns: u64 = bench_util.elapsedNs(refine_start);
752 const unknown_flag = @intFromBool(dd_refine.isUnknown(refine_root));
753
754 bench_util.stdout("weightdd_refine,{d},{d},{d},{d},{d}\n", .{
755 var_count,
756 guard_count,
757 eager_ns,
758 refine_ns,
759 unknown_flag,
760 });
761 }
762 }
763
764 test "BENCHMARK: LPSMC factor chain" {
765 const benchmark_latency = bench_util.benchmarkScope("LPSMC factor chain");
766 defer benchmark_latency.end();
767 const allocator = bench_util.allocator();
768 const bench = bench_util.BenchConfig.init();
769
770 bench_util.stdout("\n=== Benchmark: LPSMC factor chain ===\n", .{});
771 bench_util.stdout("benchmark,case,depth,outcomes,vars,nodes,lpsmc_ns,limit,program_error\n", .{});
772
773 const weight_step_def =
774 "(define (weight_step x) (if (flip 0.5) (case (factor 0.2) of Unit => (Suspend x)) (case (factor 0.8) of Unit => (Suspend x))))";
775 const chain_def =
776 "(define (chain n) (case n of O => (FinallyTrue) | S m => (weight_step (chain m))))";
777 const defs = [_][]const u8{ weight_step_def, chain_def };
778
779 const depths = [_]usize{ 4, 6 };
780 const depth_len = bench.limit(depths.len, 1);
781 const samples = bench.value(10, 3);
782
783 for (depths[0..depth_len]) |depth| {
784 const query = try std.fmt.allocPrint(allocator, "(Marginal (chain {d}))", .{depth});
785 defer allocator.free(query);
786
787 const metrics = try runLpsmc(allocator, &defs, query, samples);
788 bench_util.stdout("lpsmc_factor_chain,independent_gate,{d},{d},{d},{d},{d},{s},{d}\n", .{
789 depth,
790 metrics.outcomes,
791 metrics.vars,
792 metrics.nodes,
793 metrics.lpsmc_ns,
794 limitTag(metrics.limit_reason),
795 @intFromBool(metrics.program_error),
796 });
797 }
798 }
799
800 test "BENCHMARK: LPSMC adaptive k accuracy" {
801 const benchmark_latency = bench_util.benchmarkScope("LPSMC adaptive k accuracy");
802 defer benchmark_latency.end();
803 const allocator = bench_util.allocator();
804 const bench = bench_util.BenchConfig.init();
805
806 bench_util.stdout("\n=== Benchmark: LPSMC adaptive k accuracy ===\n", .{});
807 bench_util.stdout("benchmark,case,len,mode,k_base,k_max,prob_true,abs_error,total_k,avg_k,min_k,max_k,lpsmc_ns,limit,program_error\n", .{});
808
809 const coin_chain_def =
810 "(define (coin_chain n) (case n of O => (if (flip 0.5) FinallyTrue FinallyFalse) | S m => (if (flip 0.5) (Suspend (coin_chain m)) (Suspend (coin_chain m)))))";
811 const defs = [_][]const u8{coin_chain_def};
812
813 const lengths = [_]usize{ 3, 4 };
814 const len_count = bench.limit(lengths.len, 1);
815 const base_k = bench.value(6, 1);
816 const adaptive_max = base_k * 8;
817
818 var parse_ctx = try toplevel.ToplevelContext.init(allocator);
819 defer parse_ctx.deinit();
820 try loadDefs(&parse_ctx, &defs);
821
822 for (lengths[0..len_count]) |len| {
823 const exact_prob: f64 = 0.5;
824
825 const query = try std.fmt.allocPrint(allocator, "(Marginal (coin_chain {d}))", .{len});
826 defer allocator.free(query);
827
828 var expr_arena = std.heap.ArenaAllocator.init(allocator);
829 defer expr_arena.deinit();
830 const inner_query = try pexpr.parseExpr(expr_arena.allocator(), query, &parse_ctx.types, &parse_ctx.definitions);
831
832 const fixed_metrics = try runLpsmcAccuracyParsed(allocator, &parse_ctx, inner_query, base_k, exact_prob, false, adaptive_max);
833 try expectLpsmcAccuracy(fixed_metrics, exact_prob);
834 bench_util.stdout("lpsmc_adaptive_k,suspended_coin,{d},fixed,{d},{d},{e},{e},{d},{d:.2},{d},{d},{d},{s},{d}\n", .{
835 len,
836 base_k,
837 adaptive_max,
838 fixed_metrics.prob_true,
839 fixed_metrics.abs_error,
840 fixed_metrics.total_k,
841 fixed_metrics.avg_k,
842 fixed_metrics.min_k,
843 fixed_metrics.max_k,
844 fixed_metrics.lpsmc_ns,
845 limitTag(fixed_metrics.limit_reason),
846 @intFromBool(fixed_metrics.program_error),
847 });
848
849 const adaptive_metrics = try runLpsmcAccuracyParsed(allocator, &parse_ctx, inner_query, base_k, exact_prob, true, adaptive_max);
850 try expectLpsmcAccuracy(adaptive_metrics, exact_prob);
851 bench_util.stdout("lpsmc_adaptive_k,suspended_coin,{d},adaptive,{d},{d},{e},{e},{d},{d:.2},{d},{d},{d},{s},{d}\n", .{
852 len,
853 base_k,
854 adaptive_max,
855 adaptive_metrics.prob_true,
856 adaptive_metrics.abs_error,
857 adaptive_metrics.total_k,
858 adaptive_metrics.avg_k,
859 adaptive_metrics.min_k,
860 adaptive_metrics.max_k,
861 adaptive_metrics.lpsmc_ns,
862 limitTag(adaptive_metrics.limit_reason),
863 @intFromBool(adaptive_metrics.program_error),
864 });
865 }
866 }