lib/smt/src/properties/sat.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const hypothesis = @import("hypothesis");
3 const smt = @import("smt");
4 const model = @import("model.zig");
5
6 const Allocator = std.mem.Allocator;
7 const Literal = smt.Literal;
8 const ProofArtifact = smt.ProofArtifact;
9 const Status = smt.Status;
10
11 pub const BruteForceProperty = struct {
12 pub fn property(data: *hypothesis.ConjectureData, allocator: Allocator) !void {
13 var arena_state = std.heap.ArenaAllocator.init(allocator);
14 defer arena_state.deinit();
15 const arena = arena_state.allocator();
16
17 const formula = try model.drawFormula(data, arena);
18 var solver = try model.loadedSolver(allocator, formula);
19 defer solver.deinit();
20
21 const status = try solver.solve();
22 const expected: Status = if (model.satisfiable(formula, &.{})) .sat else .unsat;
23 try std.testing.expectEqual(expected, status);
24 try model.expectSolveEvidence(allocator, &solver, formula, &.{}, status);
25
26 const repeated = try solver.solve();
27 try std.testing.expectEqual(expected, repeated);
28 try model.expectSolveEvidence(allocator, &solver, formula, &.{}, repeated);
29 }
30 };
31
32 pub const AssumptionProperty = struct {
33 pub fn property(data: *hypothesis.ConjectureData, allocator: Allocator) !void {
34 var arena_state = std.heap.ArenaAllocator.init(allocator);
35 defer arena_state.deinit();
36 const arena = arena_state.allocator();
37
38 const formula = try model.drawFormula(data, arena);
39 const assumptions = try model.drawAssumptions(data, arena, formula.variable_count, 1);
40
41 var solver = try model.loadedSolver(allocator, formula);
42 defer solver.deinit();
43 const base_status = try solver.solve();
44 const base_expected: Status = if (model.satisfiable(formula, &.{})) .sat else .unsat;
45 try std.testing.expectEqual(base_expected, base_status);
46 try model.expectSolveEvidence(allocator, &solver, formula, &.{}, base_status);
47
48 const assumed_status = try solver.solveWithAssumptions(assumptions);
49 const assumed_expected: Status =
50 if (model.satisfiable(formula, assumptions)) .sat else .unsat;
51 try std.testing.expectEqual(assumed_expected, assumed_status);
52 try model.expectSolveEvidence(
53 allocator,
54 &solver,
55 formula,
56 assumptions,
57 assumed_status,
58 );
59
60 var unit_solver = try model.loadedSolver(allocator, formula);
61 defer unit_solver.deinit();
62 for (assumptions) |literal| {
63 try unit_solver.addClause(&.{literal});
64 }
65 const unit_status = try unit_solver.solve();
66 try std.testing.expectEqual(unit_status, assumed_status);
67
68 const repeated = try solver.solve();
69 try std.testing.expectEqual(base_expected, repeated);
70 try model.expectSolveEvidence(allocator, &solver, formula, &.{}, repeated);
71 }
72 };
73
74 pub const ClauseShuffleProperty = struct {
75 pub fn property(data: *hypothesis.ConjectureData, allocator: Allocator) !void {
76 var arena_state = std.heap.ArenaAllocator.init(allocator);
77 defer arena_state.deinit();
78 const arena = arena_state.allocator();
79
80 const formula = try model.drawFormula(data, arena);
81 var solver = try model.loadedSolver(allocator, formula);
82 defer solver.deinit();
83 const status = try solver.solve();
84 try model.expectSolveEvidence(allocator, &solver, formula, &.{}, status);
85
86 const permuted = try model.permutedFormula(data, arena, formula);
87 var shuffled_solver = try model.loadedSolver(allocator, permuted);
88 defer shuffled_solver.deinit();
89 const permuted_status = try shuffled_solver.solve();
90 try std.testing.expectEqual(status, permuted_status);
91 try model.expectSolveEvidence(
92 allocator,
93 &shuffled_solver,
94 permuted,
95 &.{},
96 permuted_status,
97 );
98
99 const redundant = try model.redundantFormula(data, arena, formula);
100 var strengthened = try model.loadedSolver(allocator, redundant);
101 defer strengthened.deinit();
102 const redundant_status = try strengthened.solve();
103 try std.testing.expectEqual(status, redundant_status);
104 try model.expectSolveEvidence(
105 allocator,
106 &strengthened,
107 redundant,
108 &.{},
109 redundant_status,
110 );
111 }
112 };
113
114 pub const BoundedStoreProperty = struct {
115 pub fn property(data: *hypothesis.ConjectureData, allocator: Allocator) !void {
116 var arena_state = std.heap.ArenaAllocator.init(allocator);
117 defer arena_state.deinit();
118 const arena = arena_state.allocator();
119
120 const formula = try model.drawFormula(data, arena);
121 var bounded = try model.loadedSolver(allocator, formula);
122 defer bounded.deinit();
123 model.configureGeneratedSolver(&bounded, 2);
124 var unbounded = try model.loadedSolver(allocator, formula);
125 defer unbounded.deinit();
126 model.configureGeneratedSolver(&unbounded, null);
127
128 _ = try model.solvePairWithAssumptions(
129 allocator,
130 &bounded,
131 &unbounded,
132 formula,
133 &.{},
134 );
135 const assumptions = try model.drawAssumptions(
136 data,
137 arena,
138 formula.variable_count,
139 1,
140 );
141 _ = try model.solvePairWithAssumptions(
142 allocator,
143 &bounded,
144 &unbounded,
145 formula,
146 assumptions,
147 );
148 _ = try model.solvePairWithAssumptions(
149 allocator,
150 &bounded,
151 &unbounded,
152 formula,
153 &.{},
154 );
155 }
156 };
157
158 pub const BoundedStoreExerciseProperty = struct {
159 pub fn property(data: *hypothesis.ConjectureData, allocator: Allocator) !void {
160 var arena_state = std.heap.ArenaAllocator.init(allocator);
161 defer arena_state.deinit();
162 const arena = arena_state.allocator();
163
164 const formula = try model.redundantFormula(
165 data,
166 arena,
167 try model.retainedPremiseFixture(arena),
168 );
169 var bounded = try model.loadedSolver(allocator, formula);
170 defer bounded.deinit();
171 model.configureGeneratedSolver(&bounded, 2);
172
173 try std.testing.expect(model.satisfiable(formula, &.{}));
174 const first_status = try bounded.solve();
175 try std.testing.expectEqual(Status.sat, first_status);
176 try model.expectSolveEvidence(allocator, &bounded, formula, &.{}, first_status);
177 if (bounded.lastSolveStats().evicted_clauses == 0) {
178 return error.TestExpectedLearnedEviction;
179 }
180 if (bounded.retainedLearnedClauses() == 0) {
181 return error.TestExpectedRetainedPremise;
182 }
183
184 var assumptions: [8]Literal = undefined;
185 for (&assumptions, 0..) |*literal, variable| {
186 literal.* = Literal.negative(@intCast(variable));
187 }
188 try std.testing.expect(!model.satisfiable(formula, &assumptions));
189 const assumed_status = try bounded.solveWithAssumptions(&assumptions);
190 try std.testing.expectEqual(Status.unsat, assumed_status);
191 try model.expectSolveEvidence(
192 allocator,
193 &bounded,
194 formula,
195 &assumptions,
196 assumed_status,
197 );
198 var artifact = (try bounded.lastProofArtifact(allocator)) orelse
199 return error.TestExpectedProofArtifact;
200 defer artifact.deinit();
201 if (artifact.clauses.items.len <= formula.clauses.len) {
202 return error.TestExpectedRetainedPremise;
203 }
204 }
205 };
206
207 pub const ArtifactSoundnessProperty = struct {
208 pub fn property(data: *hypothesis.ConjectureData, allocator: Allocator) !void {
209 var arena_state = std.heap.ArenaAllocator.init(allocator);
210 defer arena_state.deinit();
211 const arena = arena_state.allocator();
212 const formula = try model.drawFormula(data, arena);
213 const assumptions = try model.drawAssumptions(data, arena, formula.variable_count, 0);
214
215 const pivot_variable: u32 = @intCast(
216 try model.drawUsize(data, 0, formula.variable_count - 1, 0),
217 );
218 const pivot = Literal.init(pivot_variable, try data.drawBoolean());
219 var accepted = ProofArtifact.init(allocator, formula.variable_count);
220 defer accepted.deinit();
221 for (formula.clauses) |clause| try accepted.appendClause(clause);
222 try accepted.appendClause(&.{pivot});
223 try accepted.appendAssumptions(&.{pivot.negated()});
224 try accepted.appendStep(&.{});
225 try std.testing.expect(try accepted.valid());
226 try model.expectArtifactSound(&accepted);
227
228 var candidate = ProofArtifact.init(allocator, formula.variable_count);
229 defer candidate.deinit();
230 for (formula.clauses) |clause| try candidate.appendClause(clause);
231 try candidate.appendAssumptions(assumptions);
232 const prior_steps = try model.drawUsize(data, 0, 4, 1);
233 for (0..prior_steps) |_| {
234 const clause = try model.drawClause(data, arena, formula.variable_count);
235 try candidate.appendStep(clause);
236 }
237 try candidate.appendStep(&.{});
238 if (try candidate.valid()) {
239 try model.expectArtifactSound(&candidate);
240 }
241 }
242 };
243
244 test "property: solver status matches brute force on small formulas" {
245 try hypothesis.checkNamed(BruteForceProperty, "smt-sat-brute-force", model.settings(0x5a7));
246 }
247
248 test "property: bounded and unbounded solves agree with sound cores and proofs" {
249 try hypothesis.checkNamed(
250 BoundedStoreProperty,
251 "smt-sat-bounded-store",
252 model.settings(0x5aa),
253 );
254 }
255
256 test "property: bounded storage eviction and retained premises are exercised" {
257 try hypothesis.checkNamed(
258 BoundedStoreExerciseProperty,
259 "smt-sat-bounded-store-exercise",
260 model.settings(0x5ac),
261 );
262 }
263
264 test "property: assumptions behave as unit clauses with sound cores" {
265 try hypothesis.checkNamed(
266 AssumptionProperty,
267 "smt-sat-assumptions",
268 model.settings(0x5a8),
269 );
270 }
271
272 test "property: clause and literal order, duplicates, and tautologies preserve status" {
273 try hypothesis.checkNamed(
274 ClauseShuffleProperty,
275 "smt-sat-shuffle",
276 model.settings(0x5a9),
277 );
278 }
279
280 test "property: accepted proof artifacts are sound in their exact scope" {
281 try hypothesis.checkNamed(
282 ArtifactSoundnessProperty,
283 "smt-sat-artifact-soundness",
284 model.settings(0x5ab),
285 );
286 }