Skip to documentation
SLOP

tiny.pluck.bdd

Reference tiny.pluck bdd

Defined in tiny.pluck.

API (26)

Actions

Public operations.

Types and contracts

Public types and contracts.

Values and defaults

Public values and defaults.

No direct callersNo direct callstiny.pluckbdd
Static calls · unresolved targets: unknown · external targets: unknown.

Source

Source: lib/pluck/src/bdd.zig

zig
const std = @import("std");const pretty = @import("pretty");const time = @import("time.zig");const Allocator = std.mem.Allocator;const pretty_json = pretty.json;pub const VarLabel = u32;pub const NO_VAR: VarLabel = std.math.maxInt(VarLabel);pub const VarLabelHashContext = struct {    const K: u64 = 0x517cc1b727220a95;    pub fn hash(_: VarLabelHashContext, key: VarLabel) u64 {        var x = @as(u64, key) *% K;        x ^= x >> 33;        x *%= K;        x ^= x >> 29;        return x;    }    pub fn eql(_: VarLabelHashContext, a: VarLabel, b: VarLabel) bool {        return a == b;    }};pub const VarLabelSet = std.HashMapUnmanaged(VarLabel, void, VarLabelHashContext, 80);pub const NodeIndex = u32;pub const Bdd = packed struct {    index: u31,    complement: bool,    pub const TRUE = Bdd{ .index = 0, .complement = false };    pub const FALSE = Bdd{ .index = 0, .complement = true };    pub fn fromRaw(raw: u32) Bdd {        return @bitCast(raw);    }    pub fn toRaw(self: Bdd) u32 {        return @bitCast(self);    }    pub fn neg(self: Bdd) Bdd {        return Bdd{            .index = self.index,            .complement = !self.complement,        };    }    pub fn isTrue(self: Bdd) bool {        return self.index == 0 and !self.complement;    }    pub fn isFalse(self: Bdd) bool {        return self.index == 0 and self.complement;    }    pub fn isConst(self: Bdd) bool {        return self.index == 0;    }    pub fn toReg(self: Bdd) Bdd {        return Bdd{ .index = self.index, .complement = false };    }    pub fn format(        self: Bdd,        comptime fmt: []const u8,        options: std.fmt.Options,        writer: anytype,    ) !void {        _ = fmt;        _ = options;        if (self.isTrue()) {            try writer.writeAll("T");        } else if (self.isFalse()) {            try writer.writeAll("F");        } else {            if (self.complement) {                try writer.print("!{d}", .{self.index});            } else {                try writer.print("{d}", .{self.index});            }        }    }};pub const Node = struct {    var_label: VarLabel,    low: Bdd,    high: Bdd,    pub fn init(var_label: VarLabel, low: Bdd, high: Bdd) Node {        return Node{            .var_label = var_label,            .low = low,            .high = high,        };    }};const NodeHashContext = struct {    const K: u64 = 0x517cc1b727220a95;    inline fn fxHashWord(h: u64, word: u64) u64 {        return (std.math.rotl(u64, h, 5) ^ word) *% K;    }    pub fn hash(self: @This(), node: Node) u64 {        _ = self;        var h: u64 = 0;        h = fxHashWord(h, @as(u64, node.var_label));        h = fxHashWord(h, @as(u64, node.low.toRaw()));        h = fxHashWord(h, @as(u64, node.high.toRaw()));        return h;    }    pub fn eql(self: @This(), a: Node, b: Node) bool {        _ = self;        return a.var_label == b.var_label and            a.low.toRaw() == b.low.toRaw() and            a.high.toRaw() == b.high.toRaw();    }};const IteKey = struct {    f: u32,    g: u32,    h: u32,    pub fn init(f: Bdd, g: Bdd, h: Bdd) IteKey {        return IteKey{            .f = f.toRaw(),            .g = g.toRaw(),            .h = h.toRaw(),        };    }};const IteKeyHashContext = struct {    const K: u64 = 0x517cc1b727220a95;    inline fn fxHashWord(h: u64, word: u64) u64 {        return (std.math.rotl(u64, h, 5) ^ word) *% K;    }    pub fn hash(self: @This(), key: IteKey) u64 {        _ = self;        var h: u64 = 0;        h = fxHashWord(h, @as(u64, key.f));        h = fxHashWord(h, @as(u64, key.g));        h = fxHashWord(h, @as(u64, key.h));        return h;    }    pub fn eql(self: @This(), a: IteKey, b: IteKey) bool {        _ = self;        return a.f == b.f and a.g == b.g and a.h == b.h;    }};const NormalizedIte = struct {    key: IteKey,    complement_result: bool,    is_const: bool,    const_result: Bdd,    pub fn normalize(f: Bdd, g: Bdd, h: Bdd, lessThan: anytype) NormalizedIte {        var nf = f;        var ng = g;        var nh = h;        if (nf.toRaw() == ng.toRaw()) {            ng = Bdd.TRUE;        }        if (nf.toRaw() == nh.toRaw()) {            nh = Bdd.FALSE;        }        if (nf.neg().toRaw() == nh.toRaw()) {            nh = Bdd.TRUE;        }        if (nf.neg().toRaw() == ng.toRaw()) {            ng = Bdd.FALSE;        }        if (nf.isTrue()) {            return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = ng };        }        if (nf.isFalse()) {            return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = nh };        }        if (ng.isTrue() and nh.isFalse()) {            return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = nf };        }        if (ng.isFalse() and nh.isTrue()) {            return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = nf.neg() };        }        if (ng.toRaw() == nh.toRaw()) {            return NormalizedIte{ .key = undefined, .complement_result = false, .is_const = true, .const_result = ng };        }        if (ng.isTrue() and !nh.isConst() and lessThan.call(nh, nf)) {            const tmp = nf;            nf = nh;            nh = tmp;        } else if (nh.isFalse() and !ng.isConst() and lessThan.call(ng, nf)) {            const tmp = nf;            nf = ng;            ng = tmp;        } else if (nh.isTrue() and !ng.isConst() and lessThan.call(ng, nf)) {            const old_f = nf;            nf = ng.neg();            ng = old_f.neg();        } else if (ng.isFalse() and !nh.isConst() and lessThan.call(nh, nf)) {            const old_f = nf;            nf = nh.neg();            nh = old_f.neg();        } else if (ng.toRaw() == nh.neg().toRaw() and !ng.isConst() and lessThan.call(ng, nf)) {            const tmp = nf;            nf = ng;            ng = tmp;            nh = tmp.neg();        }        var complement = false;        if (nf.complement and !nh.complement) {            nf = nf.neg();            const tmp = ng;            ng = nh;            nh = tmp;        } else if (!nf.complement and ng.complement) {            ng = ng.neg();            nh = nh.neg();            complement = true;        } else if (nf.complement and nh.complement) {            nf = nf.neg();            const tmp = ng;            ng = nh.neg();            nh = tmp.neg();            complement = true;        }        return NormalizedIte{            .key = IteKey.init(nf, ng, nh),            .complement_result = complement,            .is_const = false,            .const_result = Bdd.FALSE,        };    }};const LessThanHelper = struct {    manager: *const Manager,    pub inline fn call(self: LessThanHelper, a: Bdd, b: Bdd) bool {        const va = self.manager.topVar(a);        const vb = self.manager.topVar(b);        return self.manager.lessThan(va, vb);    }};const ConditionKey = struct {    f: u32,    variable: VarLabel,    value: bool,    pub fn init(f: Bdd, variable: VarLabel, value: bool) ConditionKey {        return ConditionKey{            .f = f.toRaw(),            .variable = variable,            .value = value,        };    }};pub const LimitConfig = struct {    time_limit: ?f64,    ite_limit: ?u64,    start_time: ?i64,    start_ite_count: u64,    start_node_count: usize,    start_ite_cache_count: usize,    ite_cache_reservations: usize,    time_limit_exceeded: bool,    ite_limit_exceeded: bool,    pub fn init() LimitConfig {        return LimitConfig{            .time_limit = null,            .ite_limit = null,            .start_time = null,            .start_ite_count = 0,            .start_node_count = 0,            .start_ite_cache_count = 0,            .ite_cache_reservations = 0,            .time_limit_exceeded = false,            .ite_limit_exceeded = false,        };    }    pub fn startTimeLimit(self: *LimitConfig, limit: f64) void {        self.time_limit = limit;        self.start_time = time.milliTimestamp();        self.time_limit_exceeded = false;    }    pub fn stopTimeLimit(self: *LimitConfig) void {        self.time_limit = null;        self.start_time = null;    }    pub fn startIteLimit(        self: *LimitConfig,        limit: u64,        current_count: u64,        node_count: usize,        ite_cache_count: usize,    ) void {        std.debug.assert(self.ite_cache_reservations == 0);        self.ite_limit = limit;        self.start_ite_count = current_count;        self.start_node_count = node_count;        self.start_ite_cache_count = ite_cache_count;        self.ite_cache_reservations = 0;        self.ite_limit_exceeded = false;    }    pub fn stopIteLimit(self: *LimitConfig) void {        std.debug.assert(self.ite_cache_reservations == 0);        self.ite_limit = null;    }    pub fn checkTimeLimit(self: *LimitConfig) bool {        if (self.time_limit) |limit| {            if (self.start_time) |start| {                const now = time.milliTimestamp();                const elapsed_seconds = @as(f64, @floatFromInt(now - start)) / 1000.0;                if (elapsed_seconds >= limit) {                    self.time_limit_exceeded = true;                    return true;                }            }        }        return false;    }    pub fn checkIteLimit(self: *LimitConfig, current_count: u64) bool {        if (self.ite_limit) |limit| {            if (current_count -| self.start_ite_count >= limit) {                self.ite_limit_exceeded = true;                return true;            }        }        return false;    }    pub fn checkNodeGrowth(self: *LimitConfig, current_count: usize) bool {        if (self.ite_limit) |limit| {            const growth: u64 = @intCast(current_count -| self.start_node_count);            if (growth >= limit) {                self.ite_limit_exceeded = true;                return true;            }        }        return false;    }    pub fn reserveIteCacheGrowth(self: *LimitConfig, current_count: usize) bool {        if (self.ite_limit) |limit| {            const growth: u64 = @intCast(current_count -| self.start_ite_cache_count);            const reserved: u64 = @intCast(self.ite_cache_reservations);            if (growth +| reserved >= limit) {                self.ite_limit_exceeded = true;                return true;            }            if (self.ite_cache_reservations == std.math.maxInt(usize)) {                self.ite_limit_exceeded = true;                return true;            }            self.ite_cache_reservations += 1;        }        return false;    }    pub fn releaseIteCacheGrowth(self: *LimitConfig) void {        if (self.ite_limit == null) return;        std.debug.assert(self.ite_cache_reservations > 0);        self.ite_cache_reservations -= 1;    }    pub fn boundedAllocationFailed(self: *LimitConfig) bool {        if (self.ite_limit == null) return false;        self.ite_limit_exceeded = true;        return true;    }};pub const SiftConfig = struct {    max_distance: u32 = 5,    max_blowup: f64 = 2.0,    time_limit_ms: u64 = 10,};pub const SiftResult = struct {    original_pos: u32,    final_pos: u32,    size_delta: i64,    aborted: bool,};pub const GlobalSiftResult = struct {    total_size_delta: i64,    vars_sifted: u32,    vars_improved: u32,    original_size: usize,    final_size: usize,};pub const Manager = struct {    const TABLE_MAX_LOAD_PERCENTAGE = 80;    allocator: Allocator,    nodes: std.ArrayListUnmanaged(Node),    unique_table: std.HashMapUnmanaged(Node, NodeIndex, NodeHashContext, TABLE_MAX_LOAD_PERCENTAGE),    unique_table_grow_at: usize,    ite_cache: std.HashMapUnmanaged(IteKey, Bdd, IteKeyHashContext, TABLE_MAX_LOAD_PERCENTAGE),    ite_cache_grow_at: usize,    condition_cache: std.AutoHashMapUnmanaged(ConditionKey, Bdd),    var_order: std.ArrayListUnmanaged(u32),    min_vars: std.ArrayListUnmanaged(VarLabel),    max_vars: std.ArrayListUnmanaged(VarLabel),    num_recursive_calls: u64,    ite_cache_hits: u64,    ite_cache_misses: u64,    unique_table_grows: u64,    ite_cache_grows: u64,    limits: LimitConfig,    const INITIAL_MANAGER_CAPACITY = 4096;    const INITIAL_CONDITION_CACHE_CAPACITY = 256;    fn tableLoadThreshold(capacity: usize) usize {        return (capacity * TABLE_MAX_LOAD_PERCENTAGE) / 100;    }    pub fn init(allocator: Allocator) !Manager {        var nodes = std.ArrayListUnmanaged(Node).empty;        errdefer nodes.deinit(allocator);        var min_vars = std.ArrayListUnmanaged(VarLabel).empty;        errdefer min_vars.deinit(allocator);        var max_vars = std.ArrayListUnmanaged(VarLabel).empty;        errdefer max_vars.deinit(allocator);        try nodes.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);        try min_vars.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);        try max_vars.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);        try nodes.append(allocator, Node.init(NO_VAR, Bdd.TRUE, Bdd.TRUE));        try min_vars.append(allocator, NO_VAR);        try max_vars.append(allocator, NO_VAR);        var unique_table = std.HashMapUnmanaged(Node, NodeIndex, NodeHashContext, TABLE_MAX_LOAD_PERCENTAGE){};        errdefer unique_table.deinit(allocator);        try unique_table.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);        var ite_cache = std.HashMapUnmanaged(IteKey, Bdd, IteKeyHashContext, TABLE_MAX_LOAD_PERCENTAGE){};        errdefer ite_cache.deinit(allocator);        try ite_cache.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);        var condition_cache = std.AutoHashMapUnmanaged(ConditionKey, Bdd){};        errdefer condition_cache.deinit(allocator);        try condition_cache.ensureTotalCapacity(allocator, INITIAL_CONDITION_CACHE_CAPACITY);        return Manager{            .allocator = allocator,            .nodes = nodes,            .unique_table = unique_table,            .unique_table_grow_at = tableLoadThreshold(unique_table.capacity()),            .ite_cache = ite_cache,            .ite_cache_grow_at = tableLoadThreshold(ite_cache.capacity()),            .condition_cache = condition_cache,            .var_order = std.ArrayListUnmanaged(u32).empty,            .min_vars = min_vars,            .max_vars = max_vars,            .num_recursive_calls = 0,            .ite_cache_hits = 0,            .ite_cache_misses = 0,            .unique_table_grows = 0,            .ite_cache_grows = 0,            .limits = LimitConfig.init(),        };    }    pub fn deinit(self: *Manager) void {        self.nodes.deinit(self.allocator);        self.unique_table.deinit(self.allocator);        self.ite_cache.deinit(self.allocator);        self.condition_cache.deinit(self.allocator);        self.var_order.deinit(self.allocator);        self.min_vars.deinit(self.allocator);        self.max_vars.deinit(self.allocator);    }    pub fn numVars(self: *const Manager) usize {        return self.var_order.items.len;    }    pub fn newVar(self: *Manager, polarity: bool) Allocator.Error!Bdd {        const label: VarLabel = @intCast(self.var_order.items.len);        const node = Node.init(label, Bdd.FALSE, Bdd.TRUE);        if (!try self.prepareVariableInsert(node)) return Bdd.FALSE;        self.var_order.appendAssumeCapacity(label);        const bdd = self.insertCanonicalAssumeCapacity(node);        return if (polarity) bdd else bdd.neg();    }    pub fn newVarAtPosition(self: *Manager, position: u32, polarity: bool) Allocator.Error!Bdd {        const label: VarLabel = @intCast(self.var_order.items.len);        const node = Node.init(label, Bdd.FALSE, Bdd.TRUE);        if (!try self.prepareVariableInsert(node)) return Bdd.FALSE;        for (self.var_order.items) |*pos| {            if (pos.* >= position) {                pos.* += 1;            }        }        self.var_order.appendAssumeCapacity(position);        const bdd = self.insertCanonicalAssumeCapacity(node);        return if (polarity) bdd else bdd.neg();    }    fn prepareVariableInsert(self: *Manager, node: Node) Allocator.Error!bool {        std.debug.assert(self.unique_table.getContext(node, NodeHashContext{}) == null);        if (self.limits.checkNodeGrowth(self.nodes.items.len)) return false;        self.ensureCanonicalInsertCapacity() catch |err| {            if (self.limits.boundedAllocationFailed()) return false;            return err;        };        self.var_order.ensureUnusedCapacity(self.allocator, 1) catch |err| {            if (self.limits.boundedAllocationFailed()) return false;            return err;        };        return true;    }    fn getOrInsert(self: *Manager, node: Node) Allocator.Error!Bdd {        if (node.low.toRaw() == node.high.toRaw()) {            return node.low;        }        if (node.high.complement) {            const canonical = Node.init(                node.var_label,                node.low.neg(),                node.high.neg(),            );            return (try self.insertCanonical(canonical)).neg();        } else {            return self.insertCanonical(node);        }    }    fn insertCanonical(self: *Manager, node: Node) Allocator.Error!Bdd {        if (self.unique_table.getContext(node, NodeHashContext{})) |index| {            return Bdd{ .index = @intCast(index), .complement = false };        }        if (self.limits.checkNodeGrowth(self.nodes.items.len)) return Bdd.FALSE;        self.ensureCanonicalInsertCapacity() catch |err| {            if (self.limits.boundedAllocationFailed()) return Bdd.FALSE;            return err;        };        return self.insertCanonicalAssumeCapacity(node);    }    fn insertCanonicalAssumeCapacity(self: *Manager, node: Node) Bdd {        const entry = self.unique_table.getOrPutAssumeCapacityContext(node, NodeHashContext{});        std.debug.assert(!entry.found_existing);        const idx: u31 = @intCast(self.nodes.items.len);        self.nodes.appendAssumeCapacity(node);        const low_min = self.min_vars.items[node.low.index];        const low_max = self.max_vars.items[node.low.index];        const high_min = self.min_vars.items[node.high.index];        const high_max = self.max_vars.items[node.high.index];        var min_var = node.var_label;        if (low_min != NO_VAR and low_min < min_var) min_var = low_min;        if (high_min != NO_VAR and high_min < min_var) min_var = high_min;        var max_var = node.var_label;        if (low_max != NO_VAR and low_max > max_var) max_var = low_max;        if (high_max != NO_VAR and high_max > max_var) max_var = high_max;        self.min_vars.appendAssumeCapacity(min_var);        self.max_vars.appendAssumeCapacity(max_var);        entry.value_ptr.* = idx;        return Bdd{ .index = idx, .complement = false };    }    fn ensureCanonicalInsertCapacity(self: *Manager) Allocator.Error!void {        if (self.nodes.items.len >= self.nodes.capacity) {            const reserve = @max(self.nodes.capacity, INITIAL_MANAGER_CAPACITY);            const target = self.nodes.items.len + reserve;            try self.nodes.ensureTotalCapacity(self.allocator, target);            try self.min_vars.ensureTotalCapacity(self.allocator, target);            try self.max_vars.ensureTotalCapacity(self.allocator, target);        }        const count = self.unique_table.count();        if (count < self.unique_table_grow_at) return;        const capacity = self.unique_table.capacity();        const reserve = @max(capacity, INITIAL_MANAGER_CAPACITY);        try self.unique_table.ensureTotalCapacity(self.allocator, count + reserve);        self.unique_table_grows += 1;        self.unique_table_grow_at = tableLoadThreshold(self.unique_table.capacity());    }    pub inline fn getNode(self: *const Manager, bdd: Bdd) Node {        return self.nodes.items[bdd.index];    }    pub inline fn topVar(self: *const Manager, bdd: Bdd) VarLabel {        if (bdd.isConst()) return NO_VAR;        return self.getNode(bdd).var_label;    }    pub fn getMinVar(self: *const Manager, bdd: Bdd) VarLabel {        return self.min_vars.items[bdd.index];    }    pub fn getMaxVar(self: *const Manager, bdd: Bdd) VarLabel {        return self.max_vars.items[bdd.index];    }    pub fn low(self: *const Manager, bdd: Bdd) Bdd {        if (bdd.isConst()) return Bdd.FALSE;        const node = self.getNode(bdd);        return if (bdd.complement) node.low.neg() else node.low;    }    pub fn high(self: *const Manager, bdd: Bdd) Bdd {        if (bdd.isConst()) return Bdd.FALSE;        const node = self.getNode(bdd);        return if (bdd.complement) node.high.neg() else node.high;    }    inline fn lessThan(self: *const Manager, a: VarLabel, b: VarLabel) bool {        if (a == NO_VAR) return false;        if (b == NO_VAR) return true;        return self.var_order.items[a] < self.var_order.items[b];    }    inline fn firstEssential(self: *const Manager, f: Bdd, g: Bdd, h: Bdd) VarLabel {        const vf = self.topVar(f);        const vg = self.topVar(g);        const vh = self.topVar(h);        var result = vf;        if (self.lessThan(vg, result)) result = vg;        if (self.lessThan(vh, result)) result = vh;        return result;    }    inline fn conditionEssential(self: *const Manager, f: Bdd, lbl: VarLabel, value: bool) Bdd {        if (f.isConst()) return f;        const node = self.getNode(f);        if (node.var_label != lbl) return f;        const result = if (value) node.high else node.low;        return if (f.complement) result.neg() else result;    }    pub fn checkLimits(self: *Manager) bool {        if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) return true;        if (self.limits.checkIteLimit(self.num_recursive_calls)) {            return true;        }        if (self.num_recursive_calls % 1000 == 0) {            if (self.limits.checkTimeLimit()) {                return true;            }        }        return false;    }    pub fn iteLimitExceeded(self: *const Manager) bool {        return self.limits.ite_limit_exceeded;    }    pub fn timeLimitExceeded(self: *const Manager) bool {        return self.limits.time_limit_exceeded;    }    pub fn setTimeLimit(self: *Manager, limit_seconds: f64) void {        self.limits.time_limit = limit_seconds;        self.limits.time_limit_exceeded = false;    }    pub fn startTimeLimit(self: *Manager, limit_seconds: f64) void {        self.limits.startTimeLimit(limit_seconds);    }    pub fn stopTimeLimit(self: *Manager) void {        self.limits.stopTimeLimit();    }    pub fn resetLimitFlags(self: *Manager) void {        self.limits.time_limit_exceeded = false;        self.limits.ite_limit_exceeded = false;    }    pub fn startIteLimit(self: *Manager, limit: u64) void {        self.limits.startIteLimit(            limit,            self.num_recursive_calls,            self.nodes.items.len,            self.ite_cache.count(),        );    }    pub fn stopIteLimit(self: *Manager) void {        self.limits.stopIteLimit();    }    pub fn ite(self: *Manager, f: Bdd, g: Bdd, h: Bdd) Allocator.Error!Bdd {        self.num_recursive_calls += 1;        if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {            return Bdd.FALSE;        }        if (self.num_recursive_calls % 1000 == 0) {            if (self.checkLimits()) return Bdd.FALSE;        }        const helper = LessThanHelper{ .manager = self };        const normalized = NormalizedIte.normalize(f, g, h, helper);        if (normalized.is_const) {            return normalized.const_result;        }        if (self.ite_cache.get(normalized.key)) |cached| {            self.ite_cache_hits += 1;            return if (normalized.complement_result) cached.neg() else cached;        }        self.ite_cache_misses += 1;        if (self.limits.reserveIteCacheGrowth(self.ite_cache.count())) return Bdd.FALSE;        defer self.limits.releaseIteCacheGrowth();        const top_var = self.firstEssential(f, g, h);        const fx_t = self.conditionEssential(f, top_var, true);        const gx_t = self.conditionEssential(g, top_var, true);        const hx_t = self.conditionEssential(h, top_var, true);        const fx_f = self.conditionEssential(f, top_var, false);        const gx_f = self.conditionEssential(g, top_var, false);        const hx_f = self.conditionEssential(h, top_var, false);        const t = try self.ite(fx_t, gx_t, hx_t);        if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {            return Bdd.FALSE;        }        const e = try self.ite(fx_f, gx_f, hx_f);        if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {            return Bdd.FALSE;        }        if (t.toRaw() == e.toRaw()) {            const cache_result = if (normalized.complement_result) t.neg() else t;            if (!try self.putIteCacheNoClobber(normalized.key, cache_result)) return Bdd.FALSE;            return t;        }        const result = try self.getOrInsert(Node.init(top_var, e, t));        if (self.limits.ite_limit_exceeded) return Bdd.FALSE;        const cache_result = if (normalized.complement_result) result.neg() else result;        if (!try self.putIteCacheNoClobber(normalized.key, cache_result)) return Bdd.FALSE;        return result;    }    fn putIteCacheNoClobber(self: *Manager, key: IteKey, value: Bdd) Allocator.Error!bool {        if (!try self.ensureReservedIteCacheCapacity()) return false;        self.ite_cache.putAssumeCapacityNoClobber(key, value);        return true;    }    fn ensureReservedIteCacheCapacity(self: *Manager) Allocator.Error!bool {        const reservations = @max(self.limits.ite_cache_reservations, 1);        std.debug.assert(reservations <= std.math.maxInt(u32));        const projected = self.ite_cache.count() +| reservations;        if (projected <= self.ite_cache_grow_at) return true;        const capacity = self.ite_cache.capacity();        const reserve = @max(capacity, INITIAL_MANAGER_CAPACITY);        const target = @max(projected, self.ite_cache.count() +| reserve);        const target_size = std.math.cast(u32, target) orelse {            if (self.limits.boundedAllocationFailed()) return false;            return error.OutOfMemory;        };        self.ite_cache.ensureTotalCapacity(self.allocator, target_size) catch |err| {            if (self.limits.boundedAllocationFailed()) return false;            return err;        };        self.ite_cache_grows += 1;        self.ite_cache_grow_at = tableLoadThreshold(self.ite_cache.capacity());        return true;    }    pub fn bddAnd(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {        if (a.isFalse() or b.isFalse()) return Bdd.FALSE;        if (a.isTrue()) return b;        if (b.isTrue()) return a;        if (a.toRaw() == b.toRaw()) return a;        if (a.neg().toRaw() == b.toRaw()) return Bdd.FALSE;        var left = a;        var right = b;        if (right.toRaw() < left.toRaw()) {            const tmp = left;            left = right;            right = tmp;        }        return self.ite(left, right, Bdd.FALSE);    }    pub fn bddOr(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {        if (a.isTrue() or b.isTrue()) return Bdd.TRUE;        if (a.isFalse()) return b;        if (b.isFalse()) return a;        if (a.toRaw() == b.toRaw()) return a;        if (a.neg().toRaw() == b.toRaw()) return Bdd.TRUE;        var left = a;        var right = b;        if (right.toRaw() < left.toRaw()) {            const tmp = left;            left = right;            right = tmp;        }        return self.ite(left, Bdd.TRUE, right);    }    pub fn bddNot(_: *Manager, a: Bdd) Bdd {        return a.neg();    }    pub fn bddXor(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {        if (a.isFalse()) return b;        if (b.isFalse()) return a;        if (a.isTrue()) return b.neg();        if (b.isTrue()) return a.neg();        if (a.toRaw() == b.toRaw()) return Bdd.FALSE;        if (a.neg().toRaw() == b.toRaw()) return Bdd.TRUE;        var left = a;        var right = b;        if (right.toRaw() < left.toRaw()) {            const tmp = left;            left = right;            right = tmp;        }        return self.ite(left, right.neg(), right);    }    pub fn bddIff(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {        if (a.isFalse()) return b.neg();        if (b.isFalse()) return a.neg();        if (a.isTrue()) return b;        if (b.isTrue()) return a;        if (a.toRaw() == b.toRaw()) return Bdd.TRUE;        if (a.neg().toRaw() == b.toRaw()) return Bdd.FALSE;        var left = a;        var right = b;        if (right.toRaw() < left.toRaw()) {            const tmp = left;            left = right;            right = tmp;        }        return self.ite(left, right, right.neg());    }    pub fn bddImplies(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {        if (a.isFalse() or b.isTrue()) return Bdd.TRUE;        if (a.isTrue()) return b;        if (b.isFalse()) return a.neg();        if (a.toRaw() == b.toRaw()) return Bdd.TRUE;        if (a.neg().toRaw() == b.toRaw()) return b;        return self.bddOr(a.neg(), b);    }    pub fn eq(self: *const Manager, a: Bdd, b: Bdd) bool {        _ = self;        return a.toRaw() == b.toRaw();    }    pub fn exists(self: *Manager, f: Bdd, variable: VarLabel) Allocator.Error!Bdd {        const f_true = try self.condition(f, variable, true);        const f_false = try self.condition(f, variable, false);        return self.bddOr(f_true, f_false);    }    pub fn condition(self: *Manager, f: Bdd, variable: VarLabel, value: bool) Allocator.Error!Bdd {        return self.conditionHelper(f, variable, value);    }    fn conditionHelper(self: *Manager, f: Bdd, variable: VarLabel, value: bool) Allocator.Error!Bdd {        if (f.isConst()) return f;        const node = self.getNode(f);        if (self.lessThan(variable, node.var_label)) {            return f;        }        if (node.var_label == variable) {            const result = if (value) node.high else node.low;            return if (f.complement) result.neg() else result;        }        const key = ConditionKey.init(f, variable, value);        if (self.condition_cache.get(key)) |cached| {            return cached;        }        const low_result = try self.conditionHelper(            if (f.complement) node.low.neg() else node.low,            variable,            value,        );        const high_result = try self.conditionHelper(            if (f.complement) node.high.neg() else node.high,            variable,            value,        );        if (low_result.toRaw() == high_result.toRaw()) {            if (!try self.putConditionCache(key, low_result)) return Bdd.FALSE;            return low_result;        }        const result = try self.getOrInsert(Node.init(node.var_label, low_result, high_result));        if (self.limits.ite_limit_exceeded) return Bdd.FALSE;        if (!try self.putConditionCache(key, result)) return Bdd.FALSE;        return result;    }    fn putConditionCache(self: *Manager, key: ConditionKey, value: Bdd) Allocator.Error!bool {        self.condition_cache.put(self.allocator, key, value) catch |err| {            if (self.limits.boundedAllocationFailed()) return false;            return err;        };        return true;    }    pub fn compose(self: *Manager, f: Bdd, variable: VarLabel, g: Bdd) Allocator.Error!Bdd {        if (f.isConst()) return f;        const node = self.getNode(f);        if (self.lessThan(variable, node.var_label)) {            return f;        }        const f_low = if (f.complement) node.low.neg() else node.low;        const f_high = if (f.complement) node.high.neg() else node.high;        if (node.var_label == variable) {            return self.ite(g, f_high, f_low);        }        const low_result = try self.compose(f_low, variable, g);        const high_result = try self.compose(f_high, variable, g);        if (low_result.toRaw() == high_result.toRaw()) {            return low_result;        }        return self.getOrInsert(Node.init(node.var_label, low_result, high_result));    }    pub fn sequentialCompose(        self: *Manager,        f: Bdd,        variables: []const VarLabel,        replacements: []const Bdd,    ) Allocator.Error!Bdd {        var result = f;        for (variables, replacements) |variable, replacement| {            result = try self.compose(result, variable, replacement);        }        return result;    }    pub fn isVar(self: *const Manager, bdd: Bdd) bool {        if (bdd.isConst()) return false;        const node = self.getNode(bdd);        const low_raw = if (bdd.complement) node.low.neg() else node.low;        const high_raw = if (bdd.complement) node.high.neg() else node.high;        return low_raw.isFalse() and high_raw.isTrue();    }    pub fn hasVariable(self: *const Manager, bdd: Bdd, variable: VarLabel) bool {        if (bdd.isConst()) return false;        const node = self.getNode(bdd);        if (node.var_label == variable) return true;        return self.hasVariable(node.low.toReg(), variable) or            self.hasVariable(node.high.toReg(), variable);    }    pub fn size(self: *const Manager, bdd: Bdd) usize {        if (bdd.isConst()) return 0;        var visited = std.AutoHashMap(u31, void).init(self.allocator);        defer visited.deinit();        return self.sizeHelper(bdd, &visited);    }    fn sizeHelper(self: *const Manager, bdd: Bdd, visited: *std.AutoHashMap(u31, void)) usize {        if (bdd.isConst()) return 0;        if (visited.contains(bdd.index)) return 0;        visited.put(bdd.index, {}) catch return 0;        const node = self.getNode(bdd);        return 1 + self.sizeHelper(node.low.toReg(), visited) +            self.sizeHelper(node.high.toReg(), visited);    }    pub fn numRecursiveCalls(self: *const Manager) u64 {        return self.num_recursive_calls;    }    pub fn resetStats(self: *Manager) void {        self.num_recursive_calls = 0;    }    pub fn clearCache(self: *Manager) void {        self.ite_cache.clearRetainingCapacity();        self.ite_cache_grow_at = tableLoadThreshold(self.ite_cache.capacity());        self.condition_cache.clearRetainingCapacity();    }    pub fn getVarPosition(self: *const Manager, var_label: VarLabel) u32 {        if (var_label >= self.var_order.items.len) return @intCast(self.var_order.items.len);        return self.var_order.items[var_label];    }    pub fn totalNodeCount(self: *const Manager) usize {        return if (self.nodes.items.len > 0) self.nodes.items.len - 1 else 0;    }    pub fn getVarAtPosition(self: *const Manager, position: u32) ?VarLabel {        for (self.var_order.items, 0..) |pos, label| {            if (pos == position) return @intCast(label);        }        return null;    }    pub fn nodesAtLevel(self: *const Manager, var_label: VarLabel) usize {        var count: usize = 0;        for (self.nodes.items[1..]) |node| {            if (node.var_label == var_label) count += 1;        }        return count;    }    pub fn swapAdjacentVars(self: *Manager, upper_pos: u32, allocator: Allocator) !i64 {        const lower_pos = upper_pos + 1;        const var_upper = self.getVarAtPosition(upper_pos) orelse return 0;        const var_lower = self.getVarAtPosition(lower_pos) orelse return 0;        const size_before = self.totalNodeCount();        var nodes_to_process: std.ArrayList(u31) = .empty;        defer nodes_to_process.deinit(allocator);        for (self.nodes.items[1..], 1..) |node, idx| {            if (node.var_label == var_upper) {                try nodes_to_process.append(allocator, @intCast(idx));            }        }        for (nodes_to_process.items) |idx| {            const node = self.nodes.items[idx];            const high_child = node.high;            const low_child = node.low;            var f11: Bdd = undefined;            var f10: Bdd = undefined;            var f01: Bdd = undefined;            var f00: Bdd = undefined;            if (!high_child.isConst() and self.getNode(high_child).var_label == var_lower) {                const high_node = self.getNode(high_child);                f11 = if (high_child.complement) high_node.high.neg() else high_node.high;                f10 = if (high_child.complement) high_node.low.neg() else high_node.low;            } else {                f11 = high_child;                f10 = high_child;            }            if (!low_child.isConst() and self.getNode(low_child).var_label == var_lower) {                const low_node = self.getNode(low_child);                f01 = if (low_child.complement) low_node.high.neg() else low_node.high;                f00 = if (low_child.complement) low_node.low.neg() else low_node.low;            } else {                f01 = low_child;                f00 = low_child;            }            const new_high = try self.getOrInsert(Node.init(var_upper, f01, f11));            const new_low = try self.getOrInsert(Node.init(var_upper, f00, f10));            _ = try self.getOrInsert(Node.init(var_lower, new_low, new_high));        }        self.var_order.items[var_upper] = lower_pos;        self.var_order.items[var_lower] = upper_pos;        self.clearCache();        const size_after = self.totalNodeCount();        return @as(i64, @intCast(size_after)) - @as(i64, @intCast(size_before));    }    pub fn localSift(self: *Manager, var_label: VarLabel, config: SiftConfig, allocator: Allocator) !SiftResult {        const original_pos = self.getVarPosition(var_label);        const num_vars = self.numVars();        if (num_vars <= 1) {            return SiftResult{                .original_pos = original_pos,                .final_pos = original_pos,                .size_delta = 0,                .aborted = false,            };        }        const original_size = self.totalNodeCount();        var best_pos = original_pos;        var best_size = original_size;        var current_pos = original_pos;        var aborted = false;        var moves_down: u32 = 0;        while (moves_down < config.max_distance and current_pos + 1 < num_vars) {            const delta = try self.swapAdjacentVars(current_pos, allocator);            current_pos += 1;            moves_down += 1;            const current_size = self.totalNodeCount();            if (current_size < best_size) {                best_size = current_size;                best_pos = current_pos;            }            if (original_size > 0) {                const blowup = @as(f64, @floatFromInt(current_size)) / @as(f64, @floatFromInt(original_size));                if (blowup > config.max_blowup) {                    aborted = true;                    break;                }            }            _ = delta;        }        while (current_pos > original_pos) {            _ = try self.swapAdjacentVars(current_pos - 1, allocator);            current_pos -= 1;        }        if (!aborted) {            var moves_up: u32 = 0;            while (moves_up < config.max_distance and current_pos > 0) {                _ = try self.swapAdjacentVars(current_pos - 1, allocator);                current_pos -= 1;                moves_up += 1;                const current_size = self.totalNodeCount();                if (current_size < best_size) {                    best_size = current_size;                    best_pos = current_pos;                }                if (original_size > 0) {                    const blowup = @as(f64, @floatFromInt(current_size)) / @as(f64, @floatFromInt(original_size));                    if (blowup > config.max_blowup) {                        aborted = true;                        break;                    }                }            }        }        while (current_pos < best_pos) {            _ = try self.swapAdjacentVars(current_pos, allocator);            current_pos += 1;        }        while (current_pos > best_pos) {            _ = try self.swapAdjacentVars(current_pos - 1, allocator);            current_pos -= 1;        }        const final_size = self.totalNodeCount();        return SiftResult{            .original_pos = original_pos,            .final_pos = best_pos,            .size_delta = @as(i64, @intCast(final_size)) - @as(i64, @intCast(original_size)),            .aborted = aborted,        };    }    pub fn globalSift(self: *Manager, config: SiftConfig, allocator: Allocator, max_passes: u32) !GlobalSiftResult {        const num_vars = self.numVars();        if (num_vars <= 1) {            const node_count = self.totalNodeCount();            return GlobalSiftResult{                .total_size_delta = 0,                .vars_sifted = 0,                .vars_improved = 0,                .original_size = node_count,                .final_size = node_count,            };        }        const original_size = self.totalNodeCount();        var total_delta: i64 = 0;        var vars_sifted: u32 = 0;        var vars_improved: u32 = 0;        var pass: u32 = 0;        while (pass < max_passes) : (pass += 1) {            var improved_this_pass = false;            var var_idx: VarLabel = 0;            while (var_idx < num_vars) : (var_idx += 1) {                const result = try self.localSift(var_idx, config, allocator);                vars_sifted += 1;                if (result.size_delta < 0) {                    vars_improved += 1;                    improved_this_pass = true;                }                total_delta += result.size_delta;            }            if (!improved_this_pass) break;        }        const final_size = self.totalNodeCount();        return GlobalSiftResult{            .total_size_delta = total_delta,            .vars_sifted = vars_sifted,            .vars_improved = vars_improved,            .original_size = original_size,            .final_size = final_size,        };    }    pub fn toString(self: *const Manager, bdd: Bdd, allocator: Allocator) ![]u8 {        var buffer = std.Io.Writer.Allocating.init(allocator);        errdefer buffer.deinit();        try self.toStringHelper(bdd, &buffer.writer);        return try buffer.toOwnedSlice();    }    fn toStringHelper(self: *const Manager, bdd: Bdd, writer: anytype) !void {        if (bdd.isTrue()) {            try writer.writeAll("T");        } else if (bdd.isFalse()) {            try writer.writeAll("F");        } else {            const node = self.getNode(bdd);            if (bdd.complement) {                try writer.writeAll("!");            }            try writer.print("({d}, ", .{node.var_label});            try self.toStringHelper(node.high, writer);            try writer.writeAll(", ");            try self.toStringHelper(node.low, writer);            try writer.writeAll(")");        }    }    pub fn toJson(self: *const Manager, bdd: Bdd, allocator: Allocator) ![]u8 {        return writeBddJson(allocator, bdd, self.nodes.items);    }    pub fn printStats(self: *const Manager, allocator: Allocator) ![]u8 {        var buffer = std.Io.Writer.Allocating.init(allocator);        errdefer buffer.deinit();        const writer = &buffer.writer;        try writer.print("BDD Manager Stats:\n", .{});        try writer.print("  Variables: {d}\n", .{self.var_order.items.len});        try writer.print("  Nodes: {d}\n", .{self.nodes.items.len});        try writer.print("  Unique table entries: {d}\n", .{self.unique_table.count()});        try writer.print("  ITE cache entries: {d}\n", .{self.ite_cache.count()});        try writer.print("  Condition cache entries: {d}\n", .{self.condition_cache.count()});        try writer.print("  Recursive calls: {d}\n", .{self.num_recursive_calls});        try writer.print("  ITE cache hits: {d}\n", .{self.ite_cache_hits});        try writer.print("  ITE cache misses: {d}\n", .{self.ite_cache_misses});        try writer.print("  Unique table grows: {d}\n", .{self.unique_table_grows});        try writer.print("  ITE cache grows: {d}\n", .{self.ite_cache_grows});        const total = self.ite_cache_hits + self.ite_cache_misses;        if (total > 0) {            const hit_ratio = @as(f64, @floatFromInt(self.ite_cache_hits)) / @as(f64, @floatFromInt(total)) * 100.0;            try writer.print("  ITE cache hit ratio: {d:.1}%\n", .{hit_ratio});        }        return try buffer.toOwnedSlice();    }};pub const BddCopy = struct {    root: Bdd,    nodes: []Node,    var_order: []u32,    allocator: Allocator,    pub fn deinit(self: *BddCopy) void {        self.allocator.free(self.nodes);        self.allocator.free(self.var_order);    }    pub fn isConst(self: *const BddCopy) bool {        return self.root.isConst();    }    pub fn isTrue(self: *const BddCopy) bool {        return self.root.isTrue();    }    pub fn isFalse(self: *const BddCopy) bool {        return self.root.isFalse();    }    pub fn getNode(self: *const BddCopy, bdd: Bdd) Node {        return self.nodes[bdd.index];    }    pub fn toJson(self: *const BddCopy, allocator: Allocator) ![]u8 {        return writeBddJson(allocator, self.root, self.nodes);    }};fn writeBddJson(allocator: Allocator, root: Bdd, nodes: []const Node) ![]u8 {    var visited = std.AutoHashMap(u32, void).init(allocator);    defer visited.deinit();    try collectJsonNodes(root, nodes, &visited);    const indices = try allocator.alloc(u32, visited.count());    defer allocator.free(indices);    var index_count: usize = 0;    var iterator = visited.keyIterator();    while (iterator.next()) |index| {        indices[index_count] = index.*;        index_count += 1;    }    std.debug.assert(index_count == indices.len);    std.mem.sort(u32, indices, {}, std.sort.asc(u32));    var output = std.Io.Writer.Allocating.init(allocator);    errdefer output.deinit();    var stream = pretty_json.Writer.init(&output.writer, .minified);    const object = try stream.object();    try writeNodeRef(object, "root", root);    const node_objects = try object.object("nodes");    for (indices) |index| {        const node_object = try node_objects.formattedObject(16, "n{d}", .{index});        const node = nodes[index];        try node_object.field("var", node.var_label);        try writeNodeRef(node_object, "high", node.high);        try writeNodeRef(node_object, "low", node.low);        try node_object.end();    }    try node_objects.end();    try object.end();    return try output.toOwnedSlice();}fn collectJsonNodes(    bdd: Bdd,    nodes: []const Node,    visited: *std.AutoHashMap(u32, void),) !void {    if (bdd.isConst()) return;    const index = bdd.index;    if (visited.contains(index)) return;    try visited.put(index, {});    const node = nodes[index];    try collectJsonNodes(node.high, nodes, visited);    try collectJsonNodes(node.low, nodes, visited);}fn writeNodeRef(object: pretty_json.Object, name: []const u8, bdd: Bdd) !void {    if (bdd.isTrue()) {        try object.field(name, "true");    } else if (bdd.isFalse()) {        try object.field(name, "false");    } else if (bdd.complement) {        try object.formattedString(name, 16, "!n{d}", .{bdd.index});    } else {        try object.formattedString(name, 16, "n{d}", .{bdd.index});    }}pub fn deepCopy(manager: *const Manager, bdd: Bdd, allocator: Allocator) !BddCopy {    const nodes = try allocator.dupe(Node, manager.nodes.items);    errdefer allocator.free(nodes);    const var_order = try allocator.dupe(u32, manager.var_order.items);    return BddCopy{        .root = bdd,        .nodes = nodes,        .var_order = var_order,        .allocator = allocator,    };}test "manager initialization releases each failed allocation" {    try std.testing.checkAllAllocationFailures(std.testing.allocator, initializeManager, .{});}fn initializeManager(allocator: Allocator) !void {    var manager = try Manager.init(allocator);    defer manager.deinit();    try std.testing.expectEqual(@as(usize, 1), manager.nodes.items.len);}test "basic constants" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    try std.testing.expect(Bdd.TRUE.isTrue());    try std.testing.expect(!Bdd.TRUE.isFalse());    try std.testing.expect(Bdd.FALSE.isFalse());    try std.testing.expect(!Bdd.FALSE.isTrue());    try std.testing.expect(Bdd.TRUE.isConst());    try std.testing.expect(Bdd.FALSE.isConst());}test "variable creation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    try std.testing.expect(!x.isConst());    try std.testing.expect(!y.isConst());    try std.testing.expect(x.toRaw() != y.toRaw());    try std.testing.expect(manager.isVar(x));    try std.testing.expect(manager.isVar(y));}test "negation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const not_x = manager.bddNot(x);    try std.testing.expect(x.neg().toRaw() == not_x.toRaw());    try std.testing.expect(not_x.neg().toRaw() == x.toRaw());    try std.testing.expect(Bdd.TRUE.neg().toRaw() == Bdd.FALSE.toRaw());    try std.testing.expect(Bdd.FALSE.neg().toRaw() == Bdd.TRUE.toRaw());}test "and operation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    try std.testing.expect(manager.eq(try manager.bddAnd(x, Bdd.TRUE), x));    try std.testing.expect(manager.eq(try manager.bddAnd(x, Bdd.FALSE), Bdd.FALSE));    try std.testing.expect(manager.eq(try manager.bddAnd(x, x), x));    const x_neg = x.neg();    const result = try manager.bddAnd(x, x_neg);    try std.testing.expectEqual(Bdd.FALSE.toRaw(), result.toRaw());    const x_and_y = try manager.bddAnd(x, y);    try std.testing.expect(!x_and_y.isConst());}test "or operation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    try std.testing.expect(manager.eq(try manager.bddOr(x, Bdd.FALSE), x));    try std.testing.expect(manager.eq(try manager.bddOr(x, Bdd.TRUE), Bdd.TRUE));    try std.testing.expect(manager.eq(try manager.bddOr(x, x), x));    try std.testing.expect(manager.eq(try manager.bddOr(x, x.neg()), Bdd.TRUE));    const x_or_y = try manager.bddOr(x, y);    try std.testing.expect(!x_or_y.isConst());}test "iff and xor" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    try std.testing.expect(manager.eq(try manager.bddIff(x, x), Bdd.TRUE));    try std.testing.expect(manager.eq(try manager.bddIff(x, x.neg()), Bdd.FALSE));    try std.testing.expect(manager.eq(try manager.bddXor(x, x), Bdd.FALSE));    try std.testing.expect(manager.eq(try manager.bddXor(x, x.neg()), Bdd.TRUE));    const iff = try manager.bddIff(x, y);    const xor = try manager.bddXor(x, y);    try std.testing.expect(manager.eq(iff, xor.neg()));}test "binary boolean fast paths avoid trivial ite work" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    manager.resetStats();    try std.testing.expectEqual(Bdd.FALSE.toRaw(), (try manager.bddAnd(x, Bdd.FALSE)).toRaw());    try std.testing.expectEqual(x.toRaw(), (try manager.bddAnd(x, Bdd.TRUE)).toRaw());    try std.testing.expectEqual(x.toRaw(), (try manager.bddAnd(x, x)).toRaw());    try std.testing.expectEqual(Bdd.FALSE.toRaw(), (try manager.bddAnd(x, x.neg())).toRaw());    try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddOr(x, Bdd.TRUE)).toRaw());    try std.testing.expectEqual(x.toRaw(), (try manager.bddOr(x, Bdd.FALSE)).toRaw());    try std.testing.expectEqual(x.toRaw(), (try manager.bddOr(x, x)).toRaw());    try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddOr(x, x.neg())).toRaw());    try std.testing.expectEqual(x.toRaw(), (try manager.bddXor(x, Bdd.FALSE)).toRaw());    try std.testing.expectEqual(x.neg().toRaw(), (try manager.bddXor(x, Bdd.TRUE)).toRaw());    try std.testing.expectEqual(Bdd.FALSE.toRaw(), (try manager.bddXor(x, x)).toRaw());    try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddXor(x, x.neg())).toRaw());    try std.testing.expectEqual(x.toRaw(), (try manager.bddIff(x, Bdd.TRUE)).toRaw());    try std.testing.expectEqual(x.neg().toRaw(), (try manager.bddIff(x, Bdd.FALSE)).toRaw());    try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddIff(x, x)).toRaw());    try std.testing.expectEqual(Bdd.FALSE.toRaw(), (try manager.bddIff(x, x.neg())).toRaw());    try std.testing.expectEqual(Bdd.TRUE.toRaw(), (try manager.bddImplies(x, x)).toRaw());    try std.testing.expectEqual(x.neg().toRaw(), (try manager.bddImplies(x, Bdd.FALSE)).toRaw());    try std.testing.expectEqual(@as(u64, 0), manager.numRecursiveCalls());    const xy = try manager.bddAnd(x, y);    const hits_before = manager.ite_cache_hits;    const yx = try manager.bddAnd(y, x);    try std.testing.expectEqual(xy.toRaw(), yx.toRaw());    try std.testing.expect(manager.ite_cache_hits > hits_before);}test "ite cache reserves bulk capacity after startup" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const initial_capacity = manager.ite_cache.capacity();    const max_load = (initial_capacity * Manager.TABLE_MAX_LOAD_PERCENTAGE) / 100;    try std.testing.expectEqual(max_load, manager.ite_cache_grow_at);    for (0..max_load) |i| {        const f = Bdd{ .index = @intCast(i + 1), .complement = false };        try std.testing.expect(try manager.putIteCacheNoClobber(IteKey.init(f, Bdd.TRUE, Bdd.FALSE), Bdd.TRUE));    }    try std.testing.expectEqual(initial_capacity, manager.ite_cache.capacity());    try std.testing.expectEqual(max_load, manager.ite_cache_grow_at);    const f = Bdd{ .index = @intCast(max_load + 1), .complement = false };    try std.testing.expect(try manager.putIteCacheNoClobber(IteKey.init(f, Bdd.TRUE, Bdd.FALSE), Bdd.TRUE));    try std.testing.expect(manager.ite_cache.capacity() >= initial_capacity * 4);    try std.testing.expectEqual(        Manager.tableLoadThreshold(manager.ite_cache.capacity()),        manager.ite_cache_grow_at,    );}test "canonical table reserves bulk capacity after startup" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const initial_capacity = manager.unique_table.capacity();    const max_load = (initial_capacity * Manager.TABLE_MAX_LOAD_PERCENTAGE) / 100;    try std.testing.expectEqual(max_load, manager.unique_table_grow_at);    for (0..max_load) |_| {        _ = try manager.newVar(true);    }    try std.testing.expectEqual(initial_capacity, manager.unique_table.capacity());    try std.testing.expectEqual(max_load, manager.unique_table_grow_at);    _ = try manager.newVar(true);    try std.testing.expect(manager.unique_table.capacity() >= initial_capacity * 4);    try std.testing.expectEqual(        Manager.tableLoadThreshold(manager.unique_table.capacity()),        manager.unique_table_grow_at,    );}test "simple equality: (a OR b) AND a = a" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const a = try manager.newVar(true);    const b = try manager.newVar(true);    const a_or_b = try manager.bddOr(a, b);    const result = try manager.bddAnd(a_or_b, a);    try std.testing.expect(manager.eq(result, a));}test "condition (restrict)" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_or_y = try manager.bddOr(x, y);    const restricted = try manager.condition(x_or_y, 1, false);    try std.testing.expect(manager.eq(restricted, x));    const x_and_y = try manager.bddAnd(x, y);    const restricted2 = try manager.condition(x_and_y, 0, true);    try std.testing.expect(manager.eq(restricted2, y));}test "condition cache with shared subgraphs" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    try std.testing.expect(manager.condition_cache.capacity() < Manager.INITIAL_MANAGER_CAPACITY);    try std.testing.expect(manager.condition_cache.capacity() >= Manager.INITIAL_CONDITION_CACHE_CAPACITY);    const num_vars = 25;    var vars: [num_vars]Bdd = undefined;    for (0..num_vars) |i| {        vars[i] = try manager.newVar(true);    }    var result = vars[0];    for (1..num_vars) |i| {        result = try manager.bddXor(result, vars[i]);    }    const middle = num_vars / 2;    var others: ?Bdd = null;    for (0..num_vars) |i| {        if (i == middle) continue;        others = if (others) |acc| try manager.bddXor(acc, vars[i]) else vars[i];    }    const middle_var: VarLabel = @intCast(middle);    const restricted_true = try manager.condition(result, middle_var, true);    const restricted_false = try manager.condition(result, middle_var, false);    try std.testing.expect(manager.eq(restricted_true, manager.bddNot(others.?)));    try std.testing.expect(manager.eq(restricted_false, others.?));    try std.testing.expect(manager.condition_cache.count() > 0);    try std.testing.expect(manager.condition_cache.capacity() > 0);}test "existential quantification" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const x_and_y_and_z = try manager.bddAnd(x_and_y, z);    const result = try manager.exists(x_and_y_and_z, 1);    const expected = try manager.bddAnd(x, z);    try std.testing.expect(manager.eq(result, expected));}test "compose" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const result = try manager.compose(x_and_y, 1, z);    const expected = try manager.bddAnd(x, z);    try std.testing.expect(manager.eq(result, expected));}test "has variable" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    _ = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    try std.testing.expect(manager.hasVariable(x_and_y, 0));    try std.testing.expect(manager.hasVariable(x_and_y, 1));    try std.testing.expect(!manager.hasVariable(x_and_y, 2));    try std.testing.expect(!manager.hasVariable(Bdd.TRUE, 0));}test "size" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    try std.testing.expectEqual(@as(usize, 0), manager.size(Bdd.TRUE));    try std.testing.expectEqual(@as(usize, 0), manager.size(Bdd.FALSE));    const x = try manager.newVar(true);    try std.testing.expectEqual(@as(usize, 1), manager.size(x));    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    try std.testing.expectEqual(@as(usize, 2), manager.size(x_and_y));}test "getVarPosition and getVarAtPosition" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    _ = try manager.newVar(true);    _ = try manager.newVar(true);    _ = try manager.newVar(true);    try std.testing.expectEqual(@as(u32, 0), manager.getVarPosition(0));    try std.testing.expectEqual(@as(u32, 1), manager.getVarPosition(1));    try std.testing.expectEqual(@as(u32, 2), manager.getVarPosition(2));    try std.testing.expectEqual(@as(?VarLabel, 0), manager.getVarAtPosition(0));    try std.testing.expectEqual(@as(?VarLabel, 1), manager.getVarAtPosition(1));    try std.testing.expectEqual(@as(?VarLabel, 2), manager.getVarAtPosition(2));    try std.testing.expectEqual(@as(?VarLabel, null), manager.getVarAtPosition(3));}test "totalNodeCount" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    try std.testing.expectEqual(@as(usize, 0), manager.totalNodeCount());    _ = try manager.newVar(true);    try std.testing.expectEqual(@as(usize, 1), manager.totalNodeCount());    const y = try manager.newVar(true);    try std.testing.expectEqual(@as(usize, 2), manager.totalNodeCount());    const x = try manager.newVar(true);    _ = try manager.bddAnd(x, y);    try std.testing.expect(manager.totalNodeCount() >= 3);}test "nodesAtLevel" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    try std.testing.expectEqual(@as(usize, 1), manager.nodesAtLevel(0));    try std.testing.expectEqual(@as(usize, 1), manager.nodesAtLevel(1));    _ = try manager.bddAnd(x, y);    try std.testing.expect(manager.nodesAtLevel(0) >= 1);}test "swapAdjacentVars basic" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    _ = try manager.bddAnd(x, y);    try std.testing.expectEqual(@as(u32, 0), manager.getVarPosition(0));    try std.testing.expectEqual(@as(u32, 1), manager.getVarPosition(1));    _ = try manager.swapAdjacentVars(0, allocator);    try std.testing.expectEqual(@as(u32, 1), manager.getVarPosition(0));    try std.testing.expectEqual(@as(u32, 0), manager.getVarPosition(1));}test "localSift single variable" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    _ = try manager.newVar(true);    const result = try manager.localSift(0, SiftConfig{}, allocator);    try std.testing.expectEqual(@as(u32, 0), result.original_pos);    try std.testing.expectEqual(@as(u32, 0), result.final_pos);    try std.testing.expectEqual(@as(i64, 0), result.size_delta);    try std.testing.expect(!result.aborted);}test "localSift returns to best position" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    _ = try manager.newVar(true);    _ = try manager.newVar(true);    _ = try manager.newVar(true);    const initial_pos = manager.getVarPosition(0);    const result = try manager.localSift(0, SiftConfig{ .max_distance = 2 }, allocator);    try std.testing.expect(result.original_pos == initial_pos);    try std.testing.expect(result.final_pos <= 2);    try std.testing.expect(!result.aborted);}test "min/max variable tracking" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    try std.testing.expectEqual(NO_VAR, manager.getMinVar(Bdd.TRUE));    try std.testing.expectEqual(NO_VAR, manager.getMaxVar(Bdd.TRUE));    try std.testing.expectEqual(NO_VAR, manager.getMinVar(Bdd.FALSE));    try std.testing.expectEqual(NO_VAR, manager.getMaxVar(Bdd.FALSE));    const x = try manager.newVar(true);    try std.testing.expectEqual(@as(VarLabel, 0), manager.getMinVar(x));    try std.testing.expectEqual(@as(VarLabel, 0), manager.getMaxVar(x));    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    try std.testing.expectEqual(@as(VarLabel, 0), manager.getMinVar(x_and_y));    try std.testing.expectEqual(@as(VarLabel, 1), manager.getMaxVar(x_and_y));    const z = try manager.newVar(true);    const y_and_z = try manager.bddAnd(y, z);    try std.testing.expectEqual(@as(VarLabel, 1), manager.getMinVar(y_and_z));    try std.testing.expectEqual(@as(VarLabel, 2), manager.getMaxVar(y_and_z));    const combined = try manager.bddOr(x_and_y, y_and_z);    try std.testing.expectEqual(@as(VarLabel, 0), manager.getMinVar(combined));    try std.testing.expectEqual(@as(VarLabel, 2), manager.getMaxVar(combined));}test "complemented edge preservation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const not_x_and_y = manager.bddNot(x_and_y);    const not_x = manager.bddNot(x);    const not_y = manager.bddNot(y);    const not_x_or_not_y = try manager.bddOr(not_x, not_y);    try std.testing.expect(manager.eq(not_x_and_y, not_x_or_not_y));}test "de morgan's laws" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const a = try manager.newVar(true);    const b = try manager.newVar(true);    const lhs1 = manager.bddNot(try manager.bddAnd(a, b));    const rhs1 = try manager.bddOr(manager.bddNot(a), manager.bddNot(b));    try std.testing.expect(manager.eq(lhs1, rhs1));    const lhs2 = manager.bddNot(try manager.bddOr(a, b));    const rhs2 = try manager.bddAnd(manager.bddNot(a), manager.bddNot(b));    try std.testing.expect(manager.eq(lhs2, rhs2));}test "three variable formula" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const formula = try manager.bddOr(x_and_y, z);    const cond_z_true = try manager.condition(formula, 2, true);    try std.testing.expect(manager.eq(cond_z_true, Bdd.TRUE));    const cond_z_false = try manager.condition(formula, 2, false);    try std.testing.expect(manager.eq(cond_z_false, x_and_y));}test "implies operation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const a = try manager.newVar(true);    const b = try manager.newVar(true);    try std.testing.expect(manager.eq(try manager.bddImplies(a, a), Bdd.TRUE));    try std.testing.expect(manager.eq(try manager.bddImplies(Bdd.FALSE, a), Bdd.TRUE));    try std.testing.expect(manager.eq(try manager.bddImplies(a, Bdd.TRUE), Bdd.TRUE));    try std.testing.expect(manager.eq(try manager.bddImplies(Bdd.TRUE, a), a));    try std.testing.expect(manager.eq(try manager.bddImplies(a, Bdd.FALSE), a.neg()));    const implies = try manager.bddImplies(a, b);    const or_form = try manager.bddOr(a.neg(), b);    try std.testing.expect(manager.eq(implies, or_form));}test "recursive call counting" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const initial_calls = manager.numRecursiveCalls();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    _ = try manager.bddAnd(x, y);    try std.testing.expect(manager.numRecursiveCalls() > initial_calls);    manager.resetStats();    try std.testing.expectEqual(@as(u64, 0), manager.numRecursiveCalls());}test "newVarAtPosition" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVarAtPosition(0, true);    const z_and_x = try manager.bddAnd(z, x);    try std.testing.expectEqual(@as(VarLabel, 2), manager.topVar(z_and_x));    const x_and_y = try manager.bddAnd(x, y);    try std.testing.expect(!x_and_y.isConst());}test "sequentialCompose behavior" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const result1 = try manager.sequentialCompose(        x_and_y,        &[_]VarLabel{ 0, 1 },        &[_]Bdd{ z, z },    );    try std.testing.expect(manager.eq(result1, z));    const result2 = try manager.sequentialCompose(        x,        &[_]VarLabel{ 0, 1 },        &[_]Bdd{ y, x },    );    try std.testing.expect(manager.eq(result2, x));    const single_result = try manager.sequentialCompose(        x_and_y,        &[_]VarLabel{1},        &[_]Bdd{z},    );    const compose_result = try manager.compose(x_and_y, 1, z);    try std.testing.expect(manager.eq(single_result, compose_result));}test "newVarAtPosition preserves existing BDDs" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_or_y = try manager.bddOr(x, y);    _ = try manager.newVarAtPosition(0, true);    const cond_x_true = try manager.condition(x_or_y, 0, true);    try std.testing.expect(manager.eq(cond_x_true, Bdd.TRUE));    const cond_x_false = try manager.condition(x_or_y, 0, false);    try std.testing.expect(manager.eq(cond_x_false, y));}const DualNumber = struct {    primal: f64,    partials: []f64,    allocator: Allocator,    pub fn init(allocator: Allocator, primal: f64, num_partials: usize) !DualNumber {        const partials = try allocator.alloc(f64, num_partials);        @memset(partials, 0.0);        return DualNumber{            .primal = primal,            .partials = partials,            .allocator = allocator,        };    }    pub fn initWithPartials(allocator: Allocator, primal: f64, partials: []const f64) !DualNumber {        const owned_partials = try allocator.alloc(f64, partials.len);        @memcpy(owned_partials, partials);        return DualNumber{            .primal = primal,            .partials = owned_partials,            .allocator = allocator,        };    }    pub fn constant(allocator: Allocator, value: f64, num_partials: usize) !DualNumber {        return init(allocator, value, num_partials);    }    pub fn deinit(self: *DualNumber) void {        self.allocator.free(self.partials);    }    pub fn add(self: DualNumber, other: DualNumber) DualNumber {        for (self.partials, other.partials) |*sp, op| {            sp.* += op;        }        return DualNumber{            .primal = self.primal + other.primal,            .partials = self.partials,            .allocator = self.allocator,        };    }    pub fn mul(self: DualNumber, other: DualNumber) DualNumber {        for (self.partials, other.partials) |*sp, op| {            sp.* = self.primal * op + other.primal * sp.*;        }        return DualNumber{            .primal = self.primal * other.primal,            .partials = self.partials,            .allocator = self.allocator,        };    }    pub fn clone(self: DualNumber) !DualNumber {        return initWithPartials(self.allocator, self.primal, self.partials);    }};pub const VarWeight = struct {    low: f64,    high: f64,};const VarWeightDual = struct {    low: f64,    low_partials: []f64,    high: f64,    high_partials: []f64,};pub const WmcParams = struct {    allocator: Allocator,    num_partials: usize,    weights: std.ArrayListUnmanaged(VarWeight),    dual_weights: std.ArrayListUnmanaged(VarWeightDual),    is_dual: bool,    pub fn init(allocator: Allocator) WmcParams {        return WmcParams{            .allocator = allocator,            .num_partials = 0,            .weights = std.ArrayListUnmanaged(VarWeight).empty,            .dual_weights = std.ArrayListUnmanaged(VarWeightDual).empty,            .is_dual = false,        };    }    pub fn initDual(allocator: Allocator, num_partials: usize) WmcParams {        return WmcParams{            .allocator = allocator,            .num_partials = num_partials,            .weights = std.ArrayListUnmanaged(VarWeight).empty,            .dual_weights = std.ArrayListUnmanaged(VarWeightDual).empty,            .is_dual = true,        };    }    pub fn deinit(self: *WmcParams) void {        self.weights.deinit(self.allocator);        for (self.dual_weights.items) |*dw| {            self.allocator.free(dw.low_partials);            self.allocator.free(dw.high_partials);        }        self.dual_weights.deinit(self.allocator);    }    fn ensureCapacity(self: *WmcParams, variable: VarLabel) !void {        const needed = variable + 1;        while (self.weights.items.len < needed) {            try self.weights.append(self.allocator, VarWeight{ .low = 1.0, .high = 1.0 });        }    }    fn ensureCapacityDual(self: *WmcParams, variable: VarLabel) !void {        const needed = variable + 1;        while (self.dual_weights.items.len < needed) {            const low_partials = try self.allocator.alloc(f64, self.num_partials);            @memset(low_partials, 0.0);            const high_partials = try self.allocator.alloc(f64, self.num_partials);            @memset(high_partials, 0.0);            try self.dual_weights.append(self.allocator, VarWeightDual{                .low = 1.0,                .low_partials = low_partials,                .high = 1.0,                .high_partials = high_partials,            });        }    }    pub fn setWeight(self: *WmcParams, variable: VarLabel, low: f64, high: f64) !void {        try self.ensureCapacity(variable);        self.weights.items[variable] = VarWeight{ .low = low, .high = high };        if (self.is_dual) {            try self.ensureCapacityDual(variable);            self.dual_weights.items[variable].low = low;            self.dual_weights.items[variable].high = high;            @memset(self.dual_weights.items[variable].low_partials, 0.0);            @memset(self.dual_weights.items[variable].high_partials, 0.0);        }    }    pub fn setWeightDeriv(        self: *WmcParams,        variable: VarLabel,        low: f64,        low_partials: []const f64,        high: f64,        high_partials: []const f64,    ) !void {        std.debug.assert(self.is_dual);        std.debug.assert(low_partials.len == self.num_partials);        std.debug.assert(high_partials.len == self.num_partials);        try self.ensureCapacity(variable);        self.weights.items[variable] = VarWeight{ .low = low, .high = high };        try self.ensureCapacityDual(variable);        self.dual_weights.items[variable].low = low;        self.dual_weights.items[variable].high = high;        @memcpy(self.dual_weights.items[variable].low_partials, low_partials);        @memcpy(self.dual_weights.items[variable].high_partials, high_partials);    }    pub fn getWeight(self: *const WmcParams, variable: VarLabel) VarWeight {        if (variable >= self.weights.items.len) {            return VarWeight{ .low = 1.0, .high = 1.0 };        }        return self.weights.items[variable];    }    fn getDualWeight(self: *const WmcParams, variable: VarLabel) ?VarWeightDual {        if (!self.is_dual or variable >= self.dual_weights.items.len) {            return null;        }        return self.dual_weights.items[variable];    }};pub const WmcDualResult = struct {    primal: f64,    partials: []f64,    allocator: Allocator,    pub fn deinit(self: *WmcDualResult) void {        self.allocator.free(self.partials);    }    pub fn varPartial(self: *const WmcDualResult, index: usize) f64 {        if (index >= self.partials.len) return 0.0;        return self.partials[index];    }    pub fn numPartials(self: *const WmcDualResult) usize {        return self.partials.len;    }};pub fn wmc(manager: *const Manager, bdd: Bdd, params: *const WmcParams) f64 {    return wmcWithAllocator(manager, bdd, params, manager.allocator);}pub fn wmcWithAllocator(manager: *const Manager, bdd: Bdd, params: *const WmcParams, allocator: Allocator) f64 {    var cache = WmcDenseCache.init(allocator, manager.nodes.items.len) catch {        var hash_cache = std.AutoHashMap(u32, f64).init(allocator);        defer hash_cache.deinit();        return wmcHelperHash(manager, bdd, params, &hash_cache);    };    defer cache.deinit();    return wmcHelper(manager, bdd, params, &cache);}const WmcDenseCache = struct {    const bits_per_valid_word = @bitSizeOf(usize);    allocator: Allocator,    values: []f64,    valid_words: []usize,    fn init(allocator: Allocator, node_count: usize) Allocator.Error!WmcDenseCache {        const entry_count = node_count * 2;        const values = try allocator.alloc(f64, entry_count);        errdefer allocator.free(values);        const valid_words = try allocator.alloc(usize, validWordCount(entry_count));        @memset(valid_words, 0);        return WmcDenseCache{            .allocator = allocator,            .values = values,            .valid_words = valid_words,        };    }    fn deinit(self: *WmcDenseCache) void {        self.allocator.free(self.valid_words);        self.allocator.free(self.values);    }    fn get(self: *const WmcDenseCache, bdd: Bdd) ?f64 {        const index = cacheIndex(bdd);        if (index >= self.values.len) return null;        if (!self.isValid(index)) return null;        return self.values[index];    }    fn put(self: *WmcDenseCache, bdd: Bdd, value: f64) void {        const index = cacheIndex(bdd);        if (index < self.values.len) {            self.values[index] = value;            self.markValid(index);        }    }    fn cacheIndex(bdd: Bdd) usize {        return @as(usize, bdd.index) * 2 + @intFromBool(bdd.complement);    }    fn validWordCount(entry_count: usize) usize {        return (entry_count + bits_per_valid_word - 1) / bits_per_valid_word;    }    fn validMask(index: usize) usize {        const shift: std.math.Log2Int(usize) = @intCast(index % bits_per_valid_word);        return @as(usize, 1) << shift;    }    fn isValid(self: *const WmcDenseCache, index: usize) bool {        const word_index = index / bits_per_valid_word;        return self.valid_words[word_index] & validMask(index) != 0;    }    fn markValid(self: *WmcDenseCache, index: usize) void {        const word_index = index / bits_per_valid_word;        self.valid_words[word_index] |= validMask(index);    }};fn wmcHelper(    manager: *const Manager,    bdd: Bdd,    params: *const WmcParams,    cache: *WmcDenseCache,) f64 {    if (bdd.isTrue()) return 1.0;    if (bdd.isFalse()) return 0.0;    if (cache.get(bdd)) |cached| {        return cached;    }    const node = manager.getNode(bdd);    const weight = params.getWeight(node.var_label);    const low_child = if (bdd.complement) node.low.neg() else node.low;    const high_child = if (bdd.complement) node.high.neg() else node.high;    const low_result = wmcHelper(manager, low_child, params, cache);    const high_result = wmcHelper(manager, high_child, params, cache);    const result = weight.low * low_result + weight.high * high_result;    cache.put(bdd, result);    return result;}fn wmcHelperHash(    manager: *const Manager,    bdd: Bdd,    params: *const WmcParams,    cache: *std.AutoHashMap(u32, f64),) f64 {    if (bdd.isTrue()) return 1.0;    if (bdd.isFalse()) return 0.0;    const cache_key = bdd.toRaw();    if (cache.get(cache_key)) |cached| {        return cached;    }    const node = manager.getNode(bdd);    const weight = params.getWeight(node.var_label);    const low_child = if (bdd.complement) node.low.neg() else node.low;    const high_child = if (bdd.complement) node.high.neg() else node.high;    const low_result = wmcHelperHash(manager, low_child, params, cache);    const high_result = wmcHelperHash(manager, high_child, params, cache);    const result = weight.low * low_result + weight.high * high_result;    cache.put(cache_key, result) catch {};    return result;}pub fn wmcDual(    manager: *const Manager,    bdd: Bdd,    params: *const WmcParams,    allocator: Allocator,) !WmcDualResult {    std.debug.assert(params.is_dual);    var cache = std.AutoHashMap(u32, DualNumber).init(allocator);    defer {        var it = cache.valueIterator();        while (it.next()) |val| {            var v = val.*;            v.deinit();        }        cache.deinit();    }    var result = try wmcDualHelper(manager, bdd, params, allocator, &cache);    const partials = result.partials;    result.partials = &[_]f64{};    return WmcDualResult{        .primal = result.primal,        .partials = partials,        .allocator = allocator,    };}fn wmcDualHelper(    manager: *const Manager,    bdd: Bdd,    params: *const WmcParams,    allocator: Allocator,    cache: *std.AutoHashMap(u32, DualNumber),) !DualNumber {    if (bdd.isTrue()) {        return DualNumber.constant(allocator, 1.0, params.num_partials);    }    if (bdd.isFalse()) {        return DualNumber.constant(allocator, 0.0, params.num_partials);    }    const cache_key = bdd.toRaw();    if (cache.get(cache_key)) |cached| {        return cached.clone();    }    const node = manager.getNode(bdd);    const maybe_dual_weight = params.getDualWeight(node.var_label);    const low_child = if (bdd.complement) node.low.neg() else node.low;    const high_child = if (bdd.complement) node.high.neg() else node.high;    var result = result: {        var low_result = try wmcDualHelper(manager, low_child, params, allocator, cache);        defer low_result.deinit();        var high_result = try wmcDualHelper(manager, high_child, params, allocator, cache);        defer high_result.deinit();        var low_weight_dual: DualNumber = undefined;        var high_weight_dual: DualNumber = undefined;        if (maybe_dual_weight) |dual_weight| {            low_weight_dual = try DualNumber.initWithPartials(                allocator,                dual_weight.low,                dual_weight.low_partials,            );            errdefer low_weight_dual.deinit();            high_weight_dual = try DualNumber.initWithPartials(                allocator,                dual_weight.high,                dual_weight.high_partials,            );        } else {            low_weight_dual = try DualNumber.constant(allocator, 1.0, params.num_partials);            errdefer low_weight_dual.deinit();            high_weight_dual = try DualNumber.constant(allocator, 1.0, params.num_partials);        }        var low_term = low_weight_dual.mul(low_result);        var high_term = high_weight_dual.mul(high_result);        defer high_term.deinit();        break :result low_term.add(high_term);    };    errdefer result.deinit();    const cached = try result.clone();    cache.put(cache_key, cached) catch {        var mutable_cached = cached;        mutable_cached.deinit();    };    return result;}const WmcCacheEntry = struct {    value: f64 = 0.0,    generation: u64 = 0,};pub const WmcCacheStats = struct {    hits: u64 = 0,    misses: u64 = 0,    invalidations: u64 = 0,    evictions: u64 = 0,    pub fn hitRate(self: WmcCacheStats) f64 {        const total = self.hits + self.misses;        if (total == 0) return 0.0;        return @as(f64, @floatFromInt(self.hits)) / @as(f64, @floatFromInt(total));    }};pub const WmcContext = struct {    cache: std.ArrayListUnmanaged(WmcCacheEntry),    entry_count: usize,    params_version: u64,    structure_version: u64,    cache_generation: u64,    stats: WmcCacheStats,    allocator: Allocator,    manager: ?*const Manager,    pub fn init(allocator: Allocator) WmcContext {        return WmcContext{            .cache = .empty,            .entry_count = 0,            .params_version = 0,            .structure_version = 0,            .cache_generation = 1,            .stats = .{},            .allocator = allocator,            .manager = null,        };    }    pub fn deinit(self: *WmcContext) void {        self.cache.deinit(self.allocator);    }    pub fn wmcCached(        self: *WmcContext,        manager: *const Manager,        bdd: Bdd,        params: *const WmcParams,    ) f64 {        if (bdd.isTrue()) return 1.0;        if (bdd.isFalse()) return 0.0;        self.bindManager(manager);        if (!self.ensureCapacity(manager.nodes.items.len)) {            self.stats.misses += 1;            return wmcWithAllocator(manager, bdd, params, self.allocator);        }        if (self.getCached(bdd)) |cached| {            self.stats.hits += 1;            return cached;        }        self.stats.misses += 1;        return self.wmcHelperCached(manager, bdd, params);    }    fn wmcHelperCached(        self: *WmcContext,        manager: *const Manager,        bdd: Bdd,        params: *const WmcParams,    ) f64 {        if (bdd.isTrue()) return 1.0;        if (bdd.isFalse()) return 0.0;        if (self.getCached(bdd)) |cached| {            return cached;        }        const node = manager.getNode(bdd);        const weight = params.getWeight(node.var_label);        const low_child = if (bdd.complement) node.low.neg() else node.low;        const high_child = if (bdd.complement) node.high.neg() else node.high;        const low_result = self.wmcHelperCached(manager, low_child, params);        const high_result = self.wmcHelperCached(manager, high_child, params);        const result = weight.low * low_result + weight.high * high_result;        self.putCached(bdd, result);        return result;    }    fn ensureCapacity(self: *WmcContext, node_count: usize) bool {        const required = node_count * 2;        if (self.cache.items.len >= required) return true;        const old_len = self.cache.items.len;        self.cache.ensureTotalCapacity(self.allocator, required) catch return false;        self.cache.items.len = required;        @memset(self.cache.items[old_len..], .{});        return true;    }    fn bindManager(self: *WmcContext, manager: *const Manager) void {        if (self.manager) |bound| {            if (bound == manager) return;            self.clearEntries();        }        self.manager = manager;    }    fn clearEntries(self: *WmcContext) void {        @memset(self.cache.items, .{});        self.entry_count = 0;    }    fn getCached(self: *const WmcContext, bdd: Bdd) ?f64 {        const index = cacheIndex(bdd);        if (index >= self.cache.items.len) return null;        const entry = self.cache.items[index];        if (entry.generation != self.cache_generation) return null;        return entry.value;    }    fn putCached(self: *WmcContext, bdd: Bdd, value: f64) void {        const index = cacheIndex(bdd);        if (index >= self.cache.items.len) return;        const was_occupied = self.cache.items[index].generation != 0;        self.cache.items[index] = .{            .value = value,            .generation = self.cache_generation,        };        if (!was_occupied) {            self.entry_count += 1;        }    }    pub fn invalidateAll(self: *WmcContext) void {        self.structure_version += 1;        self.advanceGeneration();        self.stats.invalidations += 1;    }    pub fn invalidateWeights(self: *WmcContext) void {        self.params_version += 1;        self.advanceGeneration();        self.stats.invalidations += 1;    }    fn advanceGeneration(self: *WmcContext) void {        self.cache_generation +%= 1;        if (self.cache_generation == 0) {            self.clearEntries();            self.cache_generation = 1;        }    }    pub fn invalidateForVars(        self: *WmcContext,        manager: *const Manager,        vars: []const VarLabel,    ) void {        self.stats.invalidations += 1;        var removed: usize = 0;        for (self.cache.items, 0..) |*entry, index| {            if (entry.generation == 0) continue;            const bdd = bddFromCacheIndex(index);            for (vars) |var_label| {                if (manager.hasVariable(bdd, var_label)) {                    entry.* = .{};                    removed += 1;                    self.entry_count -= 1;                    break;                }            }        }        self.stats.evictions += removed;    }    pub fn trimToSize(self: *WmcContext, max_entries: usize) usize {        const current = self.entry_count;        if (current <= max_entries) return 0;        const to_evict = current - max_entries;        var evicted: usize = 0;        for (self.cache.items) |*entry| {            if (evicted >= to_evict) break;            if (entry.generation != 0) {                entry.* = .{};                evicted += 1;            }        }        self.entry_count -= evicted;        self.stats.evictions += evicted;        return evicted;    }    pub fn clear(self: *WmcContext) void {        self.clearEntries();        self.stats = .{};        self.params_version = 0;        self.structure_version = 0;        self.cache_generation = 1;        self.manager = null;    }    pub fn cacheSize(self: *const WmcContext) usize {        return self.entry_count;    }    pub fn getStats(self: *const WmcContext) WmcCacheStats {        return self.stats;    }    fn cacheIndex(bdd: Bdd) usize {        return @as(usize, bdd.index) * 2 + @intFromBool(bdd.complement);    }    fn bddFromCacheIndex(index: usize) Bdd {        return Bdd{            .index = @intCast(index / 2),            .complement = index % 2 == 1,        };    }};test "wmc scalar - constant BDDs" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try std.testing.expectApproxEqAbs(@as(f64, 1.0), wmc(&manager, Bdd.TRUE, &params), 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.0), wmc(&manager, Bdd.FALSE, &params), 1e-10);}test "wmc scalar - single variable" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    const x = try manager.newVar(true);    try std.testing.expectApproxEqAbs(@as(f64, 1.0), wmc(&manager, x, &params), 1e-10);    try params.setWeight(0, 0.3, 0.7);    try std.testing.expectApproxEqAbs(@as(f64, 0.7), wmc(&manager, x, &params), 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.3), wmc(&manager, x.neg(), &params), 1e-10);}test "wmc scalar - two variables AND" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    try std.testing.expectApproxEqAbs(@as(f64, 0.42), wmc(&manager, x_and_y, &params), 1e-10);}test "wmc scalar - two variables OR" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_or_y = try manager.bddOr(x, y);    try std.testing.expectApproxEqAbs(@as(f64, 0.88), wmc(&manager, x_or_y, &params), 1e-10);}test "WmcDenseCache - valid bits are independent" {    const allocator = std.testing.allocator;    var cache = try WmcDenseCache.init(allocator, 2);    defer cache.deinit();    const positive = Bdd{ .index = 1, .complement = false };    const negative = Bdd{ .index = 1, .complement = true };    try std.testing.expect(cache.get(positive) == null);    try std.testing.expect(cache.get(negative) == null);    cache.put(positive, 0.75);    try std.testing.expectApproxEqAbs(@as(f64, 0.75), cache.get(positive).?, 1e-10);    try std.testing.expect(cache.get(negative) == null);    cache.put(negative, 0.25);    try std.testing.expectApproxEqAbs(@as(f64, 0.75), cache.get(positive).?, 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.25), cache.get(negative).?, 1e-10);}test "wmc scalar - sum to one" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const formula = try manager.bddXor(x, y);    const wmc_formula = wmc(&manager, formula, &params);    const wmc_neg = wmc(&manager, formula.neg(), &params);    try std.testing.expectApproxEqAbs(@as(f64, 1.0), wmc_formula + wmc_neg, 1e-10);}test "wmc dual - basic gradient" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.initDual(allocator, 2);    defer params.deinit();    var x_low_partials = [_]f64{ 0.0, 0.0 };    var x_high_partials = [_]f64{ 1.0, 0.0 };    try params.setWeightDeriv(0, 0.3, &x_low_partials, 0.7, &x_high_partials);    var y_low_partials = [_]f64{ 0.0, 0.0 };    var y_high_partials = [_]f64{ 0.0, 1.0 };    try params.setWeightDeriv(1, 0.4, &y_low_partials, 0.6, &y_high_partials);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    var result = try wmcDual(&manager, x_and_y, &params, allocator);    defer result.deinit();    try std.testing.expectApproxEqAbs(@as(f64, 0.42), result.primal, 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.6), result.partials[0], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.7), result.partials[1], 1e-10);}test "wmc dual releases temporaries once on allocation failure" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.initDual(allocator, 1);    defer params.deinit();    var zero_partials = [_]f64{0.0};    var one_partials = [_]f64{1.0};    try params.setWeightDeriv(0, 0.3, &zero_partials, 0.7, &one_partials);    const x = try manager.newVar(true);    for (0..8) |fail_index| {        var failing = std.testing.FailingAllocator.init(allocator, .{            .fail_index = fail_index,        });        if (wmcDual(&manager, x, &params, failing.allocator())) |value| {            var result = value;            result.deinit();        } else |err| {            try std.testing.expect(err == error.OutOfMemory);        }    }}test "wmc dual - three variables with chain rule" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.initDual(allocator, 3);    defer params.deinit();    var zero_partials = [_]f64{ 0.0, 0.0, 0.0 };    var x_high_partials = [_]f64{ 1.0, 0.0, 0.0 };    var y_high_partials = [_]f64{ 0.0, 1.0, 0.0 };    var z_high_partials = [_]f64{ 0.0, 0.0, 1.0 };    try params.setWeightDeriv(0, 0.8, &zero_partials, 0.2, &x_high_partials);    try params.setWeightDeriv(1, 0.7, &zero_partials, 0.3, &y_high_partials);    try params.setWeightDeriv(2, 0.5, &zero_partials, 0.5, &z_high_partials);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const formula = try manager.bddOr(x_and_y, z);    var result = try wmcDual(&manager, formula, &params, allocator);    defer result.deinit();    try std.testing.expectApproxEqAbs(@as(f64, 0.53), result.primal, 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.65), result.partials[0], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.2), result.partials[1], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.94), result.partials[2], 1e-10);}test "wmc dual - negation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.initDual(allocator, 1);    defer params.deinit();    var zero_partials = [_]f64{0.0};    var one_partials = [_]f64{1.0};    try params.setWeightDeriv(0, 0.3, &zero_partials, 0.7, &one_partials);    const x = try manager.newVar(true);    var result_x = try wmcDual(&manager, x, &params, allocator);    defer result_x.deinit();    var result_not_x = try wmcDual(&manager, x.neg(), &params, allocator);    defer result_not_x.deinit();    try std.testing.expectApproxEqAbs(@as(f64, 1.0), result_x.primal + result_not_x.primal, 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 1.0), result_x.partials[0], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.0), result_not_x.partials[0], 1e-10);}test "wmc params - varPartial helper" {    const allocator = std.testing.allocator;    var params = WmcParams.initDual(allocator, 3);    defer params.deinit();    var low_partials = [_]f64{ 0.1, 0.2, 0.3 };    var high_partials = [_]f64{ 0.4, 0.5, 0.6 };    try params.setWeightDeriv(0, 0.3, &low_partials, 0.7, &high_partials);    const dw = params.getDualWeight(0).?;    try std.testing.expectApproxEqAbs(@as(f64, 0.1), dw.low_partials[0], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.2), dw.low_partials[1], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.3), dw.low_partials[2], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.4), dw.high_partials[0], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.5), dw.high_partials[1], 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.6), dw.high_partials[2], 1e-10);}test "wmc scalar - larger formula" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.5, 0.5);    try params.setWeight(1, 0.5, 0.5);    try params.setWeight(2, 0.5, 0.5);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    const x_xor_y = try manager.bddXor(x, y);    const formula = try manager.bddXor(x_xor_y, z);    const result = wmc(&manager, formula, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.5), result, 1e-10);}pub const WeightedSampleResult = struct {    sample: Bdd,    probability: f64,};pub const WeightedSampler = struct {    allocator: Allocator,    manager: *Manager,    bdd: Bdd,    params: *const WmcParams,    cache: WmcDenseCache,    var_bdds: []Bdd,    total_wmc: f64,    pub fn init(        allocator: Allocator,        manager: *Manager,        bdd: Bdd,        params: *const WmcParams,    ) !WeightedSampler {        const var_bdds = try allocator.alloc(Bdd, manager.numVars());        errdefer allocator.free(var_bdds);        for (var_bdds, 0..) |*var_bdd, label| {            var_bdd.* = try manager.getOrInsert(Node.init(@intCast(label), Bdd.FALSE, Bdd.TRUE));        }        var cache = try WmcDenseCache.init(allocator, manager.nodes.items.len);        errdefer cache.deinit();        const total_wmc = wmcHelper(manager, bdd, params, &cache);        return WeightedSampler{            .allocator = allocator,            .manager = manager,            .bdd = bdd,            .params = params,            .cache = cache,            .var_bdds = var_bdds,            .total_wmc = total_wmc,        };    }    pub fn deinit(self: *WeightedSampler) void {        self.cache.deinit();        self.allocator.free(self.var_bdds);    }    pub fn sample(self: *WeightedSampler, rng: std.Random) Allocator.Error!WeightedSampleResult {        if (self.bdd.isTrue()) {            return WeightedSampleResult{                .sample = Bdd.TRUE,                .probability = 1.0,            };        }        if (self.bdd.isFalse() or self.total_wmc == 0.0) {            return WeightedSampleResult{                .sample = Bdd.FALSE,                .probability = 0.0,            };        }        return try weightedSampleFromCache(self.manager, self.bdd, self.params, rng, 1.0, &self.cache, self.var_bdds);    }};fn weightedSampleLiteral(manager: *const Manager, bdd: Bdd, params: *const WmcParams) ?WeightedSampleResult {    if (bdd.isConst()) return null;    const node = manager.getNode(bdd);    const low_child = if (bdd.complement) node.low.neg() else node.low;    const high_child = if (bdd.complement) node.high.neg() else node.high;    const weight = params.getWeight(node.var_label);    if (low_child.isFalse() and high_child.isTrue()) {        return .{ .sample = bdd, .probability = weight.high };    }    if (low_child.isTrue() and high_child.isFalse()) {        return .{ .sample = bdd, .probability = weight.low };    }    return null;}pub fn weightedSample(    manager: *Manager,    bdd: Bdd,    params: *const WmcParams,    rng: std.Random,) Allocator.Error!WeightedSampleResult {    if (bdd.isTrue()) {        return WeightedSampleResult{            .sample = Bdd.TRUE,            .probability = 1.0,        };    }    if (bdd.isFalse()) {        return WeightedSampleResult{            .sample = Bdd.FALSE,            .probability = 0.0,        };    }    if (weightedSampleLiteral(manager, bdd, params)) |sample| {        return sample;    }    var cache = try WmcDenseCache.init(manager.allocator, manager.nodes.items.len);    defer cache.deinit();    const total_wmc = wmcHelper(manager, bdd, params, &cache);    if (total_wmc == 0.0) {        return WeightedSampleResult{            .sample = Bdd.FALSE,            .probability = 0.0,        };    }    return try weightedSampleFromCache(manager, bdd, params, rng, 1.0, &cache, &.{});}fn cachedWmc(    manager: *const Manager,    bdd: Bdd,    params: *const WmcParams,    cache: *WmcDenseCache,) f64 {    if (bdd.isTrue()) return 1.0;    if (bdd.isFalse()) return 0.0;    if (cache.get(bdd)) |cached| {        return cached;    }    return wmcHelper(manager, bdd, params, cache);}fn sampleVarBdd(manager: *Manager, var_bdds: []const Bdd, label: VarLabel) Allocator.Error!Bdd {    const index: usize = @intCast(label);    if (index < var_bdds.len) return var_bdds[index];    return manager.getOrInsert(Node.init(label, Bdd.FALSE, Bdd.TRUE));}fn weightedSampleFromCache(    manager: *Manager,    bdd: Bdd,    params: *const WmcParams,    rng: std.Random,    accumulated_weight: f64,    cache: *WmcDenseCache,    var_bdds: []const Bdd,) Allocator.Error!WeightedSampleResult {    if (bdd.isTrue()) {        return WeightedSampleResult{            .sample = Bdd.TRUE,            .probability = accumulated_weight,        };    }    if (bdd.isFalse()) {        return WeightedSampleResult{            .sample = Bdd.FALSE,            .probability = 0.0,        };    }    const node = manager.getNode(bdd);    const weight = params.getWeight(node.var_label);    const low_child = if (bdd.complement) node.low.neg() else node.low;    const high_child = if (bdd.complement) node.high.neg() else node.high;    const wmc_low = cachedWmc(manager, low_child, params, cache);    const wmc_high = cachedWmc(manager, high_child, params, cache);    const weighted_low = weight.low * wmc_low;    const weighted_high = weight.high * wmc_high;    const total = weighted_low + weighted_high;    if (total == 0.0) {        return WeightedSampleResult{            .sample = Bdd.FALSE,            .probability = 0.0,        };    }    const prob_high = weighted_high / total;    const r = rng.float(f64);    const var_bdd = try sampleVarBdd(manager, var_bdds, node.var_label);    if (r < prob_high) {        const sub_result = try weightedSampleFromCache(            manager,            high_child,            params,            rng,            accumulated_weight * weight.high,            cache,            var_bdds,        );        if (sub_result.sample.isFalse()) {            return sub_result;        }        const sample_bdd = try manager.bddAnd(var_bdd, sub_result.sample);        return WeightedSampleResult{            .sample = sample_bdd,            .probability = sub_result.probability,        };    } else {        const sub_result = try weightedSampleFromCache(            manager,            low_child,            params,            rng,            accumulated_weight * weight.low,            cache,            var_bdds,        );        if (sub_result.sample.isFalse()) {            return sub_result;        }        const sample_bdd = try manager.bddAnd(var_bdd.neg(), sub_result.sample);        return WeightedSampleResult{            .sample = sample_bdd,            .probability = sub_result.probability,        };    }}const BddPath = struct {    bdd: Bdd,    probability: f64,};fn bdd_path_more_probable(_: void, a: BddPath, b: BddPath) bool {    return a.probability > b.probability;}pub fn topKPaths(    manager: *Manager,    bdd: Bdd,    k: usize,    params: *const WmcParams,    allocator: Allocator,) !Bdd {    if (bdd.isFalse() or k == 0) {        return Bdd.FALSE;    }    if (bdd.isTrue()) {        return Bdd.TRUE;    }    var paths: std.ArrayList(BddPath) = .empty;    defer paths.deinit(allocator);    try enumeratePaths(manager, bdd, Bdd.TRUE, params, 1.0, &paths, allocator);    std.mem.sort(BddPath, paths.items, {}, bdd_path_more_probable);    var result = Bdd.FALSE;    const limit = @min(k, paths.items.len);    for (paths.items[0..limit]) |path| {        result = try manager.bddOr(result, path.bdd);    }    return result;}fn enumeratePaths(    manager: *Manager,    bdd: Bdd,    current_path: Bdd,    params: *const WmcParams,    current_prob: f64,    paths: *std.ArrayList(BddPath),    allocator: Allocator,) !void {    if (bdd.isFalse()) {        return;    }    if (bdd.isTrue()) {        try paths.append(allocator, BddPath{            .bdd = current_path,            .probability = current_prob,        });        return;    }    const node = manager.getNode(bdd);    const weight = params.getWeight(node.var_label);    const low_child = if (bdd.complement) node.low.neg() else node.low;    const high_child = if (bdd.complement) node.high.neg() else node.high;    const var_bdd = try manager.getOrInsert(Node.init(node.var_label, Bdd.FALSE, Bdd.TRUE));    if (!high_child.isFalse()) {        const new_path = try manager.bddAnd(current_path, var_bdd);        try enumeratePaths(manager, high_child, new_path, params, current_prob * weight.high, paths, allocator);    }    if (!low_child.isFalse()) {        const new_path = try manager.bddAnd(current_path, var_bdd.neg());        try enumeratePaths(manager, low_child, new_path, params, current_prob * weight.low, paths, allocator);    }}test "weighted sample - single variable" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.3, 0.7);    const x = try manager.newVar(true);    var prng = std.Random.DefaultPrng.init(12345);    const rng = prng.random();    for (0..10) |_| {        const result = try weightedSample(&manager, x, &params, rng);        try std.testing.expect(manager.eq(result.sample, x));        try std.testing.expectApproxEqAbs(@as(f64, 0.7), result.probability, 1e-10);    }}test "weighted sample - literal guard avoids allocation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.25, 0.75);    const x = try manager.newVar(true);    var empty: [0]u8 = .{};    var fixed = std.heap.FixedBufferAllocator.init(&empty);    const original_allocator = manager.allocator;    manager.allocator = fixed.allocator();    defer manager.allocator = original_allocator;    var prng = std.Random.DefaultPrng.init(20260608);    const rng = prng.random();    const positive = try weightedSample(&manager, x, &params, rng);    try std.testing.expect(manager.eq(positive.sample, x));    try std.testing.expectApproxEqAbs(@as(f64, 0.75), positive.probability, 1e-10);    const negative = try weightedSample(&manager, x.neg(), &params, rng);    try std.testing.expect(manager.eq(negative.sample, x.neg()));    try std.testing.expectApproxEqAbs(@as(f64, 0.25), negative.probability, 1e-10);}test "weighted sample - two variable AND" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.5, 0.5);    try params.setWeight(1, 0.5, 0.5);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    var prng = std.Random.DefaultPrng.init(54321);    const rng = prng.random();    for (0..20) |_| {        const result = try weightedSample(&manager, x_and_y, &params, rng);        try std.testing.expect(!result.sample.isFalse());        const check = try manager.bddImplies(result.sample, x_and_y);        try std.testing.expect(check.isTrue());    }}test "weighted sampler - deterministic sequence" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.2, 0.8);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_or_y = try manager.bddOr(x, y);    var sampler = try WeightedSampler.init(allocator, &manager, x_or_y, &params);    defer sampler.deinit();    const num_samples: usize = 32;    var expected: [num_samples]Bdd = undefined;    var prng_a = std.Random.DefaultPrng.init(2026);    const rng_a = prng_a.random();    for (0..num_samples) |idx| {        const result = try sampler.sample(rng_a);        expected[idx] = result.sample;    }    var prng_b = std.Random.DefaultPrng.init(2026);    const rng_b = prng_b.random();    for (0..num_samples) |idx| {        const result = try sampler.sample(rng_b);        try std.testing.expect(manager.eq(result.sample, expected[idx]));    }}test "weighted sampler - frequency matches exact WMC" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    const x_low: f64 = 0.25;    const x_high: f64 = 0.75;    const y_low: f64 = 0.35;    const y_high: f64 = 0.65;    try params.setWeight(0, x_low, x_high);    try params.setWeight(1, y_low, y_high);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_or_y = try manager.bddOr(x, y);    var sampler = try WeightedSampler.init(allocator, &manager, x_or_y, &params);    defer sampler.deinit();    const not_x_and_y = try manager.bddAnd(x.neg(), y);    var prng = std.Random.DefaultPrng.init(4242);    const rng = prng.random();    var count_x: usize = 0;    var count_not_x_and_y: usize = 0;    const num_samples: usize = 20000;    for (0..num_samples) |_| {        const result = try sampler.sample(rng);        if (manager.eq(result.sample, x)) {            count_x += 1;        } else if (manager.eq(result.sample, not_x_and_y)) {            count_not_x_and_y += 1;        } else {            try std.testing.expect(false);        }    }    const total_mass = x_high + x_low * y_high;    const expected_x = x_high / total_mass;    const observed_x = @as(f64, @floatFromInt(count_x)) / @as(f64, @floatFromInt(num_samples));    try std.testing.expectApproxEqAbs(expected_x, observed_x, 0.02);    try std.testing.expectEqual(num_samples, count_x + count_not_x_and_y);}test "top_k_paths - simple BDD" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.2, 0.8);    try params.setWeight(1, 0.3, 0.7);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_or_y = try manager.bddOr(x, y);    const top1 = try topKPaths(&manager, x_or_y, 1, &params, allocator);    try std.testing.expect(manager.eq(top1, x));    const top2 = try topKPaths(&manager, x_or_y, 2, &params, allocator);    try std.testing.expect(manager.eq(top2, x_or_y));}test "top_k_paths - AND formula" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const top1 = try topKPaths(&manager, x_and_y, 1, &params, allocator);    try std.testing.expect(manager.eq(top1, x_and_y));}test "limit config - ITE limit" {    var config = LimitConfig.init();    config.startIteLimit(100, 0, 0, 0);    try std.testing.expect(!config.checkIteLimit(50));    try std.testing.expect(!config.ite_limit_exceeded);    try std.testing.expect(config.checkIteLimit(100));    try std.testing.expect(config.ite_limit_exceeded);    config.stopIteLimit();    try std.testing.expect(config.ite_limit == null);}test "manager limits integration" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    manager.startIteLimit(5);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    _ = try manager.bddAnd(x, y);    try std.testing.expect(manager.num_recursive_calls > 0);    _ = manager.checkLimits();    manager.stopIteLimit();}test "manager ITE limit enforcement" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    manager.startIteLimit(3);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    const xy = try manager.bddAnd(x, y);    const xyz = try manager.bddAnd(xy, z);    _ = xyz;    _ = manager.checkLimits();    try std.testing.expect(manager.iteLimitExceeded());    manager.stopIteLimit();}test "manager ITE operation ceiling rejects later work" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const variable = try manager.newVar(true);    const node_count = manager.nodes.items.len;    const cache_count = manager.ite_cache.count();    manager.startIteLimit(1);    const admitted = try manager.ite(variable, Bdd.TRUE, Bdd.FALSE);    try std.testing.expectEqual(variable.toRaw(), admitted.toRaw());    try std.testing.expect(manager.checkLimits());    try std.testing.expect(manager.iteLimitExceeded());    const rejected = try manager.ite(variable, Bdd.TRUE, Bdd.FALSE);    try std.testing.expect(rejected.isFalse());    try std.testing.expect(manager.iteLimitExceeded());    try std.testing.expectEqual(node_count, manager.nodes.items.len);    try std.testing.expectEqual(cache_count, manager.ite_cache.count());    manager.stopIteLimit();}test "manager node growth quota admits the exact maximum without partial variables" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const node_baseline = manager.nodes.items.len;    manager.startIteLimit(2);    const first = try manager.newVar(true);    const second = try manager.newVar(true);    try std.testing.expect(!first.isFalse());    try std.testing.expect(!second.isFalse());    try std.testing.expectEqual(node_baseline + 2, manager.nodes.items.len);    try std.testing.expectEqual(@as(usize, 2), manager.var_order.items.len);    const rejected = try manager.newVar(true);    try std.testing.expect(rejected.isFalse());    try std.testing.expect(manager.iteLimitExceeded());    try std.testing.expectEqual(node_baseline + 2, manager.nodes.items.len);    try std.testing.expectEqual(@as(usize, 2), manager.var_order.items.len);    manager.stopIteLimit();    manager.startIteLimit(1);    const next = try manager.newVar(true);    try std.testing.expect(!next.isFalse());    try std.testing.expectEqual(node_baseline + 3, manager.nodes.items.len);    try std.testing.expectEqual(@as(usize, 3), manager.var_order.items.len);    manager.stopIteLimit();}test "manager ITE cache growth quota admits the exact maximum" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    manager.startIteLimit(2);    const first = IteKey.init(.{ .index = 1, .complement = false }, Bdd.TRUE, Bdd.FALSE);    const second = IteKey.init(.{ .index = 2, .complement = false }, Bdd.TRUE, Bdd.FALSE);    const rejected = IteKey.init(.{ .index = 3, .complement = false }, Bdd.TRUE, Bdd.FALSE);    try std.testing.expect(!manager.limits.reserveIteCacheGrowth(manager.ite_cache.count()));    try std.testing.expect(try manager.putIteCacheNoClobber(first, Bdd.TRUE));    manager.limits.releaseIteCacheGrowth();    try std.testing.expect(!manager.limits.reserveIteCacheGrowth(manager.ite_cache.count()));    try std.testing.expect(try manager.putIteCacheNoClobber(second, Bdd.TRUE));    manager.limits.releaseIteCacheGrowth();    try std.testing.expectEqual(@as(u32, 2), manager.ite_cache.count());    try std.testing.expect(manager.limits.reserveIteCacheGrowth(manager.ite_cache.count()));    try std.testing.expect(manager.iteLimitExceeded());    try std.testing.expectEqual(@as(u32, 2), manager.ite_cache.count());    try std.testing.expect(!manager.ite_cache.contains(rejected));    manager.stopIteLimit();}test "unbounded manager reports allocation failure" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var failing = std.testing.FailingAllocator.init(allocator, .{ .fail_index = 0 });    manager.allocator = failing.allocator();    defer manager.allocator = allocator;    try std.testing.expectError(error.OutOfMemory, manager.newVar(true));    try std.testing.expect(!manager.iteLimitExceeded());    try std.testing.expectEqual(@as(usize, 1), manager.nodes.items.len);    try std.testing.expectEqual(@as(usize, 0), manager.var_order.items.len);}test "bounded manager maps allocation failure to its quota surface" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    manager.startIteLimit(1);    var failing = std.testing.FailingAllocator.init(allocator, .{ .fail_index = 0 });    manager.allocator = failing.allocator();    defer manager.allocator = allocator;    const rejected = try manager.newVar(true);    try std.testing.expect(rejected.isFalse());    try std.testing.expect(manager.iteLimitExceeded());    try std.testing.expectEqual(@as(usize, 1), manager.nodes.items.len);    try std.testing.expectEqual(@as(usize, 0), manager.var_order.items.len);    manager.stopIteLimit();}test "condition cache allocation failure is observable" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    manager.condition_cache.deinit(allocator);    manager.condition_cache = .{};    var failing = std.testing.FailingAllocator.init(allocator, .{ .fail_index = 0 });    manager.allocator = failing.allocator();    defer manager.allocator = allocator;    const key = ConditionKey.init(Bdd.TRUE, 0, true);    try std.testing.expectError(error.OutOfMemory, manager.putConditionCache(key, Bdd.TRUE));    try std.testing.expect(!manager.iteLimitExceeded());    manager.startIteLimit(1);    failing.fail_index = failing.alloc_index;    try std.testing.expect(!try manager.putConditionCache(key, Bdd.TRUE));    try std.testing.expect(manager.iteLimitExceeded());    manager.stopIteLimit();}test "time limit API" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    manager.setTimeLimit(10.0);    try std.testing.expect(manager.limits.time_limit.? == 10.0);    try std.testing.expect(!manager.timeLimitExceeded());    manager.startTimeLimit(5.0);    try std.testing.expect(manager.limits.time_limit.? == 5.0);    manager.stopTimeLimit();    try std.testing.expect(manager.limits.time_limit == null);    manager.limits.time_limit_exceeded = true;    manager.limits.ite_limit_exceeded = true;    manager.resetLimitFlags();    try std.testing.expect(!manager.timeLimitExceeded());    try std.testing.expect(!manager.iteLimitExceeded());    manager.startTimeLimit(0.001);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    var formula = try manager.bddAnd(x, y);    for (0..100) |_| {        formula = try manager.bddOr(formula, try manager.bddAnd(y, z));        formula = try manager.bddAnd(formula, try manager.bddOr(x, z));    }    manager.stopTimeLimit();}test "toJson - constants" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const true_json = try manager.toJson(Bdd.TRUE, allocator);    defer allocator.free(true_json);    try std.testing.expectEqualStrings("{\"root\":\"true\",\"nodes\":{}}", true_json);    const false_json = try manager.toJson(Bdd.FALSE, allocator);    defer allocator.free(false_json);    try std.testing.expectEqualStrings("{\"root\":\"false\",\"nodes\":{}}", false_json);}test "toJson - variable" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const json = try manager.toJson(x, allocator);    defer allocator.free(json);    try std.testing.expect(std.mem.indexOf(u8, json, "\"root\":") != null);    try std.testing.expect(std.mem.indexOf(u8, json, "\"nodes\":") != null);    try std.testing.expect(std.mem.indexOf(u8, json, "\"var\":0") != null);    try std.testing.expect(std.mem.indexOf(u8, json, "\"high\":\"true\"") != null);    try std.testing.expect(std.mem.indexOf(u8, json, "\"low\":\"false\"") != null);}test "toJson - compound formula" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const json = try manager.toJson(x_and_y, allocator);    defer allocator.free(json);    var parsed = try std.json.parseFromSlice(std.json.Value, allocator, json, .{});    defer parsed.deinit();    try std.testing.expect(std.mem.indexOf(u8, json, "\"root\":") != null);    try std.testing.expect(std.mem.indexOf(u8, json, "\"nodes\":") != null);    try std.testing.expect(std.mem.indexOf(u8, json, "\"var\":0") != null);    try std.testing.expect(std.mem.indexOf(u8, json, "\"var\":1") != null);    try std.testing.expect(parsed.value.object.get("nodes") != null);}test "printStats" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    _ = try manager.newVar(true);    _ = try manager.newVar(true);    const stats = try manager.printStats(allocator);    defer allocator.free(stats);    try std.testing.expect(std.mem.indexOf(u8, stats, "Variables: 2") != null);    try std.testing.expect(std.mem.indexOf(u8, stats, "Nodes:") != null);    try std.testing.expect(std.mem.indexOf(u8, stats, "Recursive calls:") != null);}test "deepCopy - basic" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    var copy = try deepCopy(&manager, x_and_y, allocator);    defer copy.deinit();    try std.testing.expect(!copy.isConst());    try std.testing.expect(!copy.isTrue());    try std.testing.expect(!copy.isFalse());    const json = try copy.toJson(allocator);    defer allocator.free(json);    try std.testing.expect(std.mem.indexOf(u8, json, "\"root\":") != null);    try std.testing.expect(std.mem.indexOf(u8, json, "\"nodes\":") != null);}test "deepCopy - constants" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var true_copy = try deepCopy(&manager, Bdd.TRUE, allocator);    defer true_copy.deinit();    try std.testing.expect(true_copy.isTrue());    var false_copy = try deepCopy(&manager, Bdd.FALSE, allocator);    defer false_copy.deinit();    try std.testing.expect(false_copy.isFalse());}test "finite difference derivative validation - single variable" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const epsilon: f64 = 1e-6;    const test_probs = [_]f64{ 0.1, 0.3, 0.5, 0.7, 0.9 };    for (test_probs) |p| {        var params_dual = WmcParams.initDual(allocator, 1);        defer params_dual.deinit();        var zero_partials = [_]f64{0.0};        var one_partials = [_]f64{1.0};        try params_dual.setWeightDeriv(0, 1.0 - p, &zero_partials, p, &one_partials);        var dual_result = try wmcDual(&manager, x, &params_dual, allocator);        defer dual_result.deinit();        const analytic_grad = dual_result.partials[0];        var params_plus = WmcParams.init(allocator);        defer params_plus.deinit();        try params_plus.setWeight(0, 1.0 - (p + epsilon), p + epsilon);        var params_minus = WmcParams.init(allocator);        defer params_minus.deinit();        try params_minus.setWeight(0, 1.0 - (p - epsilon), p - epsilon);        const wmc_plus = wmc(&manager, x, &params_plus);        const wmc_minus = wmc(&manager, x, &params_minus);        const fd_grad = (wmc_plus - wmc_minus) / (2.0 * epsilon);        try std.testing.expectApproxEqAbs(analytic_grad, fd_grad, 1e-5);    }}test "finite difference derivative validation - two variable AND" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const px: f64 = 0.6;    const py: f64 = 0.7;    const epsilon: f64 = 1e-6;    var params_dual = WmcParams.initDual(allocator, 2);    defer params_dual.deinit();    var zero_partials = [_]f64{ 0.0, 0.0 };    var x_partials = [_]f64{ 1.0, 0.0 };    var y_partials = [_]f64{ 0.0, 1.0 };    try params_dual.setWeightDeriv(0, 1.0 - px, &zero_partials, px, &x_partials);    try params_dual.setWeightDeriv(1, 1.0 - py, &zero_partials, py, &y_partials);    var dual_result = try wmcDual(&manager, x_and_y, &params_dual, allocator);    defer dual_result.deinit();    var params_plus = WmcParams.init(allocator);    defer params_plus.deinit();    try params_plus.setWeight(0, 1.0 - (px + epsilon), px + epsilon);    try params_plus.setWeight(1, 1.0 - py, py);    var params_minus = WmcParams.init(allocator);    defer params_minus.deinit();    try params_minus.setWeight(0, 1.0 - (px - epsilon), px - epsilon);    try params_minus.setWeight(1, 1.0 - py, py);    const fd_grad_x = (wmc(&manager, x_and_y, &params_plus) - wmc(&manager, x_and_y, &params_minus)) / (2.0 * epsilon);    try std.testing.expectApproxEqAbs(dual_result.partials[0], fd_grad_x, 1e-5);    var params_plus_y = WmcParams.init(allocator);    defer params_plus_y.deinit();    try params_plus_y.setWeight(0, 1.0 - px, px);    try params_plus_y.setWeight(1, 1.0 - (py + epsilon), py + epsilon);    var params_minus_y = WmcParams.init(allocator);    defer params_minus_y.deinit();    try params_minus_y.setWeight(0, 1.0 - px, px);    try params_minus_y.setWeight(1, 1.0 - (py - epsilon), py - epsilon);    const fd_grad_y = (wmc(&manager, x_and_y, &params_plus_y) - wmc(&manager, x_and_y, &params_minus_y)) / (2.0 * epsilon);    try std.testing.expectApproxEqAbs(dual_result.partials[1], fd_grad_y, 1e-5);}test "finite difference derivative validation - XOR formula" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const formula = try manager.bddXor(x, y);    const px: f64 = 0.4;    const py: f64 = 0.6;    const epsilon: f64 = 1e-6;    var params_dual = WmcParams.initDual(allocator, 4);    defer params_dual.deinit();    var x_high_partials = [_]f64{ 1.0, 0.0, 0.0, 0.0 };    var x_low_partials = [_]f64{ 0.0, 1.0, 0.0, 0.0 };    var y_high_partials = [_]f64{ 0.0, 0.0, 1.0, 0.0 };    var y_low_partials = [_]f64{ 0.0, 0.0, 0.0, 1.0 };    try params_dual.setWeightDeriv(0, 1.0 - px, &x_low_partials, px, &x_high_partials);    try params_dual.setWeightDeriv(1, 1.0 - py, &y_low_partials, py, &y_high_partials);    var dual_result = try wmcDual(&manager, formula, &params_dual, allocator);    defer dual_result.deinit();    const grad_px = dual_result.partials[0] - dual_result.partials[1];    const grad_py = dual_result.partials[2] - dual_result.partials[3];    var params_px_plus = WmcParams.init(allocator);    defer params_px_plus.deinit();    try params_px_plus.setWeight(0, 1.0 - (px + epsilon), px + epsilon);    try params_px_plus.setWeight(1, 1.0 - py, py);    var params_px_minus = WmcParams.init(allocator);    defer params_px_minus.deinit();    try params_px_minus.setWeight(0, 1.0 - (px - epsilon), px - epsilon);    try params_px_minus.setWeight(1, 1.0 - py, py);    const fd_grad_x = (wmc(&manager, formula, &params_px_plus) - wmc(&manager, formula, &params_px_minus)) / (2.0 * epsilon);    try std.testing.expectApproxEqAbs(grad_px, fd_grad_x, 1e-4);    var params_py_plus = WmcParams.init(allocator);    defer params_py_plus.deinit();    try params_py_plus.setWeight(0, 1.0 - px, px);    try params_py_plus.setWeight(1, 1.0 - (py + epsilon), py + epsilon);    var params_py_minus = WmcParams.init(allocator);    defer params_py_minus.deinit();    try params_py_minus.setWeight(0, 1.0 - px, px);    try params_py_minus.setWeight(1, 1.0 - (py - epsilon), py - epsilon);    const fd_grad_y = (wmc(&manager, formula, &params_py_plus) - wmc(&manager, formula, &params_py_minus)) / (2.0 * epsilon);    try std.testing.expectApproxEqAbs(grad_py, fd_grad_y, 1e-4);}test "sampling distribution matches WMC - simple verification" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.3, 0.7);    const x = try manager.newVar(true);    var prng = std.Random.DefaultPrng.init(42);    const rng = prng.random();    var true_count: usize = 0;    const num_samples: usize = 10000;    for (0..num_samples) |_| {        const result = try weightedSample(&manager, x, &params, rng);        try std.testing.expect(manager.eq(result.sample, x));        true_count += 1;    }    try std.testing.expectEqual(num_samples, true_count);}test "sampling coverage - all paths found for OR" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.5, 0.5);    try params.setWeight(1, 0.5, 0.5);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_or_y = try manager.bddOr(x, y);    var seen_x_true = false;    var seen_x_false_y_true = false;    var prng = std.Random.DefaultPrng.init(12345);    const rng = prng.random();    for (0..1000) |_| {        const result = try weightedSample(&manager, x_or_y, &params, rng);        if (manager.eq(result.sample, x)) {            seen_x_true = true;        }        const not_x_and_y = try manager.bddAnd(x.neg(), y);        if (manager.eq(result.sample, not_x_and_y)) {            seen_x_false_y_true = true;        }    }    try std.testing.expect(seen_x_true);    try std.testing.expect(seen_x_false_y_true);}test "top_k_paths covers exact WMC" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    try params.setWeight(2, 0.5, 0.5);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    const xy = try manager.bddAnd(x, y);    const formula = try manager.bddOr(xy, z);    const exact_wmc = wmc(&manager, formula, &params);    const top_many = try topKPaths(&manager, formula, 100, &params, allocator);    const top_wmc = wmc(&manager, top_many, &params);    try std.testing.expectApproxEqAbs(exact_wmc, top_wmc, 1e-10);}test "CNF benchmark - 3-SAT clause" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const z = try manager.newVar(true);    try params.setWeight(0, 0.5, 0.5);    try params.setWeight(1, 0.5, 0.5);    try params.setWeight(2, 0.5, 0.5);    const clause1 = try manager.bddOr(try manager.bddOr(x, y), z);    const clause2 = try manager.bddOr(try manager.bddOr(x.neg(), y), z.neg());    const clause3 = try manager.bddOr(try manager.bddOr(x, y.neg()), z);    const cnf = try manager.bddAnd(try manager.bddAnd(clause1, clause2), clause3);    const result = wmc(&manager, cnf, &params);    try std.testing.expectApproxEqAbs(@as(f64, 5.0 / 8.0), result, 1e-10);}test "complement edge WMC correctness - complex formula" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const formula = try manager.bddImplies(x, y);    const neg_formula = manager.bddNot(formula);    const wmc_formula = wmc(&manager, formula, &params);    const wmc_neg = wmc(&manager, neg_formula, &params);    try std.testing.expectApproxEqAbs(@as(f64, 1.0), wmc_formula + wmc_neg, 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.72), wmc_formula, 1e-10);}test "complement edge WMC - double negation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    try params.setWeight(0, 0.25, 0.75);    const x = try manager.newVar(true);    const not_x = manager.bddNot(x);    const not_not_x = manager.bddNot(not_x);    try std.testing.expect(manager.eq(x, not_not_x));    const wmc_x = wmc(&manager, x, &params);    const wmc_nnx = wmc(&manager, not_not_x, &params);    try std.testing.expectApproxEqAbs(wmc_x, wmc_nnx, 1e-10);}test "absorption law: a AND (a OR b) = a" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const a = try manager.newVar(true);    const b = try manager.newVar(true);    const a_or_b = try manager.bddOr(a, b);    const result = try manager.bddAnd(a, a_or_b);    try std.testing.expect(manager.eq(result, a));}test "absorption law: a OR (a AND b) = a" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const a = try manager.newVar(true);    const b = try manager.newVar(true);    const a_and_b = try manager.bddAnd(a, b);    const result = try manager.bddOr(a, a_and_b);    try std.testing.expect(manager.eq(result, a));}test "distributive law: a AND (b OR c) = (a AND b) OR (a AND c)" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const a = try manager.newVar(true);    const b = try manager.newVar(true);    const c = try manager.newVar(true);    const b_or_c = try manager.bddOr(b, c);    const lhs = try manager.bddAnd(a, b_or_c);    const a_and_b = try manager.bddAnd(a, b);    const a_and_c = try manager.bddAnd(a, c);    const rhs = try manager.bddOr(a_and_b, a_and_c);    try std.testing.expect(manager.eq(lhs, rhs));}test "consensus theorem: (a AND b) OR (!a AND c) OR (b AND c) = (a AND b) OR (!a AND c)" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    const a = try manager.newVar(true);    const b = try manager.newVar(true);    const c = try manager.newVar(true);    const a_and_b = try manager.bddAnd(a, b);    const not_a_and_c = try manager.bddAnd(a.neg(), c);    const b_and_c = try manager.bddAnd(b, c);    const lhs = try manager.bddOr(try manager.bddOr(a_and_b, not_a_and_c), b_and_c);    const rhs = try manager.bddOr(a_and_b, not_a_and_c);    try std.testing.expect(manager.eq(lhs, rhs));}const AlarmFixture = struct {    alarm: Bdd,    earthquake: Bdd,    burglary: Bdd,};fn createAlarmFixture(manager: *Manager) Allocator.Error!AlarmFixture {    const earthquake = try manager.newVar(true);    const burglary = try manager.newVar(true);    const alarm = try manager.bddOr(earthquake, burglary);    return .{ .alarm = alarm, .earthquake = earthquake, .burglary = burglary };}test "fixture - alarm model WMC" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    const fixture = try createAlarmFixture(&manager);    try params.setWeight(0, 0.9999, 0.0001);    try params.setWeight(1, 0.999, 0.001);    const alarm_prob = wmc(&manager, fixture.alarm, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.0010999), alarm_prob, 1e-6);}const ConditionalFixture = struct {    result: Bdd,    earthquake: Bdd,    phone_bad: Bdd,    phone_good: Bdd,};fn createConditionalFixture(manager: *Manager) Allocator.Error!ConditionalFixture {    const earthquake = try manager.newVar(true);    const phone_bad = try manager.newVar(true);    const phone_good = try manager.newVar(true);    const case_eq = try manager.bddAnd(earthquake, phone_bad);    const case_normal = try manager.bddAnd(earthquake.neg(), phone_good);    const result = try manager.bddOr(case_eq, case_normal);    return .{ .result = result, .earthquake = earthquake, .phone_bad = phone_bad, .phone_good = phone_good };}test "fixture - conditional model WMC" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    const fixture = try createConditionalFixture(&manager);    try params.setWeight(0, 0.9999, 0.0001);    try params.setWeight(1, 0.3, 0.7);    try params.setWeight(2, 0.01, 0.99);    const phone_prob = wmc(&manager, fixture.result, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.989971), phone_prob, 1e-6);}test "WmcContext - basic caching correctness" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const result1 = ctx.wmcCached(&manager, x_and_y, &params);    const expected = wmc(&manager, x_and_y, &params);    try std.testing.expectApproxEqAbs(expected, result1, 1e-10);    const result2 = ctx.wmcCached(&manager, x_and_y, &params);    try std.testing.expectApproxEqAbs(result1, result2, 1e-10);    const stats = ctx.getStats();    try std.testing.expect(stats.hits > 0);    try std.testing.expect(stats.misses > 0);}test "WmcContext - cache invalidation on weight change" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    const x = try manager.newVar(true);    const result1 = ctx.wmcCached(&manager, x, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.7), result1, 1e-10);    try params.setWeight(0, 0.2, 0.8);    ctx.invalidateWeights();    const result2 = ctx.wmcCached(&manager, x, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.8), result2, 1e-10);}test "WmcContext - cache size and trimming" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    for (0..10) |i| {        try params.setWeight(@intCast(i), 0.5, 0.5);        const v = try manager.newVar(true);        _ = ctx.wmcCached(&manager, v, &params);    }    const size_before = ctx.cacheSize();    try std.testing.expect(size_before >= 10);    const evicted = ctx.trimToSize(5);    try std.testing.expect(evicted > 0);    try std.testing.expect(ctx.cacheSize() <= 5);}test "WmcContext - structure version invalidation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.5, 0.5);    const x = try manager.newVar(true);    _ = ctx.wmcCached(&manager, x, &params);    ctx.invalidateAll();    _ = ctx.wmcCached(&manager, x, &params);    const stats_after = ctx.getStats();    try std.testing.expect(stats_after.invalidations == 1);}test "WmcContext - hit rate calculation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    const x = try manager.newVar(true);    _ = ctx.wmcCached(&manager, x, &params);    _ = ctx.wmcCached(&manager, x, &params);    const stats = ctx.getStats();    const hit_rate = stats.hitRate();    try std.testing.expect(hit_rate > 0.0);    try std.testing.expect(hit_rate <= 1.0);}test "WmcContext - correctness on complex BDD" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    const fixture = try createAlarmFixture(&manager);    try params.setWeight(0, 0.9999, 0.0001);    try params.setWeight(1, 0.999, 0.001);    const cached_result = ctx.wmcCached(&manager, fixture.alarm, &params);    const direct_result = wmc(&manager, fixture.alarm, &params);    try std.testing.expectApproxEqAbs(direct_result, cached_result, 1e-10);}test "WmcContext - manager change clears stale entries" {    const allocator = std.testing.allocator;    var manager_a = try Manager.init(allocator);    defer manager_a.deinit();    var manager_b = try Manager.init(allocator);    defer manager_b.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const ax = try manager_a.newVar(true);    const ay = try manager_a.newVar(true);    const a_formula = try manager_a.bddAnd(ax, ay);    const bx = try manager_b.newVar(true);    const by = try manager_b.newVar(true);    const b_formula = try manager_b.bddOr(bx, by);    try std.testing.expectEqual(a_formula.toRaw(), b_formula.toRaw());    const first = ctx.wmcCached(&manager_a, a_formula, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.42), first, 1e-10);    const second = ctx.wmcCached(&manager_b, b_formula, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.88), second, 1e-10);}test "WmcContext - multiple queries same BDD" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    var sum: f64 = 0;    for (0..100) |_| {        sum += ctx.wmcCached(&manager, x_and_y, &params);    }    const expected = 0.7 * 0.6 * 100;    try std.testing.expectApproxEqAbs(expected, sum, 1e-8);    const stats = ctx.getStats();    try std.testing.expect(stats.hitRate() > 0.9);}test "WmcContext - invalidateForVars correctness" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const result1 = ctx.wmcCached(&manager, x_and_y, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.42), result1, 1e-10);    try params.setWeight(0, 0.1, 0.9);    ctx.invalidateForVars(&manager, &[_]VarLabel{0});    const result2 = ctx.wmcCached(&manager, x_and_y, &params);    const expected_new = wmc(&manager, x_and_y, &params);    try std.testing.expectApproxEqAbs(expected_new, result2, 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.54), result2, 1e-10);    try std.testing.expect(@abs(result2 - result1) > 0.1);}test "WmcContext - invalidateForVars preserves unrelated cache entries" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    _ = ctx.wmcCached(&manager, x, &params);    _ = ctx.wmcCached(&manager, y, &params);    try std.testing.expectEqual(@as(usize, 2), ctx.cacheSize());    try params.setWeight(0, 0.1, 0.9);    ctx.invalidateForVars(&manager, &[_]VarLabel{0});    try std.testing.expectEqual(@as(usize, 1), ctx.cacheSize());    const stats_before_y = ctx.getStats();    const y_result = ctx.wmcCached(&manager, y, &params);    const stats_after_y = ctx.getStats();    try std.testing.expectApproxEqAbs(@as(f64, 0.6), y_result, 1e-10);    try std.testing.expectEqual(stats_before_y.hits + 1, stats_after_y.hits);    const x_result = ctx.wmcCached(&manager, x, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.9), x_result, 1e-10);}test "WmcContext - invalidateForVars removes recursive dependent entries" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    try params.setWeight(1, 0.4, 0.6);    const x = try manager.newVar(true);    const y = try manager.newVar(true);    const x_and_y = try manager.bddAnd(x, y);    const result1 = ctx.wmcCached(&manager, x_and_y, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.42), result1, 1e-10);    try params.setWeight(1, 0.2, 0.8);    ctx.invalidateForVars(&manager, &[_]VarLabel{1});    const result2 = ctx.wmcCached(&manager, x_and_y, &params);    const expected_new = wmc(&manager, x_and_y, &params);    try std.testing.expectApproxEqAbs(expected_new, result2, 1e-10);    try std.testing.expectApproxEqAbs(@as(f64, 0.56), result2, 1e-10);}test "WmcContext - invalidateForVars keeps cache version stable" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.3, 0.7);    const x = try manager.newVar(true);    const result1 = ctx.wmcCached(&manager, x, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.7), result1, 1e-10);    try params.setWeight(0, 0.1, 0.9);    ctx.invalidateForVars(&manager, &[_]VarLabel{0});    const result2 = ctx.wmcCached(&manager, x, &params);    try std.testing.expectApproxEqAbs(@as(f64, 0.9), result2, 1e-10);    try std.testing.expectEqual(@as(u64, 0), ctx.params_version);}test "WmcContext - memory growth with lazy invalidation" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.5, 0.5);    const x = try manager.newVar(true);    for (0..10) |_| {        _ = ctx.wmcCached(&manager, x, &params);        ctx.invalidateWeights();    }    try std.testing.expect(ctx.cacheSize() >= 1);    _ = ctx.trimToSize(1);    try std.testing.expect(ctx.cacheSize() <= 1);}test "WmcContext - clear resets everything" {    const allocator = std.testing.allocator;    var manager = try Manager.init(allocator);    defer manager.deinit();    var params = WmcParams.init(allocator);    defer params.deinit();    var ctx = WmcContext.init(allocator);    defer ctx.deinit();    try params.setWeight(0, 0.5, 0.5);    const x = try manager.newVar(true);    _ = ctx.wmcCached(&manager, x, &params);    ctx.invalidateWeights();    _ = ctx.wmcCached(&manager, x, &params);    try std.testing.expect(ctx.cacheSize() > 0);    try std.testing.expect(ctx.getStats().hits > 0 or ctx.getStats().misses > 0);    ctx.clear();    try std.testing.expectEqual(@as(usize, 0), ctx.cacheSize());    try std.testing.expectEqual(@as(u64, 0), ctx.getStats().hits);    try std.testing.expectEqual(@as(u64, 0), ctx.getStats().misses);    try std.testing.expectEqual(@as(u64, 0), ctx.params_version);    try std.testing.expectEqual(@as(u64, 0), ctx.structure_version);}

Source: lib/pluck/src/root.zig:11

zig
pub const bdd = @import("bdd.zig");

Audit

Definitions1
Public names1
Members0
Version26.7.0
Revisiondaab053ee433