tiny.pluck.evaluator

1pub const CombinedIntDist = struct {2    int_dist: IntDist,3    overall_guard: Bdd,4};

1pub const IntDistWithGuard = struct {2    int_dist: IntDist,3    guard: Bdd,4};

1pub const CompileError = error{2    OutOfMemory,3    PluckError,4    InvalidExpression,5    NotImplemented,6    InvalidThunkUnion,7};

1pub const FallbackMode = enum {2    @"error",3    lpsmc,4};

1pub const InferenceMode = enum {2    exact,3    lpsmc,4};

1pub const LazyKCConfig = struct {2    max_depth: ?u32 = null,34    sample_after_max_depth: bool = false,56    use_strict_order: bool = true,78    use_reverse_order: bool = false,910    definition_order: ?*const definition_order.DefinitionOrder = null,1112    use_thunk_unions: bool = true,1314    disable_validity_tracking: bool = false,1516    disable_path_conditions: bool = false,1718    time_limit: ?f64 = null,1920    ite_limit: ?u64 = null,2122    factor_max_branches: usize = 64,2324    weight_dd_max_nodes: usize = 0,2526    fallback_mode: FallbackMode = .@"error",2728    inference_mode: InferenceMode = .exact,2930    sample_constraint: ?Bdd = null,3132    full_dist: bool = false,3334    dual: bool = false,3536    vector_size: u32 = 0,3738    state_vars: StateVars = StateVars.init(),3940    stacktrace: bool = true,4142    parallel_wmc: bool = false,4344    parallel_wmc_threshold: usize = 16,4546    parallel_wmc_threads: ?usize = null,47};

1pub const LazyKCState = struct {2    allocator: Allocator,34    manager: *Manager,56    wmc_params: WmcParams,78    weight_dd: WeightDD,910    weight_dd_root: Weight,1112    weight_dd_one: Weight,1314    deferred_weights: std.ArrayListUnmanaged(DeferredWeight),1516    cfg: LazyKCConfig,1718    stats: LazyKCStats,1920    callstack: std.ArrayList(i32),2122    var_of_callstack: std.HashMapUnmanaged(StateCallstackKey, Bdd, StateCallstackHashContext, 80),2324    sorted_callstacks: std.ArrayList(StateCallstackKey),2526    depth: u32,2728    definitions: *const Definitions,2930    current_def_name: ?Symbol,3132    stacktrace_buf: std.ArrayList(*PExpr),3334    query: ?*PExpr,3536    next_thunk_id: u32,3738    start_time: i128,3940    registry: ?*ThunkRegistry,4142    sampled_flips: std.HashMapUnmanaged(StateCallstackKey, bool, StateCallstackHashContext, 80),4344    prng: std.Random.DefaultPrng,4546    def_thunks: std.StringHashMapUnmanaged(*RuntimeValue),4748    pub const DeferredWeight = struct {49        guards: []GuardedWeight,50    };5152    pub const CallstackKey: type = callstack.CallstackKey;53    pub const CallstackHashContext: type = callstack.CallstackHashContext;54};

1pub const LazyKCStats = struct {2    pub const MaxBddSamples: usize = 32;34    time_ns: u64 = 0,56    num_forward_calls: u64 = 0,78    limit_reason: ?LimitReason = null,910    program_error: bool = false,1112    num_recursive_calls: u64 = 0,1314    ite_cache_hits: u64 = 0,1516    ite_cache_misses: u64 = 0,1718    unique_table_grows: u64 = 0,1920    ite_cache_grows: u64 = 0,2122    thunk_reuse_hits: u64 = 0,2324    thunk_reuse_misses: u64 = 0,2526    thunk_evaluations: u64 = 0,2728    thunk_cache_hits: u64 = 0,2930    variable_count: u64 = 0,3132    node_count: u64 = 0,3334    wmc_time_ns: u64 = 0,3536    refinement_time_ns: u64 = 0,3738    refinement_count: u64 = 0,3940    bdd_samples_forward_calls: [MaxBddSamples]u64 = @as([MaxBddSamples]u64, @splat(0)),4142    bdd_samples_vars: [MaxBddSamples]u64 = @as([MaxBddSamples]u64, @splat(0)),4344    bdd_samples_nodes: [MaxBddSamples]u64 = @as([MaxBddSamples]u64, @splat(0)),4546    bdd_samples_len: u8 = 0,4748    max_factor_guard_branches: usize = 0,49};

1pub const LimitReason = enum {2    max_depth,3    time_limit,4    ite_limit,5    factor_weight_too_complex,67    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};

1pub fn combineIntDists(2    allocator: Allocator,3    int_dist_results: []const IntDistWithGuard,4    manager: *Manager,5) !CombinedIntDist {6    if (int_dist_results.len == 0) {7        return .{ .int_dist = IntDist.init(&.{}), .overall_guard = Bdd.FALSE };8    }910    const width = int_dist_results[0].int_dist.bits.len;1112    const result_bits = try allocator.alloc(Bdd, width);13    for (result_bits) |*bit| {14        bit.* = Bdd.FALSE;15    }1617    var overall_guard = Bdd.FALSE;1819    for (int_dist_results) |entry| {20        std.debug.assert(entry.int_dist.bits.len == width);2122        overall_guard = try manager.bddOr(overall_guard, entry.guard);2324        for (0..width) |i| {25            const new_bit = try manager.bddAnd(entry.int_dist.bits[i], entry.guard);26            result_bits[i] = try manager.bddOr(result_bits[i], new_bit);27        }28    }2930    return .{31        .int_dist = IntDist.init(result_bits),32        .overall_guard = overall_guard,33    };34}

1pub fn enumerateIntDist(2    allocator: Allocator,3    int_dist: IntDist,4    overall_guard: Bdd,5    manager: *Manager,6) ![]World {7    const num_bits = int_dist.bits.len;8    std.debug.assert(num_bits <= 20);910    const num_values: usize = @as(usize, 1) << @intCast(num_bits);1112    var results: std.ArrayList(World) = .empty;13    defer results.deinit(allocator);1415    for (0..num_values) |i| {16        const value: u64 = @intCast(i);17        const value_guard = try intDistAtInt(int_dist, value, manager);18        const combined_guard = try manager.bddAnd(value_guard, overall_guard);1920        if (combined_guard.isFalse()) {21            continue;22        }2324        const int_val = try RuntimeValue.initNative(allocator, .{ .int = @intCast(value) });25        try results.append(allocator, World{ .value = int_val, .guard = combined_guard });26    }2728    return results.toOwnedSlice(allocator);29}

1pub fn intDistAtInt(int_dist: IntDist, value: u64, manager: *Manager) Allocator.Error!Bdd {2    var result = Bdd.TRUE;34    for (0..int_dist.bits.len) |i| {5        const bit_val = (value >> @intCast(i)) & 1 == 1;6        const bit_bdd = int_dist.bits[i];78        if (bit_val) {9            result = try manager.bddAnd(result, bit_bdd);10        } else {11            result = try manager.bddAnd(result, manager.bddNot(bit_bdd));12        }1314        if (result.isFalse()) {15            return Bdd.FALSE;16        }17    }1819    return result;20}

1pub fn processIntDistWorlds(2    allocator: Allocator,3    worlds: []World,4    manager: *Manager,5) !?[]World {6    if (worlds.len == 0) {7        return null;8    }910    const first_int_dist = worlds[0].value.maybeIntDist() orelse return null;11    const width = first_int_dist.bits.len;1213    if (width > 20) {14        return null;15    }1617    for (worlds) |world| {18        const int_dist = world.value.maybeIntDist() orelse return null;19        if (int_dist.bits.len != width) {20            return null;21        }22    }2324    const int_dist_pairs = try allocator.alloc(IntDistWithGuard, worlds.len);25    defer allocator.free(int_dist_pairs);2627    for (worlds, 0..) |world, i| {28        int_dist_pairs[i] = .{29            .int_dist = world.value.maybeIntDist().?,30            .guard = world.guard,31        };32    }3334    const combined = try combineIntDists(allocator, int_dist_pairs, manager);3536    errdefer allocator.free(combined.int_dist.bits);3738    const result = try enumerateIntDist(allocator, combined.int_dist, combined.overall_guard, manager);3940    allocator.free(combined.int_dist.bits);4142    for (worlds) |world| {43        world.value.deinit(allocator);44    }4546    return result;47}

1pub fn bindMonad(2    allocator: Allocator,3    pre_worlds: WorldsResult,4    path_condition: Bdd,5    state: *LazyKCState,6    comptime ContType: type,7    ctx: anytype,8) CompileError!WorldsResult {9    defer freeWorldsSlice(allocator, pre_worlds.worlds);1011    var nested_worlds: std.ArrayList(NestedWorld) = .empty;12    defer nested_worlds.deinit(allocator);1314    for (pre_worlds.worlds) |pre_world| {15        if (state.stats.limit_reason != null) {16            return inferenceErrorWorlds(state);17        }1819        const inner_pc = if (state.cfg.disable_path_conditions)20            Bdd.TRUE21        else22            try state.manager.bddAnd(path_condition, pre_world.guard);2324        if (inner_pc.isFalse()) {25            try nested_worlds.append(allocator, NestedWorld{26                .result = falsePathConditionWorlds(state),27                .guard = pre_world.guard,28            });29            continue;30        }3132        const post_result = try ContType.cont(allocator, pre_world.value, inner_pc, state, ctx);33        try nested_worlds.append(allocator, NestedWorld{34            .result = post_result,35            .guard = pre_world.guard,36        });37    }3839    return joinMonad(allocator, nested_worlds.items, pre_worlds.validity_guard, state);40}

1pub fn conditionWorlds(allocator: Allocator, worlds: []World, condition: Bdd, manager: *Manager) ![]World {2    const result = try allocator.alloc(World, worlds.len);3    for (worlds, 0..) |world, i| {4        result[i] = World{5            .value = world.value,6            .guard = manager.bddAnd(world.guard, condition),7        };8    }9    return result;10}

1pub fn falsePathConditionWorlds(_: *LazyKCState) WorldsResult {2    return WorldsResult{3        .worlds = &[_]World{},4        .validity_guard = Bdd.FALSE,5    };6}

1pub fn freeWorldsSlice(allocator: Allocator, worlds: []World) void {2    if (worlds.len > 0) {3        allocator.free(worlds);4    }5}

1pub fn ifThenElseMonad(2    allocator: Allocator,3    val_if_true: *RuntimeValue,4    val_if_false: *RuntimeValue,5    condition: Bdd,6    state: *LazyKCState,7) !WorldsResult {8    _ = state;9    const worlds = try allocator.alloc(World, 2);10    worlds[0] = World{ .value = val_if_true, .guard = condition };11    worlds[1] = World{ .value = val_if_false, .guard = condition.neg() };12    return WorldsResult{13        .worlds = worlds,14        .validity_guard = Bdd.TRUE,15    };16}

1pub fn inferenceErrorWorlds(_: *LazyKCState) WorldsResult {2    return WorldsResult{3        .worlds = &[_]World{},4        .validity_guard = Bdd.TRUE,5    };6}

1pub fn joinMonad(2    allocator: Allocator,3    nested_worlds: []const NestedWorld,4    pre_validity_guard: Bdd,5    state: *LazyKCState,6) CompileError!WorldsResult {7    var validity_guard = pre_validity_guard;8    if (!state.cfg.disable_validity_tracking) {9        for (nested_worlds) |nested| {10            const branch_validity_guard = try state.manager.bddImplies(nested.guard, nested.result.validity_guard);11            validity_guard = try state.manager.bddAnd(validity_guard, branch_validity_guard);12        }13    }1415    var join_results: std.ArrayList(World) = .empty;16    defer join_results.deinit(allocator);1718    var index_of_result = std.HashMap(*RuntimeValue, usize, RuntimeValueContext, 80).init(allocator);19    defer index_of_result.deinit();2021    var constructor_worlds = std.StringHashMap(std.ArrayList(World)).init(allocator);22    defer {23        if (state.cfg.use_thunk_unions) {24            var it = constructor_worlds.iterator();25            while (it.next()) |entry| {26                entry.value_ptr.deinit(allocator);27            }28        }29        constructor_worlds.deinit();30    }3132    for (nested_worlds) |nested| {33        defer freeWorldsSlice(allocator, nested.result.worlds);3435        for (nested.result.worlds) |post_world| {36            const pre_and_post = try state.manager.bddAnd(post_world.guard, nested.guard);3738            if (state.cfg.use_thunk_unions and post_world.value.data == .constructed) {39                const constructor = post_world.value.data.constructed.constructor;40                const entry = try constructor_worlds.getOrPut(constructor);41                if (!entry.found_existing) {42                    entry.value_ptr.* = std.ArrayList(World).empty;43                }44                try entry.value_ptr.append(allocator, World{45                    .value = post_world.value,46                    .guard = pre_and_post,47                });48                continue;49            }5051            if (index_of_result.get(post_world.value)) |result_idx| {52                const old_guard = join_results.items[result_idx].guard;53                const new_guard = try state.manager.bddOr(old_guard, pre_and_post);54                join_results.items[result_idx].guard = new_guard;55            } else {56                const idx = join_results.items.len;57                try index_of_result.put(post_world.value, idx);58                try join_results.append(allocator, World{59                    .value = post_world.value,60                    .guard = pre_and_post,61                });62            }63        }64    }6566    if (state.cfg.use_thunk_unions) {67        var ctor_iter = constructor_worlds.iterator();68        while (ctor_iter.next()) |entry| {69            const constructor = entry.key_ptr.*;70            const worlds = entry.value_ptr.items;7172            if (worlds.len == 0) {73                continue;74            }7576            var value_to_guard = std.HashMap(*RuntimeValue, Bdd, RuntimeValueContext, 80).init(allocator);77            defer value_to_guard.deinit();7879            for (worlds) |world| {80                if (value_to_guard.get(world.value)) |old_guard| {81                    const new_guard = try state.manager.bddOr(old_guard, world.guard);82                    try value_to_guard.put(world.value, new_guard);83                } else {84                    try value_to_guard.put(world.value, world.guard);85                }86            }8788            if (value_to_guard.count() <= 1) {89                var single_iter = value_to_guard.iterator();90                while (single_iter.next()) |val_entry| {91                    try join_results.append(allocator, World{92                        .value = val_entry.key_ptr.*,93                        .guard = val_entry.value_ptr.*,94                    });95                }96                continue;97            }9899            var first_iter = value_to_guard.iterator();100            const first_entry = first_iter.next() orelse continue;101            const first_val = first_entry.key_ptr.*;102            if (first_val.data != .constructed) {103                var fallback_iter = value_to_guard.iterator();104                while (fallback_iter.next()) |val_entry| {105                    try join_results.append(allocator, World{106                        .value = val_entry.key_ptr.*,107                        .guard = val_entry.value_ptr.*,108                    });109                }110                continue;111            }112113            const arg_count = first_val.data.constructed.args.len;114            var arg_inputs = try allocator.alloc(std.ArrayList(LazyKCThunkUnion.ThunkInput), arg_count);115            defer {116                for (arg_inputs) |*list| {117                    list.deinit(allocator);118                }119                allocator.free(arg_inputs);120            }121            for (arg_inputs) |*list| {122                list.* = .empty;123            }124125            var can_union = true;126            var overall_guard = Bdd.FALSE;127            var value_iter = value_to_guard.iterator();128            while (value_iter.next()) |val_entry| {129                const val = val_entry.key_ptr.*;130                const guard = val_entry.value_ptr.*;131                overall_guard = try state.manager.bddOr(overall_guard, guard);132133                if (val.data != .constructed) {134                    can_union = false;135                    break;136                }137                const c = val.data.constructed;138                if (c.args.len != arg_count) {139                    can_union = false;140                    break;141                }142                for (c.args, 0..) |arg, i| {143                    const can_union_arg = switch (arg.data) {144                        .lazy_kc_thunk, .lazy_kc_thunk_union => true,145                        else => false,146                    };147                    if (!can_union_arg) {148                        can_union = false;149                        break;150                    }151                    try arg_inputs[i].append(allocator, .{152                        .value = arg,153                        .outer_guard = guard,154                    });155                }156                if (!can_union) {157                    break;158                }159            }160161            if (!can_union) {162                var fallback_iter = value_to_guard.iterator();163                while (fallback_iter.next()) |val_entry| {164                    try join_results.append(allocator, World{165                        .value = val_entry.key_ptr.*,166                        .guard = val_entry.value_ptr.*,167                    });168                }169                continue;170            }171172            const union_args = try allocator.alloc(*RuntimeValue, arg_count);173            var created: usize = 0;174            errdefer {175                for (union_args[0..created]) |arg| {176                    arg.deinit(allocator);177                }178                allocator.free(union_args);179            }180181            for (arg_inputs, 0..) |*list, i| {182                const thunk_union = try LazyKCThunkUnion.init(allocator, state.manager, list.items);183                const union_val = try RuntimeValue.initLazyKCThunkUnion(allocator, thunk_union);184                union_args[i] = union_val;185                created += 1;186            }187188            const combined_val = try RuntimeValue.initConstructed(allocator, constructor, union_args);189            try join_results.append(allocator, World{190                .value = combined_val,191                .guard = overall_guard,192            });193        }194    }195196    return WorldsResult{197        .worlds = try join_results.toOwnedSlice(allocator),198        .validity_guard = validity_guard,199    };200}

1pub fn programErrorWorlds(_: *LazyKCState) WorldsResult {2    return WorldsResult{3        .worlds = &[_]World{},4        .validity_guard = Bdd.TRUE,5    };6}

1pub fn pureMonad(allocator: Allocator, val: *RuntimeValue, _: *LazyKCState) !WorldsResult {2    const worlds = try allocator.alloc(World, 1);3    worlds[0] = World{ .value = val, .guard = Bdd.TRUE };4    return WorldsResult{5        .worlds = worlds,6        .validity_guard = Bdd.TRUE,7    };8}

1pub fn compareCallstacks(a: []const i32, b: []const i32) std.math.Order {2    const min_len = @min(a.len, b.len);3    for (0..min_len) |i| {4        if (a[i] < b[i]) return .lt;5        if (a[i] > b[i]) return .gt;6    }7    if (a.len < b.len) return .lt;8    if (a.len > b.len) return .gt;9    return .eq;10}

