lib/pluck/src/toplevel/result.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const pluck = @import("../root.zig");
3 const Allocator = std.mem.Allocator;
4
5 const evaluator = pluck.evaluator;
6 const LazyKCStats = evaluator.LazyKCStats;
7 const LimitReason = evaluator.LimitReason;
8
9 const top_types = @import("types.zig");
10 const QueryOutcome = top_types.QueryOutcome;
11 const SourceLocation = top_types.SourceLocation;
12
13 const QueryOutcomeProbabilityOrder = struct {
14 fn lessThan(_: void, a: QueryOutcome, b: QueryOutcome) bool {
15 return a.probability > b.probability;
16 }
17 };
18
19 pub const QueryResult = struct {
20 outcomes: []QueryOutcome,
21 stats: LazyKCStats,
22 limit_reason: ?LimitReason,
23 program_error: bool,
24 allocator: Allocator,
25 source_location: ?SourceLocation = null,
26
27 pub fn deinit(self: *QueryResult) void {
28 for (self.outcomes) |outcome| {
29 self.allocator.free(outcome.value_str);
30 }
31 self.allocator.free(self.outcomes);
32 }
33
34 pub fn clone(self: *const QueryResult, allocator: Allocator) !QueryResult {
35 const new_outcomes = try allocator.alloc(QueryOutcome, self.outcomes.len);
36 var allocated_count: usize = 0;
37 errdefer {
38 for (new_outcomes[0..allocated_count]) |outcome| {
39 allocator.free(outcome.value_str);
40 }
41 allocator.free(new_outcomes);
42 }
43
44 for (self.outcomes, 0..) |outcome, i| {
45 new_outcomes[i] = .{
46 .value_str = try allocator.dupe(u8, outcome.value_str),
47 .probability = outcome.probability,
48 };
49 allocated_count += 1;
50 }
51
52 return .{
53 .outcomes = new_outcomes,
54 .stats = self.stats,
55 .limit_reason = self.limit_reason,
56 .program_error = self.program_error,
57 .allocator = allocator,
58 .source_location = self.source_location,
59 };
60 }
61
62 fn formatProbability(writer: anytype, value_str: []const u8, prob: f64) !void {
63 if (prob >= 1e-4 or prob == 0.0) {
64 try writer.print("{s}: {d:.6}\n", .{ value_str, prob });
65 } else {
66 try writer.print("{s}: {e}\n", .{ value_str, prob });
67 }
68 }
69
70 pub fn print(self: *const QueryResult, writer: anytype) !void {
71 if (self.limit_reason) |reason| {
72 try writer.print("Query hit limit: {s}\n", .{reason.message()});
73 }
74 if (self.program_error) {
75 try writer.writeAll("Query encountered program error\n");
76 return;
77 }
78
79 if (self.outcomes.len == 0) {
80 try writer.writeAll("No outcomes (probability 0)\n");
81 return;
82 }
83
84 const sorted = self.allocator.alloc(QueryOutcome, self.outcomes.len) catch {
85 for (self.outcomes) |outcome| {
86 try formatProbability(writer, outcome.value_str, outcome.probability);
87 }
88 return;
89 };
90 defer self.allocator.free(sorted);
91 @memcpy(sorted, self.outcomes);
92
93 std.mem.sort(QueryOutcome, sorted, {}, QueryOutcomeProbabilityOrder.lessThan);
94
95 for (sorted) |outcome| {
96 if (outcome.probability > 0) {
97 try formatProbability(writer, outcome.value_str, outcome.probability);
98 }
99 }
100
101 const time_ms = @as(f64, @floatFromInt(self.stats.time_ns)) / 1_000_000.0;
102 try writer.print("\nTime: {d:.3}ms\n", .{time_ms});
103 if (self.stats.wmc_time_ns > 0) {
104 const wmc_ms = @as(f64, @floatFromInt(self.stats.wmc_time_ns)) / 1_000_000.0;
105 try writer.print("WMC time: {d:.3}ms\n", .{wmc_ms});
106 }
107 if (self.stats.refinement_time_ns > 0) {
108 const refine_ms = @as(f64, @floatFromInt(self.stats.refinement_time_ns)) / 1_000_000.0;
109 try writer.print("Refinement time: {d:.3}ms ({d} refinements)\n", .{
110 refine_ms,
111 self.stats.refinement_count,
112 });
113 }
114
115 if (self.stats.num_recursive_calls > 0) {
116 try writer.print("ITE calls: {d}\n", .{self.stats.num_recursive_calls});
117 }
118 if (self.stats.num_forward_calls > 0) {
119 try writer.print("Forward calls: {d}\n", .{self.stats.num_forward_calls});
120 }
121
122 if (self.stats.variable_count > 0) {
123 try writer.print("BDD variables: {d}\n", .{self.stats.variable_count});
124 }
125 if (self.stats.node_count > 0) {
126 try writer.print("BDD nodes: {d}\n", .{self.stats.node_count});
127 }
128
129 if (self.stats.unique_table_grows > 0) {
130 try writer.print("BDD unique table grows: {d}\n", .{self.stats.unique_table_grows});
131 }
132 if (self.stats.ite_cache_grows > 0) {
133 try writer.print("ITE cache grows: {d}\n", .{self.stats.ite_cache_grows});
134 }
135
136 const total_cache = self.stats.ite_cache_hits + self.stats.ite_cache_misses;
137 if (total_cache > 0) {
138 const hit_ratio = @as(f64, @floatFromInt(self.stats.ite_cache_hits)) / @as(f64, @floatFromInt(total_cache)) * 100.0;
139 try writer.print("ITE cache: {d} hits, {d} misses ({d:.1}% hit rate)\n", .{
140 self.stats.ite_cache_hits,
141 self.stats.ite_cache_misses,
142 hit_ratio,
143 });
144 }
145
146 const total_thunks = self.stats.thunk_reuse_hits + self.stats.thunk_reuse_misses;
147 if (total_thunks > 0) {
148 const reuse_ratio = @as(f64, @floatFromInt(self.stats.thunk_reuse_hits)) / @as(f64, @floatFromInt(total_thunks)) * 100.0;
149 try writer.print("Thunk creation: {d} reused, {d} new ({d:.1}% reuse)\n", .{
150 self.stats.thunk_reuse_hits,
151 self.stats.thunk_reuse_misses,
152 reuse_ratio,
153 });
154 }
155
156 if (self.stats.thunk_evaluations > 0) {
157 const cache_ratio = @as(f64, @floatFromInt(self.stats.thunk_cache_hits)) / @as(f64, @floatFromInt(self.stats.thunk_evaluations)) * 100.0;
158 try writer.print("Thunk eval: {d} total, {d} cache hits ({d:.1}% hit rate)\n", .{
159 self.stats.thunk_evaluations,
160 self.stats.thunk_cache_hits,
161 cache_ratio,
162 });
163 }
164 }
165 };