tiny.pluck.bdd.Manager

1pub const Manager = struct {2    const TABLE_MAX_LOAD_PERCENTAGE = 80;34    allocator: Allocator,56    nodes: std.ArrayListUnmanaged(Node),78    unique_table: std.HashMapUnmanaged(Node, NodeIndex, NodeHashContext, TABLE_MAX_LOAD_PERCENTAGE),910    unique_table_grow_at: usize,1112    ite_cache: std.HashMapUnmanaged(IteKey, Bdd, IteKeyHashContext, TABLE_MAX_LOAD_PERCENTAGE),1314    ite_cache_grow_at: usize,1516    condition_cache: std.AutoHashMapUnmanaged(ConditionKey, Bdd),1718    var_order: std.ArrayListUnmanaged(u32),1920    min_vars: std.ArrayListUnmanaged(VarLabel),2122    max_vars: std.ArrayListUnmanaged(VarLabel),2324    num_recursive_calls: u64,2526    ite_cache_hits: u64,2728    ite_cache_misses: u64,2930    unique_table_grows: u64,3132    ite_cache_grows: u64,3334    limits: LimitConfig,3536    const INITIAL_MANAGER_CAPACITY = 4096;37    const INITIAL_CONDITION_CACHE_CAPACITY = 256;3839    fn tableLoadThreshold(capacity: usize) usize {40        return (capacity * TABLE_MAX_LOAD_PERCENTAGE) / 100;41    }4243    pub fn init(allocator: Allocator) !Manager {44        var nodes = std.ArrayListUnmanaged(Node).empty;45        errdefer nodes.deinit(allocator);4647        var min_vars = std.ArrayListUnmanaged(VarLabel).empty;48        errdefer min_vars.deinit(allocator);4950        var max_vars = std.ArrayListUnmanaged(VarLabel).empty;51        errdefer max_vars.deinit(allocator);5253        try nodes.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);54        try min_vars.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);55        try max_vars.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);5657        try nodes.append(allocator, Node.init(NO_VAR, Bdd.TRUE, Bdd.TRUE));58        try min_vars.append(allocator, NO_VAR);59        try max_vars.append(allocator, NO_VAR);6061        var unique_table = std.HashMapUnmanaged(Node, NodeIndex, NodeHashContext, TABLE_MAX_LOAD_PERCENTAGE){};62        errdefer unique_table.deinit(allocator);63        try unique_table.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);6465        var ite_cache = std.HashMapUnmanaged(IteKey, Bdd, IteKeyHashContext, TABLE_MAX_LOAD_PERCENTAGE){};66        errdefer ite_cache.deinit(allocator);67        try ite_cache.ensureTotalCapacity(allocator, INITIAL_MANAGER_CAPACITY);6869        var condition_cache = std.AutoHashMapUnmanaged(ConditionKey, Bdd){};70        errdefer condition_cache.deinit(allocator);71        try condition_cache.ensureTotalCapacity(allocator, INITIAL_CONDITION_CACHE_CAPACITY);7273        return Manager{74            .allocator = allocator,75            .nodes = nodes,76            .unique_table = unique_table,77            .unique_table_grow_at = tableLoadThreshold(unique_table.capacity()),78            .ite_cache = ite_cache,79            .ite_cache_grow_at = tableLoadThreshold(ite_cache.capacity()),80            .condition_cache = condition_cache,81            .var_order = std.ArrayListUnmanaged(u32).empty,82            .min_vars = min_vars,83            .max_vars = max_vars,84            .num_recursive_calls = 0,85            .ite_cache_hits = 0,86            .ite_cache_misses = 0,87            .unique_table_grows = 0,88            .ite_cache_grows = 0,89            .limits = LimitConfig.init(),90        };91    }9293    pub fn deinit(self: *Manager) void {94        self.nodes.deinit(self.allocator);95        self.unique_table.deinit(self.allocator);96        self.ite_cache.deinit(self.allocator);97        self.condition_cache.deinit(self.allocator);98        self.var_order.deinit(self.allocator);99        self.min_vars.deinit(self.allocator);100        self.max_vars.deinit(self.allocator);101    }102103    pub fn numVars(self: *const Manager) usize {104        return self.var_order.items.len;105    }106107    pub fn newVar(self: *Manager, polarity: bool) Allocator.Error!Bdd {108        const label: VarLabel = @intCast(self.var_order.items.len);109        const node = Node.init(label, Bdd.FALSE, Bdd.TRUE);110111        if (!try self.prepareVariableInsert(node)) return Bdd.FALSE;112113        self.var_order.appendAssumeCapacity(label);114        const bdd = self.insertCanonicalAssumeCapacity(node);115116        return if (polarity) bdd else bdd.neg();117    }118119    pub fn newVarAtPosition(self: *Manager, position: u32, polarity: bool) Allocator.Error!Bdd {120        const label: VarLabel = @intCast(self.var_order.items.len);121        const node = Node.init(label, Bdd.FALSE, Bdd.TRUE);122123        if (!try self.prepareVariableInsert(node)) return Bdd.FALSE;124125        for (self.var_order.items) |*pos| {126            if (pos.* >= position) {127                pos.* += 1;128            }129        }130        self.var_order.appendAssumeCapacity(position);131132        const bdd = self.insertCanonicalAssumeCapacity(node);133134        return if (polarity) bdd else bdd.neg();135    }136137    fn prepareVariableInsert(self: *Manager, node: Node) Allocator.Error!bool {138        std.debug.assert(self.unique_table.getContext(node, NodeHashContext{}) == null);139        if (self.limits.checkNodeGrowth(self.nodes.items.len)) return false;140        self.ensureCanonicalInsertCapacity() catch |err| {141            if (self.limits.boundedAllocationFailed()) return false;142            return err;143        };144        self.var_order.ensureUnusedCapacity(self.allocator, 1) catch |err| {145            if (self.limits.boundedAllocationFailed()) return false;146            return err;147        };148        return true;149    }150151    fn getOrInsert(self: *Manager, node: Node) Allocator.Error!Bdd {152        if (node.low.toRaw() == node.high.toRaw()) {153            return node.low;154        }155156        if (node.high.complement) {157            const canonical = Node.init(158                node.var_label,159                node.low.neg(),160                node.high.neg(),161            );162            return (try self.insertCanonical(canonical)).neg();163        } else {164            return self.insertCanonical(node);165        }166    }167168    fn insertCanonical(self: *Manager, node: Node) Allocator.Error!Bdd {169        if (self.unique_table.getContext(node, NodeHashContext{})) |index| {170            return Bdd{ .index = @intCast(index), .complement = false };171        }172        if (self.limits.checkNodeGrowth(self.nodes.items.len)) return Bdd.FALSE;173        self.ensureCanonicalInsertCapacity() catch |err| {174            if (self.limits.boundedAllocationFailed()) return Bdd.FALSE;175            return err;176        };177178        return self.insertCanonicalAssumeCapacity(node);179    }180181    fn insertCanonicalAssumeCapacity(self: *Manager, node: Node) Bdd {182        const entry = self.unique_table.getOrPutAssumeCapacityContext(node, NodeHashContext{});183        std.debug.assert(!entry.found_existing);184185        const idx: u31 = @intCast(self.nodes.items.len);186        self.nodes.appendAssumeCapacity(node);187188        const low_min = self.min_vars.items[node.low.index];189        const low_max = self.max_vars.items[node.low.index];190        const high_min = self.min_vars.items[node.high.index];191        const high_max = self.max_vars.items[node.high.index];192193        var min_var = node.var_label;194        if (low_min != NO_VAR and low_min < min_var) min_var = low_min;195        if (high_min != NO_VAR and high_min < min_var) min_var = high_min;196197        var max_var = node.var_label;198        if (low_max != NO_VAR and low_max > max_var) max_var = low_max;199        if (high_max != NO_VAR and high_max > max_var) max_var = high_max;200201        self.min_vars.appendAssumeCapacity(min_var);202        self.max_vars.appendAssumeCapacity(max_var);203        entry.value_ptr.* = idx;204205        return Bdd{ .index = idx, .complement = false };206    }207208    fn ensureCanonicalInsertCapacity(self: *Manager) Allocator.Error!void {209        if (self.nodes.items.len >= self.nodes.capacity) {210            const reserve = @max(self.nodes.capacity, INITIAL_MANAGER_CAPACITY);211            const target = self.nodes.items.len + reserve;212            try self.nodes.ensureTotalCapacity(self.allocator, target);213            try self.min_vars.ensureTotalCapacity(self.allocator, target);214            try self.max_vars.ensureTotalCapacity(self.allocator, target);215        }216217        const count = self.unique_table.count();218        if (count < self.unique_table_grow_at) return;219220        const capacity = self.unique_table.capacity();221        const reserve = @max(capacity, INITIAL_MANAGER_CAPACITY);222        try self.unique_table.ensureTotalCapacity(self.allocator, count + reserve);223        self.unique_table_grows += 1;224        self.unique_table_grow_at = tableLoadThreshold(self.unique_table.capacity());225    }226227    pub inline fn getNode(self: *const Manager, bdd: Bdd) Node {228        return self.nodes.items[bdd.index];229    }230231    pub inline fn topVar(self: *const Manager, bdd: Bdd) VarLabel {232        if (bdd.isConst()) return NO_VAR;233        return self.getNode(bdd).var_label;234    }235236    pub fn getMinVar(self: *const Manager, bdd: Bdd) VarLabel {237        return self.min_vars.items[bdd.index];238    }239240    pub fn getMaxVar(self: *const Manager, bdd: Bdd) VarLabel {241        return self.max_vars.items[bdd.index];242    }243244    pub fn low(self: *const Manager, bdd: Bdd) Bdd {245        if (bdd.isConst()) return Bdd.FALSE;246        const node = self.getNode(bdd);247        return if (bdd.complement) node.low.neg() else node.low;248    }249250    pub fn high(self: *const Manager, bdd: Bdd) Bdd {251        if (bdd.isConst()) return Bdd.FALSE;252        const node = self.getNode(bdd);253        return if (bdd.complement) node.high.neg() else node.high;254    }255256    inline fn lessThan(self: *const Manager, a: VarLabel, b: VarLabel) bool {257        if (a == NO_VAR) return false;258        if (b == NO_VAR) return true;259        return self.var_order.items[a] < self.var_order.items[b];260    }261262    inline fn firstEssential(self: *const Manager, f: Bdd, g: Bdd, h: Bdd) VarLabel {263        const vf = self.topVar(f);264        const vg = self.topVar(g);265        const vh = self.topVar(h);266267        var result = vf;268        if (self.lessThan(vg, result)) result = vg;269        if (self.lessThan(vh, result)) result = vh;270        return result;271    }272273    inline fn conditionEssential(self: *const Manager, f: Bdd, lbl: VarLabel, value: bool) Bdd {274        if (f.isConst()) return f;275        const node = self.getNode(f);276        if (node.var_label != lbl) return f;277278        const result = if (value) node.high else node.low;279        return if (f.complement) result.neg() else result;280    }281282    pub fn checkLimits(self: *Manager) bool {283        if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) return true;284        if (self.limits.checkIteLimit(self.num_recursive_calls)) {285            return true;286        }287        if (self.num_recursive_calls % 1000 == 0) {288            if (self.limits.checkTimeLimit()) {289                return true;290            }291        }292        return false;293    }294295    pub fn iteLimitExceeded(self: *const Manager) bool {296        return self.limits.ite_limit_exceeded;297    }298299    pub fn timeLimitExceeded(self: *const Manager) bool {300        return self.limits.time_limit_exceeded;301    }302303    pub fn setTimeLimit(self: *Manager, limit_seconds: f64) void {304        self.limits.time_limit = limit_seconds;305        self.limits.time_limit_exceeded = false;306    }307308    pub fn startTimeLimit(self: *Manager, limit_seconds: f64) void {309        self.limits.startTimeLimit(limit_seconds);310    }311312    pub fn stopTimeLimit(self: *Manager) void {313        self.limits.stopTimeLimit();314    }315316    pub fn resetLimitFlags(self: *Manager) void {317        self.limits.time_limit_exceeded = false;318        self.limits.ite_limit_exceeded = false;319    }320321    pub fn startIteLimit(self: *Manager, limit: u64) void {322        self.limits.startIteLimit(323            limit,324            self.num_recursive_calls,325            self.nodes.items.len,326            self.ite_cache.count(),327        );328    }329330    pub fn stopIteLimit(self: *Manager) void {331        self.limits.stopIteLimit();332    }333334    pub fn ite(self: *Manager, f: Bdd, g: Bdd, h: Bdd) Allocator.Error!Bdd {335        self.num_recursive_calls += 1;336337        if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {338            return Bdd.FALSE;339        }340341        if (self.num_recursive_calls % 1000 == 0) {342            if (self.checkLimits()) return Bdd.FALSE;343        }344345        const helper = LessThanHelper{ .manager = self };346        const normalized = NormalizedIte.normalize(f, g, h, helper);347348        if (normalized.is_const) {349            return normalized.const_result;350        }351352        if (self.ite_cache.get(normalized.key)) |cached| {353            self.ite_cache_hits += 1;354            return if (normalized.complement_result) cached.neg() else cached;355        }356        self.ite_cache_misses += 1;357358        if (self.limits.reserveIteCacheGrowth(self.ite_cache.count())) return Bdd.FALSE;359        defer self.limits.releaseIteCacheGrowth();360361        const top_var = self.firstEssential(f, g, h);362363        const fx_t = self.conditionEssential(f, top_var, true);364        const gx_t = self.conditionEssential(g, top_var, true);365        const hx_t = self.conditionEssential(h, top_var, true);366        const fx_f = self.conditionEssential(f, top_var, false);367        const gx_f = self.conditionEssential(g, top_var, false);368        const hx_f = self.conditionEssential(h, top_var, false);369370        const t = try self.ite(fx_t, gx_t, hx_t);371        if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {372            return Bdd.FALSE;373        }374        const e = try self.ite(fx_f, gx_f, hx_f);375376        if (self.limits.ite_limit_exceeded or self.limits.time_limit_exceeded) {377            return Bdd.FALSE;378        }379380        if (t.toRaw() == e.toRaw()) {381            const cache_result = if (normalized.complement_result) t.neg() else t;382            if (!try self.putIteCacheNoClobber(normalized.key, cache_result)) return Bdd.FALSE;383            return t;384        }385386        const result = try self.getOrInsert(Node.init(top_var, e, t));387        if (self.limits.ite_limit_exceeded) return Bdd.FALSE;388389        const cache_result = if (normalized.complement_result) result.neg() else result;390        if (!try self.putIteCacheNoClobber(normalized.key, cache_result)) return Bdd.FALSE;391392        return result;393    }394395    fn putIteCacheNoClobber(self: *Manager, key: IteKey, value: Bdd) Allocator.Error!bool {396        if (!try self.ensureReservedIteCacheCapacity()) return false;397        self.ite_cache.putAssumeCapacityNoClobber(key, value);398        return true;399    }400401    fn ensureReservedIteCacheCapacity(self: *Manager) Allocator.Error!bool {402        const reservations = @max(self.limits.ite_cache_reservations, 1);403        std.debug.assert(reservations <= std.math.maxInt(u32));404        const projected = self.ite_cache.count() +| reservations;405        if (projected <= self.ite_cache_grow_at) return true;406407        const capacity = self.ite_cache.capacity();408        const reserve = @max(capacity, INITIAL_MANAGER_CAPACITY);409        const target = @max(projected, self.ite_cache.count() +| reserve);410        const target_size = std.math.cast(u32, target) orelse {411            if (self.limits.boundedAllocationFailed()) return false;412            return error.OutOfMemory;413        };414        self.ite_cache.ensureTotalCapacity(self.allocator, target_size) catch |err| {415            if (self.limits.boundedAllocationFailed()) return false;416            return err;417        };418        self.ite_cache_grows += 1;419        self.ite_cache_grow_at = tableLoadThreshold(self.ite_cache.capacity());420        return true;421    }422423    pub fn bddAnd(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {424        if (a.isFalse() or b.isFalse()) return Bdd.FALSE;425        if (a.isTrue()) return b;426        if (b.isTrue()) return a;427        if (a.toRaw() == b.toRaw()) return a;428        if (a.neg().toRaw() == b.toRaw()) return Bdd.FALSE;429430        var left = a;431        var right = b;432        if (right.toRaw() < left.toRaw()) {433            const tmp = left;434            left = right;435            right = tmp;436        }437        return self.ite(left, right, Bdd.FALSE);438    }439440    pub fn bddOr(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {441        if (a.isTrue() or b.isTrue()) return Bdd.TRUE;442        if (a.isFalse()) return b;443        if (b.isFalse()) return a;444        if (a.toRaw() == b.toRaw()) return a;445        if (a.neg().toRaw() == b.toRaw()) return Bdd.TRUE;446447        var left = a;448        var right = b;449        if (right.toRaw() < left.toRaw()) {450            const tmp = left;451            left = right;452            right = tmp;453        }454        return self.ite(left, Bdd.TRUE, right);455    }456457    pub fn bddNot(_: *Manager, a: Bdd) Bdd {458        return a.neg();459    }460461    pub fn bddXor(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {462        if (a.isFalse()) return b;463        if (b.isFalse()) return a;464        if (a.isTrue()) return b.neg();465        if (b.isTrue()) return a.neg();466        if (a.toRaw() == b.toRaw()) return Bdd.FALSE;467        if (a.neg().toRaw() == b.toRaw()) return Bdd.TRUE;468469        var left = a;470        var right = b;471        if (right.toRaw() < left.toRaw()) {472            const tmp = left;473            left = right;474            right = tmp;475        }476        return self.ite(left, right.neg(), right);477    }478479    pub fn bddIff(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {480        if (a.isFalse()) return b.neg();481        if (b.isFalse()) return a.neg();482        if (a.isTrue()) return b;483        if (b.isTrue()) return a;484        if (a.toRaw() == b.toRaw()) return Bdd.TRUE;485        if (a.neg().toRaw() == b.toRaw()) return Bdd.FALSE;486487        var left = a;488        var right = b;489        if (right.toRaw() < left.toRaw()) {490            const tmp = left;491            left = right;492            right = tmp;493        }494        return self.ite(left, right, right.neg());495    }496497    pub fn bddImplies(self: *Manager, a: Bdd, b: Bdd) Allocator.Error!Bdd {498        if (a.isFalse() or b.isTrue()) return Bdd.TRUE;499        if (a.isTrue()) return b;500        if (b.isFalse()) return a.neg();501        if (a.toRaw() == b.toRaw()) return Bdd.TRUE;502        if (a.neg().toRaw() == b.toRaw()) return b;503        return self.bddOr(a.neg(), b);504    }505506    pub fn eq(self: *const Manager, a: Bdd, b: Bdd) bool {507        _ = self;508        return a.toRaw() == b.toRaw();509    }510511    pub fn exists(self: *Manager, f: Bdd, variable: VarLabel) Allocator.Error!Bdd {512        const f_true = try self.condition(f, variable, true);513        const f_false = try self.condition(f, variable, false);514        return self.bddOr(f_true, f_false);515    }516517    pub fn condition(self: *Manager, f: Bdd, variable: VarLabel, value: bool) Allocator.Error!Bdd {518        return self.conditionHelper(f, variable, value);519    }520521    fn conditionHelper(self: *Manager, f: Bdd, variable: VarLabel, value: bool) Allocator.Error!Bdd {522        if (f.isConst()) return f;523524        const node = self.getNode(f);525526        if (self.lessThan(variable, node.var_label)) {527            return f;528        }529530        if (node.var_label == variable) {531            const result = if (value) node.high else node.low;532            return if (f.complement) result.neg() else result;533        }534535        const key = ConditionKey.init(f, variable, value);536        if (self.condition_cache.get(key)) |cached| {537            return cached;538        }539540        const low_result = try self.conditionHelper(541            if (f.complement) node.low.neg() else node.low,542            variable,543            value,544        );545        const high_result = try self.conditionHelper(546            if (f.complement) node.high.neg() else node.high,547            variable,548            value,549        );550551        if (low_result.toRaw() == high_result.toRaw()) {552            if (!try self.putConditionCache(key, low_result)) return Bdd.FALSE;553            return low_result;554        }555556        const result = try self.getOrInsert(Node.init(node.var_label, low_result, high_result));557        if (self.limits.ite_limit_exceeded) return Bdd.FALSE;558559        if (!try self.putConditionCache(key, result)) return Bdd.FALSE;560561        return result;562    }563564    fn putConditionCache(self: *Manager, key: ConditionKey, value: Bdd) Allocator.Error!bool {565        self.condition_cache.put(self.allocator, key, value) catch |err| {566            if (self.limits.boundedAllocationFailed()) return false;567            return err;568        };569        return true;570    }571572    pub fn compose(self: *Manager, f: Bdd, variable: VarLabel, g: Bdd) Allocator.Error!Bdd {573        if (f.isConst()) return f;574575        const node = self.getNode(f);576577        if (self.lessThan(variable, node.var_label)) {578            return f;579        }580581        const f_low = if (f.complement) node.low.neg() else node.low;582        const f_high = if (f.complement) node.high.neg() else node.high;583584        if (node.var_label == variable) {585            return self.ite(g, f_high, f_low);586        }587588        const low_result = try self.compose(f_low, variable, g);589        const high_result = try self.compose(f_high, variable, g);590591        if (low_result.toRaw() == high_result.toRaw()) {592            return low_result;593        }594595        return self.getOrInsert(Node.init(node.var_label, low_result, high_result));596    }597598    pub fn sequentialCompose(599        self: *Manager,600        f: Bdd,601        variables: []const VarLabel,602        replacements: []const Bdd,603    ) Allocator.Error!Bdd {604        var result = f;605        for (variables, replacements) |variable, replacement| {606            result = try self.compose(result, variable, replacement);607        }608        return result;609    }610611    pub fn isVar(self: *const Manager, bdd: Bdd) bool {612        if (bdd.isConst()) return false;613        const node = self.getNode(bdd);614        const low_raw = if (bdd.complement) node.low.neg() else node.low;615        const high_raw = if (bdd.complement) node.high.neg() else node.high;616        return low_raw.isFalse() and high_raw.isTrue();617    }618619    pub fn hasVariable(self: *const Manager, bdd: Bdd, variable: VarLabel) bool {620        if (bdd.isConst()) return false;621622        const node = self.getNode(bdd);623        if (node.var_label == variable) return true;624625        return self.hasVariable(node.low.toReg(), variable) or626            self.hasVariable(node.high.toReg(), variable);627    }628629    pub fn size(self: *const Manager, bdd: Bdd) usize {630        if (bdd.isConst()) return 0;631632        var visited = std.AutoHashMap(u31, void).init(self.allocator);633        defer visited.deinit();634635        return self.sizeHelper(bdd, &visited);636    }637638    fn sizeHelper(self: *const Manager, bdd: Bdd, visited: *std.AutoHashMap(u31, void)) usize {639        if (bdd.isConst()) return 0;640        if (visited.contains(bdd.index)) return 0;641642        visited.put(bdd.index, {}) catch return 0;643644        const node = self.getNode(bdd);645        return 1 + self.sizeHelper(node.low.toReg(), visited) +646            self.sizeHelper(node.high.toReg(), visited);647    }648649    pub fn numRecursiveCalls(self: *const Manager) u64 {650        return self.num_recursive_calls;651    }652653    pub fn resetStats(self: *Manager) void {654        self.num_recursive_calls = 0;655    }656657    pub fn clearCache(self: *Manager) void {658        self.ite_cache.clearRetainingCapacity();659        self.ite_cache_grow_at = tableLoadThreshold(self.ite_cache.capacity());660        self.condition_cache.clearRetainingCapacity();661    }662663    pub fn getVarPosition(self: *const Manager, var_label: VarLabel) u32 {664        if (var_label >= self.var_order.items.len) return @intCast(self.var_order.items.len);665        return self.var_order.items[var_label];666    }667668    pub fn totalNodeCount(self: *const Manager) usize {669        return if (self.nodes.items.len > 0) self.nodes.items.len - 1 else 0;670    }671672    pub fn getVarAtPosition(self: *const Manager, position: u32) ?VarLabel {673        for (self.var_order.items, 0..) |pos, label| {674            if (pos == position) return @intCast(label);675        }676        return null;677    }678679    pub fn nodesAtLevel(self: *const Manager, var_label: VarLabel) usize {680        var count: usize = 0;681        for (self.nodes.items[1..]) |node| {682            if (node.var_label == var_label) count += 1;683        }684        return count;685    }686687    pub fn swapAdjacentVars(self: *Manager, upper_pos: u32, allocator: Allocator) !i64 {688        const lower_pos = upper_pos + 1;689690        const var_upper = self.getVarAtPosition(upper_pos) orelse return 0;691        const var_lower = self.getVarAtPosition(lower_pos) orelse return 0;692693        const size_before = self.totalNodeCount();694695        var nodes_to_process: std.ArrayList(u31) = .empty;696        defer nodes_to_process.deinit(allocator);697698        for (self.nodes.items[1..], 1..) |node, idx| {699            if (node.var_label == var_upper) {700                try nodes_to_process.append(allocator, @intCast(idx));701            }702        }703704        for (nodes_to_process.items) |idx| {705            const node = self.nodes.items[idx];706            const high_child = node.high;707            const low_child = node.low;708709            var f11: Bdd = undefined;710            var f10: Bdd = undefined;711            var f01: Bdd = undefined;712            var f00: Bdd = undefined;713714            if (!high_child.isConst() and self.getNode(high_child).var_label == var_lower) {715                const high_node = self.getNode(high_child);716                f11 = if (high_child.complement) high_node.high.neg() else high_node.high;717                f10 = if (high_child.complement) high_node.low.neg() else high_node.low;718            } else {719                f11 = high_child;720                f10 = high_child;721            }722723            if (!low_child.isConst() and self.getNode(low_child).var_label == var_lower) {724                const low_node = self.getNode(low_child);725                f01 = if (low_child.complement) low_node.high.neg() else low_node.high;726                f00 = if (low_child.complement) low_node.low.neg() else low_node.low;727            } else {728                f01 = low_child;729                f00 = low_child;730            }731732            const new_high = try self.getOrInsert(Node.init(var_upper, f01, f11));733            const new_low = try self.getOrInsert(Node.init(var_upper, f00, f10));734735            _ = try self.getOrInsert(Node.init(var_lower, new_low, new_high));736        }737738        self.var_order.items[var_upper] = lower_pos;739        self.var_order.items[var_lower] = upper_pos;740741        self.clearCache();742743        const size_after = self.totalNodeCount();744        return @as(i64, @intCast(size_after)) - @as(i64, @intCast(size_before));745    }746747    pub fn localSift(self: *Manager, var_label: VarLabel, config: SiftConfig, allocator: Allocator) !SiftResult {748        const original_pos = self.getVarPosition(var_label);749        const num_vars = self.numVars();750751        if (num_vars <= 1) {752            return SiftResult{753                .original_pos = original_pos,754                .final_pos = original_pos,755                .size_delta = 0,756                .aborted = false,757            };758        }759760        const original_size = self.totalNodeCount();761        var best_pos = original_pos;762        var best_size = original_size;763        var current_pos = original_pos;764        var aborted = false;765766        var moves_down: u32 = 0;767        while (moves_down < config.max_distance and current_pos + 1 < num_vars) {768            const delta = try self.swapAdjacentVars(current_pos, allocator);769            current_pos += 1;770            moves_down += 1;771772            const current_size = self.totalNodeCount();773            if (current_size < best_size) {774                best_size = current_size;775                best_pos = current_pos;776            }777778            if (original_size > 0) {779                const blowup = @as(f64, @floatFromInt(current_size)) / @as(f64, @floatFromInt(original_size));780                if (blowup > config.max_blowup) {781                    aborted = true;782                    break;783                }784            }785            _ = delta;786        }787788        while (current_pos > original_pos) {789            _ = try self.swapAdjacentVars(current_pos - 1, allocator);790            current_pos -= 1;791        }792793        if (!aborted) {794            var moves_up: u32 = 0;795            while (moves_up < config.max_distance and current_pos > 0) {796                _ = try self.swapAdjacentVars(current_pos - 1, allocator);797                current_pos -= 1;798                moves_up += 1;799800                const current_size = self.totalNodeCount();801                if (current_size < best_size) {802                    best_size = current_size;803                    best_pos = current_pos;804                }805806                if (original_size > 0) {807                    const blowup = @as(f64, @floatFromInt(current_size)) / @as(f64, @floatFromInt(original_size));808                    if (blowup > config.max_blowup) {809                        aborted = true;810                        break;811                    }812                }813            }814        }815816        while (current_pos < best_pos) {817            _ = try self.swapAdjacentVars(current_pos, allocator);818            current_pos += 1;819        }820        while (current_pos > best_pos) {821            _ = try self.swapAdjacentVars(current_pos - 1, allocator);822            current_pos -= 1;823        }824825        const final_size = self.totalNodeCount();826        return SiftResult{827            .original_pos = original_pos,828            .final_pos = best_pos,829            .size_delta = @as(i64, @intCast(final_size)) - @as(i64, @intCast(original_size)),830            .aborted = aborted,831        };832    }833834    pub fn globalSift(self: *Manager, config: SiftConfig, allocator: Allocator, max_passes: u32) !GlobalSiftResult {835        const num_vars = self.numVars();836        if (num_vars <= 1) {837            const node_count = self.totalNodeCount();838            return GlobalSiftResult{839                .total_size_delta = 0,840                .vars_sifted = 0,841                .vars_improved = 0,842                .original_size = node_count,843                .final_size = node_count,844            };845        }846847        const original_size = self.totalNodeCount();848        var total_delta: i64 = 0;849        var vars_sifted: u32 = 0;850        var vars_improved: u32 = 0;851852        var pass: u32 = 0;853        while (pass < max_passes) : (pass += 1) {854            var improved_this_pass = false;855856            var var_idx: VarLabel = 0;857            while (var_idx < num_vars) : (var_idx += 1) {858                const result = try self.localSift(var_idx, config, allocator);859                vars_sifted += 1;860861                if (result.size_delta < 0) {862                    vars_improved += 1;863                    improved_this_pass = true;864                }865                total_delta += result.size_delta;866            }867868            if (!improved_this_pass) break;869        }870871        const final_size = self.totalNodeCount();872        return GlobalSiftResult{873            .total_size_delta = total_delta,874            .vars_sifted = vars_sifted,875            .vars_improved = vars_improved,876            .original_size = original_size,877            .final_size = final_size,878        };879    }880881    pub fn toString(self: *const Manager, bdd: Bdd, allocator: Allocator) ![]u8 {882        var buffer = std.Io.Writer.Allocating.init(allocator);883        errdefer buffer.deinit();884885        try self.toStringHelper(bdd, &buffer.writer);886        return try buffer.toOwnedSlice();887    }888889    fn toStringHelper(self: *const Manager, bdd: Bdd, writer: anytype) !void {890        if (bdd.isTrue()) {891            try writer.writeAll("T");892        } else if (bdd.isFalse()) {893            try writer.writeAll("F");894        } else {895            const node = self.getNode(bdd);896            if (bdd.complement) {897                try writer.writeAll("!");898            }899            try writer.print("({d}, ", .{node.var_label});900            try self.toStringHelper(node.high, writer);901            try writer.writeAll(", ");902            try self.toStringHelper(node.low, writer);903            try writer.writeAll(")");904        }905    }906907    pub fn toJson(self: *const Manager, bdd: Bdd, allocator: Allocator) ![]u8 {908        return writeBddJson(allocator, bdd, self.nodes.items);909    }910911    pub fn printStats(self: *const Manager, allocator: Allocator) ![]u8 {912        var buffer = std.Io.Writer.Allocating.init(allocator);913        errdefer buffer.deinit();914        const writer = &buffer.writer;915916        try writer.print("BDD Manager Stats:\n", .{});917        try writer.print("  Variables: {d}\n", .{self.var_order.items.len});918        try writer.print("  Nodes: {d}\n", .{self.nodes.items.len});919        try writer.print("  Unique table entries: {d}\n", .{self.unique_table.count()});920        try writer.print("  ITE cache entries: {d}\n", .{self.ite_cache.count()});921        try writer.print("  Condition cache entries: {d}\n", .{self.condition_cache.count()});922        try writer.print("  Recursive calls: {d}\n", .{self.num_recursive_calls});923        try writer.print("  ITE cache hits: {d}\n", .{self.ite_cache_hits});924        try writer.print("  ITE cache misses: {d}\n", .{self.ite_cache_misses});925        try writer.print("  Unique table grows: {d}\n", .{self.unique_table_grows});926        try writer.print("  ITE cache grows: {d}\n", .{self.ite_cache_grows});927        const total = self.ite_cache_hits + self.ite_cache_misses;928        if (total > 0) {929            const hit_ratio = @as(f64, @floatFromInt(self.ite_cache_hits)) / @as(f64, @floatFromInt(total)) * 100.0;930            try writer.print("  ITE cache hit ratio: {d:.1}%\n", .{hit_ratio});931        }932933        return try buffer.toOwnedSlice();934    }935};