tiny.pluck.bdd.WmcContext

1pub const WmcContext = struct {2    cache: std.ArrayListUnmanaged(WmcCacheEntry),34    entry_count: usize,56    params_version: u64,78    structure_version: u64,910    cache_generation: u64,1112    stats: WmcCacheStats,1314    allocator: Allocator,1516    manager: ?*const Manager,1718    pub fn init(allocator: Allocator) WmcContext {19        return WmcContext{20            .cache = .empty,21            .entry_count = 0,22            .params_version = 0,23            .structure_version = 0,24            .cache_generation = 1,25            .stats = .{},26            .allocator = allocator,27            .manager = null,28        };29    }3031    pub fn deinit(self: *WmcContext) void {32        self.cache.deinit(self.allocator);33    }3435    pub fn wmcCached(36        self: *WmcContext,37        manager: *const Manager,38        bdd: Bdd,39        params: *const WmcParams,40    ) f64 {41        if (bdd.isTrue()) return 1.0;42        if (bdd.isFalse()) return 0.0;43        self.bindManager(manager);44        if (!self.ensureCapacity(manager.nodes.items.len)) {45            self.stats.misses += 1;46            return wmcWithAllocator(manager, bdd, params, self.allocator);47        }4849        if (self.getCached(bdd)) |cached| {50            self.stats.hits += 1;51            return cached;52        }5354        self.stats.misses += 1;55        return self.wmcHelperCached(manager, bdd, params);56    }5758    fn wmcHelperCached(59        self: *WmcContext,60        manager: *const Manager,61        bdd: Bdd,62        params: *const WmcParams,63    ) f64 {64        if (bdd.isTrue()) return 1.0;65        if (bdd.isFalse()) return 0.0;6667        if (self.getCached(bdd)) |cached| {68            return cached;69        }7071        const node = manager.getNode(bdd);72        const weight = params.getWeight(node.var_label);7374        const low_child = if (bdd.complement) node.low.neg() else node.low;75        const high_child = if (bdd.complement) node.high.neg() else node.high;7677        const low_result = self.wmcHelperCached(manager, low_child, params);78        const high_result = self.wmcHelperCached(manager, high_child, params);7980        const result = weight.low * low_result + weight.high * high_result;8182        self.putCached(bdd, result);8384        return result;85    }8687    fn ensureCapacity(self: *WmcContext, node_count: usize) bool {88        const required = node_count * 2;89        if (self.cache.items.len >= required) return true;9091        const old_len = self.cache.items.len;92        self.cache.ensureTotalCapacity(self.allocator, required) catch return false;93        self.cache.items.len = required;94        @memset(self.cache.items[old_len..], .{});95        return true;96    }9798    fn bindManager(self: *WmcContext, manager: *const Manager) void {99        if (self.manager) |bound| {100            if (bound == manager) return;101            self.clearEntries();102        }103        self.manager = manager;104    }105106    fn clearEntries(self: *WmcContext) void {107        @memset(self.cache.items, .{});108        self.entry_count = 0;109    }110111    fn getCached(self: *const WmcContext, bdd: Bdd) ?f64 {112        const index = cacheIndex(bdd);113        if (index >= self.cache.items.len) return null;114        const entry = self.cache.items[index];115        if (entry.generation != self.cache_generation) return null;116        return entry.value;117    }118119    fn putCached(self: *WmcContext, bdd: Bdd, value: f64) void {120        const index = cacheIndex(bdd);121        if (index >= self.cache.items.len) return;122        const was_occupied = self.cache.items[index].generation != 0;123        self.cache.items[index] = .{124            .value = value,125            .generation = self.cache_generation,126        };127        if (!was_occupied) {128            self.entry_count += 1;129        }130    }131132    pub fn invalidateAll(self: *WmcContext) void {133        self.structure_version += 1;134        self.advanceGeneration();135        self.stats.invalidations += 1;136    }137138    pub fn invalidateWeights(self: *WmcContext) void {139        self.params_version += 1;140        self.advanceGeneration();141        self.stats.invalidations += 1;142    }143144    fn advanceGeneration(self: *WmcContext) void {145        self.cache_generation +%= 1;146        if (self.cache_generation == 0) {147            self.clearEntries();148            self.cache_generation = 1;149        }150    }151152    pub fn invalidateForVars(153        self: *WmcContext,154        manager: *const Manager,155        vars: []const VarLabel,156    ) void {157        self.stats.invalidations += 1;158159        var removed: usize = 0;160        for (self.cache.items, 0..) |*entry, index| {161            if (entry.generation == 0) continue;162            const bdd = bddFromCacheIndex(index);163            for (vars) |var_label| {164                if (manager.hasVariable(bdd, var_label)) {165                    entry.* = .{};166                    removed += 1;167                    self.entry_count -= 1;168                    break;169                }170            }171        }172173        self.stats.evictions += removed;174    }175176    pub fn trimToSize(self: *WmcContext, max_entries: usize) usize {177        const current = self.entry_count;178        if (current <= max_entries) return 0;179180        const to_evict = current - max_entries;181        var evicted: usize = 0;182183        for (self.cache.items) |*entry| {184            if (evicted >= to_evict) break;185            if (entry.generation != 0) {186                entry.* = .{};187                evicted += 1;188            }189        }190191        self.entry_count -= evicted;192        self.stats.evictions += evicted;193        return evicted;194    }195196    pub fn clear(self: *WmcContext) void {197        self.clearEntries();198        self.stats = .{};199        self.params_version = 0;200        self.structure_version = 0;201        self.cache_generation = 1;202        self.manager = null;203    }204205    pub fn cacheSize(self: *const WmcContext) usize {206        return self.entry_count;207    }208209    pub fn getStats(self: *const WmcContext) WmcCacheStats {210        return self.stats;211    }212213    fn cacheIndex(bdd: Bdd) usize {214        return @as(usize, bdd.index) * 2 + @intFromBool(bdd.complement);215    }216217    fn bddFromCacheIndex(index: usize) Bdd {218        return Bdd{219            .index = @intCast(index / 2),220            .complement = index % 2 == 1,221        };222    }223};