tiny.pluck.state

1pub const CallstackKey = struct {2    callstack: []const i32,3    prob: f64,4};

1pub fn checkLimits(state: *LazyKCState) bool {2    if (state.stats.limit_reason != null) return true;34    if (state.manager.iteLimitExceeded()) {5        state.stats.limit_reason = .ite_limit;6        return true;7    }89    if (state.cfg.max_depth) |max| {10        if (state.depth > max and !state.cfg.sample_after_max_depth) {11            state.stats.limit_reason = .max_depth;12            return true;13        }14    }1516    if (state.manager.limits.checkTimeLimit()) {17        state.stats.limit_reason = .time_limit;18        return true;19    }2021    if (state.manager.limits.checkIteLimit(state.manager.num_recursive_calls)) {22        state.stats.limit_reason = .ite_limit;23        return true;24    }2526    return false;27}

1pub fn clearSampledFlips(state: *LazyKCState) void {2    var sampled_iter = state.sampled_flips.iterator();3    while (sampled_iter.next()) |entry| {4        state.allocator.free(entry.key_ptr.callstack);5    }6    state.sampled_flips.clearRetainingCapacity();7}

1pub fn currentAddress(state: *LazyKCState, p: f64) !Bdd {2    return currentAddressForCallstack(state, state.callstack.items, p);3}

1pub fn currentAddressForCallstack(state: *LazyKCState, callstack_items: []const i32, p: f64) !Bdd {2    const key = StateCallstackKey{3        .callstack = callstack_items,4        .prob = p,5    };67    if (state.var_of_callstack.get(key)) |existing| {8        return existing;9    }1011    const addr = if (state.cfg.use_strict_order) blk: {12        const pos = findInsertPosition(state, key);13        const new_var = try state.manager.newVarAtPosition(@intCast(pos), true);14        if (state.manager.iteLimitExceeded()) break :blk Bdd.FALSE;1516        const callstack_copy = try state.allocator.dupe(i32, callstack_items);17        const new_key = StateCallstackKey{ .callstack = callstack_copy, .prob = p };18        try state.sorted_callstacks.insert(state.allocator, pos, new_key);1920        break :blk new_var;21    } else blk: {22        break :blk try state.manager.newVar(true);23    };2425    if (state.manager.iteLimitExceeded()) return Bdd.FALSE;2627    const callstack_copy = try state.allocator.dupe(i32, callstack_items);28    try state.var_of_callstack.put(29        state.allocator,30        StateCallstackKey{ .callstack = callstack_copy, .prob = p },31        addr,32    );3334    try state.wmc_params.setWeight(state.manager.topVar(addr), 1.0 - p, p);3536    return addr;37}

1pub fn deinit(state: *LazyKCState) void {2    state.callstack.deinit(state.allocator);3    var iter = state.var_of_callstack.iterator();4    while (iter.next()) |entry| {5        state.allocator.free(entry.key_ptr.callstack);6    }7    state.var_of_callstack.deinit(state.allocator);8    for (state.sorted_callstacks.items) |key| {9        state.allocator.free(key.callstack);10    }11    state.sorted_callstacks.deinit(state.allocator);12    clearSampledFlips(state);13    state.sampled_flips.deinit(state.allocator);14    state.stacktrace_buf.deinit(state.allocator);15    state.wmc_params.deinit();16    for (state.deferred_weights.items) |deferred| {17        state.allocator.free(deferred.guards);18    }19    state.deferred_weights.deinit(state.allocator);20    state.weight_dd.deinit();21    state.def_thunks.deinit(state.allocator);22}

1pub fn findInsertPosition(state: *const LazyKCState, key: StateCallstackKey) usize {2    const items = state.sorted_callstacks.items;34    var left: usize = 0;5    var right: usize = items.len;67    while (left < right) {8        const mid = left + (right - left) / 2;9        const cmp = callstack.compareCallstacks(items[mid].callstack, key.callstack);10        if (state.cfg.use_reverse_order) {11            if (cmp == .gt) {12                left = mid + 1;13            } else {14                right = mid;15            }16        } else {17            if (cmp == .lt) {18                left = mid + 1;19            } else {20                right = mid;21            }22        }23    }2425    return left;26}

1pub fn init(2    allocator: Allocator,3    manager: *Manager,4    definitions: *const Definitions,5    cfg: LazyKCConfig,6) LazyKCState {7    return initChecked(allocator, manager, definitions, cfg) catch8        @panic("LazyKCState.init: out of memory");9}

1pub fn initChecked(2    allocator: Allocator,3    manager: *Manager,4    definitions: *const Definitions,5    cfg: LazyKCConfig,6) !LazyKCState {7    const wmc_params = if (cfg.dual)8        WmcParams.initDual(allocator, cfg.vector_size)9    else10        WmcParams.init(allocator);1112    var weight_dd_state = WeightDD.init(allocator, manager) catch |err| switch (err) {13        error.OutOfMemory => return error.OutOfMemory,14        error.NaNWeight, error.NonFiniteWeight => unreachable,15    };16    const weight_one = weight_dd_state.leaf(1.0) catch |err| switch (err) {17        error.OutOfMemory => return error.OutOfMemory,18        error.NaNWeight, error.NonFiniteWeight => unreachable,19    };2021    const now = time.nanoTimestamp();22    return LazyKCState{23        .allocator = allocator,24        .manager = manager,25        .wmc_params = wmc_params,26        .weight_dd = weight_dd_state,27        .weight_dd_root = weight_one,28        .weight_dd_one = weight_one,29        .deferred_weights = .empty,30        .cfg = cfg,31        .stats = LazyKCStats{},32        .callstack = .empty,33        .var_of_callstack = .empty,34        .sorted_callstacks = .empty,35        .depth = 0,36        .definitions = definitions,37        .current_def_name = null,38        .stacktrace_buf = .empty,39        .query = null,40        .next_thunk_id = 0,41        .start_time = now,42        .registry = null,43        .sampled_flips = .{},44        .prng = std.Random.DefaultPrng.init(@intCast(@max(0, now))),45        .def_thunks = .{},46    };47}