1const std = @import("std");2const time = @import("time.zig");3const Allocator = std.mem.Allocator;45const pexpr = @import("pexpr.zig");6const PExpr = pexpr.PExpr;7const Head = pexpr.Head;8const Symbol = pexpr.Symbol;9const Definitions = pexpr.Definitions;1011const runtime = @import("runtime.zig");12const Env = runtime.Env;13const RuntimeValue = runtime.RuntimeValue;14const Closure = runtime.Closure;15const LazyKCThunk = runtime.LazyKCThunk;16const LazyKCThunkUnion = runtime.LazyKCThunkUnion;17const StateVars = runtime.StateVars;18const GuardedWorld = runtime.GuardedWorld;19const GuardedWorlds = runtime.GuardedWorlds;2021const bdd = @import("bdd.zig");22const Bdd = bdd.Bdd;23const Manager = bdd.Manager;24const WmcParams = bdd.WmcParams;25const VarLabel = bdd.VarLabel;2627const weight_dd = @import("weight.zig");28const GuardedWeight = weight_dd.GuardedWeight;2930const wmc_module = @import("wmc.zig");31const thunk_registry = @import("registry.zig");32const lpsmc_module = @import("lpsmc.zig");33const int_dist_module = @import("dist.zig");34const state_module = @import("state/root.zig");35const monad_ops = @import("monad.zig");3637pub const Callstack = []const i32;3839pub const World = GuardedWorld;4041pub const WorldsResult = GuardedWorlds;4243pub const CompileError = monad_ops.CompileError;4445pub const RuntimeValueContext = runtime.RuntimeValueContext;46pub const NestedWorld = runtime.NestedWorld;4748pub const WeightedResult = wmc_module.WeightedResult;49const DeferredWmcCaches = wmc_module.DeferredCaches;50pub const computeWmcParallel = wmc_module.computeWmcParallel;51pub const computeWmcSequential = wmc_module.computeWmcSequential;5253pub const ThunkId = thunk_registry.ThunkId;54pub const ThunkIdContext = thunk_registry.ThunkIdContext;55pub const ThunkRegistry = thunk_registry.ThunkRegistry;56pub const ThunkIdSet = thunk_registry.ThunkIdSet;57pub const ThunkDependencies = thunk_registry.ThunkDependencies;5859pub const VarLabelSet = bdd.VarLabelSet;6061pub const PathChoice = lpsmc_module.PathChoice;62pub const SubproblemCache = lpsmc_module.SubproblemCache;63pub const LPSMCVarianceStats = lpsmc_module.LPSMCVarianceStats;64pub const AdaptiveKPolicy = lpsmc_module.AdaptiveKPolicy;65pub const LpsmcRunStats = lpsmc_module.LpsmcRunStats;66pub const EvaluatorOps = lpsmc_module.EvaluatorOps;67pub const IncrementalLPSMC = lpsmc_module.IncrementalLPSMC;6869pub const IntDistWithGuard = int_dist_module.IntDistWithGuard;70pub const CombinedIntDist = int_dist_module.CombinedIntDist;71pub const combineIntDists = int_dist_module.combineIntDists;72pub const intDistAtInt = int_dist_module.intDistAtInt;73pub const enumerateIntDist = int_dist_module.enumerateIntDist;74pub const processIntDistWorlds = int_dist_module.processIntDistWorlds;7576pub const LazyKCConfig = state_module.LazyKCConfig;77pub const LimitReason = state_module.LimitReason;78pub const LazyKCStats = state_module.LazyKCStats;79pub const LazyKCState = state_module.LazyKCState;80pub const compareCallstacks = state_module.compareCallstacks;81pub const FallbackMode = state_module.FallbackMode;82pub const InferenceMode = state_module.InferenceMode;8384pub const programErrorWorlds = monad_ops.programErrorWorlds;85pub const inferenceErrorWorlds = monad_ops.inferenceErrorWorlds;86pub const falsePathConditionWorlds = monad_ops.falsePathConditionWorlds;87pub const freeWorldsSlice = monad_ops.freeWorldsSlice;88pub const pureMonad = monad_ops.pureMonad;89pub const ifThenElseMonad = monad_ops.ifThenElseMonad;90pub const conditionWorlds = monad_ops.conditionWorlds;91pub const bindMonad = monad_ops.bindMonad;92pub const joinMonad = monad_ops.joinMonad;9394const DeferredWmcError = error{95    OutOfMemory,96    NodeLimitExceeded,97};9899fn wmcForState(state: *LazyKCState, guard: Bdd) DeferredWmcError!f64 {100    return wmcWithDeferred(state, guard, state.allocator);101}102103fn wmcForStateWithAllocator(state: *LazyKCState, guard: Bdd, allocator: Allocator) DeferredWmcError!f64 {104    return wmcWithDeferred(state, guard, allocator);105}106107fn wmcWithDeferred(state: *LazyKCState, guard: Bdd, allocator: Allocator) DeferredWmcError!f64 {108    var caches = DeferredWmcCaches.init(allocator);109    defer caches.deinit();110    return wmcWithDeferredCached(state, guard, &caches);111}112113fn wmcWithDeferredCached(state: *LazyKCState, guard: Bdd, caches: *DeferredWmcCaches) DeferredWmcError!f64 {114    if (state.deferred_weights.items.len == 0) {115        return weight_dd.wmcWeightedWithCache(116            &state.weight_dd,117            guard,118            state.weight_dd_root,119            &state.wmc_params,120            &caches.weighted,121        );122    }123124    return wmcWithDeferredInner(state, guard, 0, &caches.deferred, &caches.weighted);125}126127fn wmcWithDeferredInner(128    state: *LazyKCState,129    guard: Bdd,130    index: usize,131    deferred_cache: *std.AutoHashMap(u64, f64),132    weighted_cache: *std.AutoHashMap(u64, f64),133) DeferredWmcError!f64 {134    if (guard.isFalse()) return 0.0;135    if (index >= state.deferred_weights.items.len) {136        return weight_dd.wmcWeightedWithCache(137            &state.weight_dd,138            guard,139            state.weight_dd_root,140            &state.wmc_params,141            weighted_cache,142        );143    }144145    const cache_key: u64 = (@as(u64, @intCast(index)) << 32) | @as(u64, guard.toRaw());146    if (deferred_cache.get(cache_key)) |cached| {147        return cached;148    }149150    const deferred = state.deferred_weights.items[index];151    const limit = state.cfg.weight_dd_max_nodes;152    if (limit != 0 and deferred.guards.len > limit) {153        return error.NodeLimitExceeded;154    }155156    var total: f64 = 0.0;157    for (deferred.guards) |entry| {158        if (entry.weight == 0.0) continue;159        if (entry.guard.isFalse()) continue;160161        const combined = state.manager.bddAnd(guard, entry.guard) catch return error.OutOfMemory;162        if (combined.isFalse()) continue;163        const sub = try wmcWithDeferredInner(state, combined, index + 1, deferred_cache, weighted_cache);164        total += entry.weight * sub;165    }166167    deferred_cache.put(cache_key, total) catch {};168    return total;169}170171fn evaluateThunkOp(172    allocator: Allocator,173    val: *RuntimeValue,174    path_condition: Bdd,175    state_ptr: *anyopaque,176) anyerror!lpsmc_module.WorldsResult {177    const state: *LazyKCState = @ptrCast(@alignCast(state_ptr));178    return evaluateThunk(allocator, val, path_condition, state);179}180181fn freeWorldsSliceOp(allocator: Allocator, worlds: []World) void {182    freeWorldsSlice(allocator, worlds);183}184185fn setWeightOp(wmc_params: *WmcParams, variable: VarLabel, low: f64, high: f64) Allocator.Error!void {186    return wmc_params.setWeight(variable, low, high);187}188189pub fn createEvaluatorOps(state: *LazyKCState) EvaluatorOps {190    return EvaluatorOps{191        .evaluateThunk = evaluateThunkOp,192        .freeWorldsSlice = freeWorldsSliceOp,193        .setWeight = setWeightOp,194        .state = state,195        .wmc_params = &state.wmc_params,196    };197}198199pub fn subproblemMonteCarloImpl(200    allocator: Allocator,201    suspendible_thunk: *RuntimeValue,202    evidence_thunk: ?*RuntimeValue,203    k: usize,204    k_policy: AdaptiveKPolicy,205    state: *LazyKCState,206    manager: *Manager,207    external_rng: ?std.Random,208) ![]World {209    const ops = createEvaluatorOps(state);210    const raw_worlds = try lpsmc_module.subproblemMonteCarloImpl(211        allocator,212        suspendible_thunk,213        evidence_thunk,214        k,215        k_policy,216        ops,217        manager,218        external_rng,219    );220    return inferFullDistribution(allocator, raw_worlds, state);221}222223pub fn tracedCompileInner(224    expr: *PExpr,225    env: Env,226    path_condition: Bdd,227    state: *LazyKCState,228    strict_order_index: i32,229) CompileError!WorldsResult {230    if (path_condition.isFalse()) {231        return falsePathConditionWorlds(state);232    }233234    if (state_module.checkLimits(state)) {235        return inferenceErrorWorlds(state);236    }237238    state.depth += 1;239    defer state.depth -= 1;240241    try state_module.pushCallstack(state, strict_order_index);242    defer state_module.popCallstack(state);243244    if (state.cfg.stacktrace) {245        try state.stacktrace_buf.append(state.allocator, expr);246    }247    defer {248        if (state.cfg.stacktrace and state.stacktrace_buf.items.len > 0) {249            _ = state.stacktrace_buf.pop();250        }251    }252253    const result = try compileInner(expr, env, path_condition, state);254255    state.stats.num_forward_calls += 1;256    state_module.maybeSampleBdd(state);257258    if (state_module.checkLimits(state)) {259        return inferenceErrorWorlds(state);260    }261262    return result;263}264265pub fn compileInner(266    expr: *PExpr,267    env: Env,268    path_condition: Bdd,269    state: *LazyKCState,270) CompileError!WorldsResult {271    const allocator = state.allocator;272273    return switch (expr.head) {274        .app => compileApp(expr, env, path_condition, state),275        .abs => compileAbs(allocator, expr, env, path_condition, state),276        .var_ref => |v| compileVar(allocator, v.name, env, path_condition, state),277        .defined => |d| compileDefined(d.name, env, path_condition, state),278        .construct => |c| compileConstruct(allocator, c.constructor, expr.args, env, path_condition, state),279        .case_of => compileCaseOf(expr, env, path_condition, state),280        .y_combinator => compileY(allocator, expr, env, path_condition, state),281        .flip => compileFlip(allocator, expr, env, path_condition, state),282        .factor => compileFactor(allocator, expr, env, path_condition, state),283        .const_native => |n| compileConstNative(allocator, n, state),284        .native_eq => compileNativeEq(allocator, expr, env, path_condition, state),285        .get_args => compileGetArgs(allocator, expr, env, path_condition, state),286        .get_constructor => compileGetConstructor(allocator, expr, env, path_condition, state),287        .f_div => compileFloatBinop(allocator, .div, expr, env, path_condition, state),288        .f_mul => compileFloatBinop(allocator, .mul, expr, env, path_condition, state),289        .f_add => compileFloatBinop(allocator, .add, expr, env, path_condition, state),290        .f_sub => compileFloatBinop(allocator, .sub, expr, env, path_condition, state),291        .print_op => tracedCompileInner(expr.args[0], env, path_condition, state, 0),292        .error_op => error.PluckError,293        .pbool => compilePBool(allocator, expr, env, path_condition, state),294        .mk_int => compileMkInt(allocator, expr, state),295        .mk_int_weighted => compileMkIntWeighted(allocator, expr, env, path_condition, state),296        .int_dist_eq => compileIntDistEq(allocator, expr, env, path_condition, state),297        .get_config => compileGetConfig(allocator, state),298        .type_def => error.InvalidExpression,299    };300}301302const CompileAppContinuation = struct {303    pub fn cont(304        alloc: Allocator,305        f: *RuntimeValue,306        inner_pc: Bdd,307        s: *LazyKCState,308        ctx: anytype,309    ) !WorldsResult {310        const thunk = ctx.thunk;311        const orig_env = ctx.env;312        _ = orig_env;313314        switch (f.data) {315            .closure => |closure| {316                const thunk_val = try RuntimeValue.initLazyKCThunk(alloc, thunk);317                const new_env = try closure.env.extend(alloc, closure.name, thunk_val);318                return switch (closure.expr) {319                    .pexpr => |body| tracedCompileInner(body, new_env, inner_pc, s, 2),320                    .thunk => error.NotImplemented,321                };322            },323            else => return programErrorWorlds(s),324        }325    }326};327328fn compileApp(329    expr: *PExpr,330    env: Env,331    path_condition: Bdd,332    state: *LazyKCState,333) CompileError!WorldsResult {334    const allocator = state.allocator;335336    const arg_thunk = try makeThunk(allocator, expr.args[1], env, 1, state);337338    const func_result = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);339340    return bindMonad(341        allocator,342        func_result,343        path_condition,344        state,345        CompileAppContinuation,346        .{ .thunk = arg_thunk, .env = env },347    );348}349350fn compileAbs(351    allocator: Allocator,352    expr: *PExpr,353    env: Env,354    path_condition: Bdd,355    state: *LazyKCState,356) !WorldsResult {357    _ = path_condition;358359    const var_name = expr.head.abs.var_name;360    const closure = try Closure.init(allocator, expr.args[0], env, var_name);361    const val = try RuntimeValue.initClosure(allocator, closure);362    return pureMonad(allocator, val, state);363}364365fn compileVar(366    allocator: Allocator,367    name: Symbol,368    env: Env,369    path_condition: Bdd,370    state: *LazyKCState,371) !WorldsResult {372    const v = env.get(name) orelse return programErrorWorlds(state);373374    if (v.isThunk()) {375        return evaluateThunk(allocator, v, path_condition, state);376    }377378    return pureMonad(allocator, v, state);379}380381fn compileDefined(382    name: Symbol,383    env: Env,384    path_condition: Bdd,385    state: *LazyKCState,386) !WorldsResult {387    const allocator = state.allocator;388389    if (env.get(name)) |v| {390        if (v.isThunk()) {391            return evaluateThunk(allocator, v, path_condition, state);392        }393        return pureMonad(allocator, v, state);394    }395396    const def_expr = state.definitions.lookup(name) orelse return programErrorWorlds(state);397398    const saved_def = state.current_def_name;399    state.current_def_name = name;400    defer state.current_def_name = saved_def;401402    if (state.def_thunks.get(name)) |thunk_val| {403        return evaluateThunk(allocator, thunk_val, path_condition, state);404    }405406    var strict_index: i32 = 0;407    if (state.cfg.definition_order) |order| {408        if (order.getIndex(name)) |idx| {409            strict_index = idx;410        }411    }412    const thunk = try makeThunk(allocator, def_expr, Env.empty, strict_index, state);413    const thunk_val = try RuntimeValue.initLazyKCThunk(allocator, thunk);414    try state.def_thunks.put(allocator, name, thunk_val);415416    return evaluateThunk(allocator, thunk_val, path_condition, state);417}418419fn compileConstruct(420    allocator: Allocator,421    constructor: Symbol,422    args: []const *PExpr,423    env: Env,424    path_condition: Bdd,425    state: *LazyKCState,426) !WorldsResult {427    _ = path_condition;428429    const thunked_args = try allocator.alloc(*RuntimeValue, args.len);430    for (args, 0..) |arg, i| {431        const thunk = try makeThunk(allocator, arg, env, @intCast(i + 1), state);432        thunked_args[i] = try RuntimeValue.initLazyKCThunk(allocator, thunk);433    }434435    const val = try RuntimeValue.initConstructed(allocator, constructor, thunked_args);436    return pureMonad(allocator, val, state);437}438439const CaseGuardMatchKind = enum {440    constructor,441    wildcard,442    capture,443};444445fn isWildcardCaseGuard(guard: pexpr.CaseOfGuard) bool {446    return guard.args.len == 0 and std.mem.eql(u8, guard.constructor, "_");447}448449fn isCaptureCaseGuard(guard: pexpr.CaseOfGuard) bool {450    return guard.args.len == 0 and guard.constructor.len > 0 and !std.ascii.isUpper(guard.constructor[0]) and !std.mem.eql(u8, guard.constructor, "_");451}452453const CompileCaseContinuation = struct {454    pub fn cont(455        alloc: Allocator,456        scrutinee: *RuntimeValue,457        inner_pc: Bdd,458        s: *LazyKCState,459        ctx: anytype,460    ) !WorldsResult {461        const e = ctx.expr;462        const branches_inner = ctx.branches;463        const orig_env = ctx.env;464        const constructed = if (scrutinee.data == .constructed)465            scrutinee.data.constructed466        else467            null;468469        var branch_idx: ?usize = null;470        var match_kind: CaseGuardMatchKind = .constructor;471        for (branches_inner, 0..) |guard, i| {472            if (constructed) |c| {473                if (std.mem.eql(u8, guard.constructor, c.constructor)) {474                    branch_idx = i;475                    match_kind = .constructor;476                    break;477                }478            }479            if (isWildcardCaseGuard(guard)) {480                branch_idx = i;481                match_kind = .wildcard;482                break;483            }484            if (isCaptureCaseGuard(guard)) {485                branch_idx = i;486                match_kind = .capture;487                break;488            }489        }490491        if (branch_idx == null) {492            return programErrorWorlds(s);493        }494495        const idx = branch_idx.?;496        const guard = branches_inner[idx];497        const case_expr = e.args[idx + 1];498499        var new_env = orig_env;500        switch (match_kind) {501            .constructor => {502                const c = constructed orelse return programErrorWorlds(s);503                if (guard.args.len != c.args.len) {504                    return programErrorWorlds(s);505                }506                for (guard.args, c.args) |name, arg| {507                    new_env = try new_env.extend(alloc, name, arg);508                }509            },510            .wildcard => {},511            .capture => {512                new_env = try new_env.extend(alloc, guard.constructor, scrutinee);513            },514        }515516        return tracedCompileInner(case_expr, new_env, inner_pc, s, @intCast(idx + 1));517    }518};519520fn compileCaseOf(521    expr: *PExpr,522    env: Env,523    path_condition: Bdd,524    state: *LazyKCState,525) !WorldsResult {526    const allocator = state.allocator;527    const branches = expr.head.case_of.branches;528529    const scrutinee_result = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);530531    return bindMonad(532        allocator,533        scrutinee_result,534        path_condition,535        state,536        CompileCaseContinuation,537        .{ .expr = expr, .branches = branches, .env = env },538    );539}540541fn compileY(542    allocator: Allocator,543    expr: *PExpr,544    env: Env,545    path_condition: Bdd,546    state: *LazyKCState,547) !WorldsResult {548    _ = path_condition;549550    const rec_lambda = expr.args[0];551    if (rec_lambda.head != .abs) return programErrorWorlds(state);552553    const arg_lambda = rec_lambda.args[0];554    if (arg_lambda.head != .abs) return programErrorWorlds(state);555556    const rec_name = rec_lambda.head.abs.var_name;557    const arg_name = arg_lambda.head.abs.var_name;558    const body = arg_lambda.args[0];559560    const closure = try Closure.makeSelfLoop(allocator, body, env, rec_name, arg_name);561    const val = try RuntimeValue.initClosure(allocator, closure);562    return pureMonad(allocator, val, state);563}564565const FlipOutcome = union(enum) {566    addr: Bdd,567    sampled: bool,568};569570fn sampleFlipForCallstack(571    allocator: Allocator,572    callstack: []const i32,573    p: f64,574    state: *LazyKCState,575) CompileError!bool {576    const lookup_key = LazyKCState.CallstackKey{577        .callstack = callstack,578        .prob = p,579    };580    if (state.sampled_flips.get(lookup_key)) |sampled_true| {581        return sampled_true;582    }583584    const random = state.prng.random();585    const sampled_true = random.float(f64) < p;586    const callstack_copy = try allocator.dupe(i32, callstack);587    const store_key = LazyKCState.CallstackKey{588        .callstack = callstack_copy,589        .prob = p,590    };591    state.sampled_flips.put(allocator, store_key, sampled_true) catch {592        allocator.free(callstack_copy);593        return CompileError.OutOfMemory;594    };595    return sampled_true;596}597598fn resolveFlipForCallstack(599    allocator: Allocator,600    callstack: []const i32,601    p: f64,602    state: *LazyKCState,603) CompileError!FlipOutcome {604    if (state.cfg.sample_after_max_depth) {605        if (state.cfg.max_depth) |max| {606            if (state.depth > max) {607                const lookup_key = LazyKCState.CallstackKey{608                    .callstack = callstack,609                    .prob = p,610                };611                if (!state.var_of_callstack.contains(lookup_key)) {612                    return .{ .sampled = try sampleFlipForCallstack(allocator, callstack, p, state) };613                }614            }615        }616    }617618    const addr = try state_module.currentAddressForCallstack(state, callstack, p);619    return .{ .addr = addr };620}621622const CompileFlipContinuation = struct {623    pub fn cont(624        alloc: Allocator,625        p_val: *RuntimeValue,626        inner_pc: Bdd,627        s: *LazyKCState,628        ctx: anytype,629    ) CompileError!WorldsResult {630        _ = ctx;631        _ = inner_pc;632633        const p = switch (p_val.data) {634            .native => |n| switch (n) {635                .float => |f| f,636                else => return programErrorWorlds(s),637            },638            else => return programErrorWorlds(s),639        };640641        if (p < 0.0 or p > 1.0) {642            return programErrorWorlds(s);643        }644645        if (@abs(p) < 1e-10) {646            const false_val = try RuntimeValue.initFalse(alloc);647            return pureMonad(alloc, false_val, s);648        }649        if (@abs(p - 1.0) < 1e-10) {650            const true_val = try RuntimeValue.initTrue(alloc);651            return pureMonad(alloc, true_val, s);652        }653654        try state_module.pushCallstack(s, 1);655        defer state_module.popCallstack(s);656657        if (s.cfg.sample_constraint) |constraint| {658            const addr = try state_module.currentAddress(s, p);659            const implies_true = try s.manager.bddImplies(constraint, addr);660            if (implies_true.isTrue()) {661                const true_val = try RuntimeValue.initTrue(alloc);662                return pureMonad(alloc, true_val, s);663            }664            const implies_false = try s.manager.bddImplies(constraint, addr.neg());665            if (implies_false.isTrue()) {666                const false_val = try RuntimeValue.initFalse(alloc);667                return pureMonad(alloc, false_val, s);668            }669            const sampled_true = try sampleFlipForCallstack(alloc, s.callstack.items, p, s);670            if (sampled_true) {671                const true_val = try RuntimeValue.initTrue(alloc);672                return pureMonad(alloc, true_val, s);673            } else {674                const false_val = try RuntimeValue.initFalse(alloc);675                return pureMonad(alloc, false_val, s);676            }677        }678679        if (s.cfg.sample_after_max_depth) {680            if (s.cfg.max_depth) |max| {681                if (s.depth > max) {682                    const lookup_key = LazyKCState.CallstackKey{683                        .callstack = s.callstack.items,684                        .prob = p,685                    };686                    if (!s.var_of_callstack.contains(lookup_key)) {687                        const sampled_true = try sampleFlipForCallstack(688                            alloc,689                            s.callstack.items,690                            p,691                            s,692                        );693                        if (sampled_true) {694                            const true_val = try RuntimeValue.initTrue(alloc);695                            return pureMonad(alloc, true_val, s);696                        } else {697                            const false_val = try RuntimeValue.initFalse(alloc);698                            return pureMonad(alloc, false_val, s);699                        }700                    }701                }702            }703        }704        const addr = try state_module.currentAddress(s, p);705706        const true_val = try RuntimeValue.initTrue(alloc);707        const false_val = try RuntimeValue.initFalse(alloc);708709        const worlds = try alloc.alloc(World, 2);710        worlds[0] = World{ .value = true_val, .guard = addr };711        worlds[1] = World{ .value = false_val, .guard = addr.neg() };712        return WorldsResult{713            .worlds = worlds,714            .validity_guard = Bdd.TRUE,715        };716    }717};718719fn compileFlip(720    allocator: Allocator,721    expr: *PExpr,722    env: Env,723    path_condition: Bdd,724    state: *LazyKCState,725) !WorldsResult {726    const prob_result = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);727728    return bindMonad(allocator, prob_result, path_condition, state, CompileFlipContinuation, {});729}730731fn collectFactorWeightWorlds(732    allocator: Allocator,733    out: *std.ArrayList(World),734    value: *RuntimeValue,735    guard: Bdd,736    path_condition: Bdd,737    state: *LazyKCState,738) CompileError!void {739    if (state.stats.limit_reason != null) return;740    if (guard.isFalse()) return;741742    switch (value.data) {743        .lazy_kc_thunk, .lazy_kc_thunk_union => {744            const inner_pc = if (state.cfg.disable_path_conditions)745                Bdd.TRUE746            else747                try state.manager.bddAnd(path_condition, guard);748            const result = try evaluateThunk(allocator, value, inner_pc, state);749            defer freeWorldsSlice(allocator, result.worlds);750751            for (result.worlds) |world| {752                const combined_guard = try state.manager.bddAnd(guard, world.guard);753                try collectFactorWeightWorlds(754                    allocator,755                    out,756                    world.value,757                    combined_guard,758                    path_condition,759                    state,760                );761                if (state.stats.limit_reason != null) return;762            }763        },764        else => {765            try out.append(allocator, World{ .value = value, .guard = guard });766        },767    }768}769770const WeightSymbolicResult = union(enum) {771    ok: []GuardedWeight,772    fail,773    invalid,774};775776fn compileWeightSymbolic(777    allocator: Allocator,778    worlds: []const World,779) CompileError!WeightSymbolicResult {780    var guards: std.ArrayList(GuardedWeight) = .empty;781    defer guards.deinit(allocator);782783    for (worlds) |world| {784        if (world.guard.isFalse()) continue;785        if (world.value.isThunk()) return .fail;786787        const weight = valueToFloat(world.value) orelse return .invalid;788        if (!std.math.isFinite(weight) or weight < 0.0) return .invalid;789        if (weight == 0.0) continue;790791        try guards.append(allocator, .{792            .guard = world.guard,793            .weight = weight,794        });795    }796797    const owned = try guards.toOwnedSlice(allocator);798    return .{ .ok = owned };799}800801fn emptyFactorResult(validity_guard: Bdd) WorldsResult {802    return WorldsResult{803        .worlds = &[_]World{},804        .validity_guard = validity_guard,805    };806}807808fn unitFactorResult(allocator: Allocator, guard: Bdd, validity_guard: Bdd) CompileError!WorldsResult {809    const unit_val = try RuntimeValue.initConstructed(allocator, "Unit", &[_]*RuntimeValue{});810    const worlds = try allocator.alloc(World, 1);811    worlds[0] = World{ .value = unit_val, .guard = guard };812    return WorldsResult{813        .worlds = worlds,814        .validity_guard = validity_guard,815    };816}817818fn finishFactorFromGuardList(819    allocator: Allocator,820    guards: []const GuardedWeight,821    validity_guard: Bdd,822    state: *LazyKCState,823) CompileError!WorldsResult {824    var output: std.ArrayList(World) = .empty;825    defer output.deinit(allocator);826827    const unit_val = try RuntimeValue.initConstructed(allocator, "Unit", &[_]*RuntimeValue{});828829    for (guards) |entry| {830        if (entry.guard.isFalse()) continue;831        if (entry.weight == 0.0) continue;832833        if (@abs(entry.weight - 1.0) < 1e-12) {834            try output.append(allocator, World{ .value = unit_val, .guard = entry.guard });835            continue;836        }837838        const factor_var = try state.manager.newVar(true);839        try state.wmc_params.setWeight(state.manager.topVar(factor_var), 1.0, entry.weight);840        const combined_guard = try state.manager.bddAnd(entry.guard, factor_var);841        try output.append(allocator, World{ .value = unit_val, .guard = combined_guard });842    }843844    if (output.items.len == 0) {845        return emptyFactorResult(validity_guard);846    }847848    const worlds = try output.toOwnedSlice(allocator);849    return WorldsResult{850        .worlds = worlds,851        .validity_guard = validity_guard,852    };853}854855fn deferFactorGuards(856    allocator: Allocator,857    guards: []const GuardedWeight,858    path_condition: Bdd,859    validity_guard: Bdd,860    state: *LazyKCState,861) CompileError!WorldsResult {862    var restricted: std.ArrayList(GuardedWeight) = .empty;863    defer restricted.deinit(allocator);864    try restricted.ensureTotalCapacity(allocator, guards.len);865866    for (guards) |entry| {867        if (entry.weight == 0.0) continue;868        if (entry.guard.isFalse()) continue;869        const combined_guard = if (state.cfg.disable_path_conditions)870            entry.guard871        else872            state.manager.bddAnd(entry.guard, path_condition) catch return error.OutOfMemory;873        if (combined_guard.isFalse()) continue;874        try restricted.append(allocator, .{875            .guard = combined_guard,876            .weight = entry.weight,877        });878    }879880    const owned = try restricted.toOwnedSlice(allocator);881    if (owned.len == 0) {882        allocator.free(owned);883        return emptyFactorResult(validity_guard);884    }885886    try state.deferred_weights.append(allocator, .{ .guards = owned });887    return unitFactorResult(allocator, Bdd.TRUE, validity_guard);888}889890fn finishFactorWeightDdError(891    err: weight_dd.ApplyError,892    allocator: Allocator,893    guards: []const GuardedWeight,894    path_condition: Bdd,895    validity_guard: Bdd,896    state: *LazyKCState,897) CompileError!WorldsResult {898    return switch (err) {899        error.OutOfMemory => error.OutOfMemory,900        error.NodeLimitExceeded => deferFactorGuards(allocator, guards, path_condition, validity_guard, state),901        error.NaNWeight, error.NonFiniteWeight => programErrorWorlds(state),902    };903}904905fn finishFactorWithWeightDD(906    allocator: Allocator,907    guards: []const GuardedWeight,908    path_condition: Bdd,909    validity_guard: Bdd,910    state: *LazyKCState,911) CompileError!WorldsResult {912    const node_limit = if (state.cfg.inference_mode == .lpsmc) 0 else state.cfg.weight_dd_max_nodes;913    const current_pc = if (state.cfg.disable_path_conditions) Bdd.TRUE else path_condition;914915    const refine_start = time.nanoTimestamp();916    defer {917        const elapsed = time.nanoTimestamp() - refine_start;918        state.stats.refinement_time_ns += @intCast(@max(0, elapsed));919        state.stats.refinement_count += 1;920    }921922    const weight_root = state.weight_dd.refineWeight(guards, node_limit) catch |err| {923        return finishFactorWeightDdError(err, allocator, guards, current_pc, validity_guard, state);924    };925926    if (node_limit != 0) {927        _ = state.weight_dd.nodeCountLimited(weight_root, node_limit) catch |err| {928            return finishFactorWeightDdError(err, allocator, guards, current_pc, validity_guard, state);929        };930    }931932    const gated_weight = if (node_limit != 0)933        state.weight_dd.iteLimited(current_pc, weight_root, state.weight_dd_one, node_limit) catch |err| {934            return finishFactorWeightDdError(err, allocator, guards, current_pc, validity_guard, state);935        }936    else937        state.weight_dd.ite(current_pc, weight_root, state.weight_dd_one) catch |err| {938            return finishFactorWeightDdError(err, allocator, guards, current_pc, validity_guard, state);939        };940941    const new_root = if (node_limit != 0)942        state.weight_dd.mulLimited(state.weight_dd_root, gated_weight, node_limit) catch |err| {943            return finishFactorWeightDdError(err, allocator, guards, current_pc, validity_guard, state);944        }945    else946        state.weight_dd.mul(state.weight_dd_root, gated_weight) catch |err| {947            return finishFactorWeightDdError(err, allocator, guards, current_pc, validity_guard, state);948        };949950    state.weight_dd_root = new_root;951    return unitFactorResult(allocator, Bdd.TRUE, validity_guard);952}953954fn finishFactorFromGuards(955    allocator: Allocator,956    guards: []const GuardedWeight,957    path_condition: Bdd,958    validity_guard: Bdd,959    state: *LazyKCState,960) CompileError!WorldsResult {961    if (guards.len == 0) {962        return emptyFactorResult(validity_guard);963    }964965    const use_weight_dd = state.cfg.factor_max_branches != 0 and966        guards.len > state.cfg.factor_max_branches;967968    if (guards.len > state.stats.max_factor_guard_branches) {969        state.stats.max_factor_guard_branches = guards.len;970    }971972    if (!use_weight_dd) {973        return finishFactorFromGuardList(allocator, guards, validity_guard, state);974    }975976    return finishFactorWithWeightDD(allocator, guards, path_condition, validity_guard, state);977}978979fn compileFactor(980    allocator: Allocator,981    expr: *PExpr,982    env: Env,983    path_condition: Bdd,984    state: *LazyKCState,985) CompileError!WorldsResult {986    const weight_result = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);987    defer freeWorldsSlice(allocator, weight_result.worlds);988989    const validity_guard = weight_result.validity_guard;990991    if (state.stats.limit_reason != null) {992        return inferenceErrorWorlds(state);993    }994995    if (weight_result.worlds.len == 0) {996        return WorldsResult{997            .worlds = &[_]World{},998            .validity_guard = validity_guard,999        };1000    }10011002    const symbolic = try compileWeightSymbolic(allocator, weight_result.worlds);1003    switch (symbolic) {1004        .ok => |guards| {1005            defer allocator.free(guards);1006            return finishFactorFromGuards(allocator, guards, path_condition, validity_guard, state);1007        },1008        .invalid => return programErrorWorlds(state),1009        .fail => {},1010    }10111012    const fallback_limit = state.cfg.factor_max_branches;1013    if (fallback_limit != 0 and weight_result.worlds.len > fallback_limit) {1014        state.stats.limit_reason = .factor_weight_too_complex;1015        return inferenceErrorWorlds(state);1016    }10171018    var weight_worlds: std.ArrayList(World) = .empty;1019    defer weight_worlds.deinit(allocator);10201021    for (weight_result.worlds) |world| {1022        try collectFactorWeightWorlds(1023            allocator,1024            &weight_worlds,1025            world.value,1026            world.guard,1027            path_condition,1028            state,1029        );1030        if (state.stats.limit_reason != null) {1031            return inferenceErrorWorlds(state);1032        }1033    }10341035    if (fallback_limit != 0 and weight_worlds.items.len > fallback_limit) {1036        state.stats.limit_reason = .factor_weight_too_complex;1037        return inferenceErrorWorlds(state);1038    }10391040    const fallback = try compileWeightSymbolic(allocator, weight_worlds.items);1041    switch (fallback) {1042        .ok => |guards| {1043            defer allocator.free(guards);1044            return finishFactorFromGuards(allocator, guards, path_condition, validity_guard, state);1045        },1046        .invalid => return programErrorWorlds(state),1047        .fail => {1048            state.stats.limit_reason = .factor_weight_too_complex;1049            return inferenceErrorWorlds(state);1050        },1051    }1052}10531054fn compileConstNative(1055    allocator: Allocator,1056    native: pexpr.NativeValue,1057    state: *LazyKCState,1058) !WorldsResult {1059    const data: runtime.NativeValueData = switch (native) {1060        .int => |i| .{ .int = i },1061        .float => |f| .{ .float = f },1062        .symbol => |s| .{ .symbol = s },1063        .bool_val => |b| .{ .bool_val = b },1064    };1065    const val = try RuntimeValue.initNative(allocator, data);1066    return pureMonad(allocator, val, state);1067}10681069const NativeEqSecondContinuation = struct {1070    pub fn cont(1071        inner_alloc: Allocator,1072        arg2: *RuntimeValue,1073        _: Bdd,1074        inner_s: *LazyKCState,1075        inner_ctx: anytype,1076    ) CompileError!WorldsResult {1077        const a1 = inner_ctx.arg1;10781079        const eq = if (a1.data == .native and arg2.data == .native)1080            a1.data.native.eql(arg2.data.native)1081        else1082            false;10831084        const result_val = if (eq)1085            try RuntimeValue.initTrue(inner_alloc)1086        else1087            try RuntimeValue.initFalse(inner_alloc);10881089        return pureMonad(inner_alloc, result_val, inner_s);1090    }1091};10921093const NativeEqFirstContinuation = struct {1094    pub fn cont(1095        alloc: Allocator,1096        arg1: *RuntimeValue,1097        inner_pc: Bdd,1098        s: *LazyKCState,1099        ctx: anytype,1100    ) CompileError!WorldsResult {1101        const result2 = try tracedCompileInner(ctx.expr.args[1], ctx.env, inner_pc, s, 1);1102        return bindMonad(1103            alloc,1104            result2,1105            inner_pc,1106            s,1107            NativeEqSecondContinuation,1108            .{ .arg1 = arg1 },1109        );1110    }1111};11121113fn compileNativeEq(1114    allocator: Allocator,1115    expr: *PExpr,1116    env: Env,1117    path_condition: Bdd,1118    state: *LazyKCState,1119) !WorldsResult {1120    const result1 = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);11211122    return bindMonad(1123        allocator,1124        result1,1125        path_condition,1126        state,1127        NativeEqFirstContinuation,1128        .{ .expr = expr, .env = env },1129    );1130}11311132const FloatBinopType = enum { div, mul, add, sub };11331134fn valueToFloat(val: *RuntimeValue) ?f64 {1135    return switch (val.data) {1136        .native => |n| switch (n) {1137            .float => |f| f,1138            .int => |i| @as(f64, @floatFromInt(i)),1139            else => null,1140        },1141        .constructed => {1142            if (val.maybeNat()) |nat_val| {1143                return @as(f64, @floatFromInt(nat_val));1144            }1145            return null;1146        },1147        else => null,1148    };1149}11501151const FloatBinopSecondContinuation = struct {1152    pub fn cont(1153        inner_alloc: Allocator,1154        arg2: *RuntimeValue,1155        _: Bdd,1156        inner_s: *LazyKCState,1157        inner_ctx: anytype,1158    ) CompileError!WorldsResult {1159        const a1 = inner_ctx.arg1;1160        const operation = inner_ctx.op;11611162        const v1 = valueToFloat(a1) orelse return programErrorWorlds(inner_s);1163        const v2 = valueToFloat(arg2) orelse return programErrorWorlds(inner_s);11641165        const result_f = switch (operation) {1166            .div => v1 / v2,1167            .mul => v1 * v2,1168            .add => v1 + v2,1169            .sub => v1 - v2,1170        };11711172        const val = try RuntimeValue.initNative(inner_alloc, .{ .float = result_f });1173        return pureMonad(inner_alloc, val, inner_s);1174    }1175};11761177const FloatBinopFirstContinuation = struct {1178    pub fn cont(1179        alloc: Allocator,1180        arg1: *RuntimeValue,1181        inner_pc: Bdd,1182        s: *LazyKCState,1183        ctx: anytype,1184    ) CompileError!WorldsResult {1185        const result2 = try tracedCompileInner(ctx.expr.args[1], ctx.env, inner_pc, s, 1);1186        return bindMonad(1187            alloc,1188            result2,1189            inner_pc,1190            s,1191            FloatBinopSecondContinuation,1192            .{ .arg1 = arg1, .op = ctx.op },1193        );1194    }1195};11961197fn compileFloatBinop(1198    allocator: Allocator,1199    op: FloatBinopType,1200    expr: *PExpr,1201    env: Env,1202    path_condition: Bdd,1203    state: *LazyKCState,1204) !WorldsResult {1205    const result1 = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);12061207    return bindMonad(1208        allocator,1209        result1,1210        path_condition,1211        state,1212        FloatBinopFirstContinuation,1213        .{ .expr = expr, .env = env, .op = op },1214    );1215}12161217const GetArgsContinuation = struct {1218    pub fn cont(1219        alloc: Allocator,1220        val: *RuntimeValue,1221        _: Bdd,1222        s: *LazyKCState,1223        ctx: anytype,1224    ) !WorldsResult {1225        _ = ctx;12261227        if (val.data != .constructed) {1228            return programErrorWorlds(s);1229        }12301231        const c = val.data.constructed;12321233        var list = try RuntimeValue.initConstructed(alloc, "Nil", &[_]*RuntimeValue{});1234        var i = c.args.len;1235        while (i > 0) {1236            i -= 1;1237            const args_slice = try alloc.alloc(*RuntimeValue, 2);1238            args_slice[0] = c.args[i];1239            args_slice[1] = list;1240            list = try RuntimeValue.initConstructed(alloc, "Cons", args_slice);1241        }12421243        return pureMonad(alloc, list, s);1244    }1245};12461247fn compileGetArgs(1248    allocator: Allocator,1249    expr: *PExpr,1250    env: Env,1251    path_condition: Bdd,1252    state: *LazyKCState,1253) !WorldsResult {1254    const result = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);12551256    return bindMonad(allocator, result, path_condition, state, GetArgsContinuation, {});1257}12581259const GetConstructorContinuation = struct {1260    pub fn cont(1261        alloc: Allocator,1262        val: *RuntimeValue,1263        _: Bdd,1264        s: *LazyKCState,1265        ctx: anytype,1266    ) !WorldsResult {1267        _ = ctx;12681269        if (val.data != .constructed) {1270            return programErrorWorlds(s);1271        }12721273        const c = val.data.constructed;1274        const sym_val = try RuntimeValue.initNative(alloc, .{ .symbol = c.constructor });1275        return pureMonad(alloc, sym_val, s);1276    }1277};12781279fn compileGetConstructor(1280    allocator: Allocator,1281    expr: *PExpr,1282    env: Env,1283    path_condition: Bdd,1284    state: *LazyKCState,1285) !WorldsResult {1286    const result = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);12871288    return bindMonad(allocator, result, path_condition, state, GetConstructorContinuation, {});1289}12901291fn logAddExp(a: f64, b: f64) f64 {1292    if (a == -std.math.inf(f64)) return b;1293    if (b == -std.math.inf(f64)) return a;1294    if (a > b) {1295        return a + @log(1.0 + @exp(b - a));1296    } else {1297        return b + @log(1.0 + @exp(a - b));1298    }1299}13001301const PBoolContinuation = struct {1302    pub fn cont(1303        alloc: Allocator,1304        cond_val: *RuntimeValue,1305        _: Bdd,1306        s: *LazyKCState,1307        ctx: anytype,1308    ) CompileError!WorldsResult {1309        const p_t = ctx;13101311        if (cond_val.data != .constructed) {1312            return programErrorWorlds(s);1313        }1314        const c = cond_val.data.constructed;13151316        const prob_val = try RuntimeValue.initNative(alloc, .{ .float = p_t });13171318        const args = try alloc.alloc(*RuntimeValue, 2);1319        args[0] = prob_val;1320        args[1] = cond_val;13211322        if (std.mem.eql(u8, c.constructor, "True") or std.mem.eql(u8, c.constructor, "False")) {1323            const pbool_val = try RuntimeValue.initConstructed(alloc, "PBool", args);1324            return pureMonad(alloc, pbool_val, s);1325        }13261327        return programErrorWorlds(s);1328    }1329};13301331fn compilePBool(1332    allocator: Allocator,1333    expr: *PExpr,1334    env: Env,1335    path_condition: Bdd,1336    state: *LazyKCState,1337) !WorldsResult {1338    const cond_result = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);13391340    var log_p_true: f64 = -std.math.inf(f64);1341    var log_p_false: f64 = -std.math.inf(f64);13421343    for (cond_result.worlds) |world| {1344        if (world.value.data != .constructed) continue;1345        const c = world.value.data.constructed;1346        const prob = wmcForState(state, world.guard) catch |err| switch (err) {1347            error.OutOfMemory => return error.OutOfMemory,1348            error.NodeLimitExceeded => {1349                state.stats.limit_reason = .factor_weight_too_complex;1350                freeWorldsSlice(allocator, cond_result.worlds);1351                return inferenceErrorWorlds(state);1352            },1353        };1354        const log_prob = if (prob > 0) @log(prob) else -std.math.inf(f64);13551356        if (std.mem.eql(u8, c.constructor, "True")) {1357            log_p_true = logAddExp(log_p_true, log_prob);1358        } else if (std.mem.eql(u8, c.constructor, "False")) {1359            log_p_false = logAddExp(log_p_false, log_prob);1360        }1361    }13621363    const log_total = logAddExp(log_p_true, log_p_false);1364    const prob_true: f64 = if (log_total > -std.math.inf(f64))1365        @exp(log_p_true - log_total)1366    else1367        0.0;13681369    return bindMonad(allocator, cond_result, path_condition, state, PBoolContinuation, prob_true);1370}13711372fn compileMkInt(1373    allocator: Allocator,1374    expr: *PExpr,1375    state: *LazyKCState,1376) !WorldsResult {1377    const bitwidth_expr = expr.args[0];1378    const val_expr = expr.args[1];13791380    const bitwidth: u6 = switch (bitwidth_expr.head) {1381        .const_native => |n| switch (n) {1382            .int => |i| @intCast(i),1383            else => return programErrorWorlds(state),1384        },1385        else => return programErrorWorlds(state),1386    };13871388    const value: u64 = switch (val_expr.head) {1389        .const_native => |n| switch (n) {1390            .int => |i| @bitCast(i),1391            else => return programErrorWorlds(state),1392        },1393        else => return programErrorWorlds(state),1394    };13951396    const bits = try allocator.alloc(Bdd, bitwidth);1397    for (0..bitwidth) |i| {1398        const bit_set = (value >> @intCast(i)) & 1 == 1;1399        bits[i] = if (bit_set) Bdd.TRUE else Bdd.FALSE;1400    }14011402    const int_dist = runtime.IntDist.init(bits);1403    const val = try RuntimeValue.initNative(allocator, .{ .int_dist = int_dist });14041405    return pureMonad(allocator, val, state);1406}14071408const MkIntWeightedContinuation = struct {1409    pub fn cont(1410        alloc: Allocator,1411        list_val: *RuntimeValue,1412        inner_pc: Bdd,1413        s: *LazyKCState,1414        ctx: anytype,1415    ) CompileError!WorldsResult {1416        _ = inner_pc;1417        const bw = ctx.bitwidth;14181419        const pairs = try extractListForcingThunks(alloc, list_val, s) orelse1420            return programErrorWorlds(s);1421        defer alloc.free(pairs);14221423        if (pairs.len == 0) {1424            return programErrorWorlds(s);1425        }14261427        var values = try alloc.alloc(u64, pairs.len);1428        defer alloc.free(values);1429        var probs = try alloc.alloc(f64, pairs.len);1430        defer alloc.free(probs);14311432        for (pairs, 0..) |pair, i| {1433            const forced_pair = try forceValue(alloc, pair, s);14341435            const p = forced_pair.maybePair() orelse return programErrorWorlds(s);14361437            const forced_fst = try forceValue(alloc, p.fst, s);1438            values[i] = switch (forced_fst.data) {1439                .native => |n| switch (n) {1440                    .int => |iv| @bitCast(iv),1441                    else => return programErrorWorlds(s),1442                },1443                else => return programErrorWorlds(s),1444            };14451446            const forced_snd = try forceValue(alloc, p.snd, s);1447            probs[i] = switch (forced_snd.data) {1448                .native => |n| switch (n) {1449                    .float => |f| f,1450                    else => return programErrorWorlds(s),1451                },1452                else => return programErrorWorlds(s),1453            };1454        }14551456        return createWeightedIntDist(alloc, bw, values, probs, s);1457    }1458};14591460fn compileMkIntWeighted(1461    allocator: Allocator,1462    expr: *PExpr,1463    env: Env,1464    path_condition: Bdd,1465    state: *LazyKCState,1466) !WorldsResult {1467    const bitwidth_expr = expr.args[0];1468    const bitwidth: u6 = switch (bitwidth_expr.head) {1469        .const_native => |n| switch (n) {1470            .int => |i| @intCast(i),1471            else => return programErrorWorlds(state),1472        },1473        else => return programErrorWorlds(state),1474    };14751476    const list_result = try tracedCompileInner(expr.args[1], env, path_condition, state, 0);14771478    return bindMonad(1479        allocator,1480        list_result,1481        path_condition,1482        state,1483        MkIntWeightedContinuation,1484        .{ .bitwidth = bitwidth },1485    );1486}14871488pub fn forceValue(1489    allocator: Allocator,1490    val: *RuntimeValue,1491    state: *LazyKCState,1492) !*RuntimeValue {1493    switch (val.data) {1494        .lazy_kc_thunk, .lazy_kc_thunk_union => {1495            const result = try evaluateThunk(allocator, val, Bdd.TRUE, state);1496            defer freeWorldsSlice(allocator, result.worlds);1497            if (result.worlds.len == 0) return error.PluckError;1498            return result.worlds[0].value;1499        },1500        else => return val,1501    }1502}15031504pub fn forceValueDeterministic(1505    allocator: Allocator,1506    val: *RuntimeValue,1507    state: *LazyKCState,1508) !*RuntimeValue {1509    switch (val.data) {1510        .lazy_kc_thunk, .lazy_kc_thunk_union => {1511            const result = try evaluateThunk(allocator, val, Bdd.TRUE, state);1512            defer freeWorldsSlice(allocator, result.worlds);1513            if (result.worlds.len != 1) return error.PluckError;1514            return result.worlds[0].value;1515        },1516        else => return val,1517    }1518}15191520fn extractListForcingThunks(1521    allocator: Allocator,1522    val: *RuntimeValue,1523    state: *LazyKCState,1524) !?[]*RuntimeValue {1525    var items: std.ArrayList(*RuntimeValue) = .empty;1526    errdefer items.deinit(allocator);15271528    var current = val;1529    while (true) {1530        current = try forceValue(allocator, current, state);15311532        switch (current.data) {1533            .constructed => |c| {1534                if (std.mem.eql(u8, c.constructor, "Nil") and c.args.len == 0) {1535                    const slice = try items.toOwnedSlice(allocator);1536                    return slice;1537                } else if (std.mem.eql(u8, c.constructor, "Cons") and c.args.len == 2) {1538                    const head = try forceValue(allocator, c.args[0], state);1539                    try items.append(allocator, head);1540                    current = c.args[1];1541                } else {1542                    items.deinit(allocator);1543                    return null;1544                }1545            },1546            else => {1547                items.deinit(allocator);1548                return null;1549            },1550        }1551    }1552}15531554pub fn extractNatForcingThunks(1555    allocator: Allocator,1556    val: *RuntimeValue,1557    max_value: i64,1558    state: *LazyKCState,1559) !?i64 {1560    var current = val;1561    var count: i64 = 0;15621563    while (true) {1564        current = try forceValueDeterministic(allocator, current, state);15651566        switch (current.data) {1567            .constructed => |c| {1568                if (std.mem.eql(u8, c.constructor, "O") and c.args.len == 0) {1569                    return count;1570                } else if (std.mem.eql(u8, c.constructor, "S") and c.args.len == 1) {1571                    count += 1;1572                    if (count > max_value) {1573                        return null;1574                    }1575                    current = c.args[0];1576                } else {1577                    return null;1578                }1579            },1580            else => return null,1581        }1582    }1583}15841585fn createWeightedIntDist(1586    allocator: Allocator,1587    bitwidth: u6,1588    values: []const u64,1589    probs: []const f64,1590    state: *LazyKCState,1591) !WorldsResult {1592    const n = values.len;15931594    var total_prob: f64 = 0;1595    for (probs) |p| {1596        if (p < 0 or p != p or std.math.isInf(p)) {1597            return programErrorWorlds(state);1598        }1599        total_prob += p;1600    }1601    if (total_prob <= 0 or @abs(total_prob - 1.0) > 1e-6) {1602        if (total_prob <= 0) {1603            return programErrorWorlds(state);1604        }1605    }16061607    const norm_probs = try allocator.alloc(f64, n);1608    defer allocator.free(norm_probs);1609    for (probs, 0..) |p, i| {1610        norm_probs[i] = p / total_prob;1611    }16121613    if (n == 1) {1614        const bits = try allocator.alloc(Bdd, bitwidth);1615        for (0..bitwidth) |i| {1616            const bit_set = (values[0] >> @intCast(i)) & 1 == 1;1617            bits[i] = if (bit_set) Bdd.TRUE else Bdd.FALSE;1618        }1619        const int_dist = runtime.IntDist.init(bits);1620        const val = try RuntimeValue.initNative(allocator, .{ .int_dist = int_dist });1621        return pureMonad(allocator, val, state);1622    }16231624    const selector_guards = try allocator.alloc(Bdd, n);1625    defer allocator.free(selector_guards);16261627    var remaining_prob: f64 = 1.0;1628    var not_selected_yet = Bdd.TRUE;16291630    for (0..n) |i| {1631        try state_module.pushCallstack(state, @intCast(i + 100));1632        defer state_module.popCallstack(state);16331634        if (i == n - 1) {1635            selector_guards[i] = not_selected_yet;1636        } else {1637            const cond_prob: f64 = if (remaining_prob > 1e-10)1638                norm_probs[i] / remaining_prob1639            else1640                0.5;16411642            const flip_var = try state_module.currentAddress(state, cond_prob);16431644            selector_guards[i] = try state.manager.bddAnd(not_selected_yet, flip_var);16451646            not_selected_yet = try state.manager.bddAnd(not_selected_yet, flip_var.neg());1647            remaining_prob -= norm_probs[i];1648        }1649    }16501651    const bits = try allocator.alloc(Bdd, bitwidth);1652    for (0..bitwidth) |bit_pos| {1653        var bit_bdd = Bdd.FALSE;16541655        for (values, 0..) |value, val_idx| {1656            const bit_set = (value >> @intCast(bit_pos)) & 1 == 1;1657            if (bit_set) {1658                bit_bdd = try state.manager.bddOr(bit_bdd, selector_guards[val_idx]);1659            }1660        }16611662        bits[bit_pos] = bit_bdd;1663    }16641665    const int_dist = runtime.IntDist.init(bits);1666    const val = try RuntimeValue.initNative(allocator, .{ .int_dist = int_dist });16671668    return pureMonad(allocator, val, state);1669}16701671const IntDistEqSecondContinuation = struct {1672    pub fn cont(1673        inner_alloc: Allocator,1674        second_val: *RuntimeValue,1675        _: Bdd,1676        inner_state: *LazyKCState,1677        inner_ctx: anytype,1678    ) CompileError!WorldsResult {1679        const second_int_dist = switch (second_val.data) {1680            .native => |n| switch (n) {1681                .int_dist => |d| d,1682                else => return programErrorWorlds(inner_state),1683            },1684            else => return programErrorWorlds(inner_state),1685        };16861687        const eq_bdd = try inner_ctx.first_dist.eql(second_int_dist, inner_state.manager);16881689        const true_val = try RuntimeValue.initTrue(inner_alloc);1690        const false_val = try RuntimeValue.initFalse(inner_alloc);16911692        return ifThenElseMonad(inner_alloc, true_val, false_val, eq_bdd, inner_state);1693    }1694};16951696const IntDistEqFirstContinuation = struct {1697    pub fn cont(1698        alloc: Allocator,1699        first_val: *RuntimeValue,1700        inner_pc: Bdd,1701        s: *LazyKCState,1702        ctx: anytype,1703    ) CompileError!WorldsResult {1704        const first_int_dist = switch (first_val.data) {1705            .native => |n| switch (n) {1706                .int_dist => |d| d,1707                else => return programErrorWorlds(s),1708            },1709            else => return programErrorWorlds(s),1710        };17111712        const second_result = try tracedCompileInner(ctx.expr.args[1], ctx.env, inner_pc, s, 1);1713        return bindMonad(1714            alloc,1715            second_result,1716            inner_pc,1717            s,1718            IntDistEqSecondContinuation,1719            .{ .first_dist = first_int_dist },1720        );1721    }1722};17231724fn compileIntDistEq(1725    allocator: Allocator,1726    expr: *PExpr,1727    env: Env,1728    path_condition: Bdd,1729    state: *LazyKCState,1730) !WorldsResult {1731    const first_result = try tracedCompileInner(expr.args[0], env, path_condition, state, 0);17321733    return bindMonad(1734        allocator,1735        first_result,1736        path_condition,1737        state,1738        IntDistEqFirstContinuation,1739        .{ .expr = expr, .env = env },1740    );1741}17421743fn makePair(allocator: Allocator, key: *RuntimeValue, value: *RuntimeValue) !*RuntimeValue {1744    const args = try allocator.alloc(*RuntimeValue, 2);1745    args[0] = key;1746    args[1] = value;1747    return RuntimeValue.initConstructed(allocator, "Pair", args);1748}17491750fn makeOptionalInt(allocator: Allocator, maybe_val: ?u64) !*RuntimeValue {1751    if (maybe_val) |val| {1752        const inner = try RuntimeValue.initNative(allocator, .{ .int = @intCast(val) });1753        const args = try allocator.alloc(*RuntimeValue, 1);1754        args[0] = inner;1755        return RuntimeValue.initConstructed(allocator, "Some", args);1756    } else {1757        return RuntimeValue.initConstructed(allocator, "None", &[_]*RuntimeValue{});1758    }1759}17601761fn makeOptionalFloat(allocator: Allocator, maybe_val: ?f64) !*RuntimeValue {1762    if (maybe_val) |val| {1763        const inner = try RuntimeValue.initNative(allocator, .{ .float = val });1764        const args = try allocator.alloc(*RuntimeValue, 1);1765        args[0] = inner;1766        return RuntimeValue.initConstructed(allocator, "Some", args);1767    } else {1768        return RuntimeValue.initConstructed(allocator, "None", &[_]*RuntimeValue{});1769    }1770}17711772const ConfigPrepender = struct {1773    fn prepend(1774        alloc: Allocator,1775        l: *RuntimeValue,1776        key_str: []const u8,1777        val: *RuntimeValue,1778    ) !*RuntimeValue {1779        const key = try RuntimeValue.initNative(alloc, .{ .symbol = key_str });1780        const pair = try makePair(alloc, key, val);1781        const cons_args = try alloc.alloc(*RuntimeValue, 2);1782        cons_args[0] = pair;1783        cons_args[1] = l;1784        return RuntimeValue.initConstructed(alloc, "Cons", cons_args);1785    }1786};17871788fn compileGetConfig(1789    allocator: Allocator,1790    state: *LazyKCState,1791) !WorldsResult {1792    const cfg = state.cfg;17931794    var list = try RuntimeValue.initConstructed(allocator, "Nil", &[_]*RuntimeValue{});17951796    const parallel_wmc_val = if (cfg.parallel_wmc)1797        try RuntimeValue.initTrue(allocator)1798    else1799        try RuntimeValue.initFalse(allocator);1800    list = try ConfigPrepender.prepend(allocator, list, "parallel_wmc", parallel_wmc_val);18011802    const use_strict_order_val = if (cfg.use_strict_order)1803        try RuntimeValue.initTrue(allocator)1804    else1805        try RuntimeValue.initFalse(allocator);1806    list = try ConfigPrepender.prepend(allocator, list, "use_strict_order", use_strict_order_val);18071808    const use_reverse_order_val = if (cfg.use_reverse_order)1809        try RuntimeValue.initTrue(allocator)1810    else1811        try RuntimeValue.initFalse(allocator);1812    list = try ConfigPrepender.prepend(allocator, list, "use_reverse_order", use_reverse_order_val);18131814    const ite_limit_val = try makeOptionalInt(allocator, cfg.ite_limit);1815    list = try ConfigPrepender.prepend(allocator, list, "ite_limit", ite_limit_val);18161817    const time_limit_val = try makeOptionalFloat(allocator, cfg.time_limit);1818    list = try ConfigPrepender.prepend(allocator, list, "time_limit", time_limit_val);18191820    const sample_after_max_depth_val = if (cfg.sample_after_max_depth)1821        try RuntimeValue.initTrue(allocator)1822    else1823        try RuntimeValue.initFalse(allocator);1824    list = try ConfigPrepender.prepend(1825        allocator,1826        list,1827        "sample_after_max_depth",1828        sample_after_max_depth_val,1829    );18301831    const max_depth_u64: ?u64 = if (cfg.max_depth) |d| @as(u64, d) else null;1832    const max_depth_val = try makeOptionalInt(allocator, max_depth_u64);1833    list = try ConfigPrepender.prepend(allocator, list, "max_depth", max_depth_val);18341835    return pureMonad(allocator, list, state);1836}18371838pub fn makeThunk(1839    allocator: Allocator,1840    expr: *PExpr,1841    env: Env,1842    strict_order_index: i32,1843    state: *LazyKCState,1844) !*LazyKCThunk {1845    if (expr.head == .var_ref) {1846        if (env.get(expr.head.var_ref.name)) |v| {1847            if (v.data == .lazy_kc_thunk) {1848                state.stats.thunk_reuse_hits += 1;1849                return v.data.lazy_kc_thunk;1850            }1851        }1852    }1853    state.stats.thunk_reuse_misses += 1;18541855    const thunk = try LazyKCThunk.init(1856        allocator,1857        expr,1858        env,1859        strict_order_index,1860        state.callstack.items,1861    );18621863    if (state.registry) |registry| {1864        try registry.registerWithContext(thunk, expr, state.callstack.items, state.current_def_name);1865    }18661867    return thunk;1868}18691870pub fn evaluateThunk(1871    allocator: Allocator,1872    val: *RuntimeValue,1873    path_condition: Bdd,1874    state: *LazyKCState,1875) !WorldsResult {1876    switch (val.data) {1877        .lazy_kc_thunk => |thunk| return evaluateLazyKCThunk(allocator, thunk, path_condition, state),1878        .lazy_kc_thunk_union => |union_thunk| return evaluateThunkUnion(allocator, union_thunk, path_condition, state),1879        else => return pureMonad(allocator, val, state),1880    }1881}18821883const ThunkCacheContinuation = struct {1884    pub fn cont(1885        alloc: Allocator,1886        hit_cache: *RuntimeValue,1887        inner_pc: Bdd,1888        s: *LazyKCState,1889        ctx: anytype,1890    ) CompileError!WorldsResult {1891        const t = ctx.thunk;1892        const cached_result = ctx.cached;18931894        const is_true = switch (hit_cache.data) {1895            .constructed => |c| std.mem.eql(u8, c.constructor, "True"),1896            else => false,1897        };18981899        if (is_true) {1900            const worlds_copy = try alloc.alloc(World, cached_result.worlds.len);1901            @memcpy(worlds_copy, cached_result.worlds);1902            return WorldsResult{1903                .worlds = worlds_copy,1904                .validity_guard = cached_result.validity_guard,1905            };1906        } else {1907            return evaluateThunkNoCache(alloc, t, inner_pc, s);1908        }1909    }1910};19111912fn evaluateLazyKCThunk(1913    allocator: Allocator,1914    thunk: *LazyKCThunk,1915    path_condition: Bdd,1916    state: *LazyKCState,1917) !WorldsResult {1918    state.stats.thunk_evaluations += 1;19191920    if (path_condition.isFalse()) {1921        return falsePathConditionWorlds(state);1922    }19231924    if (state.cfg.sample_constraint != null) {1925        return evaluateThunkNoCache(allocator, thunk, path_condition, state);1926    }19271928    for (thunk.cache.items) |cached| {1929        const cache_valid_for_path = try state.manager.bddImplies(path_condition, cached.validity_guard);1930        if (cache_valid_for_path.isTrue()) {1931            state.stats.thunk_cache_hits += 1;1932            const worlds_copy = try allocator.alloc(World, cached.worlds.len);1933            @memcpy(worlds_copy, cached.worlds);1934            return WorldsResult{1935                .worlds = worlds_copy,1936                .validity_guard = cached.validity_guard,1937            };1938        }1939    }19401941    if (thunk.cache.items.len == 0) {1942        const result = try evaluateThunkNoCache(allocator, thunk, path_condition, state);1943        const cache_copy = try allocator.alloc(World, result.worlds.len);1944        @memcpy(cache_copy, result.worlds);1945        try thunk.cache.append(allocator, GuardedWorlds{1946            .worlds = cache_copy,1947            .validity_guard = result.validity_guard,1948        });1949        return result;1950    }19511952    const cached = thunk.cache.items[0];1953    const cached_validity_guard = cached.validity_guard;19541955    const true_val = try RuntimeValue.initTrue(allocator);1956    defer true_val.deinit(allocator);1957    const false_val = try RuntimeValue.initFalse(allocator);1958    defer false_val.deinit(allocator);1959    const hit_cache_worlds = try ifThenElseMonad(allocator, true_val, false_val, cached_validity_guard, state);19601961    const extended_pc = try state.manager.bddOr(path_condition, cached_validity_guard);19621963    const result = try bindMonad(1964        allocator,1965        hit_cache_worlds,1966        extended_pc,1967        state,1968        ThunkCacheContinuation,1969        .{ .thunk = thunk, .cached = cached },1970    );19711972    freeWorldsSlice(allocator, thunk.cache.items[0].worlds);1973    const cache_copy = try allocator.alloc(World, result.worlds.len);1974    @memcpy(cache_copy, result.worlds);1975    thunk.cache.items[0] = GuardedWorlds{1976        .worlds = cache_copy,1977        .validity_guard = result.validity_guard,1978    };19791980    return result;1981}19821983fn evaluateThunkNoCache(1984    allocator: Allocator,1985    thunk: *LazyKCThunk,1986    path_condition: Bdd,1987    state: *LazyKCState,1988) CompileError!WorldsResult {1989    const old_callstack = try state.allocator.dupe(i32, state.callstack.items);1990    defer state.allocator.free(old_callstack);19911992    state.callstack.clearRetainingCapacity();1993    try state.callstack.appendSlice(state.allocator, thunk.callstack);1994    defer {1995        state.callstack.clearRetainingCapacity();1996        state.callstack.appendSlice(state.allocator, old_callstack) catch {};1997    }19981999    return switch (thunk.expr) {2000        .pexpr => |e| tracedCompileInner(e, thunk.env, path_condition, state, thunk.strict_order_index),2001        .thunk => |inner| evaluateLazyKCThunk(allocator, inner, path_condition, state),2002    };2003}20042005fn evaluateThunkUnion(2006    allocator: Allocator,2007    union_thunk: *LazyKCThunkUnion,2008    path_condition: Bdd,2009    state: *LazyKCState,2010) !WorldsResult {2011    if (path_condition.isFalse()) {2012        return falsePathConditionWorlds(state);2013    }20142015    var all_worlds: std.ArrayList(World) = .empty;2016    defer all_worlds.deinit(allocator);20172018    var overall_validity_guard = Bdd.TRUE;20192020    for (union_thunk.thunks) |tg| {2021        const inner_pc = try state.manager.bddAnd(path_condition, tg.guard);2022        if (inner_pc.isFalse()) {2023            continue;2024        }20252026        const result = try evaluateLazyKCThunk(allocator, tg.thunk, inner_pc, state);2027        defer freeWorldsSlice(allocator, result.worlds);20282029        for (result.worlds) |world| {2030            const combined_guard = try state.manager.bddAnd(world.guard, tg.guard);2031            try all_worlds.append(allocator, World{ .value = world.value, .guard = combined_guard });2032        }20332034        if (!state.cfg.disable_validity_tracking) {2035            const branch_validity_guard = try state.manager.bddImplies(tg.guard, result.validity_guard);2036            overall_validity_guard = try state.manager.bddAnd(overall_validity_guard, branch_validity_guard);2037        }2038    }20392040    const worlds = try all_worlds.toOwnedSlice(allocator);2041    return WorldsResult{2042        .worlds = worlds,2043        .validity_guard = overall_validity_guard,2044    };2045}20462047pub const CompileResult = struct {2048    weighted_results: []WeightedResult,2049    stats: LazyKCStats,2050    raw_worlds: ?[]World,2051};20522053fn computeWmcDeferredSequential(2054    allocator: Allocator,2055    worlds: []const World,2056    state: *LazyKCState,2057) DeferredWmcError![]WeightedResult {2058    var weighted_results = try allocator.alloc(WeightedResult, worlds.len);2059    errdefer allocator.free(weighted_results);20602061    var caches = DeferredWmcCaches.init(allocator);2062    defer caches.deinit();20632064    for (worlds, 0..) |world, i| {2065        const prob = try wmcWithDeferredCached(state, world.guard, &caches);2066        weighted_results[i] = WeightedResult{2067            .value = world.value,2068            .probability = prob,2069        };2070    }2071    return weighted_results;2072}20732074pub fn compile(2075    allocator: Allocator,2076    cache_allocator: Allocator,2077    expr: *PExpr,2078    definitions: *const Definitions,2079    manager: *Manager,2080    cfg: LazyKCConfig,2081) !CompileResult {2082    const start_time = time.nanoTimestamp();20832084    var state = try state_module.initChecked(allocator, manager, definitions, cfg);2085    defer state_module.deinit(&state);20862087    state.query = expr;2088    state_module.startTimeLimit(&state);2089    defer state_module.stopTimeLimit(&state);20902091    const worlds_result = tracedCompileInner(expr, Env.empty, Bdd.TRUE, &state, 0) catch |err| switch (err) {2092        error.PluckError => {2093            state.stats.program_error = true;2094            state.stats.time_ns = @intCast(@max(0, time.nanoTimestamp() - start_time));2095            return CompileResult{2096                .weighted_results = &[_]WeightedResult{},2097                .stats = state.stats,2098                .raw_worlds = null,2099            };2100        },2101        else => return err,2102    };21032104    if (state.stats.limit_reason != null) {2105        freeWorldsSlice(allocator, worlds_result.worlds);2106        state.stats.time_ns = @intCast(@max(0, time.nanoTimestamp() - start_time));2107        return CompileResult{2108            .weighted_results = &[_]WeightedResult{},2109            .stats = state.stats,2110            .raw_worlds = null,2111        };2112    }21132114    var worlds = worlds_result.worlds;21152116    if (cfg.full_dist) {2117        const new_worlds = try inferFullDistribution(allocator, worlds, &state);2118        freeWorldsSlice(allocator, worlds);2119        worlds = new_worlds;2120    }21212122    if (try processIntDistWorlds(allocator, worlds, manager)) |int_worlds| {2123        freeWorldsSlice(allocator, worlds);2124        worlds = int_worlds;2125    }21262127    const has_deferred = state.deferred_weights.items.len > 0;2128    const use_parallel = !has_deferred and cfg.parallel_wmc and worlds.len >= cfg.parallel_wmc_threshold;2129    const wmc_start = time.nanoTimestamp();2130    defer {2131        const elapsed = time.nanoTimestamp() - wmc_start;2132        state.stats.wmc_time_ns = @intCast(@max(0, elapsed));2133    }21342135    const weighted_results = if (has_deferred)2136        computeWmcDeferredSequential(allocator, worlds, &state) catch |err| switch (err) {2137            error.OutOfMemory => return error.OutOfMemory,2138            error.NodeLimitExceeded => {2139                state.stats.limit_reason = .factor_weight_too_complex;2140                freeWorldsSlice(allocator, worlds);2141                state.stats.time_ns = @intCast(@max(0, time.nanoTimestamp() - start_time));2142                return CompileResult{2143                    .weighted_results = &[_]WeightedResult{},2144                    .stats = state.stats,2145                    .raw_worlds = null,2146                };2147            },2148        }2149    else if (use_parallel)2150        try computeWmcParallel(2151            allocator,2152            cache_allocator,2153            worlds,2154            &state.wmc_params,2155            &state.weight_dd,2156            state.weight_dd_root,2157            cfg.parallel_wmc_threads,2158        )2159    else2160        try computeWmcSequential(2161            allocator,2162            worlds,2163            &state.wmc_params,2164            &state.weight_dd,2165            state.weight_dd_root,2166        );21672168    state_module.recordFinalBddSample(&state);2169    state_module.recordManagerStats(&state);2170    state.stats.time_ns = @intCast(@max(0, time.nanoTimestamp() - start_time));21712172    return CompileResult{2173        .weighted_results = weighted_results,2174        .stats = state.stats,2175        .raw_worlds = worlds,2176    };2177}21782179pub fn processPosteriorQuery(2180    allocator: Allocator,2181    query_thunk: *RuntimeValue,2182    evidence_thunk: *RuntimeValue,2183    state: *LazyKCState,2184) ![]World {2185    const evidence_result = try evaluateThunk(allocator, evidence_thunk, Bdd.TRUE, state);2186    defer freeWorldsSlice(allocator, evidence_result.worlds);21872188    var query_worlds: std.ArrayList(World) = .empty;2189    errdefer {2190        for (query_worlds.items) |w| {2191            _ = w;2192        }2193        query_worlds.deinit(allocator);2194    }21952196    for (evidence_result.worlds) |evidence_world| {2197        if (evidence_world.value.data == .constructed) {2198            const c = evidence_world.value.data.constructed;2199            if (std.mem.eql(u8, c.constructor, "True") and c.args.len == 0) {2200                const query_result = try evaluateThunk(2201                    allocator,2202                    query_thunk,2203                    evidence_world.guard,2204                    state,2205                );2206                defer freeWorldsSlice(allocator, query_result.worlds);22072208                for (query_result.worlds) |query_world| {2209                    const combined_guard = try state.manager.bddAnd(evidence_world.guard, query_world.guard);2210                    if (!combined_guard.isFalse()) {2211                        try query_worlds.append(allocator, World{2212                            .value = query_world.value,2213                            .guard = combined_guard,2214                        });2215                    }2216                }2217            }2218        }2219    }22202221    const initial_worlds = try query_worlds.toOwnedSlice(allocator);2222    defer allocator.free(initial_worlds);22232224    return inferFullDistribution(allocator, initial_worlds, state);2225}22262227pub fn processMarginalQuery(2228    allocator: Allocator,2229    query_thunk: *RuntimeValue,2230    state: *LazyKCState,2231) ![]World {2232    const query_result = try evaluateThunk(allocator, query_thunk, Bdd.TRUE, state);2233    defer freeWorldsSlice(allocator, query_result.worlds);22342235    return inferFullDistribution(allocator, query_result.worlds, state);2236}22372238pub fn inferFullDistribution(2239    allocator: Allocator,2240    initial_worlds: []World,2241    state: *LazyKCState,2242) ![]World {2243    var queue: std.ArrayList(World) = .empty;2244    defer queue.deinit(allocator);22452246    var resolved: std.ArrayList(World) = .empty;2247    defer resolved.deinit(allocator);22482249    var thunk_path: std.ArrayList(usize) = .empty;2250    defer thunk_path.deinit(allocator);22512252    try queue.appendSlice(allocator, initial_worlds);22532254    while (queue.items.len > 0) {2255        if (state.manager.limits.checkTimeLimit()) {2256            state.stats.limit_reason = .time_limit;2257            break;2258        }22592260        const current = queue.pop().?;22612262        if (!try runtime.findFirstThunkInto(allocator, current.value, &thunk_path)) {2263            try resolved.append(allocator, current);2264            continue;2265        }22662267        const path = thunk_path.items;2268        const thunk_val = runtime.getValueAtPath(current.value, path) orelse {2269            try resolved.append(allocator, current);2270            continue;2271        };22722273        const sub_result = try evaluateThunk(allocator, thunk_val, current.guard, state);2274        defer freeWorldsSlice(allocator, sub_result.worlds);22752276        for (sub_result.worlds) |sub_world| {2277            const new_val = try runtime.replaceAtPath(2278                allocator,2279                current.value,2280                path,2281                sub_world.value,2282            );2283            const combined_guard = try state.manager.bddAnd(current.guard, sub_world.guard);2284            try queue.append(allocator, World{ .value = new_val, .guard = combined_guard });2285        }2286    }22872288    return resolved.toOwnedSlice(allocator);2289}22902291test "pure monad" {2292    const allocator = std.testing.allocator;22932294    var manager = try Manager.init(allocator);2295    defer manager.deinit();22962297    var defs = pexpr.Definitions.init(allocator);2298    defer defs.deinit();22992300    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2301    defer state_module.deinit(&state);23022303    const val = try RuntimeValue.initTrue(allocator);2304    defer val.deinit(allocator);23052306    const result = try pureMonad(allocator, val, &state);2307    defer freeWorldsSlice(allocator, result.worlds);23082309    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);2310    try std.testing.expect(result.worlds[0].guard.isTrue());2311}23122313test "if then else monad" {2314    const allocator = std.testing.allocator;23152316    var manager = try Manager.init(allocator);2317    defer manager.deinit();23182319    var defs = pexpr.Definitions.init(allocator);2320    defer defs.deinit();23212322    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2323    defer state_module.deinit(&state);23242325    const true_val = try RuntimeValue.initTrue(allocator);2326    defer true_val.deinit(allocator);23272328    const false_val = try RuntimeValue.initFalse(allocator);2329    defer false_val.deinit(allocator);23302331    const x = try manager.newVar(true);2332    const result = try ifThenElseMonad(allocator, true_val, false_val, x, &state);2333    defer freeWorldsSlice(allocator, result.worlds);23342335    try std.testing.expectEqual(@as(usize, 2), result.worlds.len);2336}23372338test "joinMonad merges structurally identical values - pluck-rs-ui3" {2339    const allocator = std.testing.allocator;23402341    var manager = try Manager.init(allocator);2342    defer manager.deinit();23432344    var defs = pexpr.Definitions.init(allocator);2345    defer defs.deinit();23462347    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2348    defer state_module.deinit(&state);23492350    const true_val1 = try RuntimeValue.initTrue(allocator);2351    defer true_val1.deinit(allocator);23522353    const true_val2 = try RuntimeValue.initTrue(allocator);2354    defer true_val2.deinit(allocator);23552356    try std.testing.expect(true_val1.eql(true_val2));2357    try std.testing.expect(true_val1 != true_val2);23582359    const x = try manager.newVar(true);23602361    const worlds1 = try allocator.alloc(World, 1);2362    worlds1[0] = World{ .value = true_val1, .guard = Bdd.TRUE };23632364    const worlds2 = try allocator.alloc(World, 1);2365    worlds2[0] = World{ .value = true_val2, .guard = Bdd.TRUE };23662367    const nested_worlds = [_]NestedWorld{2368        NestedWorld{2369            .result = WorldsResult{2370                .worlds = worlds1,2371                .validity_guard = Bdd.TRUE,2372            },2373            .guard = x,2374        },2375        NestedWorld{2376            .result = WorldsResult{2377                .worlds = worlds2,2378                .validity_guard = Bdd.TRUE,2379            },2380            .guard = x.neg(),2381        },2382    };23832384    const result = try joinMonad(allocator, &nested_worlds, Bdd.TRUE, &state);2385    defer allocator.free(result.worlds);23862387    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);23882389    try std.testing.expectEqual(Bdd.TRUE, result.worlds[0].guard);2390}23912392test "joinMonad merges identical IntDist values - pluck-rs-ui3" {2393    const allocator = std.testing.allocator;23942395    var manager = try Manager.init(allocator);2396    defer manager.deinit();23972398    var defs = pexpr.Definitions.init(allocator);2399    defer defs.deinit();24002401    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2402    defer state_module.deinit(&state);24032404    const bits1 = try allocator.alloc(Bdd, 8);2405    for (bits1) |*bit| bit.* = Bdd.FALSE;2406    bits1[1] = Bdd.TRUE;2407    bits1[3] = Bdd.TRUE;2408    bits1[5] = Bdd.TRUE;24092410    const bits2 = try allocator.alloc(Bdd, 8);2411    for (bits2) |*bit| bit.* = Bdd.FALSE;2412    bits2[1] = Bdd.TRUE;2413    bits2[3] = Bdd.TRUE;2414    bits2[5] = Bdd.TRUE;24152416    const intdist1 = try RuntimeValue.initNative(allocator, .{ .int_dist = runtime.IntDist.init(bits1) });2417    defer intdist1.deinit(allocator);24182419    const intdist2 = try RuntimeValue.initNative(allocator, .{ .int_dist = runtime.IntDist.init(bits2) });2420    defer intdist2.deinit(allocator);24212422    try std.testing.expect(intdist1.eql(intdist2));2423    try std.testing.expect(intdist1 != intdist2);24242425    const x = try manager.newVar(true);24262427    const worlds1 = try allocator.alloc(World, 1);2428    worlds1[0] = World{ .value = intdist1, .guard = Bdd.TRUE };24292430    const worlds2 = try allocator.alloc(World, 1);2431    worlds2[0] = World{ .value = intdist2, .guard = Bdd.TRUE };24322433    const nested_worlds = [_]NestedWorld{2434        NestedWorld{2435            .result = WorldsResult{ .worlds = worlds1, .validity_guard = Bdd.TRUE },2436            .guard = x,2437        },2438        NestedWorld{2439            .result = WorldsResult{ .worlds = worlds2, .validity_guard = Bdd.TRUE },2440            .guard = x.neg(),2441        },2442    };24432444    const result = try joinMonad(allocator, &nested_worlds, Bdd.TRUE, &state);2445    defer allocator.free(result.worlds);24462447    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);2448    try std.testing.expectEqual(Bdd.TRUE, result.worlds[0].guard);2449}24502451test "joinMonad collapses constructor worlds with thunk unions" {2452    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2453    defer arena.deinit();2454    const allocator = arena.allocator();24552456    var manager = try Manager.init(allocator);2457    defer manager.deinit();24582459    var defs = pexpr.Definitions.init(allocator);2460    defer defs.deinit();24612462    var state = try state_module.initChecked(allocator, &manager, &defs, .{ .use_thunk_unions = true });2463    defer state_module.deinit(&state);24642465    const expr1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });2466    const expr2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });24672468    const thunk1 = try makeThunk(allocator, expr1, Env.empty, 0, &state);2469    const thunk2 = try makeThunk(allocator, expr2, Env.empty, 1, &state);24702471    const thunk_val1 = try RuntimeValue.initLazyKCThunk(allocator, thunk1);2472    const thunk_val2 = try RuntimeValue.initLazyKCThunk(allocator, thunk2);24732474    const args1 = try allocator.alloc(*RuntimeValue, 1);2475    args1[0] = thunk_val1;2476    const val1 = try RuntimeValue.initConstructed(allocator, "Box", args1);24772478    const args2 = try allocator.alloc(*RuntimeValue, 1);2479    args2[0] = thunk_val2;2480    const val2 = try RuntimeValue.initConstructed(allocator, "Box", args2);24812482    try std.testing.expect(!val1.eql(val2));24832484    const x = try manager.newVar(true);24852486    const worlds1 = try allocator.alloc(World, 1);2487    worlds1[0] = World{ .value = val1, .guard = Bdd.TRUE };24882489    const worlds2 = try allocator.alloc(World, 1);2490    worlds2[0] = World{ .value = val2, .guard = Bdd.TRUE };24912492    const nested_worlds = [_]NestedWorld{2493        NestedWorld{2494            .result = WorldsResult{ .worlds = worlds1, .validity_guard = Bdd.TRUE },2495            .guard = x,2496        },2497        NestedWorld{2498            .result = WorldsResult{ .worlds = worlds2, .validity_guard = Bdd.TRUE },2499            .guard = x.neg(),2500        },2501    };25022503    const result = try joinMonad(allocator, &nested_worlds, Bdd.TRUE, &state);2504    defer allocator.free(result.worlds);25052506    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);2507    try std.testing.expectEqual(Bdd.TRUE, result.worlds[0].guard);25082509    const combined = result.worlds[0].value;2510    try std.testing.expect(combined.data == .constructed);2511    const c = combined.data.constructed;2512    try std.testing.expect(std.mem.eql(u8, c.constructor, "Box"));2513    try std.testing.expectEqual(@as(usize, 1), c.args.len);2514    try std.testing.expect(c.args[0].data == .lazy_kc_thunk_union);2515    try std.testing.expectEqual(@as(usize, 2), c.args[0].data.lazy_kc_thunk_union.thunks.len);2516}25172518fn contains_thunk(union_thunk: *LazyKCThunkUnion, thunk: *LazyKCThunk) bool {2519    for (union_thunk.thunks) |tg| {2520        if (tg.thunk == thunk) return true;2521    }2522    return false;2523}25242525test "joinMonad collapses list constructors with thunk unions" {2526    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2527    defer arena.deinit();2528    const allocator = arena.allocator();25292530    var manager = try Manager.init(allocator);2531    defer manager.deinit();25322533    var defs = pexpr.Definitions.init(allocator);2534    defer defs.deinit();25352536    var state = try state_module.initChecked(allocator, &manager, &defs, .{ .use_thunk_unions = true });2537    defer state_module.deinit(&state);25382539    const head_expr1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });2540    const head_expr2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });25412542    const tail_head1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 3 } });2543    const tail_nil1 = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });2544    const tail_expr1 = try pexpr.PExpr.initWithArgs(2545        allocator,2546        .{ .construct = .{ .constructor = "Cons" } },2547        &[_]*pexpr.PExpr{ tail_head1, tail_nil1 },2548    );25492550    const tail_head2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });2551    const tail_nil2 = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });2552    const tail_expr2 = try pexpr.PExpr.initWithArgs(2553        allocator,2554        .{ .construct = .{ .constructor = "Cons" } },2555        &[_]*pexpr.PExpr{ tail_head2, tail_nil2 },2556    );25572558    const head_thunk1 = try makeThunk(allocator, head_expr1, Env.empty, 0, &state);2559    const head_thunk2 = try makeThunk(allocator, head_expr2, Env.empty, 1, &state);2560    const tail_thunk1 = try makeThunk(allocator, tail_expr1, Env.empty, 2, &state);2561    const tail_thunk2 = try makeThunk(allocator, tail_expr2, Env.empty, 3, &state);25622563    const head_val1 = try RuntimeValue.initLazyKCThunk(allocator, head_thunk1);2564    const head_val2 = try RuntimeValue.initLazyKCThunk(allocator, head_thunk2);2565    const tail_val1 = try RuntimeValue.initLazyKCThunk(allocator, tail_thunk1);2566    const tail_val2 = try RuntimeValue.initLazyKCThunk(allocator, tail_thunk2);25672568    const args1 = try allocator.alloc(*RuntimeValue, 2);2569    args1[0] = head_val1;2570    args1[1] = tail_val1;2571    const list1 = try RuntimeValue.initConstructed(allocator, "Cons", args1);25722573    const args2 = try allocator.alloc(*RuntimeValue, 2);2574    args2[0] = head_val2;2575    args2[1] = tail_val2;2576    const list2 = try RuntimeValue.initConstructed(allocator, "Cons", args2);25772578    try std.testing.expect(!list1.eql(list2));25792580    const x = try manager.newVar(true);2581    const worlds1 = try allocator.alloc(World, 1);2582    worlds1[0] = World{ .value = list1, .guard = Bdd.TRUE };25832584    const worlds2 = try allocator.alloc(World, 1);2585    worlds2[0] = World{ .value = list2, .guard = Bdd.TRUE };25862587    const nested_worlds = [_]NestedWorld{2588        NestedWorld{2589            .result = WorldsResult{ .worlds = worlds1, .validity_guard = Bdd.TRUE },2590            .guard = x,2591        },2592        NestedWorld{2593            .result = WorldsResult{ .worlds = worlds2, .validity_guard = Bdd.TRUE },2594            .guard = x.neg(),2595        },2596    };25972598    const result = try joinMonad(allocator, &nested_worlds, Bdd.TRUE, &state);2599    defer allocator.free(result.worlds);26002601    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);2602    try std.testing.expectEqual(Bdd.TRUE, result.worlds[0].guard);26032604    const combined = result.worlds[0].value;2605    try std.testing.expect(combined.data == .constructed);2606    const c = combined.data.constructed;2607    try std.testing.expect(std.mem.eql(u8, c.constructor, "Cons"));2608    try std.testing.expectEqual(@as(usize, 2), c.args.len);26092610    try std.testing.expect(c.args[0].data == .lazy_kc_thunk_union);2611    try std.testing.expect(c.args[1].data == .lazy_kc_thunk_union);26122613    const head_union = c.args[0].data.lazy_kc_thunk_union;2614    const tail_union = c.args[1].data.lazy_kc_thunk_union;26152616    try std.testing.expectEqual(@as(usize, 2), head_union.thunks.len);2617    try std.testing.expectEqual(@as(usize, 2), tail_union.thunks.len);26182619    try std.testing.expect(contains_thunk(head_union, head_thunk1));2620    try std.testing.expect(contains_thunk(head_union, head_thunk2));2621    try std.testing.expect(contains_thunk(tail_union, tail_thunk1));2622    try std.testing.expect(contains_thunk(tail_union, tail_thunk2));26232624    var formatted_buf = std.Io.Writer.Allocating.init(allocator);2625    defer formatted_buf.deinit();2626    try combined.format("", .{}, &formatted_buf.writer);2627    try std.testing.expect(std.mem.indexOf(u8, formatted_buf.written(), "LazyKCThunkUnion") != null);2628}26292630test "joinMonad collapses nested constructors with thunk unions" {2631    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2632    defer arena.deinit();2633    const allocator = arena.allocator();26342635    var manager = try Manager.init(allocator);2636    defer manager.deinit();26372638    var defs = pexpr.Definitions.init(allocator);2639    defer defs.deinit();26402641    var state = try state_module.initChecked(allocator, &manager, &defs, .{ .use_thunk_unions = true });2642    defer state_module.deinit(&state);26432644    const list_head1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 10 } });2645    const list_nil1 = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });2646    const list_expr1 = try pexpr.PExpr.initWithArgs(2647        allocator,2648        .{ .construct = .{ .constructor = "Cons" } },2649        &[_]*pexpr.PExpr{ list_head1, list_nil1 },2650    );26512652    const list_head2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 20 } });2653    const list_nil2 = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });2654    const list_expr2 = try pexpr.PExpr.initWithArgs(2655        allocator,2656        .{ .construct = .{ .constructor = "Cons" } },2657        &[_]*pexpr.PExpr{ list_head2, list_nil2 },2658    );26592660    const pair_left1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });2661    const pair_right1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });2662    const pair_expr1 = try pexpr.PExpr.initWithArgs(2663        allocator,2664        .{ .construct = .{ .constructor = "Pair" } },2665        &[_]*pexpr.PExpr{ pair_left1, pair_right1 },2666    );26672668    const pair_left2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 3 } });2669    const pair_right2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });2670    const pair_expr2 = try pexpr.PExpr.initWithArgs(2671        allocator,2672        .{ .construct = .{ .constructor = "Pair" } },2673        &[_]*pexpr.PExpr{ pair_left2, pair_right2 },2674    );26752676    const left_thunk1 = try makeThunk(allocator, list_expr1, Env.empty, 0, &state);2677    const left_thunk2 = try makeThunk(allocator, list_expr2, Env.empty, 1, &state);2678    const right_thunk1 = try makeThunk(allocator, pair_expr1, Env.empty, 2, &state);2679    const right_thunk2 = try makeThunk(allocator, pair_expr2, Env.empty, 3, &state);26802681    const left_val1 = try RuntimeValue.initLazyKCThunk(allocator, left_thunk1);2682    const left_val2 = try RuntimeValue.initLazyKCThunk(allocator, left_thunk2);2683    const right_val1 = try RuntimeValue.initLazyKCThunk(allocator, right_thunk1);2684    const right_val2 = try RuntimeValue.initLazyKCThunk(allocator, right_thunk2);26852686    const node_args1 = try allocator.alloc(*RuntimeValue, 2);2687    node_args1[0] = left_val1;2688    node_args1[1] = right_val1;2689    const node1 = try RuntimeValue.initConstructed(allocator, "Node", node_args1);26902691    const node_args2 = try allocator.alloc(*RuntimeValue, 2);2692    node_args2[0] = left_val2;2693    node_args2[1] = right_val2;2694    const node2 = try RuntimeValue.initConstructed(allocator, "Node", node_args2);26952696    try std.testing.expect(!node1.eql(node2));26972698    const x = try manager.newVar(true);2699    const worlds1 = try allocator.alloc(World, 1);2700    worlds1[0] = World{ .value = node1, .guard = Bdd.TRUE };27012702    const worlds2 = try allocator.alloc(World, 1);2703    worlds2[0] = World{ .value = node2, .guard = Bdd.TRUE };27042705    const nested_worlds = [_]NestedWorld{2706        NestedWorld{2707            .result = WorldsResult{ .worlds = worlds1, .validity_guard = Bdd.TRUE },2708            .guard = x,2709        },2710        NestedWorld{2711            .result = WorldsResult{ .worlds = worlds2, .validity_guard = Bdd.TRUE },2712            .guard = x.neg(),2713        },2714    };27152716    const result = try joinMonad(allocator, &nested_worlds, Bdd.TRUE, &state);2717    defer allocator.free(result.worlds);27182719    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);2720    try std.testing.expectEqual(Bdd.TRUE, result.worlds[0].guard);27212722    const combined = result.worlds[0].value;2723    try std.testing.expect(combined.data == .constructed);2724    const c = combined.data.constructed;2725    try std.testing.expect(std.mem.eql(u8, c.constructor, "Node"));2726    try std.testing.expectEqual(@as(usize, 2), c.args.len);2727    try std.testing.expect(c.args[0].data == .lazy_kc_thunk_union);2728    try std.testing.expect(c.args[1].data == .lazy_kc_thunk_union);27292730    try std.testing.expectEqual(@as(usize, 2), c.args[0].data.lazy_kc_thunk_union.thunks.len);2731    try std.testing.expectEqual(@as(usize, 2), c.args[1].data.lazy_kc_thunk_union.thunks.len);2732}27332734test "callstack ordering" {2735    const a: []const i32 = &[_]i32{ 1, 2, 3 };2736    const b: []const i32 = &[_]i32{ 1, 2, 4 };2737    const c: []const i32 = &[_]i32{ 1, 2 };27382739    try std.testing.expectEqual(std.math.Order.lt, compareCallstacks(a, b));2740    try std.testing.expectEqual(std.math.Order.gt, compareCallstacks(b, a));2741    try std.testing.expectEqual(std.math.Order.gt, compareCallstacks(a, c));2742    try std.testing.expectEqual(std.math.Order.eq, compareCallstacks(a, a));2743}27442745fn make_callstack(allocator: Allocator, value: i32) ![]i32 {2746    const slice = try allocator.alloc(i32, 1);2747    slice[0] = value;2748    return slice;2749}27502751test "findInsertPosition respects use_reverse_order flag" {2752    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2753    defer arena.deinit();2754    const allocator = arena.allocator();27552756    var manager = try Manager.init(allocator);2757    defer manager.deinit();27582759    var defs = pexpr.Definitions.init(allocator);2760    defer defs.deinit();27612762    {2763        var state = try state_module.initChecked(allocator, &manager, &defs, .{ .use_reverse_order = false });2764        defer state_module.deinit(&state);27652766        const cs1 = try make_callstack(allocator, 1);2767        const cs3 = try make_callstack(allocator, 3);2768        const cs5 = try make_callstack(allocator, 5);2769        try state.sorted_callstacks.append(allocator, .{ .callstack = cs1, .prob = 0.5 });2770        try state.sorted_callstacks.append(allocator, .{ .callstack = cs3, .prob = 0.5 });2771        try state.sorted_callstacks.append(allocator, .{ .callstack = cs5, .prob = 0.5 });27722773        const cs2 = try make_callstack(allocator, 2);2774        const pos2 = state_module.findInsertPosition(&state, .{ .callstack = cs2, .prob = 0.5 });2775        try std.testing.expectEqual(@as(usize, 1), pos2);27762777        const cs0 = try make_callstack(allocator, 0);2778        const pos0 = state_module.findInsertPosition(&state, .{ .callstack = cs0, .prob = 0.5 });2779        try std.testing.expectEqual(@as(usize, 0), pos0);27802781        const cs6 = try make_callstack(allocator, 6);2782        const pos6 = state_module.findInsertPosition(&state, .{ .callstack = cs6, .prob = 0.5 });2783        try std.testing.expectEqual(@as(usize, 3), pos6);2784    }27852786    {2787        var state = try state_module.initChecked(allocator, &manager, &defs, .{ .use_reverse_order = true });2788        defer state_module.deinit(&state);27892790        const cs5 = try make_callstack(allocator, 5);2791        const cs3 = try make_callstack(allocator, 3);2792        const cs1 = try make_callstack(allocator, 1);2793        try state.sorted_callstacks.append(allocator, .{ .callstack = cs5, .prob = 0.5 });2794        try state.sorted_callstacks.append(allocator, .{ .callstack = cs3, .prob = 0.5 });2795        try state.sorted_callstacks.append(allocator, .{ .callstack = cs1, .prob = 0.5 });27962797        const cs4 = try make_callstack(allocator, 4);2798        const pos4 = state_module.findInsertPosition(&state, .{ .callstack = cs4, .prob = 0.5 });2799        try std.testing.expectEqual(@as(usize, 1), pos4);28002801        const cs6 = try make_callstack(allocator, 6);2802        const pos6 = state_module.findInsertPosition(&state, .{ .callstack = cs6, .prob = 0.5 });2803        try std.testing.expectEqual(@as(usize, 0), pos6);28042805        const cs0 = try make_callstack(allocator, 0);2806        const pos0 = state_module.findInsertPosition(&state, .{ .callstack = cs0, .prob = 0.5 });2807        try std.testing.expectEqual(@as(usize, 3), pos0);2808    }2809}28102811test "flip produces path-condition-independent guards" {2812    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2813    defer arena.deinit();2814    const allocator = arena.allocator();28152816    var manager = try Manager.init(allocator);2817    defer manager.deinit();28182819    var defs = pexpr.Definitions.init(allocator);2820    defer defs.deinit();28212822    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2823    defer state_module.deinit(&state);28242825    const prob_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.5 } });2826    const flip_expr = try pexpr.PExpr.initWithArgs(allocator, .flip, &[_]*pexpr.PExpr{prob_expr});28272828    const pc_var = try manager.newVar(true);28292830    const result = try compileInner(flip_expr, Env.empty, pc_var, &state);28312832    try std.testing.expectEqual(@as(usize, 2), result.worlds.len);28332834    const true_guard = result.worlds[0].guard;2835    const false_guard = result.worlds[1].guard;28362837    try std.testing.expect(manager.eq(true_guard.neg(), false_guard));28382839    const implies_pc = try manager.bddImplies(true_guard, pc_var);2840    try std.testing.expect(!implies_pc.isTrue());2841}28422843const BindIdentityContinuation = struct {2844    pub fn cont(2845        alloc: Allocator,2846        value: *RuntimeValue,2847        _: Bdd,2848        state: *LazyKCState,2849        _: anytype,2850    ) CompileError!WorldsResult {2851        return pureMonad(alloc, value, state);2852    }2853};28542855test "bindMonad frees input worlds slice" {2856    const allocator = std.testing.allocator;28572858    var manager = try Manager.init(allocator);2859    defer manager.deinit();28602861    var defs = pexpr.Definitions.init(allocator);2862    defer defs.deinit();28632864    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2865    defer state_module.deinit(&state);28662867    const val1 = try RuntimeValue.initNative(allocator, .{ .int = 1 });2868    const val2 = try RuntimeValue.initNative(allocator, .{ .int = 2 });2869    defer val1.deinit(allocator);2870    defer val2.deinit(allocator);28712872    const input_worlds = try allocator.alloc(World, 2);2873    input_worlds[0] = World{ .value = val1, .guard = Bdd.TRUE };2874    input_worlds[1] = World{ .value = val2, .guard = Bdd.TRUE };28752876    const input = WorldsResult{2877        .worlds = input_worlds,2878        .validity_guard = Bdd.TRUE,2879    };28802881    const result = try bindMonad(allocator, input, Bdd.TRUE, &state, BindIdentityContinuation, {});2882    defer freeWorldsSlice(allocator, result.worlds);28832884    try std.testing.expectEqual(@as(usize, 2), result.worlds.len);2885}28862887test "thunk cache returns equivalent guards on hit" {2888    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2889    defer arena.deinit();2890    const allocator = arena.allocator();28912892    var manager = try Manager.init(allocator);2893    defer manager.deinit();28942895    var defs = pexpr.Definitions.init(allocator);2896    defer defs.deinit();28972898    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2899    defer state_module.deinit(&state);29002901    const val_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 42 } });29022903    const thunk = try makeThunk(allocator, val_expr, Env.empty, 0, &state);29042905    const result1 = try evaluateLazyKCThunk(allocator, thunk, Bdd.TRUE, &state);29062907    try std.testing.expectEqual(@as(usize, 1), thunk.cache.items.len);29082909    const result2 = try evaluateLazyKCThunk(allocator, thunk, Bdd.TRUE, &state);29102911    try std.testing.expectEqual(result1.worlds.len, result2.worlds.len);2912    for (result1.worlds, result2.worlds) |w1, w2| {2913        try std.testing.expect(manager.eq(w1.guard, w2.guard));2914    }2915}29162917test "mk_int creates IntDist with correct bits" {2918    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2919    defer arena.deinit();2920    const allocator = arena.allocator();29212922    var manager = try Manager.init(allocator);2923    defer manager.deinit();29242925    var defs = pexpr.Definitions.init(allocator);2926    defer defs.deinit();29272928    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2929    defer state_module.deinit(&state);29302931    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });2932    const value_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 5 } });2933    const mk_int_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int, &[_]*pexpr.PExpr{ bitwidth_expr, value_expr });29342935    const result = try compileInner(mk_int_expr, Env.empty, Bdd.TRUE, &state);29362937    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);29382939    const val = result.worlds[0].value;2940    try std.testing.expect(val.data == .native);2941    try std.testing.expect(val.data.native == .int_dist);29422943    const int_dist = val.data.native.int_dist;2944    try std.testing.expectEqual(@as(usize, 4), int_dist.bits.len);29452946    try std.testing.expect(int_dist.bits[0].isTrue());2947    try std.testing.expect(int_dist.bits[1].isFalse());2948    try std.testing.expect(int_dist.bits[2].isTrue());2949    try std.testing.expect(int_dist.bits[3].isFalse());2950}29512952test "int_dist_eq with equal values returns True" {2953    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2954    defer arena.deinit();2955    const allocator = arena.allocator();29562957    var manager = try Manager.init(allocator);2958    defer manager.deinit();29592960    var defs = pexpr.Definitions.init(allocator);2961    defer defs.deinit();29622963    var state = try state_module.initChecked(allocator, &manager, &defs, .{});2964    defer state_module.deinit(&state);29652966    const bitwidth_expr1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });2967    const value_expr1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 7 } });2968    const mk_int_expr1 = try pexpr.PExpr.initWithArgs(allocator, .mk_int, &[_]*pexpr.PExpr{ bitwidth_expr1, value_expr1 });29692970    const bitwidth_expr2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });2971    const value_expr2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 7 } });2972    const mk_int_expr2 = try pexpr.PExpr.initWithArgs(allocator, .mk_int, &[_]*pexpr.PExpr{ bitwidth_expr2, value_expr2 });29732974    const eq_expr = try pexpr.PExpr.initWithArgs(allocator, .int_dist_eq, &[_]*pexpr.PExpr{ mk_int_expr1, mk_int_expr2 });29752976    const result = try compileInner(eq_expr, Env.empty, Bdd.TRUE, &state);29772978    try std.testing.expect(result.worlds.len >= 1);29792980    var found_true = false;2981    for (result.worlds) |world| {2982        if (world.value.data == .constructed) {2983            const c = world.value.data.constructed;2984            if (std.mem.eql(u8, c.constructor, "True") and world.guard.isTrue()) {2985                found_true = true;2986            }2987        }2988    }2989    try std.testing.expect(found_true);2990}29912992test "int_dist_eq with different values returns False" {2993    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);2994    defer arena.deinit();2995    const allocator = arena.allocator();29962997    var manager = try Manager.init(allocator);2998    defer manager.deinit();29993000    var defs = pexpr.Definitions.init(allocator);3001    defer defs.deinit();30023003    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3004    defer state_module.deinit(&state);30053006    const bitwidth_expr1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });3007    const value_expr1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 5 } });3008    const mk_int_expr1 = try pexpr.PExpr.initWithArgs(allocator, .mk_int, &[_]*pexpr.PExpr{ bitwidth_expr1, value_expr1 });30093010    const bitwidth_expr2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });3011    const value_expr2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 7 } });3012    const mk_int_expr2 = try pexpr.PExpr.initWithArgs(allocator, .mk_int, &[_]*pexpr.PExpr{ bitwidth_expr2, value_expr2 });30133014    const eq_expr = try pexpr.PExpr.initWithArgs(allocator, .int_dist_eq, &[_]*pexpr.PExpr{ mk_int_expr1, mk_int_expr2 });30153016    const result = try compileInner(eq_expr, Env.empty, Bdd.TRUE, &state);30173018    try std.testing.expect(result.worlds.len >= 1);30193020    var found_false = false;3021    for (result.worlds) |world| {3022        if (world.value.data == .constructed) {3023            const c = world.value.data.constructed;3024            if (std.mem.eql(u8, c.constructor, "False") and world.guard.isTrue()) {3025                found_false = true;3026            }3027        }3028    }3029    try std.testing.expect(found_false);3030}30313032test "pbool with deterministic True" {3033    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3034    defer arena.deinit();3035    const allocator = arena.allocator();30363037    var manager = try Manager.init(allocator);3038    defer manager.deinit();30393040    var defs = pexpr.Definitions.init(allocator);3041    defer defs.deinit();30423043    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3044    defer state_module.deinit(&state);30453046    const true_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "True" } }, &[_]*pexpr.PExpr{});3047    const pbool_expr = try pexpr.PExpr.initWithArgs(allocator, .pbool, &[_]*pexpr.PExpr{true_expr});30483049    const result = try compileInner(pbool_expr, Env.empty, Bdd.TRUE, &state);30503051    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);30523053    const val = result.worlds[0].value;3054    try std.testing.expect(val.data == .constructed);3055    try std.testing.expect(std.mem.eql(u8, val.data.constructed.constructor, "PBool"));30563057    const prob_val = val.data.constructed.args[0];3058    try std.testing.expect(prob_val.data == .native);3059    try std.testing.expect(prob_val.data.native == .float);3060    try std.testing.expectApproxEqAbs(@as(f64, 1.0), prob_val.data.native.float, 1e-10);3061}30623063test "pbool with deterministic False" {3064    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3065    defer arena.deinit();3066    const allocator = arena.allocator();30673068    var manager = try Manager.init(allocator);3069    defer manager.deinit();30703071    var defs = pexpr.Definitions.init(allocator);3072    defer defs.deinit();30733074    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3075    defer state_module.deinit(&state);30763077    const false_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "False" } }, &[_]*pexpr.PExpr{});3078    const pbool_expr = try pexpr.PExpr.initWithArgs(allocator, .pbool, &[_]*pexpr.PExpr{false_expr});30793080    const result = try compileInner(pbool_expr, Env.empty, Bdd.TRUE, &state);30813082    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);30833084    const val = result.worlds[0].value;3085    try std.testing.expect(val.data == .constructed);3086    try std.testing.expect(std.mem.eql(u8, val.data.constructed.constructor, "PBool"));30873088    const prob_val = val.data.constructed.args[0];3089    try std.testing.expect(prob_val.data == .native);3090    try std.testing.expect(prob_val.data.native == .float);3091    try std.testing.expectApproxEqAbs(@as(f64, 0.0), prob_val.data.native.float, 1e-10);3092}30933094test "pbool with flip(0.5)" {3095    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3096    defer arena.deinit();3097    const allocator = arena.allocator();30983099    var manager = try Manager.init(allocator);3100    defer manager.deinit();31013102    var defs = pexpr.Definitions.init(allocator);3103    defer defs.deinit();31043105    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3106    defer state_module.deinit(&state);31073108    const prob_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.5 } });3109    const flip_expr = try pexpr.PExpr.initWithArgs(allocator, .flip, &[_]*pexpr.PExpr{prob_expr});3110    const pbool_expr = try pexpr.PExpr.initWithArgs(allocator, .pbool, &[_]*pexpr.PExpr{flip_expr});31113112    const result = try compileInner(pbool_expr, Env.empty, Bdd.TRUE, &state);31133114    try std.testing.expectEqual(@as(usize, 2), result.worlds.len);31153116    for (result.worlds) |world| {3117        try std.testing.expect(world.value.data == .constructed);3118        try std.testing.expect(std.mem.eql(u8, world.value.data.constructed.constructor, "PBool"));31193120        const prob_val = world.value.data.constructed.args[0];3121        try std.testing.expect(prob_val.data == .native);3122        try std.testing.expect(prob_val.data.native == .float);3123        try std.testing.expectApproxEqAbs(@as(f64, 0.5), prob_val.data.native.float, 1e-10);3124    }3125}31263127test "mk_int_weighted with single value is deterministic" {3128    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3129    defer arena.deinit();3130    const allocator = arena.allocator();31313132    var manager = try Manager.init(allocator);3133    defer manager.deinit();31343135    var defs = pexpr.Definitions.init(allocator);3136    defer defs.deinit();31373138    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3139    defer state_module.deinit(&state);31403141    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });31423143    const pair_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 5 } });3144    const pair_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 1.0 } });3145    const pair_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair_val, pair_prob });31463147    const nil_expr = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });3148    const list_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair_expr, nil_expr });31493150    const mk_int_weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bitwidth_expr, list_expr });31513152    const result = try compileInner(mk_int_weighted_expr, Env.empty, Bdd.TRUE, &state);31533154    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);31553156    const val = result.worlds[0].value;3157    try std.testing.expect(val.data == .native);3158    try std.testing.expect(val.data.native == .int_dist);31593160    const int_dist = val.data.native.int_dist;3161    try std.testing.expectEqual(@as(usize, 4), int_dist.bits.len);31623163    try std.testing.expect(int_dist.bits[0].isTrue());3164    try std.testing.expect(int_dist.bits[1].isFalse());3165    try std.testing.expect(int_dist.bits[2].isTrue());3166    try std.testing.expect(int_dist.bits[3].isFalse());3167}31683169test "mk_int_weighted with two equal probability values" {3170    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3171    defer arena.deinit();3172    const allocator = arena.allocator();31733174    var manager = try Manager.init(allocator);3175    defer manager.deinit();31763177    var defs = pexpr.Definitions.init(allocator);3178    defer defs.deinit();31793180    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3181    defer state_module.deinit(&state);31823183    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });31843185    const pair1_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });3186    const pair1_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.5 } });3187    const pair1_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair1_val, pair1_prob });31883189    const pair2_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });3190    const pair2_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.5 } });3191    const pair2_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair2_val, pair2_prob });31923193    const nil_expr = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });3194    const cons2 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair2_expr, nil_expr });3195    const list_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair1_expr, cons2 });31963197    const mk_int_weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bitwidth_expr, list_expr });31983199    const result = try compileInner(mk_int_weighted_expr, Env.empty, Bdd.TRUE, &state);32003201    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);32023203    const val = result.worlds[0].value;3204    try std.testing.expect(val.data == .native);3205    try std.testing.expect(val.data.native == .int_dist);32063207    const int_dist = val.data.native.int_dist;3208    try std.testing.expectEqual(@as(usize, 4), int_dist.bits.len);32093210    try std.testing.expect(int_dist.bits[2].isFalse());3211    try std.testing.expect(int_dist.bits[3].isFalse());32123213    try std.testing.expect(!int_dist.bits[0].isTrue() and !int_dist.bits[0].isFalse());3214    try std.testing.expect(!int_dist.bits[1].isTrue() and !int_dist.bits[1].isFalse());32153216    try std.testing.expect(manager.eq(int_dist.bits[0], int_dist.bits[1].neg()));3217}32183219test "mk_int_weighted WMC gives correct probabilities" {3220    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3221    defer arena.deinit();3222    const allocator = arena.allocator();32233224    var manager = try Manager.init(allocator);3225    defer manager.deinit();32263227    var defs = pexpr.Definitions.init(allocator);3228    defer defs.deinit();32293230    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3231    defer state_module.deinit(&state);32323233    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });32343235    const pair1_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 3 } });3236    const pair1_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.7 } });3237    const pair1_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair1_val, pair1_prob });32383239    const pair2_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 5 } });3240    const pair2_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.3 } });3241    const pair2_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair2_val, pair2_prob });32423243    const nil_expr = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });3244    const cons2 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair2_expr, nil_expr });3245    const list_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair1_expr, cons2 });32463247    const mk_int_weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bitwidth_expr, list_expr });32483249    const result = try compileInner(mk_int_weighted_expr, Env.empty, Bdd.TRUE, &state);32503251    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);32523253    const val = result.worlds[0].value;3254    try std.testing.expect(val.data == .native);3255    try std.testing.expect(val.data.native == .int_dist);32563257    const int_dist = val.data.native.int_dist;32583259    const p_bit0 = try wmcForState(&state, int_dist.bits[0]);3260    const p_bit1 = try wmcForState(&state, int_dist.bits[1]);3261    const p_bit2 = try wmcForState(&state, int_dist.bits[2]);3262    const p_bit3 = try wmcForState(&state, int_dist.bits[3]);32633264    try std.testing.expectApproxEqAbs(@as(f64, 1.0), p_bit0, 1e-10);32653266    try std.testing.expectApproxEqAbs(@as(f64, 0.7), p_bit1, 1e-10);32673268    try std.testing.expectApproxEqAbs(@as(f64, 0.3), p_bit2, 1e-10);32693270    try std.testing.expectApproxEqAbs(@as(f64, 0.0), p_bit3, 1e-10);3271}32723273test "mk_int_weighted int_dist_eq works correctly" {3274    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3275    defer arena.deinit();3276    const allocator = arena.allocator();32773278    var manager = try Manager.init(allocator);3279    defer manager.deinit();32803281    var defs = pexpr.Definitions.init(allocator);3282    defer defs.deinit();32833284    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3285    defer state_module.deinit(&state);32863287    const bw1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });32883289    const p1_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 3 } });3290    const p1_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.6 } });3291    const p1_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ p1_val, p1_prob });32923293    const p2_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 5 } });3294    const p2_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.4 } });3295    const p2_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ p2_val, p2_prob });32963297    const nil1 = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });3298    const cons2_1 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ p2_expr, nil1 });3299    const list1 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ p1_expr, cons2_1 });33003301    const weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bw1, list1 });33023303    const bw2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });3304    const v2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 3 } });3305    const const_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int, &[_]*pexpr.PExpr{ bw2, v2 });33063307    const eq_expr = try pexpr.PExpr.initWithArgs(allocator, .int_dist_eq, &[_]*pexpr.PExpr{ weighted_expr, const_expr });33083309    const result = try compileInner(eq_expr, Env.empty, Bdd.TRUE, &state);33103311    try std.testing.expectEqual(@as(usize, 2), result.worlds.len);33123313    var p_true: f64 = 0;3314    var p_false: f64 = 0;3315    for (result.worlds) |world| {3316        if (world.value.data == .constructed) {3317            const c = world.value.data.constructed;3318            const prob = try wmcForState(&state, world.guard);3319            if (std.mem.eql(u8, c.constructor, "True")) {3320                p_true = prob;3321            } else if (std.mem.eql(u8, c.constructor, "False")) {3322                p_false = prob;3323            }3324        }3325    }33263327    try std.testing.expectApproxEqAbs(@as(f64, 0.6), p_true, 1e-10);3328    try std.testing.expectApproxEqAbs(@as(f64, 0.4), p_false, 1e-10);3329}33303331test "mk_int_weighted with three values" {3332    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3333    defer arena.deinit();3334    const allocator = arena.allocator();33353336    var manager = try Manager.init(allocator);3337    defer manager.deinit();33383339    var defs = pexpr.Definitions.init(allocator);3340    defer defs.deinit();33413342    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3343    defer state_module.deinit(&state);33443345    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });33463347    const pair1_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });3348    const pair1_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.5 } });3349    const pair1_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair1_val, pair1_prob });33503351    const pair2_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });3352    const pair2_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.3 } });3353    const pair2_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair2_val, pair2_prob });33543355    const pair3_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 3 } });3356    const pair3_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.2 } });3357    const pair3_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair3_val, pair3_prob });33583359    const nil_expr = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });3360    const cons3 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair3_expr, nil_expr });3361    const cons2 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair2_expr, cons3 });3362    const list_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair1_expr, cons2 });33633364    const mk_int_weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bitwidth_expr, list_expr });33653366    const result = try compileInner(mk_int_weighted_expr, Env.empty, Bdd.TRUE, &state);33673368    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);33693370    const val = result.worlds[0].value;3371    try std.testing.expect(val.data == .native);3372    try std.testing.expect(val.data.native == .int_dist);33733374    const int_dist = val.data.native.int_dist;33753376    const p_bit0 = try wmcForState(&state, int_dist.bits[0]);3377    const p_bit1 = try wmcForState(&state, int_dist.bits[1]);3378    const p_bit2 = try wmcForState(&state, int_dist.bits[2]);3379    const p_bit3 = try wmcForState(&state, int_dist.bits[3]);33803381    try std.testing.expectApproxEqAbs(@as(f64, 0.7), p_bit0, 1e-10);3382    try std.testing.expectApproxEqAbs(@as(f64, 0.5), p_bit1, 1e-10);3383    try std.testing.expectApproxEqAbs(@as(f64, 0.0), p_bit2, 1e-10);3384    try std.testing.expectApproxEqAbs(@as(f64, 0.0), p_bit3, 1e-10);3385}33863387test "mk_int_weighted with four values verifies cascade correctness" {3388    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3389    defer arena.deinit();3390    const allocator = arena.allocator();33913392    var manager = try Manager.init(allocator);3393    defer manager.deinit();33943395    var defs = pexpr.Definitions.init(allocator);3396    defer defs.deinit();33973398    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3399    defer state_module.deinit(&state);34003401    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });34023403    const pair0_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 0 } });3404    const pair0_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.1 } });3405    const pair0_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair0_val, pair0_prob });34063407    const pair1_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });3408    const pair1_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.2 } });3409    const pair1_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair1_val, pair1_prob });34103411    const pair2_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });3412    const pair2_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.3 } });3413    const pair2_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair2_val, pair2_prob });34143415    const pair3_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 3 } });3416    const pair3_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.4 } });3417    const pair3_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair3_val, pair3_prob });34183419    const nil_expr = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });3420    const cons3 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair3_expr, nil_expr });3421    const cons2 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair2_expr, cons3 });3422    const cons1 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair1_expr, cons2 });3423    const list_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair0_expr, cons1 });34243425    const mk_int_weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bitwidth_expr, list_expr });34263427    const result = try compileInner(mk_int_weighted_expr, Env.empty, Bdd.TRUE, &state);34283429    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);34303431    const val = result.worlds[0].value;3432    try std.testing.expect(val.data == .native);3433    try std.testing.expect(val.data.native == .int_dist);34343435    const int_dist = val.data.native.int_dist;34363437    const p_bit0 = try wmcForState(&state, int_dist.bits[0]);3438    const p_bit1 = try wmcForState(&state, int_dist.bits[1]);3439    const p_bit2 = try wmcForState(&state, int_dist.bits[2]);3440    const p_bit3 = try wmcForState(&state, int_dist.bits[3]);34413442    try std.testing.expectApproxEqAbs(@as(f64, 0.6), p_bit0, 1e-10);3443    try std.testing.expectApproxEqAbs(@as(f64, 0.7), p_bit1, 1e-10);3444    try std.testing.expectApproxEqAbs(@as(f64, 0.0), p_bit2, 1e-10);3445    try std.testing.expectApproxEqAbs(@as(f64, 0.0), p_bit3, 1e-10);3446}34473448test "mk_int_weighted validates negative probabilities" {3449    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3450    defer arena.deinit();3451    const allocator = arena.allocator();34523453    var manager = try Manager.init(allocator);3454    defer manager.deinit();34553456    var defs = pexpr.Definitions.init(allocator);3457    defer defs.deinit();34583459    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3460    defer state_module.deinit(&state);34613462    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });34633464    const pair1_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });3465    const pair1_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = -0.5 } });3466    const pair1_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair1_val, pair1_prob });34673468    const pair2_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });3469    const pair2_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.5 } });3470    const pair2_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair2_val, pair2_prob });34713472    const nil_expr = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });3473    const cons2 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair2_expr, nil_expr });3474    const list_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair1_expr, cons2 });34753476    const mk_int_weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bitwidth_expr, list_expr });34773478    const result = try compileInner(mk_int_weighted_expr, Env.empty, Bdd.TRUE, &state);34793480    try std.testing.expectEqual(@as(usize, 0), result.worlds.len);3481}34823483test "mk_int_weighted validates infinite probabilities" {3484    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3485    defer arena.deinit();3486    const allocator = arena.allocator();34873488    var manager = try Manager.init(allocator);3489    defer manager.deinit();34903491    var defs = pexpr.Definitions.init(allocator);3492    defer defs.deinit();34933494    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3495    defer state_module.deinit(&state);34963497    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });34983499    const pair1_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });3500    const pair1_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = std.math.inf(f64) } });3501    const pair1_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair1_val, pair1_prob });35023503    const pair2_val = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });3504    const pair2_prob = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.5 } });3505    const pair2_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ pair2_val, pair2_prob });35063507    const nil_expr = try pexpr.PExpr.init(allocator, .{ .construct = .{ .constructor = "Nil" } });3508    const cons2 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair2_expr, nil_expr });3509    const list_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair1_expr, cons2 });35103511    const mk_int_weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bitwidth_expr, list_expr });35123513    const result_inf = try compileInner(mk_int_weighted_expr, Env.empty, Bdd.TRUE, &state);35143515    try std.testing.expectEqual(@as(usize, 0), result_inf.worlds.len);3516}35173518test "parallel WMC respects threshold" {3519    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3520    defer arena.deinit();3521    const allocator = arena.allocator();35223523    var manager = try Manager.init(allocator);3524    defer manager.deinit();35253526    var defs = pexpr.Definitions.init(allocator);3527    defer defs.deinit();35283529    const prob_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.5 } });3530    const flip_expr = try pexpr.PExpr.initWithArgs(allocator, .flip, &[_]*pexpr.PExpr{prob_expr});35313532    const result_seq = try compile(allocator, allocator, flip_expr, &defs, &manager, .{3533        .parallel_wmc = false,3534    });35353536    const result_high_thresh = try compile(allocator, allocator, flip_expr, &defs, &manager, .{3537        .parallel_wmc = true,3538        .parallel_wmc_threshold = 100,3539    });35403541    try std.testing.expectEqual(@as(usize, 2), result_seq.weighted_results.len);3542    try std.testing.expectEqual(@as(usize, 2), result_high_thresh.weighted_results.len);35433544    var total_seq: f64 = 0;3545    var total_high: f64 = 0;3546    for (result_seq.weighted_results) |wr| {3547        total_seq += wr.probability;3548    }3549    for (result_high_thresh.weighted_results) |wr| {3550        total_high += wr.probability;3551    }3552    try std.testing.expectApproxEqAbs(@as(f64, 1.0), total_seq, 1e-10);3553    try std.testing.expectApproxEqAbs(@as(f64, 1.0), total_high, 1e-10);3554}35553556test "thunk cache respects path condition - regression for pluck-rs-0cb" {3557    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3558    defer arena.deinit();3559    const allocator = arena.allocator();35603561    var manager = try Manager.init(allocator);3562    defer manager.deinit();35633564    var defs = pexpr.Definitions.init(allocator);3565    defer defs.deinit();35663567    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3568    defer state_module.deinit(&state);35693570    const b_var = try manager.newVar(true);3571    const not_b_var = b_var.neg();35723573    const expr1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 1 } });3574    const thunk1 = try makeThunk(allocator, expr1, Env.empty, 0, &state);35753576    _ = try evaluateLazyKCThunk(allocator, thunk1, b_var, &state);35773578    try std.testing.expectEqual(@as(usize, 1), thunk1.cache.items.len);3579    try std.testing.expect(thunk1.cache.items[0].validity_guard.isTrue());35803581    const implies_check = try manager.bddImplies(not_b_var, thunk1.cache.items[0].validity_guard);3582    try std.testing.expect(implies_check.isTrue());35833584    const expr2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 42 } });3585    const thunk2 = try makeThunk(allocator, expr2, Env.empty, 0, &state);35863587    _ = try evaluateLazyKCThunk(allocator, thunk2, b_var, &state);3588    try std.testing.expectEqual(@as(usize, 1), thunk2.cache.items.len);35893590    const result2_notb_first = try evaluateLazyKCThunk(allocator, thunk2, not_b_var, &state);35913592    try std.testing.expectEqual(@as(usize, 1), thunk2.cache.items.len);35933594    try std.testing.expect(result2_notb_first.worlds.len >= 1);3595    for (result2_notb_first.worlds) |world| {3596        try std.testing.expectEqual(@as(i64, 42), world.value.data.native.int);3597    }35983599    const result2_b_after = try evaluateLazyKCThunk(allocator, thunk2, b_var, &state);3600    try std.testing.expect(result2_b_after.worlds.len >= 1);3601    for (result2_b_after.worlds) |world| {3602        try std.testing.expectEqual(@as(i64, 42), world.value.data.native.int);3603    }36043605    const d_var = try manager.newVar(true);3606    const e_var = try manager.newVar(true);3607    const expr4 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 77 } });3608    const thunk4 = try makeThunk(allocator, expr4, Env.empty, 0, &state);36093610    _ = try evaluateLazyKCThunk(allocator, thunk4, d_var, &state);3611    try std.testing.expect(thunk4.cache.items[0].validity_guard.isTrue());36123613    const implies_e = try manager.bddImplies(e_var, thunk4.cache.items[0].validity_guard);3614    try std.testing.expect(implies_e.isTrue());36153616    const result4_e = try evaluateLazyKCThunk(allocator, thunk4, e_var, &state);3617    for (result4_e.worlds) |world| {3618        try std.testing.expectEqual(@as(i64, 77), world.value.data.native.int);3619    }36203621    try std.testing.expect(thunk4.cache.items[0].validity_guard.isTrue());36223623    const not_d = d_var.neg();3624    const not_e = e_var.neg();3625    const third_path = try state.manager.bddAnd(not_d, not_e);36263627    const implies_third = try state.manager.bddImplies(third_path, thunk4.cache.items[0].validity_guard);3628    try std.testing.expect(implies_third.isTrue());36293630    const result4_third = try evaluateLazyKCThunk(allocator, thunk4, third_path, &state);3631    for (result4_third.worlds) |world| {3632        try std.testing.expectEqual(@as(i64, 77), world.value.data.native.int);3633    }3634}36353636test "thunk cache - repro program level regression for pluck-rs-0cb" {3637    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3638    defer arena.deinit();3639    const allocator = arena.allocator();36403641    var manager = try Manager.init(allocator);3642    defer manager.deinit();36433644    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);3645    defer types.deinit();36463647    var defs = pexpr.Definitions.init(allocator);3648    defer defs.deinit();36493650    const expr = try pexpr.parseExpr(allocator, "(let [b (flip 0.5) x (if b 1 2)] (case b of True => x | False => x))", &types, &defs);36513652    const result = try compile(allocator, allocator, expr, &defs, &manager, .{ .full_dist = true });36533654    var prob_1: f64 = 0.0;3655    var prob_2: f64 = 0.0;3656    var found_count: usize = 0;36573658    for (result.weighted_results) |wr| {3659        const val = wr.value;3660        if (val.data == .native) {3661            switch (val.data.native) {3662                .int => |int_val| {3663                    found_count += 1;3664                    if (int_val == 1) {3665                        prob_1 += wr.probability;3666                    } else if (int_val == 2) {3667                        prob_2 += wr.probability;3668                    }3669                },3670                else => {},3671            }3672        } else if (val.data == .constructed) {3673            const ctor = val.data.constructed.constructor;3674            if (std.mem.eql(u8, ctor, "S") or std.mem.eql(u8, ctor, "O")) {3675                var nat_val: i64 = 0;3676                var current = val;3677                while (current.data == .constructed and3678                    std.mem.eql(u8, current.data.constructed.constructor, "S"))3679                {3680                    nat_val += 1;3681                    current = current.data.constructed.args[0];3682                }3683                found_count += 1;3684                if (nat_val == 1) {3685                    prob_1 += wr.probability;3686                } else if (nat_val == 2) {3687                    prob_2 += wr.probability;3688                }3689            }3690        }3691    }36923693    try std.testing.expectEqual(@as(usize, 2), found_count);36943695    try std.testing.expectApproxEqAbs(@as(f64, 0.5), prob_1, 1e-10);3696    try std.testing.expectApproxEqAbs(@as(f64, 0.5), prob_2, 1e-10);3697}36983699test "factor supports guarded weights" {3700    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3701    defer arena.deinit();3702    const allocator = arena.allocator();37033704    var manager = try Manager.init(allocator);3705    defer manager.deinit();37063707    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);3708    defer types.deinit();37093710    var defs = pexpr.Definitions.init(allocator);3711    defer defs.deinit();37123713    const expr_src =3714        "(let [b (flip 0.5)] " ++3715        "(case (factor (if b 0.2 0.8)) of Unit => b))";3716    const expr = try pexpr.parseExpr(allocator, expr_src, &types, &defs);37173718    const result = try compile(allocator, allocator, expr, &defs, &manager, .{ .full_dist = true });37193720    var prob_true: f64 = 0.0;3721    var prob_false: f64 = 0.0;3722    var total: f64 = 0.0;3723    for (result.weighted_results) |wr| {3724        total += wr.probability;3725        if (wr.value.isTrue()) prob_true += wr.probability;3726        if (wr.value.isFalse()) prob_false += wr.probability;3727    }37283729    try std.testing.expect(total > 0.0);3730    try std.testing.expectApproxEqAbs(@as(f64, 0.2), prob_true / total, 1e-10);3731    try std.testing.expectApproxEqAbs(@as(f64, 0.8), prob_false / total, 1e-10);3732}37333734test "factor defers WeightDD refinement when node limit is small" {3735    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3736    defer arena.deinit();3737    const allocator = arena.allocator();37383739    var manager = try Manager.init(allocator);3740    defer manager.deinit();37413742    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);3743    defer types.deinit();37443745    var defs = pexpr.Definitions.init(allocator);3746    defer defs.deinit();37473748    const expr_src =3749        "(let [b (flip 0.5)] " ++3750        "(case (factor (if b 0.2 0.8)) of Unit => b))";3751    const expr = try pexpr.parseExpr(allocator, expr_src, &types, &defs);37523753    const result = try compile(allocator, allocator, expr, &defs, &manager, .{3754        .full_dist = true,3755        .factor_max_branches = 1,3756        .weight_dd_max_nodes = 2,3757    });37583759    try std.testing.expect(result.stats.limit_reason == null);37603761    var prob_true: f64 = 0.0;3762    var prob_false: f64 = 0.0;3763    var total: f64 = 0.0;3764    for (result.weighted_results) |wr| {3765        total += wr.probability;3766        if (wr.value.isTrue()) prob_true += wr.probability;3767        if (wr.value.isFalse()) prob_false += wr.probability;3768    }37693770    try std.testing.expect(total > 0.0);3771    try std.testing.expectApproxEqAbs(@as(f64, 0.2), prob_true / total, 1e-10);3772    try std.testing.expectApproxEqAbs(@as(f64, 0.8), prob_false / total, 1e-10);3773}37743775test "factor prunes zero-weight branch" {3776    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3777    defer arena.deinit();3778    const allocator = arena.allocator();37793780    var manager = try Manager.init(allocator);3781    defer manager.deinit();37823783    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);3784    defer types.deinit();37853786    var defs = pexpr.Definitions.init(allocator);3787    defer defs.deinit();37883789    const expr_src =3790        "(let [b (flip 0.5)] " ++3791        "(case (factor (if b 0.0 1.0)) of Unit => b))";3792    const expr = try pexpr.parseExpr(allocator, expr_src, &types, &defs);37933794    const result = try compile(allocator, allocator, expr, &defs, &manager, .{ .full_dist = true });37953796    var prob_true: f64 = 0.0;3797    var prob_false: f64 = 0.0;3798    var total: f64 = 0.0;3799    for (result.weighted_results) |wr| {3800        total += wr.probability;3801        if (wr.value.isTrue()) prob_true += wr.probability;3802        if (wr.value.isFalse()) prob_false += wr.probability;3803    }38043805    try std.testing.expect(total > 0.0);3806    try std.testing.expectApproxEqAbs(@as(f64, 0.0), prob_true / total, 1e-10);3807    try std.testing.expectApproxEqAbs(@as(f64, 1.0), prob_false / total, 1e-10);3808}38093810test "factor WeightDD composes multiple factors" {3811    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3812    defer arena.deinit();3813    const allocator = arena.allocator();38143815    var manager = try Manager.init(allocator);3816    defer manager.deinit();38173818    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);3819    defer types.deinit();38203821    var defs = pexpr.Definitions.init(allocator);3822    defer defs.deinit();38233824    const expr_src =3825        "(let [b (flip 0.5)] " ++3826        "(case (factor (if b 0.2 0.8)) of Unit => " ++3827        "(case (factor (if b 0.5 1.5)) of Unit => b)))";3828    const expr = try pexpr.parseExpr(allocator, expr_src, &types, &defs);38293830    const result = try compile(allocator, allocator, expr, &defs, &manager, .{3831        .full_dist = true,3832        .factor_max_branches = 1,3833    });38343835    var prob_true: f64 = 0.0;3836    var prob_false: f64 = 0.0;3837    var total: f64 = 0.0;3838    for (result.weighted_results) |wr| {3839        total += wr.probability;3840        if (wr.value.isTrue()) prob_true += wr.probability;3841        if (wr.value.isFalse()) prob_false += wr.probability;3842    }38433844    try std.testing.expect(total > 0.0);3845    const norm_true = prob_true / total;3846    const norm_false = prob_false / total;3847    try std.testing.expectApproxEqAbs(@as(f64, 0.07692307692307693), norm_true, 1e-10);3848    try std.testing.expectApproxEqAbs(@as(f64, 0.9230769230769231), norm_false, 1e-10);3849}38503851test "factor WeightDD respects branch guards" {3852    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3853    defer arena.deinit();3854    const allocator = arena.allocator();38553856    var manager = try Manager.init(allocator);3857    defer manager.deinit();38583859    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);3860    defer types.deinit();38613862    var defs = pexpr.Definitions.init(allocator);3863    defer defs.deinit();38643865    const expr_src =3866        "(let [b (flip 0.5) c (flip 0.5)] " ++3867        "(if c (case (factor (if b 0.2 0.8)) of Unit => b) b))";3868    const expr = try pexpr.parseExpr(allocator, expr_src, &types, &defs);38693870    const result = try compile(allocator, allocator, expr, &defs, &manager, .{3871        .full_dist = true,3872        .factor_max_branches = 1,3873    });38743875    var prob_true: f64 = 0.0;3876    var prob_false: f64 = 0.0;3877    var total: f64 = 0.0;3878    for (result.weighted_results) |wr| {3879        total += wr.probability;3880        if (wr.value.isTrue()) prob_true += wr.probability;3881        if (wr.value.isFalse()) prob_false += wr.probability;3882    }38833884    try std.testing.expect(total > 0.0);3885    const norm_true = prob_true / total;3886    const norm_false = prob_false / total;3887    try std.testing.expectApproxEqAbs(@as(f64, 0.4), norm_true, 1e-10);3888    try std.testing.expectApproxEqAbs(@as(f64, 0.6), norm_false, 1e-10);3889}38903891fn expectGuardsCoverAndDisjoint(manager: *Manager, guards: []const GuardedWeight) !void {3892    var coverage = Bdd.FALSE;3893    for (guards) |entry| {3894        coverage = try manager.bddOr(coverage, entry.guard);3895    }3896    try std.testing.expect(coverage.isTrue());38973898    for (guards, 0..) |entry, i| {3899        var j: usize = i + 1;3900        while (j < guards.len) : (j += 1) {3901            const overlap = try manager.bddAnd(entry.guard, guards[j].guard);3902            try std.testing.expect(overlap.isFalse());3903        }3904    }3905}39063907fn expectWeightSet(guards: []const GuardedWeight, expected: []const f64) !void {3908    for (expected) |target| {3909        var found = false;3910        for (guards) |entry| {3911            if (@abs(entry.weight - target) < 1e-12) {3912                found = true;3913                break;3914            }3915        }3916        try std.testing.expect(found);3917    }3918}39193920test "symbolic weight compiler handles boolean chain" {3921    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3922    defer arena.deinit();3923    const allocator = arena.allocator();39243925    var manager = try Manager.init(allocator);3926    defer manager.deinit();39273928    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);3929    defer types.deinit();39303931    var defs = pexpr.Definitions.init(allocator);3932    defer defs.deinit();39333934    const expr_src =3935        "(let [a (flip 0.5) b (flip 0.5)] " ++3936        "(if a 0.2 (if b 0.3 0.5)))";3937    const expr = try pexpr.parseExpr(allocator, expr_src, &types, &defs);39383939    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3940    defer state_module.deinit(&state);39413942    const result = try compileInner(expr, Env.empty, Bdd.TRUE, &state);3943    defer freeWorldsSlice(allocator, result.worlds);39443945    const symbolic = try compileWeightSymbolic(allocator, result.worlds);3946    switch (symbolic) {3947        .ok => |guards| {3948            defer allocator.free(guards);3949            try std.testing.expectEqual(@as(usize, 3), guards.len);3950            try expectWeightSet(guards, &[_]f64{ 0.2, 0.3, 0.5 });3951            try expectGuardsCoverAndDisjoint(&manager, guards);3952        },3953        else => try std.testing.expect(false),3954    }3955}39563957test "symbolic weight compiler handles int_dist_eq" {3958    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3959    defer arena.deinit();3960    const allocator = arena.allocator();39613962    var manager = try Manager.init(allocator);3963    defer manager.deinit();39643965    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);3966    defer types.deinit();3967    try types.defineType("pair", &.{3968        .{ .name = "Pair", .args = &.{ "nat", "nat" } },3969    });39703971    var defs = pexpr.Definitions.init(allocator);3972    defer defs.deinit();39733974    const expr_src =3975        "(let [x (mk_int_weighted @2 [(Pair @1 0.5) (Pair @3 0.5)])] " ++3976        "(if (int_dist_eq x (mk_int @2 @1)) 0.1 0.9))";3977    const expr = try pexpr.parseExpr(allocator, expr_src, &types, &defs);39783979    var state = try state_module.initChecked(allocator, &manager, &defs, .{});3980    defer state_module.deinit(&state);39813982    const result = try compileInner(expr, Env.empty, Bdd.TRUE, &state);3983    defer freeWorldsSlice(allocator, result.worlds);39843985    const symbolic = try compileWeightSymbolic(allocator, result.worlds);3986    switch (symbolic) {3987        .ok => |guards| {3988            defer allocator.free(guards);3989            try std.testing.expectEqual(@as(usize, 2), guards.len);3990            try expectWeightSet(guards, &[_]f64{ 0.1, 0.9 });3991            try expectGuardsCoverAndDisjoint(&manager, guards);3992        },3993        else => try std.testing.expect(false),3994    }3995}39963997test "symbolic weight compiler handles nested if/case" {3998    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);3999    defer arena.deinit();4000    const allocator = arena.allocator();40014002    var manager = try Manager.init(allocator);4003    defer manager.deinit();40044005    var types = try pexpr.TypeRegistry.initWithDefaults(allocator);4006    defer types.deinit();40074008    var defs = pexpr.Definitions.init(allocator);4009    defer defs.deinit();40104011    const expr_src =4012        "(let [b (flip 0.5) c (flip 0.5)] " ++4013        "(case b of True => (if c 0.2 0.4) | " ++4014        "False => (case c of True => 0.6 | False => 0.8)))";4015    const expr = try pexpr.parseExpr(allocator, expr_src, &types, &defs);40164017    var state = try state_module.initChecked(allocator, &manager, &defs, .{});4018    defer state_module.deinit(&state);40194020    const result = try compileInner(expr, Env.empty, Bdd.TRUE, &state);4021    defer freeWorldsSlice(allocator, result.worlds);40224023    const symbolic = try compileWeightSymbolic(allocator, result.worlds);4024    switch (symbolic) {4025        .ok => |guards| {4026            defer allocator.free(guards);4027            try std.testing.expectEqual(@as(usize, 4), guards.len);4028            try expectWeightSet(guards, &[_]f64{ 0.2, 0.4, 0.6, 0.8 });4029            try expectGuardsCoverAndDisjoint(&manager, guards);4030        },4031        else => try std.testing.expect(false),4032    }4033}40344035test "IntDist enumeration - deterministic value" {4036    const allocator = std.testing.allocator;40374038    var manager = try Manager.init(allocator);4039    defer manager.deinit();40404041    var defs = pexpr.Definitions.init(allocator);4042    defer defs.deinit();40434044    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 4 } });4045    const value_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 5 } });4046    const mk_int_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int, &[_]*pexpr.PExpr{ bitwidth_expr, value_expr });4047    defer mk_int_expr.deinit(allocator);40484049    const result = try compile(allocator, allocator, mk_int_expr, &defs, &manager, .{});4050    defer {4051        for (result.weighted_results) |wr| {4052            wr.value.deinit(allocator);4053        }4054        allocator.free(result.weighted_results);4055        if (result.raw_worlds) |worlds| {4056            allocator.free(worlds);4057        }4058    }40594060    try std.testing.expectEqual(@as(usize, 1), result.weighted_results.len);40614062    const wr = result.weighted_results[0];4063    try std.testing.expect(wr.value.data == .native);4064    try std.testing.expect(wr.value.data.native == .int);4065    try std.testing.expectEqual(@as(i64, 5), wr.value.data.native.int);40664067    try std.testing.expectApproxEqAbs(@as(f64, 1.0), wr.probability, 1e-10);4068}40694070test "IntDist enumeration - weighted values" {4071    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);4072    defer arena.deinit();4073    const allocator = arena.allocator();40744075    var manager = try Manager.init(allocator);4076    defer manager.deinit();40774078    var defs = pexpr.Definitions.init(allocator);4079    defer defs.deinit();40804081    const bitwidth_expr = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 3 } });4082    const val1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 2 } });4083    const prob1 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.3 } });4084    const pair1 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ val1, prob1 });4085    const val2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .int = 5 } });4086    const prob2 = try pexpr.PExpr.init(allocator, .{ .const_native = .{ .float = 0.7 } });4087    const pair2 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Pair" } }, &[_]*pexpr.PExpr{ val2, prob2 });4088    const nil = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Nil" } }, &[_]*pexpr.PExpr{});4089    const cons2 = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair2, nil });4090    const pairs_list = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ pair1, cons2 });4091    const mk_int_weighted_expr = try pexpr.PExpr.initWithArgs(allocator, .mk_int_weighted, &[_]*pexpr.PExpr{ bitwidth_expr, pairs_list });40924093    const result = try compile(allocator, allocator, mk_int_weighted_expr, &defs, &manager, .{});40944095    try std.testing.expectEqual(@as(usize, 2), result.weighted_results.len);40964097    var prob_2: f64 = 0;4098    var prob_5: f64 = 0;40994100    for (result.weighted_results) |wr| {4101        if (wr.value.data == .native and wr.value.data.native == .int) {4102            if (wr.value.data.native.int == 2) {4103                prob_2 = wr.probability;4104            } else if (wr.value.data.native.int == 5) {4105                prob_5 = wr.probability;4106            }4107        }4108    }41094110    try std.testing.expectApproxEqAbs(@as(f64, 0.3), prob_2, 1e-10);4111    try std.testing.expectApproxEqAbs(@as(f64, 0.7), prob_5, 1e-10);4112}41134114test "combineIntDists - combines two IntDists under different guards" {4115    const allocator = std.testing.allocator;41164117    var manager = try Manager.init(allocator);4118    defer manager.deinit();41194120    const g = try manager.newVar(true);41214122    const bits1 = try allocator.alloc(Bdd, 3);4123    defer allocator.free(bits1);4124    bits1[0] = Bdd.FALSE;4125    bits1[1] = Bdd.TRUE;4126    bits1[2] = Bdd.FALSE;41274128    const bits2 = try allocator.alloc(Bdd, 3);4129    defer allocator.free(bits2);4130    bits2[0] = Bdd.TRUE;4131    bits2[1] = Bdd.FALSE;4132    bits2[2] = Bdd.TRUE;41334134    const pairs = try allocator.alloc(IntDistWithGuard, 2);4135    defer allocator.free(pairs);4136    pairs[0] = .{ .int_dist = runtime.IntDist.init(bits1), .guard = g };4137    pairs[1] = .{ .int_dist = runtime.IntDist.init(bits2), .guard = g.neg() };41384139    const combined = try combineIntDists(allocator, pairs, &manager);4140    defer allocator.free(combined.int_dist.bits);41414142    try std.testing.expect(combined.overall_guard.isTrue());41434144    try std.testing.expectEqual(combined.int_dist.bits.len, 3);4145    try std.testing.expectEqual(combined.int_dist.bits[0].toRaw(), g.neg().toRaw());4146    try std.testing.expectEqual(combined.int_dist.bits[1].toRaw(), g.toRaw());4147    try std.testing.expectEqual(combined.int_dist.bits[2].toRaw(), g.neg().toRaw());4148}41494150test "enumerateIntDist - deterministic value" {4151    const allocator = std.testing.allocator;41524153    var manager = try Manager.init(allocator);4154    defer manager.deinit();41554156    const bits = try allocator.alloc(Bdd, 2);4157    defer allocator.free(bits);4158    bits[0] = Bdd.TRUE;4159    bits[1] = Bdd.TRUE;41604161    const int_dist = runtime.IntDist.init(bits);41624163    const results = try enumerateIntDist(allocator, int_dist, Bdd.TRUE, &manager);4164    defer {4165        for (results) |world| {4166            world.value.deinit(allocator);4167        }4168        allocator.free(results);4169    }41704171    try std.testing.expectEqual(@as(usize, 1), results.len);4172    try std.testing.expect(results[0].value.data == .native);4173    try std.testing.expect(results[0].value.data.native == .int);4174    try std.testing.expectEqual(@as(i64, 3), results[0].value.data.native.int);4175    try std.testing.expect(results[0].guard.isTrue());4176}41774178test "enumerateIntDist - non-deterministic" {4179    const allocator = std.testing.allocator;41804181    var manager = try Manager.init(allocator);4182    defer manager.deinit();41834184    const x = try manager.newVar(true);41854186    const bits = try allocator.alloc(Bdd, 1);4187    defer allocator.free(bits);4188    bits[0] = x;41894190    const int_dist = runtime.IntDist.init(bits);41914192    const results = try enumerateIntDist(allocator, int_dist, Bdd.TRUE, &manager);4193    defer {4194        for (results) |world| {4195            world.value.deinit(allocator);4196        }4197        allocator.free(results);4198    }41994200    try std.testing.expectEqual(@as(usize, 2), results.len);42014202    var found_0 = false;4203    var found_1 = false;4204    for (results) |world| {4205        const val = world.value.data.native.int;4206        if (val == 0) {4207            try std.testing.expectEqual(world.guard.toRaw(), x.neg().toRaw());4208            found_0 = true;4209        } else if (val == 1) {4210            try std.testing.expectEqual(world.guard.toRaw(), x.toRaw());4211            found_1 = true;4212        }4213    }4214    try std.testing.expect(found_0);4215    try std.testing.expect(found_1);4216}42174218test "get_constructor extracts constructor name from ADT value" {4219    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);4220    defer arena.deinit();4221    const allocator = arena.allocator();42224223    var manager = try Manager.init(allocator);4224    defer manager.deinit();42254226    var defs = pexpr.Definitions.init(allocator);4227    defer defs.deinit();42284229    var state = try state_module.initChecked(allocator, &manager, &defs, .{});4230    defer state_module.deinit(&state);42314232    const true_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "True" } }, &[_]*pexpr.PExpr{});4233    const get_ctor_expr = try pexpr.PExpr.initWithArgs(allocator, .get_constructor, &[_]*pexpr.PExpr{true_expr});42344235    const result = try compileInner(get_ctor_expr, Env.empty, Bdd.TRUE, &state);42364237    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);42384239    const val = result.worlds[0].value;4240    try std.testing.expect(val.data == .native);4241    try std.testing.expect(val.data.native == .symbol);4242    try std.testing.expectEqualStrings("True", val.data.native.symbol);4243}42444245test "get_constructor extracts constructor name from Cons value" {4246    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);4247    defer arena.deinit();4248    const allocator = arena.allocator();42494250    var manager = try Manager.init(allocator);4251    defer manager.deinit();42524253    var defs = pexpr.Definitions.init(allocator);4254    defer defs.deinit();42554256    var state = try state_module.initChecked(allocator, &manager, &defs, .{});4257    defer state_module.deinit(&state);42584259    const o_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "O" } }, &[_]*pexpr.PExpr{});4260    const nil_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Nil" } }, &[_]*pexpr.PExpr{});4261    const cons_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ o_expr, nil_expr });4262    const get_ctor_expr = try pexpr.PExpr.initWithArgs(allocator, .get_constructor, &[_]*pexpr.PExpr{cons_expr});42634264    const result = try compileInner(get_ctor_expr, Env.empty, Bdd.TRUE, &state);42654266    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);42674268    const val = result.worlds[0].value;4269    try std.testing.expect(val.data == .native);4270    try std.testing.expect(val.data.native == .symbol);4271    try std.testing.expectEqualStrings("Cons", val.data.native.symbol);4272}42734274test "get_args extracts empty arguments from nullary constructor" {4275    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);4276    defer arena.deinit();4277    const allocator = arena.allocator();42784279    var manager = try Manager.init(allocator);4280    defer manager.deinit();42814282    var defs = pexpr.Definitions.init(allocator);4283    defer defs.deinit();42844285    var state = try state_module.initChecked(allocator, &manager, &defs, .{});4286    defer state_module.deinit(&state);42874288    const true_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "True" } }, &[_]*pexpr.PExpr{});4289    const get_args_expr = try pexpr.PExpr.initWithArgs(allocator, .get_args, &[_]*pexpr.PExpr{true_expr});42904291    const result = try compileInner(get_args_expr, Env.empty, Bdd.TRUE, &state);42924293    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);42944295    const val = result.worlds[0].value;4296    try std.testing.expect(val.data == .constructed);4297    try std.testing.expectEqualStrings("Nil", val.data.constructed.constructor);4298    try std.testing.expectEqual(@as(usize, 0), val.data.constructed.args.len);4299}43004301test "get_args extracts arguments from Cons constructor" {4302    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);4303    defer arena.deinit();4304    const allocator = arena.allocator();43054306    var manager = try Manager.init(allocator);4307    defer manager.deinit();43084309    var defs = pexpr.Definitions.init(allocator);4310    defer defs.deinit();43114312    var state = try state_module.initChecked(allocator, &manager, &defs, .{});4313    defer state_module.deinit(&state);43144315    const o_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "O" } }, &[_]*pexpr.PExpr{});4316    const nil_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Nil" } }, &[_]*pexpr.PExpr{});4317    const cons_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "Cons" } }, &[_]*pexpr.PExpr{ o_expr, nil_expr });4318    const get_args_expr = try pexpr.PExpr.initWithArgs(allocator, .get_args, &[_]*pexpr.PExpr{cons_expr});43194320    const result = try compileInner(get_args_expr, Env.empty, Bdd.TRUE, &state);43214322    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);43234324    const val = result.worlds[0].value;4325    try std.testing.expect(val.data == .constructed);4326    try std.testing.expectEqualStrings("Cons", val.data.constructed.constructor);4327    try std.testing.expectEqual(@as(usize, 2), val.data.constructed.args.len);43284329    const first = val.data.constructed.args[0];4330    const first_result = try evaluateThunk(allocator, first, Bdd.TRUE, &state);4331    try std.testing.expectEqual(@as(usize, 1), first_result.worlds.len);4332    const first_val = first_result.worlds[0].value;4333    try std.testing.expect(first_val.data == .constructed);4334    try std.testing.expectEqualStrings("O", first_val.data.constructed.constructor);43354336    const rest = val.data.constructed.args[1];4337    const rest_result = try evaluateThunk(allocator, rest, Bdd.TRUE, &state);4338    try std.testing.expectEqual(@as(usize, 1), rest_result.worlds.len);4339    const rest_val = rest_result.worlds[0].value;4340    try std.testing.expect(rest_val.data == .constructed);4341    try std.testing.expectEqualStrings("Cons", rest_val.data.constructed.constructor);43424343    const second = rest_val.data.constructed.args[0];4344    const second_result = try evaluateThunk(allocator, second, Bdd.TRUE, &state);4345    try std.testing.expectEqual(@as(usize, 1), second_result.worlds.len);4346    const second_val = second_result.worlds[0].value;4347    try std.testing.expect(second_val.data == .constructed);4348    try std.testing.expectEqualStrings("Nil", second_val.data.constructed.constructor);43494350    const tail = rest_val.data.constructed.args[1];4351    const tail_result = try evaluateThunk(allocator, tail, Bdd.TRUE, &state);4352    try std.testing.expectEqual(@as(usize, 1), tail_result.worlds.len);4353    const tail_val = tail_result.worlds[0].value;4354    try std.testing.expect(tail_val.data == .constructed);4355    try std.testing.expectEqualStrings("Nil", tail_val.data.constructed.constructor);4356}43574358test "get_args with S(O) returns single-element list" {4359    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);4360    defer arena.deinit();4361    const allocator = arena.allocator();43624363    var manager = try Manager.init(allocator);4364    defer manager.deinit();43654366    var defs = pexpr.Definitions.init(allocator);4367    defer defs.deinit();43684369    var state = try state_module.initChecked(allocator, &manager, &defs, .{});4370    defer state_module.deinit(&state);43714372    const o_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "O" } }, &[_]*pexpr.PExpr{});4373    const s_expr = try pexpr.PExpr.initWithArgs(allocator, .{ .construct = .{ .constructor = "S" } }, &[_]*pexpr.PExpr{o_expr});4374    const get_args_expr = try pexpr.PExpr.initWithArgs(allocator, .get_args, &[_]*pexpr.PExpr{s_expr});43754376    const result = try compileInner(get_args_expr, Env.empty, Bdd.TRUE, &state);43774378    try std.testing.expectEqual(@as(usize, 1), result.worlds.len);43794380    const val = result.worlds[0].value;4381    try std.testing.expect(val.data == .constructed);4382    try std.testing.expectEqualStrings("Cons", val.data.constructed.constructor);4383    try std.testing.expectEqual(@as(usize, 2), val.data.constructed.args.len);43844385    const first = val.data.constructed.args[0];4386    const first_result = try evaluateThunk(allocator, first, Bdd.TRUE, &state);4387    try std.testing.expectEqual(@as(usize, 1), first_result.worlds.len);4388    const first_val = first_result.worlds[0].value;4389    try std.testing.expect(first_val.data == .constructed);4390    try std.testing.expectEqualStrings("O", first_val.data.constructed.constructor);43914392    const rest = val.data.constructed.args[1];4393    const rest_result = try evaluateThunk(allocator, rest, Bdd.TRUE, &state);4394    try std.testing.expectEqual(@as(usize, 1), rest_result.worlds.len);4395    const rest_val = rest_result.worlds[0].value;4396    try std.testing.expect(rest_val.data == .constructed);4397    try std.testing.expectEqualStrings("Nil", rest_val.data.constructed.constructor);4398}43994400test "ThunkRegistry basic operations" {4401    const allocator = std.testing.allocator;44024403    var registry = ThunkRegistry.init(allocator);4404    defer registry.deinit();44054406    var manager = try Manager.init(allocator);4407    defer manager.deinit();44084409    const expr = try PExpr.init(allocator, .{ .const_native = .{ .float = 1.0 } });4410    defer expr.deinit(allocator);44114412    const callstack: []const i32 = &[_]i32{ 0, 1, 2 };4413    const thunk = try LazyKCThunk.init(allocator, expr, Env.empty, 0, callstack);4414    defer thunk.deinit(allocator);44154416    try registry.register(thunk, expr, callstack);44174418    try std.testing.expectEqual(@as(usize, 1), registry.count());44194420    const id = ThunkId.init(expr, callstack);4421    const found = registry.get(id);4422    try std.testing.expect(found != null);4423    try std.testing.expect(found.? == thunk);4424}44254426test "ThunkId stability across lookups" {4427    const allocator = std.testing.allocator;44284429    const expr = try PExpr.init(allocator, .{ .const_native = .{ .float = 42.0 } });4430    defer expr.deinit(allocator);44314432    const callstack1: []const i32 = &[_]i32{ 1, 2, 3 };4433    const callstack2: []const i32 = &[_]i32{ 1, 2, 3 };44344435    const id1 = ThunkId.init(expr, callstack1);4436    const id2 = ThunkId.init(expr, callstack2);44374438    try std.testing.expect(id1.eql(id2));4439    try std.testing.expectEqual(id1.hash(), id2.hash());44404441    const callstack3: []const i32 = &[_]i32{ 1, 2, 4 };4442    const id3 = ThunkId.init(expr, callstack3);4443    try std.testing.expect(!id1.eql(id3));4444}44454446test "ThunkRegistry refineVariable restricts guards" {4447    const allocator = std.testing.allocator;44484449    var manager = try Manager.init(allocator);4450    defer manager.deinit();44514452    var registry = ThunkRegistry.init(allocator);4453    defer registry.deinit();44544455    const expr = try PExpr.init(allocator, .{ .const_native = .{ .float = 1.0 } });4456    defer expr.deinit(allocator);44574458    const callstack: []const i32 = &[_]i32{};4459    const thunk = try LazyKCThunk.init(allocator, expr, Env.empty, 0, callstack);4460    defer thunk.deinit(allocator);44614462    try registry.register(thunk, expr, callstack);44634464    const x = try manager.newVar(true);4465    const y = try manager.newVar(true);44664467    const guard = try manager.bddAnd(x, y);44684469    const dummy_val = try RuntimeValue.initNative(allocator, .{ .int = 42 });4470    defer dummy_val.deinit(allocator);44714472    const worlds_slice = try allocator.alloc(World, 1);4473    worlds_slice[0] = .{ .value = dummy_val, .guard = guard };44744475    try thunk.cache.append(allocator, .{4476        .worlds = worlds_slice,4477        .validity_guard = guard,4478    });44794480    try registry.refineVariable(&manager, 0, true);44814482    try std.testing.expectEqual(@as(usize, 1), thunk.cache.items.len);4483    const new_validity_guard = thunk.cache.items[0].validity_guard;4484    try std.testing.expect(manager.eq(new_validity_guard, y));44854486    const new_world_guard = thunk.cache.items[0].worlds[0].guard;4487    try std.testing.expect(manager.eq(new_world_guard, y));4488}44894490test "ThunkDependencies basic operations" {4491    const allocator = std.testing.allocator;44924493    var deps = ThunkDependencies.init(allocator);4494    defer deps.deinit();44954496    const id1 = ThunkId{ .session = .{ .expr_ptr = 0x1000, .callstack_hash = 100 } };4497    const id2 = ThunkId{ .session = .{ .expr_ptr = 0x2000, .callstack_hash = 200 } };44984499    try deps.addDependency(id1, 0);4500    try deps.addDependency(id1, 1);4501    try deps.addDependency(id2, 1);4502    try deps.addDependency(id2, 2);45034504    const vars1 = deps.getVariables(id1).?;4505    try std.testing.expect(vars1.contains(0));4506    try std.testing.expect(vars1.contains(1));4507    try std.testing.expect(!vars1.contains(2));45084509    const thunks_for_var1 = deps.getThunks(1).?;4510    try std.testing.expect(thunks_for_var1.contains(id1));4511    try std.testing.expect(thunks_for_var1.contains(id2));45124513    const thunks_for_var0 = deps.getThunks(0).?;4514    try std.testing.expect(thunks_for_var0.contains(id1));4515    try std.testing.expect(!thunks_for_var0.contains(id2));4516}45174518test "ThunkDependencies dirty marking" {4519    const allocator = std.testing.allocator;45204521    var deps = ThunkDependencies.init(allocator);4522    defer deps.deinit();45234524    const id1 = ThunkId{ .session = .{ .expr_ptr = 0x1000, .callstack_hash = 100 } };4525    const id2 = ThunkId{ .session = .{ .expr_ptr = 0x2000, .callstack_hash = 200 } };45264527    try deps.addDependency(id1, 0);4528    try deps.addDependency(id1, 1);4529    try deps.addDependency(id2, 1);45304531    try std.testing.expectEqual(@as(usize, 0), deps.dirtyCount());4532    try std.testing.expect(!deps.isDirty(id1));45334534    try deps.markDirty(0);4535    try std.testing.expectEqual(@as(usize, 1), deps.dirtyCount());4536    try std.testing.expect(deps.isDirty(id1));4537    try std.testing.expect(!deps.isDirty(id2));45384539    deps.clearDirty(id1);4540    try std.testing.expectEqual(@as(usize, 0), deps.dirtyCount());45414542    try deps.markDirty(1);4543    try std.testing.expectEqual(@as(usize, 2), deps.dirtyCount());4544    try std.testing.expect(deps.isDirty(id1));4545    try std.testing.expect(deps.isDirty(id2));45464547    deps.clearAllDirty();4548    try std.testing.expectEqual(@as(usize, 0), deps.dirtyCount());4549}45504551test "ThunkDependencies removeThunk cleans up correctly" {4552    const allocator = std.testing.allocator;45534554    var deps = ThunkDependencies.init(allocator);4555    defer deps.deinit();45564557    const id1 = ThunkId{ .session = .{ .expr_ptr = 0x1000, .callstack_hash = 100 } };4558    const id2 = ThunkId{ .session = .{ .expr_ptr = 0x2000, .callstack_hash = 200 } };45594560    try deps.addDependency(id1, 0);4561    try deps.addDependency(id1, 1);4562    try deps.addDependency(id2, 1);45634564    try deps.markDirty(0);4565    try std.testing.expect(deps.isDirty(id1));45664567    deps.removeThunk(id1);45684569    try std.testing.expect(deps.getVariables(id1) == null);45704571    const thunks_for_var0 = deps.getThunks(0).?;4572    try std.testing.expect(!thunks_for_var0.contains(id1));45734574    const thunks_for_var1 = deps.getThunks(1).?;4575    try std.testing.expect(!thunks_for_var1.contains(id1));4576    try std.testing.expect(thunks_for_var1.contains(id2));45774578    try std.testing.expect(!deps.isDirty(id1));4579}45804581test "IncrementalLPSMC init and deinit" {4582    const allocator = std.testing.allocator;4583    var lpsmc = lpsmc_module.init(allocator);4584    defer lpsmc_module.deinit(&lpsmc);45854586    try std.testing.expectEqual(@as(u32, 0), lpsmc.last_iteration_count);4587    try std.testing.expectEqual(@as(f64, 1.0), lpsmc.final_multiplier);4588    try std.testing.expectEqual(@as(usize, 0), lpsmc.subproblem_cache.count());4589    try std.testing.expectEqual(@as(usize, 0), lpsmc.path_choices.count());4590}45914592test "IncrementalLPSMC affectsPathChoices" {4593    const allocator = std.testing.allocator;4594    var lpsmc = lpsmc_module.init(allocator);4595    defer lpsmc_module.deinit(&lpsmc);45964597    var deps = VarLabelSet{};4598    try deps.put(allocator, 1, {});4599    try deps.put(allocator, 2, {});46004601    try lpsmc.path_choices.put(allocator, 0, PathChoice{4602        .top_k_bdd = Bdd.TRUE,4603        .sampled_bdd = null,4604        .sampled_probability = 0.0,4605        .k_used = 1,4606        .ess_ratio = 1.0,4607        .depends_on_vars = deps,4608    });46094610    try std.testing.expect(lpsmc_module.affectsPathChoices(&lpsmc, 1));4611    try std.testing.expect(lpsmc_module.affectsPathChoices(&lpsmc, 2));4612    try std.testing.expect(!lpsmc_module.affectsPathChoices(&lpsmc, 3));4613}46144615test "IncrementalLPSMC getAffectedSubproblems" {4616    const allocator = std.testing.allocator;4617    var lpsmc = lpsmc_module.init(allocator);4618    defer lpsmc_module.deinit(&lpsmc);46194620    try lpsmc_module.recordDependency(&lpsmc, 0, 1);4621    try lpsmc_module.recordDependency(&lpsmc, 1, 1);4622    try lpsmc_module.recordDependency(&lpsmc, 2, 2);46234624    var affected1: std.ArrayList(u32) = .empty;4625    defer affected1.deinit(allocator);4626    try lpsmc_module.getAffectedSubproblems(&lpsmc, 1, &affected1);4627    try std.testing.expectEqual(@as(usize, 2), affected1.items.len);46284629    var affected2: std.ArrayList(u32) = .empty;4630    defer affected2.deinit(allocator);4631    try lpsmc_module.getAffectedSubproblems(&lpsmc, 2, &affected2);4632    try std.testing.expectEqual(@as(usize, 1), affected2.items.len);46334634    var affected3: std.ArrayList(u32) = .empty;4635    defer affected3.deinit(allocator);4636    try lpsmc_module.getAffectedSubproblems(&lpsmc, 3, &affected3);4637    try std.testing.expectEqual(@as(usize, 0), affected3.items.len);4638}46394640test "IncrementalLPSMC clearCaches" {4641    const allocator = std.testing.allocator;4642    var lpsmc = lpsmc_module.init(allocator);4643    defer lpsmc_module.deinit(&lpsmc);46444645    var deps = VarLabelSet{};4646    try deps.put(allocator, 1, {});46474648    try lpsmc.path_choices.put(allocator, 0, PathChoice{4649        .top_k_bdd = Bdd.TRUE,4650        .sampled_bdd = null,4651        .sampled_probability = 0.0,4652        .k_used = 1,4653        .ess_ratio = 1.0,4654        .depends_on_vars = deps,4655    });46564657    try lpsmc_module.recordDependency(&lpsmc, 0, 1);4658    lpsmc.last_iteration_count = 5;4659    lpsmc.final_multiplier = 2.5;46604661    lpsmc_module.clearCaches(&lpsmc);46624663    try std.testing.expectEqual(@as(u32, 0), lpsmc.last_iteration_count);4664    try std.testing.expectEqual(@as(f64, 1.0), lpsmc.final_multiplier);4665    try std.testing.expectEqual(@as(usize, 0), lpsmc.path_choices.count());4666    try std.testing.expectEqual(@as(usize, 0), lpsmc.var_to_subproblems.count());4667}46684669test "LPSMCVarianceStats effective sample size" {4670    var stats = LPSMCVarianceStats{};46714672    try std.testing.expectEqual(@as(f64, 0.0), stats.effectiveSampleSize());4673    try std.testing.expectEqual(@as(f64, 1.0), stats.essRatio());46744675    stats.recordWeight(1.0);4676    stats.recordWeight(1.0);4677    stats.recordWeight(1.0);4678    try std.testing.expectApproxEqAbs(@as(f64, 3.0), stats.effectiveSampleSize(), 0.01);4679    try std.testing.expectApproxEqAbs(@as(f64, 1.0), stats.essRatio(), 0.01);4680}46814682test "LPSMCVarianceStats high variance detection" {4683    var stats = LPSMCVarianceStats{};46844685    stats.recordWeight(1.0);4686    stats.recordWeight(1.0);4687    try std.testing.expect(!stats.isHighVariance(0.5));46884689    var high_var_stats = LPSMCVarianceStats{};4690    high_var_stats.recordWeight(0.1);4691    high_var_stats.recordWeight(0.1);4692    high_var_stats.recordWeight(100.0);4693    try std.testing.expect(high_var_stats.essRatio() < 0.5);4694}46954696test "LPSMCVarianceStats max multiplier tracking" {4697    var stats = LPSMCVarianceStats{};46984699    try std.testing.expectEqual(@as(f64, 1.0), stats.max_multiplier);47004701    stats.recordWeight(2.0);4702    try std.testing.expectEqual(@as(f64, 2.0), stats.max_multiplier);47034704    stats.recordWeight(1.0);4705    try std.testing.expectEqual(@as(f64, 2.0), stats.max_multiplier);47064707    stats.recordWeight(10.0);4708    try std.testing.expectEqual(@as(f64, 10.0), stats.max_multiplier);4709}47104711test "IncrementalLPSMC clearCaches resets variance stats" {4712    const allocator = std.testing.allocator;4713    var lpsmc = lpsmc_module.init(allocator);4714    defer lpsmc_module.deinit(&lpsmc);47154716    lpsmc.variance_stats.recordWeight(5.0);4717    lpsmc.variance_stats.recordWeight(10.0);4718    lpsmc.variance_stats.high_variance_warning = true;47194720    try std.testing.expectEqual(@as(u32, 2), lpsmc.variance_stats.num_samples);4721    try std.testing.expect(lpsmc.variance_stats.high_variance_warning);47224723    lpsmc_module.clearCaches(&lpsmc);47244725    try std.testing.expectEqual(@as(u32, 0), lpsmc.variance_stats.num_samples);4726    try std.testing.expectEqual(@as(f64, 0.0), lpsmc.variance_stats.sum_weights);4727    try std.testing.expect(!lpsmc.variance_stats.high_variance_warning);4728}