lib/pluck/src/toplevel/config.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const pluck = @import("../root.zig");
3 const evaluator = pluck.evaluator;
4 const LazyKCConfig = evaluator.LazyKCConfig;
5 const LimitReason = evaluator.LimitReason;
6
7 const def_order = pluck.definition_order;
8 const DefinitionOrderMode = def_order.DefinitionOrderMode;
9 const limits = pluck.limits;
10
11 pub const ConfigError = error{
12 InvalidTimeLimit,
13 InvalidFallbackK,
14 InvalidAdaptiveKMax,
15 InvalidWorkerCount,
16 };
17
18 pub const ToplevelConfig = struct {
19 max_depth: ?u32 = null,
20 ite_limit: ?u64 = limits.default_agent_ite_limit,
21 time_limit: ?f64 = null,
22 sample_after_max_depth: bool = false,
23 use_strict_order: bool = true,
24 use_reverse_order: bool = false,
25 var_order_fallback: bool = false,
26 definition_order_mode: DefinitionOrderMode = .none,
27 parallel_wmc: bool = false,
28 verbose: bool = false,
29 rng_seed: ?u64 = null,
30 lpsmc_rng_seed: ?u64 = null,
31 lpsmc_adaptive_k: bool = false,
32 lpsmc_adaptive_k_max: usize = 64,
33 lpsmc_workers: usize = 1,
34
35 factor_max_branches: usize = 64,
36
37 weight_dd_max_nodes: usize = 0,
38
39 fallback_mode: evaluator.FallbackMode = .@"error",
40
41 fallback_lpsmc_k: usize = 10,
42 };
43
44 pub fn OptionalField(comptime T: type) type {
45 return union(enum) {
46 keep,
47 set: T,
48 clear,
49 };
50 }
51
52 pub const VarOrderSetting = enum {
53 strict,
54 reverse,
55 creation,
56 topo,
57 min_fill,
58 auto,
59 };
60
61 pub const ToplevelConfigPatch = struct {
62 max_depth: OptionalField(u32) = .keep,
63 ite_limit: OptionalField(u64) = .keep,
64 time_limit: OptionalField(f64) = .keep,
65 sample_after_max_depth: ?bool = null,
66 var_order: ?VarOrderSetting = null,
67 parallel_wmc: ?bool = null,
68 verbose: ?bool = null,
69 rng_seed: OptionalField(u64) = .keep,
70 lpsmc_rng_seed: OptionalField(u64) = .keep,
71 lpsmc_adaptive_k: ?bool = null,
72 lpsmc_adaptive_k_max: ?usize = null,
73 lpsmc_workers: ?usize = null,
74 factor_max_branches: ?usize = null,
75 weight_dd_max_nodes: ?usize = null,
76 fallback_mode: ?evaluator.FallbackMode = null,
77 fallback_lpsmc_k: ?usize = null,
78 };
79
80 pub fn patched(base: ToplevelConfig, patch: ToplevelConfigPatch) ConfigError!ToplevelConfig {
81 var next = base;
82 try applyPatchInPlace(&next, patch);
83 return next;
84 }
85
86 pub fn applyPatch(config: *ToplevelConfig, patch: ToplevelConfigPatch) ConfigError!void {
87 config.* = try patched(config.*, patch);
88 }
89
90 fn applyPatchInPlace(config: *ToplevelConfig, patch: ToplevelConfigPatch) ConfigError!void {
91 applyOptional(u32, &config.max_depth, patch.max_depth);
92 applyOptional(u64, &config.ite_limit, patch.ite_limit);
93 switch (patch.time_limit) {
94 .keep => {},
95 .clear => config.time_limit = null,
96 .set => |seconds| {
97 if (!std.math.isFinite(seconds) or seconds < 0) return ConfigError.InvalidTimeLimit;
98 config.time_limit = seconds;
99 },
100 }
101 if (patch.sample_after_max_depth) |value| config.sample_after_max_depth = value;
102 if (patch.var_order) |setting| applyVarOrderSetting(config, setting);
103 if (patch.parallel_wmc) |value| config.parallel_wmc = value;
104 if (patch.verbose) |value| config.verbose = value;
105 applyOptional(u64, &config.rng_seed, patch.rng_seed);
106 applyOptional(u64, &config.lpsmc_rng_seed, patch.lpsmc_rng_seed);
107 if (patch.lpsmc_adaptive_k) |value| config.lpsmc_adaptive_k = value;
108 if (patch.lpsmc_adaptive_k_max) |value| {
109 if (value == 0) return ConfigError.InvalidAdaptiveKMax;
110 config.lpsmc_adaptive_k_max = value;
111 }
112 if (patch.lpsmc_workers) |value| {
113 if (value == 0) return ConfigError.InvalidWorkerCount;
114 config.lpsmc_workers = value;
115 }
116 if (patch.factor_max_branches) |value| config.factor_max_branches = value;
117 if (patch.weight_dd_max_nodes) |value| config.weight_dd_max_nodes = value;
118 if (patch.fallback_mode) |value| config.fallback_mode = value;
119 if (patch.fallback_lpsmc_k) |value| {
120 if (value == 0) return ConfigError.InvalidFallbackK;
121 config.fallback_lpsmc_k = value;
122 }
123 }
124
125 fn applyOptional(comptime T: type, target: *?T, patch: OptionalField(T)) void {
126 switch (patch) {
127 .keep => {},
128 .clear => target.* = null,
129 .set => |value| target.* = value,
130 }
131 }
132
133 pub fn applyVarOrderSetting(config: *ToplevelConfig, setting: VarOrderSetting) void {
134 switch (setting) {
135 .strict => {
136 config.use_strict_order = true;
137 config.use_reverse_order = false;
138 config.var_order_fallback = false;
139 config.definition_order_mode = .none;
140 },
141 .reverse => {
142 config.use_strict_order = true;
143 config.use_reverse_order = true;
144 config.var_order_fallback = false;
145 config.definition_order_mode = .none;
146 },
147 .creation => {
148 config.use_strict_order = false;
149 config.use_reverse_order = false;
150 config.var_order_fallback = false;
151 config.definition_order_mode = .none;
152 },
153 .topo => {
154 config.use_strict_order = true;
155 config.use_reverse_order = false;
156 config.var_order_fallback = false;
157 config.definition_order_mode = .topological;
158 },
159 .min_fill => {
160 config.use_strict_order = true;
161 config.use_reverse_order = false;
162 config.var_order_fallback = false;
163 config.definition_order_mode = .min_fill;
164 },
165 .auto => {
166 config.use_strict_order = true;
167 config.use_reverse_order = false;
168 config.var_order_fallback = true;
169 config.definition_order_mode = .none;
170 },
171 }
172 }
173
174 pub const VarOrderMode = enum {
175 strict,
176 reverse,
177 creation,
178 };
179
180 pub const VarOrderCandidates = struct {
181 modes: [3]VarOrderMode,
182 len: u8,
183 };
184
185 pub fn varOrderModeFromConfig(config: ToplevelConfig) VarOrderMode {
186 if (!config.use_strict_order) return .creation;
187 return if (config.use_reverse_order) .reverse else .strict;
188 }
189
190 pub fn applyVarOrder(cfg: *LazyKCConfig, mode: VarOrderMode) void {
191 switch (mode) {
192 .strict => {
193 cfg.use_strict_order = true;
194 cfg.use_reverse_order = false;
195 },
196 .reverse => {
197 cfg.use_strict_order = true;
198 cfg.use_reverse_order = true;
199 },
200 .creation => {
201 cfg.use_strict_order = false;
202 cfg.use_reverse_order = false;
203 },
204 }
205 }
206
207 pub fn buildVarOrderCandidates(current: VarOrderMode, enable_fallback: bool) VarOrderCandidates {
208 var candidates = VarOrderCandidates{
209 .modes = .{ current, .strict, .strict },
210 .len = 1,
211 };
212 if (!enable_fallback) return candidates;
213
214 switch (current) {
215 .strict => {
216 candidates.modes[1] = .reverse;
217 candidates.modes[2] = .creation;
218 },
219 .reverse => {
220 candidates.modes[1] = .strict;
221 candidates.modes[2] = .creation;
222 },
223 .creation => {
224 candidates.modes[1] = .strict;
225 candidates.modes[2] = .reverse;
226 },
227 }
228 candidates.len = 3;
229 return candidates;
230 }
231
232 pub fn buildAdaptiveKPolicy(config: ToplevelConfig, base_k: usize) evaluator.AdaptiveKPolicy {
233 var policy = evaluator.AdaptiveKPolicy{};
234 policy.enabled = config.lpsmc_adaptive_k;
235 if (policy.enabled) {
236 policy.min_k = @max(base_k, 1);
237 }
238 policy.max_k = @max(policy.min_k, config.lpsmc_adaptive_k_max);
239 return policy;
240 }
241
242 pub fn shouldFallbackVarOrder(reason: LimitReason) bool {
243 return reason == .time_limit or reason == .ite_limit;
244 }
245
246 test "toplevel config defaults to the agent BDD quota and can clear it" {
247 var cfg = ToplevelConfig{};
248 try std.testing.expectEqual(@as(?u64, limits.default_agent_ite_limit), cfg.ite_limit);
249
250 try applyPatch(&cfg, .{ .ite_limit = .clear });
251 try std.testing.expect(cfg.ite_limit == null);
252 }
253
254 test "config patch sets and clears embedding fields" {
255 var cfg = ToplevelConfig{};
256 try applyPatch(&cfg, .{
257 .max_depth = .{ .set = 12 },
258 .time_limit = .{ .set = 0.25 },
259 .rng_seed = .{ .set = 42 },
260 .var_order = .min_fill,
261 .fallback_mode = .lpsmc,
262 .fallback_lpsmc_k = 7,
263 });
264
265 try std.testing.expectEqual(@as(?u32, 12), cfg.max_depth);
266 try std.testing.expectEqual(@as(?f64, 0.25), cfg.time_limit);
267 try std.testing.expectEqual(@as(?u64, 42), cfg.rng_seed);
268 try std.testing.expect(cfg.use_strict_order);
269 try std.testing.expect(!cfg.use_reverse_order);
270 try std.testing.expect(!cfg.var_order_fallback);
271 try std.testing.expectEqual(DefinitionOrderMode.min_fill, cfg.definition_order_mode);
272 try std.testing.expectEqual(evaluator.FallbackMode.lpsmc, cfg.fallback_mode);
273 try std.testing.expectEqual(@as(usize, 7), cfg.fallback_lpsmc_k);
274
275 try applyPatch(&cfg, .{
276 .max_depth = .clear,
277 .time_limit = .clear,
278 .rng_seed = .clear,
279 .var_order = .creation,
280 });
281
282 try std.testing.expect(cfg.max_depth == null);
283 try std.testing.expect(cfg.time_limit == null);
284 try std.testing.expect(cfg.rng_seed == null);
285 try std.testing.expect(!cfg.use_strict_order);
286 try std.testing.expect(!cfg.use_reverse_order);
287 }
288
289 test "config patch validates bounded fields" {
290 var cfg = ToplevelConfig{};
291 cfg.max_depth = 9;
292 try std.testing.expectError(ConfigError.InvalidTimeLimit, applyPatch(&cfg, .{ .time_limit = .{ .set = -1 } }));
293 try std.testing.expectEqual(@as(?u32, 9), cfg.max_depth);
294 try std.testing.expectError(ConfigError.InvalidFallbackK, applyPatch(&cfg, .{ .fallback_lpsmc_k = 0 }));
295 try std.testing.expectError(ConfigError.InvalidAdaptiveKMax, applyPatch(&cfg, .{ .lpsmc_adaptive_k_max = 0 }));
296 try std.testing.expectError(ConfigError.InvalidWorkerCount, applyPatch(&cfg, .{ .lpsmc_workers = 0 }));
297 }