1pub fn maybeSampleBdd(state: *LazyKCState) void {2    const calls = state.stats.num_forward_calls;3    if (calls == 0) return;4    if (!std.math.isPowerOfTwo(calls)) return;5    recordBddSample(state);6}

1pub fn popCallstack(state: *LazyKCState) void {2    _ = state.callstack.pop();3}

1pub fn pushCallstack(state: *LazyKCState, index: i32) !void {2    try state.callstack.append(state.allocator, index);3}

1pub fn recordBddSample(state: *LazyKCState) void {2    if (@as(usize, state.stats.bdd_samples_len) >= LazyKCStats.MaxBddSamples) return;3    const idx: usize = @intCast(state.stats.bdd_samples_len);4    state.stats.bdd_samples_forward_calls[idx] = state.stats.num_forward_calls;5    state.stats.bdd_samples_vars[idx] = @intCast(state.manager.var_order.items.len);6    state.stats.bdd_samples_nodes[idx] = @intCast(state.manager.nodes.items.len);7    state.stats.bdd_samples_len += 1;8}

1pub fn recordFinalBddSample(state: *LazyKCState) void {2    const calls = state.stats.num_forward_calls;3    if (calls == 0) return;4    if (state.stats.bdd_samples_len > 0) {5        const last_idx: usize = @intCast(state.stats.bdd_samples_len - 1);6        if (state.stats.bdd_samples_forward_calls[last_idx] == calls) return;7    }8    recordBddSample(state);9}

1pub fn recordManagerStats(state: *LazyKCState) void {2    if (state.stats.limit_reason == null and state.manager.iteLimitExceeded()) {3        state.stats.limit_reason = .ite_limit;4    }5    if (state.stats.limit_reason == null and state.manager.timeLimitExceeded()) {6        state.stats.limit_reason = .time_limit;7    }8    state.stats.num_recursive_calls = state.manager.num_recursive_calls;9    state.stats.ite_cache_hits = state.manager.ite_cache_hits;10    state.stats.ite_cache_misses = state.manager.ite_cache_misses;11    state.stats.unique_table_grows = state.manager.unique_table_grows;12    state.stats.ite_cache_grows = state.manager.ite_cache_grows;13    state.stats.variable_count = state.manager.var_order.items.len;14    state.stats.node_count = state.manager.nodes.items.len;15}

1pub fn startTimeLimit(state: *LazyKCState) void {2    state.start_time = time.nanoTimestamp();3    if (state.cfg.time_limit) |limit| {4        state.manager.limits.startTimeLimit(limit);5    }6    if (state.cfg.ite_limit) |limit| {7        state.manager.startIteLimit(limit);8    }9}

1pub fn stopTimeLimit(state: *LazyKCState) void {2    state.manager.limits.stopTimeLimit();3    state.manager.stopIteLimit();4    const elapsed = time.nanoTimestamp() - state.start_time;5    state.stats.time_ns = @intCast(@max(0, elapsed));6}

1pub const state = @import("state/root.zig");

1const config = @import("config.zig");2const stats = @import("stats.zig");3const callstack = @import("callstack.zig");4const machine = @import("machine.zig");56pub const LazyKCConfig = config.LazyKCConfig;7pub const FallbackMode = config.FallbackMode;8pub const InferenceMode = config.InferenceMode;910pub const LimitReason = stats.LimitReason;11pub const LazyKCStats = stats.LazyKCStats;1213pub const CallstackKey = callstack.CallstackKey;14pub const CallstackHashContext = callstack.CallstackHashContext;15pub const compareCallstacks = callstack.compareCallstacks;1617pub const LazyKCState = machine.LazyKCState;18pub const init = machine.init;19pub const initChecked = machine.initChecked;20pub const deinit = machine.deinit;21pub const startTimeLimit = machine.startTimeLimit;22pub const stopTimeLimit = machine.stopTimeLimit;23pub const checkLimits = machine.checkLimits;24pub const recordBddSample = machine.recordBddSample;25pub const maybeSampleBdd = machine.maybeSampleBdd;26pub const recordFinalBddSample = machine.recordFinalBddSample;27pub const recordManagerStats = machine.recordManagerStats;28pub const clearSampledFlips = machine.clearSampledFlips;29pub const currentAddress = machine.currentAddress;30pub const currentAddressForCallstack = machine.currentAddressForCallstack;31pub const findInsertPosition = machine.findInsertPosition;32pub const pushCallstack = machine.pushCallstack;33pub const popCallstack = machine.popCallstack;