lib/pluck/src/state/stats.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 pub const LimitReason = enum {
 2     max_depth,
 3     time_limit,
 4     ite_limit,
 5     factor_weight_too_complex,
 6 
 7     pub fn message(self: LimitReason) []const u8 {
 8         return switch (self) {
 9             .max_depth => "max_depth limit exceeded (consider increasing --max-depth or using bounded distributions)",
10             .time_limit => "time limit exceeded",
11             .ite_limit => "BDD work quota exceeded (model may be too complex)",
12             .factor_weight_too_complex => "factor weight too complex for exact KC (retry with --fallback-mode=lpsmc)",
13         };
14     }
15 };
16 
17 pub const LazyKCStats = struct {
18     pub const MaxBddSamples: usize = 32;
19 
20     time_ns: u64 = 0,
21 
22     num_forward_calls: u64 = 0,
23 
24     limit_reason: ?LimitReason = null,
25 
26     program_error: bool = false,
27 
28     num_recursive_calls: u64 = 0,
29 
30     ite_cache_hits: u64 = 0,
31 
32     ite_cache_misses: u64 = 0,
33 
34     unique_table_grows: u64 = 0,
35 
36     ite_cache_grows: u64 = 0,
37 
38     thunk_reuse_hits: u64 = 0,
39 
40     thunk_reuse_misses: u64 = 0,
41 
42     thunk_evaluations: u64 = 0,
43 
44     thunk_cache_hits: u64 = 0,
45 
46     variable_count: u64 = 0,
47 
48     node_count: u64 = 0,
49 
50     wmc_time_ns: u64 = 0,
51 
52     refinement_time_ns: u64 = 0,
53 
54     refinement_count: u64 = 0,
55 
56     bdd_samples_forward_calls: [MaxBddSamples]u64 = @as([MaxBddSamples]u64, @splat(0)),
57 
58     bdd_samples_vars: [MaxBddSamples]u64 = @as([MaxBddSamples]u64, @splat(0)),
59 
60     bdd_samples_nodes: [MaxBddSamples]u64 = @as([MaxBddSamples]u64, @splat(0)),
61 
62     bdd_samples_len: u8 = 0,
63 
64     max_factor_guard_branches: usize = 0,
65 };