lib/smt/src/properties/model.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const hypothesis = @import("hypothesis");
3 const smt = @import("smt");
4
5 const Allocator = std.mem.Allocator;
6 const Literal = smt.Literal;
7 const ProofArtifact = smt.ProofArtifact;
8 const Solver = smt.Solver;
9 const Status = smt.Status;
10
11 const max_variables: usize = 8;
12 const max_clauses: usize = 20;
13 const max_clause_len: usize = 4;
14 const max_assignments: usize = @as(usize, 1) << max_variables;
15 const generated_conflict_budget: usize = 4_096;
16
17 pub const Formula = struct {
18 variable_count: u32,
19 clauses: [][]Literal,
20 };
21
22 pub fn settings(seed: u64) hypothesis.Settings {
23 return hypothesis.Settings.dev()
24 .withSeed(seed)
25 .withDatabase("zig-out/hypothesis-failures/smt");
26 }
27
28 pub fn drawUsize(
29 data: *hypothesis.ConjectureData,
30 min: usize,
31 max: usize,
32 shrink_towards: usize,
33 ) !usize {
34 return @intCast(try data.drawInteger(
35 @intCast(min),
36 @intCast(max),
37 @intCast(shrink_towards),
38 ));
39 }
40
41 pub fn drawFormula(data: *hypothesis.ConjectureData, arena: Allocator) !Formula {
42 const variable_count: u32 = @intCast(
43 try drawUsize(data, 1, max_variables, 3),
44 );
45 const clause_count = try drawUsize(data, 0, max_clauses, 4);
46 const clauses = try arena.alloc([]Literal, clause_count);
47 for (clauses) |*clause| {
48 clause.* = try drawClause(data, arena, variable_count);
49 }
50 return .{ .variable_count = variable_count, .clauses = clauses };
51 }
52
53 pub fn retainedPremiseFixture(arena: Allocator) !Formula {
54 const source = [_][3]i8{
55 .{ -4, 1, 8 },
56 .{ -7, 6, -3 },
57 .{ 8, 2, 1 },
58 .{ 8, -3, -5 },
59 .{ -2, 1, 4 },
60 .{ 5, -7, 2 },
61 .{ 5, -7, -2 },
62 .{ 3, -6, -2 },
63 .{ 1, -6, -8 },
64 .{ 7, -8, 6 },
65 .{ 6, 2, 7 },
66 .{ 1, -8, -4 },
67 .{ 7, -6, -5 },
68 .{ 3, 4, 8 },
69 .{ -7, -4, -6 },
70 .{ 3, 1, -7 },
71 .{ 7, -2, 8 },
72 .{ -6, -7, -1 },
73 .{ -7, 1, -3 },
74 .{ -6, 5, -3 },
75 };
76 const clauses = try arena.alloc([]Literal, source.len);
77 for (source, clauses) |signed_clause, *clause| {
78 clause.* = try arena.alloc(Literal, signed_clause.len);
79 for (signed_clause, clause.*) |signed, *literal| {
80 const magnitude = if (signed < 0) -signed else signed;
81 literal.* = Literal.init(@intCast(magnitude - 1), signed > 0);
82 }
83 }
84 return .{ .variable_count = max_variables, .clauses = clauses };
85 }
86
87 pub fn drawClause(
88 data: *hypothesis.ConjectureData,
89 arena: Allocator,
90 variable_count: u32,
91 ) ![]Literal {
92 const len = try drawUsize(data, 0, max_clause_len, 2);
93 const literals = try arena.alloc(Literal, len);
94 for (literals) |*literal| {
95 const variable: u32 = @intCast(try drawUsize(data, 0, variable_count - 1, 0));
96 literal.* = Literal.init(variable, try data.drawBoolean());
97 }
98 return literals;
99 }
100
101 pub fn drawAssumptions(
102 data: *hypothesis.ConjectureData,
103 arena: Allocator,
104 variable_count: u32,
105 minimum: usize,
106 ) ![]Literal {
107 const count = try drawUsize(data, minimum, 3, minimum);
108 const assumptions = try arena.alloc(Literal, count);
109 for (assumptions) |*literal| {
110 const variable: u32 = @intCast(try drawUsize(data, 0, variable_count - 1, 0));
111 literal.* = Literal.init(variable, try data.drawBoolean());
112 }
113 return assumptions;
114 }
115
116 pub fn permutedFormula(
117 data: *hypothesis.ConjectureData,
118 arena: Allocator,
119 formula: Formula,
120 ) !Formula {
121 const clauses = try arena.alloc([]Literal, formula.clauses.len);
122 for (formula.clauses, clauses) |source, *target| {
123 target.* = try arena.dupe(Literal, source);
124 for (0..4) |_| {
125 if (target.len < 2) break;
126 const left = try drawUsize(data, 0, target.len - 1, 0);
127 const right = try drawUsize(data, 0, target.len - 1, 0);
128 std.mem.swap(Literal, &target.*[left], &target.*[right]);
129 }
130 }
131 for (0..4) |_| {
132 if (clauses.len < 2) break;
133 const left = try drawUsize(data, 0, clauses.len - 1, 0);
134 const right = try drawUsize(data, 0, clauses.len - 1, 0);
135 std.mem.swap([]Literal, &clauses[left], &clauses[right]);
136 }
137 return .{ .variable_count = formula.variable_count, .clauses = clauses };
138 }
139
140 pub fn redundantFormula(
141 data: *hypothesis.ConjectureData,
142 arena: Allocator,
143 formula: Formula,
144 ) !Formula {
145 const duplicate_count: usize = if (formula.clauses.len == 0) 0 else 1;
146 const clauses = try arena.alloc([]Literal, formula.clauses.len + 1 + duplicate_count);
147 @memcpy(clauses[0..formula.clauses.len], formula.clauses);
148 const variable: u32 = @intCast(try drawUsize(data, 0, formula.variable_count - 1, 0));
149 const tautology = try arena.alloc(Literal, 2);
150 tautology[0] = Literal.positive(variable);
151 tautology[1] = Literal.negative(variable);
152 clauses[formula.clauses.len] = tautology;
153 if (duplicate_count == 1) {
154 const duplicate = try drawUsize(data, 0, formula.clauses.len - 1, 0);
155 clauses[formula.clauses.len + 1] = formula.clauses[duplicate];
156 }
157 return .{ .variable_count = formula.variable_count, .clauses = clauses };
158 }
159
160 pub fn loadedSolver(allocator: Allocator, formula: Formula) !Solver {
161 var solver = Solver.init(allocator);
162 errdefer solver.deinit();
163 for (0..formula.variable_count) |_| {
164 _ = try solver.addVariable();
165 }
166 for (formula.clauses) |clause| {
167 try solver.addClause(clause);
168 }
169 return solver;
170 }
171
172 fn literalSatisfied(literal: Literal, assignment: u32) bool {
173 const bit = (assignment >> @intCast(literal.variable())) & 1 == 1;
174 return bit == literal.isPositive();
175 }
176
177 fn clauseSatisfied(clause: []const Literal, assignment: u32) bool {
178 for (clause) |literal| {
179 if (literalSatisfied(literal, assignment)) return true;
180 }
181 return false;
182 }
183
184 fn formulaSatisfied(formula: Formula, assignment: u32) bool {
185 for (formula.clauses) |clause| {
186 if (!clauseSatisfied(clause, assignment)) return false;
187 }
188 return true;
189 }
190
191 fn assumptionsSatisfied(assumptions: []const Literal, assignment: u32) bool {
192 for (assumptions) |literal| {
193 if (!literalSatisfied(literal, assignment)) return false;
194 }
195 return true;
196 }
197
198 fn assignmentCount(variable_count: usize) usize {
199 std.debug.assert(variable_count <= max_variables);
200 return @as(usize, 1) << @intCast(variable_count);
201 }
202
203 pub fn satisfiable(formula: Formula, assumptions: []const Literal) bool {
204 const assignments = assignmentCount(formula.variable_count);
205 for (0..assignments) |assignment_index| {
206 const assignment: u32 = @intCast(assignment_index);
207 if (formulaSatisfied(formula, assignment) and
208 assumptionsSatisfied(assumptions, assignment)) return true;
209 }
210 return false;
211 }
212
213 fn expectModelSatisfies(
214 solver: *const Solver,
215 formula: Formula,
216 assumptions: []const Literal,
217 ) !void {
218 for (formula.clauses) |clause| {
219 for (clause) |literal| {
220 if (solver.literalValue(literal) == .true) break;
221 } else {
222 return error.TestExpectedSatisfiedClause;
223 }
224 }
225 for (assumptions) |literal| {
226 try std.testing.expectEqual(.true, solver.literalValue(literal));
227 }
228 }
229
230 fn expectLiteralSubset(part: []const Literal, whole: []const Literal) !void {
231 for (part) |candidate| {
232 for (whole) |literal| {
233 if (candidate.raw == literal.raw) break;
234 } else {
235 return error.TestExpectedLiteralSubset;
236 }
237 }
238 }
239
240 fn artifactScopeSatisfied(artifact: *const ProofArtifact, assignment: u32) bool {
241 for (artifact.clauses.items) |clause| {
242 if (!clauseSatisfied(clause.literals, assignment)) return false;
243 }
244 return assumptionsSatisfied(artifact.assumptions.items, assignment);
245 }
246
247 fn artifactScopeSatisfiable(artifact: *const ProofArtifact) bool {
248 const assignments = assignmentCount(artifact.variable_count);
249 for (0..assignments) |assignment_index| {
250 if (artifactScopeSatisfied(artifact, @intCast(assignment_index))) return true;
251 }
252 return false;
253 }
254
255 pub fn expectArtifactSound(artifact: *const ProofArtifact) !void {
256 try std.testing.expect(artifact.variable_count <= max_variables);
257 try std.testing.expect(artifact.steps.items.len > 0);
258 var prefix_models: [max_assignments]bool = @splat(false);
259 const assignments = assignmentCount(artifact.variable_count);
260 for (0..assignments) |assignment_index| {
261 prefix_models[assignment_index] =
262 artifactScopeSatisfied(artifact, @intCast(assignment_index));
263 }
264 for (artifact.steps.items) |step| {
265 for (0..assignments) |assignment_index| {
266 if (!prefix_models[assignment_index]) continue;
267 const assignment: u32 = @intCast(assignment_index);
268 try std.testing.expect(clauseSatisfied(step.literals, assignment));
269 prefix_models[assignment_index] = clauseSatisfied(step.literals, assignment);
270 }
271 }
272 try std.testing.expectEqual(
273 @as(usize, 0),
274 artifact.steps.items[artifact.steps.items.len - 1].literals.len,
275 );
276 try std.testing.expect(!artifactScopeSatisfiable(artifact));
277 }
278
279 fn clauseEntailedByFormula(formula: Formula, clause: []const Literal) bool {
280 const assignments = assignmentCount(formula.variable_count);
281 for (0..assignments) |assignment_index| {
282 const assignment: u32 = @intCast(assignment_index);
283 if (formulaSatisfied(formula, assignment) and
284 !clauseSatisfied(clause, assignment)) return false;
285 }
286 return true;
287 }
288
289 fn expectRetainedPremisesEntailed(
290 formula: Formula,
291 artifact: *const ProofArtifact,
292 ) !void {
293 for (formula.clauses) |clause| {
294 if (clause.len != 0) continue;
295 try std.testing.expect(!satisfiable(formula, &.{}));
296 for (artifact.clauses.items) |artifact_clause| {
297 if (artifact_clause.literals.len == 0) return;
298 }
299 return error.TestExpectedEmptyClause;
300 }
301 try std.testing.expect(artifact.clauses.items.len >= formula.clauses.len);
302 for (formula.clauses, artifact.clauses.items[0..formula.clauses.len]) |
303 expected,
304 actual,
305 | {
306 try std.testing.expectEqualSlices(Literal, expected, actual.literals);
307 }
308 for (artifact.clauses.items[formula.clauses.len..]) |clause| {
309 try std.testing.expect(clauseEntailedByFormula(formula, clause.literals));
310 }
311 }
312
313 fn expectUnsatEvidence(
314 allocator: Allocator,
315 solver: *const Solver,
316 formula: Formula,
317 supplied_assumptions: []const Literal,
318 ) !void {
319 const core = solver.lastUnsatCore();
320 try expectLiteralSubset(core, supplied_assumptions);
321 try std.testing.expect(!satisfiable(formula, core));
322 var artifact = (try solver.lastProofArtifact(allocator)) orelse
323 return error.TestExpectedProofArtifact;
324 defer artifact.deinit();
325 try expectLiteralSubset(artifact.assumptions.items, supplied_assumptions);
326 try std.testing.expect(try artifact.valid());
327 try expectArtifactSound(&artifact);
328 try expectRetainedPremisesEntailed(formula, &artifact);
329 }
330
331 pub fn expectSolveEvidence(
332 allocator: Allocator,
333 solver: *const Solver,
334 formula: Formula,
335 assumptions: []const Literal,
336 status: Status,
337 ) !void {
338 switch (status) {
339 .sat => try expectModelSatisfies(solver, formula, assumptions),
340 .unsat => try expectUnsatEvidence(allocator, solver, formula, assumptions),
341 .unknown => return error.TestUnexpectedUnknown,
342 }
343 }
344
345 pub fn configureGeneratedSolver(solver: *Solver, learned_limit: ?usize) void {
346 solver.max_learned_clauses = learned_limit;
347 solver.conflict_budget = generated_conflict_budget;
348 solver.setRestartPolicy(.{ .first_conflict_interval = 1, .growth = 1 });
349 }
350
351 pub fn solvePairWithAssumptions(
352 allocator: Allocator,
353 bounded: *Solver,
354 unbounded: *Solver,
355 formula: Formula,
356 assumptions: []const Literal,
357 ) !Status {
358 const bounded_status = try bounded.solveWithAssumptions(assumptions);
359 const unbounded_status = try unbounded.solveWithAssumptions(assumptions);
360 const expected: Status = if (satisfiable(formula, assumptions)) .sat else .unsat;
361 try std.testing.expectEqual(expected, bounded_status);
362 try std.testing.expectEqual(expected, unbounded_status);
363 try expectSolveEvidence(allocator, bounded, formula, assumptions, bounded_status);
364 try expectSolveEvidence(allocator, unbounded, formula, assumptions, unbounded_status);
365 try std.testing.expect(bounded.replaceableLearnedClauses() <= 3);
366 return bounded_status;
367 }
368
369 test "semantic proof oracle rejects a circular self-visible trace" {
370 var artifact = ProofArtifact.init(std.testing.allocator, 1);
371 defer artifact.deinit();
372 try artifact.appendStep(&.{Literal.positive(0)});
373 try artifact.appendStep(&.{Literal.negative(0)});
374 try artifact.appendStep(&.{});
375 try std.testing.expectError(error.TestUnexpectedResult, expectArtifactSound(&artifact));
376 }