lib/pluck/src/properties/bdd.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const hypothesis = @import("hypothesis");
3 const pluck = @import("pluck");
4
5 const Allocator = std.mem.Allocator;
6 const Bdd = pluck.bdd.Bdd;
7 const Manager = pluck.bdd.Manager;
8 const WmcParams = pluck.bdd.WmcParams;
9 const wmc = pluck.bdd.wmc;
10
11 const var_count = 4;
12 const assignment_count = 1 << var_count;
13 const stack_cap = 24;
14 const truth_mask = std.math.maxInt(u16);
15
16 const Stack = struct {
17 bdds: [stack_cap]Bdd = undefined,
18 truths: [stack_cap]u16 = undefined,
19 len: usize = 0,
20 next_replace: usize = 0,
21
22 fn push(self: *Stack, value: Bdd, truth: u16) void {
23 if (self.len < stack_cap) {
24 self.bdds[self.len] = value;
25 self.truths[self.len] = truth;
26 self.len += 1;
27 return;
28 }
29
30 const slot = self.next_replace % stack_cap;
31 self.next_replace += 1;
32 self.bdds[slot] = value;
33 self.truths[slot] = truth;
34 }
35 };
36
37 pub fn settings() hypothesis.Settings {
38 var out = hypothesis.Settings.quick()
39 .withSeed(0x706c_7563_6b62_6464)
40 .withDatabase("zig-out/hypothesis-failures/pluck");
41 out.max_examples = 64;
42 return out;
43 }
44
45 fn assignmentMask(assignment: usize) u16 {
46 return @as(u16, 1) << @as(u4, @intCast(assignment));
47 }
48
49 fn assignmentBit(assignment: usize, variable: usize) bool {
50 return ((assignment >> @intCast(variable)) & 1) != 0;
51 }
52
53 fn truthAt(table: u16, assignment: usize) bool {
54 return (table & assignmentMask(assignment)) != 0;
55 }
56
57 fn truthVar(variable: usize) u16 {
58 var out: u16 = 0;
59 for (0..assignment_count) |assignment| {
60 if (assignmentBit(assignment, variable)) {
61 out |= assignmentMask(assignment);
62 }
63 }
64 return out;
65 }
66
67 fn eval(manager: *const Manager, value: Bdd, assignment: usize) bool {
68 if (value.isTrue()) return true;
69 if (value.isFalse()) return false;
70
71 const node = manager.getNode(value);
72 const child = if (assignmentBit(assignment, node.var_label))
73 manager.high(value)
74 else
75 manager.low(value);
76 return eval(manager, child, assignment);
77 }
78
79 fn truthTable(manager: *const Manager, value: Bdd) u16 {
80 var out: u16 = 0;
81 for (0..assignment_count) |assignment| {
82 if (eval(manager, value, assignment)) {
83 out |= assignmentMask(assignment);
84 }
85 }
86 return out;
87 }
88
89 fn restrict(table: u16, variable: usize, value: bool) u16 {
90 const variable_mask = @as(usize, 1) << @intCast(variable);
91 var out: u16 = 0;
92 for (0..assignment_count) |assignment| {
93 const source = if (value)
94 assignment | variable_mask
95 else
96 assignment & ~variable_mask;
97 if (truthAt(table, source)) {
98 out |= assignmentMask(assignment);
99 }
100 }
101 return out;
102 }
103
104 fn exists(table: u16, variable: usize) u16 {
105 return restrict(table, variable, false) | restrict(table, variable, true);
106 }
107
108 fn modelCount(table: u16, low: *const [var_count]f64, high: *const [var_count]f64) f64 {
109 var total: f64 = 0.0;
110 for (0..assignment_count) |assignment| {
111 if (!truthAt(table, assignment)) continue;
112
113 var mass: f64 = 1.0;
114 for (0..var_count) |variable| {
115 mass *= if (assignmentBit(assignment, variable)) high[variable] else low[variable];
116 }
117 total += mass;
118 }
119 return total;
120 }
121
122 fn stackIndex(data: *hypothesis.ConjectureData, len: usize) !usize {
123 return @intCast(try data.drawInteger(0, len - 1, 0));
124 }
125
126 fn variableIndex(data: *hypothesis.ConjectureData) !usize {
127 return @intCast(try data.drawInteger(0, var_count - 1, 0));
128 }
129
130 fn pushConstant(data: *hypothesis.ConjectureData, stack: *Stack) !void {
131 const value = try data.drawBoolean();
132 stack.push(if (value) Bdd.TRUE else Bdd.FALSE, if (value) truth_mask else 0);
133 }
134
135 fn pushVariable(data: *hypothesis.ConjectureData, stack: *Stack, vars: *const [var_count]Bdd) !void {
136 const variable = try variableIndex(data);
137 stack.push(vars[variable], truthVar(variable));
138 }
139
140 pub const TruthTableProperty = struct {
141 pub fn property(data: *hypothesis.ConjectureData, allocator: Allocator) !void {
142 var manager = try Manager.init(allocator);
143 defer manager.deinit();
144
145 var vars: [var_count]Bdd = undefined;
146 for (&vars) |*slot| {
147 slot.* = try manager.newVar(true);
148 }
149
150 var stack: Stack = .{};
151 stack.push(Bdd.FALSE, 0);
152 stack.push(Bdd.TRUE, truth_mask);
153 for (vars, 0..) |variable_bdd, variable| {
154 stack.push(variable_bdd, truthVar(variable));
155 }
156
157 const operation_count: usize = @intCast(try data.drawInteger(8, 64, 24));
158 for (0..operation_count) |_| {
159 const op = try data.drawInteger(0, 9, 0);
160 switch (op) {
161 0 => try pushConstant(data, &stack),
162 1 => try pushVariable(data, &stack, &vars),
163 2 => {
164 const index = try stackIndex(data, stack.len);
165 stack.push(manager.bddNot(stack.bdds[index]), ~stack.truths[index]);
166 },
167 3 => {
168 const a = try stackIndex(data, stack.len);
169 const b = try stackIndex(data, stack.len);
170 stack.push(try manager.bddAnd(stack.bdds[a], stack.bdds[b]), stack.truths[a] & stack.truths[b]);
171 },
172 4 => {
173 const a = try stackIndex(data, stack.len);
174 const b = try stackIndex(data, stack.len);
175 stack.push(try manager.bddOr(stack.bdds[a], stack.bdds[b]), stack.truths[a] | stack.truths[b]);
176 },
177 5 => {
178 const a = try stackIndex(data, stack.len);
179 const b = try stackIndex(data, stack.len);
180 stack.push(try manager.bddXor(stack.bdds[a], stack.bdds[b]), stack.truths[a] ^ stack.truths[b]);
181 },
182 6 => {
183 const a = try stackIndex(data, stack.len);
184 const b = try stackIndex(data, stack.len);
185 stack.push(try manager.bddIff(stack.bdds[a], stack.bdds[b]), ~(stack.truths[a] ^ stack.truths[b]));
186 },
187 7 => {
188 const a = try stackIndex(data, stack.len);
189 const b = try stackIndex(data, stack.len);
190 stack.push(try manager.bddImplies(stack.bdds[a], stack.bdds[b]), ~stack.truths[a] | stack.truths[b]);
191 },
192 8 => {
193 const index = try stackIndex(data, stack.len);
194 const variable = try variableIndex(data);
195 if (try data.drawBoolean()) {
196 stack.push(
197 try manager.condition(stack.bdds[index], @intCast(variable), true),
198 restrict(stack.truths[index], variable, true),
199 );
200 } else {
201 stack.push(
202 try manager.exists(stack.bdds[index], @intCast(variable)),
203 exists(stack.truths[index], variable),
204 );
205 }
206 },
207 9 => {
208 const f = try stackIndex(data, stack.len);
209 const g = try stackIndex(data, stack.len);
210 const h = try stackIndex(data, stack.len);
211 stack.push(
212 try manager.ite(stack.bdds[f], stack.bdds[g], stack.bdds[h]),
213 (stack.truths[f] & stack.truths[g]) | (~stack.truths[f] & stack.truths[h]),
214 );
215 },
216 else => unreachable,
217 }
218 }
219
220 for (0..stack.len) |index| {
221 try std.testing.expectEqual(stack.truths[index], truthTable(&manager, stack.bdds[index]));
222 }
223
224 var params = WmcParams.init(allocator);
225 defer params.deinit();
226 var low: [var_count]f64 = undefined;
227 var high: [var_count]f64 = undefined;
228 for (0..var_count) |variable| {
229 high[variable] = @as(f64, @floatFromInt(try data.drawInteger(1, 9, 5))) / 10.0;
230 low[variable] = 1.0 - high[variable];
231 try params.setWeight(@intCast(variable), low[variable], high[variable]);
232 }
233
234 const index = try stackIndex(data, stack.len);
235 const expected = modelCount(stack.truths[index], &low, &high);
236 try std.testing.expectApproxEqAbs(expected, wmc(&manager, stack.bdds[index], ¶ms), 1e-9);
237 }
238 };
239
240 test "pbt: BDD operations preserve truth-table semantics" {
241 try hypothesis.checkNamed(TruthTableProperty, "pluck-bdd-truth-table", settings());
242 }