lib/smt/src/term.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! The formulas the package solves are trees of typed expressions over Booleans, integers,
2 //! bit-vectors and arrays, with named constants and uninterpreted functions, and each expression
3 //! has a sort.
4 //!
5 //! A caller builds a formula one operator at a time and needs each piece to be a small value it can
6 //! reuse as an operand of larger pieces. The encoder and the SMT-LIB writer walk every expression
7 //! and read its operator, its operands and its sort.
8 //!
9 //! Formulas share subexpressions, as `x` appears in both `x + 1` and `x < x + 1`, so the pieces
10 //! refer to one another and need one owner. Each operator accepts operands of particular sorts, and
11 //! a formula with a mismatched operand has no meaning.
12 //!
13 //! [SMT-LIB](https://smt-lib.org/) defines the sorts and operators of its theories: Booleans with
14 //! equality, integers, fixed-size bit-vectors, arrays and uninterpreted functions. The term kinds
15 //! here carry SMT-LIB's operator names, and the SMT-LIB writer and parser map each kind to its
16 //! standard operator.
17 //!
18 //! Every term lives in one table that owns every term and function declaration it holds, a
19 //! *context* (`Context`), and each term is its 32-bit index in that table (`Term`). Building a term
20 //! appends one entry and returns its index, so an index stays valid until the table is freed, and
21 //! building one expression twice gives two indexes.
22 //!
23 //! The builders copy the names and operand lists they receive, so a caller may free its own slices
24 //! after the call. The builders check no sorts, except that `function` refuses a second declaration
25 //! of one name with other sorts and `apply` checks its arguments against the declaration. `sortOf`
26 //! computes a term's sort on demand and reports a mismatch. A builder stores operand indexes as
27 //! given, so an index that names no earlier term leaves a term on which `sortOf` fails or recurses
28 //! without end.
29 //!
30 //! Arrays map a bit-vector index to a bit-vector element, and their sort records the two widths
31 //! (`ArraySort`). Integer terms can be built, sorted and written as SMT-LIB, and the bit-vector
32 //! encoder refuses them. The SMT-LIB parser returns, and the writer reads, a logic name with the
33 //! list of terms asserted over one table, a *script* (`Script`). Freeing the table frees every
34 //! term, name and operand list at once, and nothing frees a single term.
35 const std = @import("std");
36
37 /// The shape of an array sort: the width of its bit-vector index and the width of its bit-vector
38 /// element. Code that declares an array constant builds one to give the array's shape, as the
39 /// encoder's array tests do. The bit-vector encoder accepts an index of at most eight bits.
40 pub const ArraySort = struct {
41 /// The width of the index in bits. The index of every read or write of the array has this
42 /// width.
43 index_width: u32,
44 /// The width of each element in bits. A read of the array is a bit-vector of this width.
45 element_width: u32,
46 };
47
48 /// The sort of a term: Boolean, integer, a bit-vector of a given width, or an array from
49 /// bit-vectors to bit-vectors. Code declares every constant and function with a sort, and `sortOf`
50 /// returns one for every term.
51 pub const Sort = union(enum) {
52 /// The Boolean sort. SMT-LIB writes it `Bool`.
53 bool,
54 /// The sort of mathematical integers. SMT-LIB writes it `Int`. The bit-vector encoder refuses
55 /// terms of this sort with `UnsupportedTerm`.
56 int,
57 /// A bit-vector sort, with its width in bits as the payload. SMT-LIB writes it `(_ BitVec n)`.
58 /// Any width is accepted, 0 and widths above 128 included. A bit-vector constant wider than 128
59 /// bits makes the encoder panic. A named constant wider than 128 bits encodes, and
60 /// `Encoder.model` returns `ModelValueTooWide` for it.
61 bitvec: u32,
62 /// An array sort, with its index and element widths as the payload. SMT-LIB writes it
63 /// `(Array (_ BitVec i) (_ BitVec e))`.
64 array: ArraySort,
65
66 /// Writes the sort in SMT-LIB syntax: `Bool`, `Int`, `(_ BitVec n)` or
67 /// `(Array (_ BitVec i) (_ BitVec e))`. The SMT-LIB writer calls it to print the sort of every
68 /// declaration. The function returns only the writer's errors.
69 pub fn write(self: Sort, writer: *std.Io.Writer) std.Io.Writer.Error!void {
70 switch (self) {
71 .bool => try writer.writeAll("Bool"),
72 .int => try writer.writeAll("Int"),
73 .bitvec => |width| try writer.print("(_ BitVec {d})", .{width}),
74 .array => |array| try writer.print(
75 "(Array (_ BitVec {d}) (_ BitVec {d}))",
76 .{ array.index_width, array.element_width },
77 ),
78 }
79 }
80
81 /// Returns true when the two sorts have the same kind and the same widths. `sortOf` and
82 /// `function` call it to compare the sort an operator needs with the sort it got.
83 pub fn eql(self: Sort, other: Sort) bool {
84 return std.meta.eql(self, other);
85 }
86 };
87
88 /// A term, named by its index in the table of the `Context` that built it. Every builder returns
89 /// one and every operand is one, so callers pass terms around as plain integers. The index means
90 /// nothing in another `Context`. The index stays valid until its `Context` is freed.
91 pub const Term = u32;
92 /// A function declaration, named by its index in the declaration table of the `Context` that holds
93 /// it. `function` returns one, and `apply` takes one to build an application.
94 pub const Function = u32;
95
96 /// The payload of a named constant: its name and its sort. Code that walks terms reads it from a
97 /// `.symbol` term to learn a constant's name and sort.
98 pub const SymbolExpr = struct {
99 /// The constant's name, a copy the `Context` owns and frees. Two constants may share a name,
100 /// because every call to `symbol` builds a new term.
101 name: []const u8,
102 /// The constant's sort.
103 sort: Sort,
104 };
105
106 /// The payload of a function application: the declared function and its argument terms. Code that
107 /// walks terms reads it from an `.apply` term to learn which function is applied to which
108 /// arguments.
109 pub const ApplyExpr = struct {
110 /// The applied function's index in the declaration table.
111 function: Function,
112 /// The argument terms in declaration order, a copy the `Context` owns and frees.
113 args: []const Term,
114 };
115
116 /// The payload of a bit-vector constant: its value and its width. Code that walks terms reads it
117 /// from a `.bitvec` term to learn a constant's bits.
118 pub const BitVecExpr = struct {
119 /// The constant's bits as an unsigned number: bit i of the number is bit i of the vector,
120 /// counted from the least significant. Nothing checks the value against the width, and the
121 /// encoder reads only the low `width` bits.
122 value: u128,
123 /// The constant's width in bits. A width above 128 makes the encoder panic.
124 width: u32,
125 };
126
127 /// The payload of a two-operand term: the left operand term `lhs` and the right operand term `rhs`.
128 /// Code that walks terms reads it from every two-operand term, such as `.eq`, `.bvadd` or `.bvult`.
129 pub const BinaryOperands = struct {
130 lhs: Term,
131 rhs: Term,
132 };
133
134 /// The payload of an array read: the array term `array` and the index term `index`. Code that walks
135 /// terms reads it from an `.array_select` term.
136 pub const ArraySelectExpr = struct {
137 array: Term,
138 index: Term,
139 };
140
141 /// The payload of an array write: the array term `array`, the index term `index` and the element
142 /// term `value` stored there. Code that walks terms reads it from an `.array_store` term.
143 pub const ArrayStoreExpr = struct {
144 array: Term,
145 index: Term,
146 value: Term,
147 };
148
149 /// The payload of a bit range taken from the bit-vector term `operand`, between two bit positions.
150 /// Code that walks terms reads it from a `.bvextract` term.
151 pub const BitVecExtractExpr = struct {
152 operand: Term,
153 /// The position of the highest bit taken, counted from 0 at the least significant bit. The
154 /// position has to be below the operand's width, or `sortOf` and the encoder report
155 /// `InvalidBitVectorRange`.
156 high: u32,
157 /// The position of the lowest bit taken, counted from 0 at the least significant bit. The
158 /// position has to be at most `high`, or `sortOf` and the encoder report
159 /// `InvalidBitVectorRange`.
160 low: u32,
161 };
162
163 /// The payload of a widening of the bit-vector term `operand`. Code that walks terms reads it from
164 /// a `.bvzeroext` or `.bvsignext` term.
165 pub const BitVecExtendExpr = struct {
166 operand: Term,
167 /// The number of bits added above the operand's most significant bit.
168 extra: u32,
169 };
170
171 /// The payload of a rotation of the bit-vector term `operand` by a fixed number of bits. Code that
172 /// walks terms reads it from a `.bvrotl` or `.bvrotr` term.
173 pub const BitVecRotateExpr = struct {
174 operand: Term,
175 /// The number of positions to rotate. The encoder takes it modulo the operand's width, so 5 on
176 /// a 4-bit operand rotates by 1.
177 amount: u32,
178 };
179
180 /// One declared function: its name, the sorts of its arguments and the sort of its result. Code
181 /// that walks the declarations reads one per function, as the SMT-LIB writer does for each
182 /// `declare-fun`.
183 pub const FunctionDecl = struct {
184 /// The function's name, a copy the `Context` owns and frees. The name is unique among the
185 /// declarations of one `Context`.
186 name: []const u8,
187 /// The sorts of the arguments in order, a copy the `Context` owns and frees. The slice length
188 /// is the function's arity: 0 declares a constant function.
189 params: []const Sort,
190 /// The sort of every application's result.
191 result: Sort,
192 };
193
194 /// One term: a tag naming its operator and a payload holding its operands. Code that walks a
195 /// formula switches on it, as the encoder and the SMT-LIB writer do for every term. The `Context`
196 /// stores one per term, and a term's index is its position in that table. A tag named after an
197 /// SMT-LIB operator reads and writes as that operator, and each tag whose name differs gives its
198 /// SMT-LIB spelling. The bit-vector encoder refuses the integer tags (`int`, `add`, `mul`, `le`,
199 /// `lt`, `ge`, `gt`) and `distinct` with `UnsupportedTerm`.
200 pub const Expr = union(enum) {
201 /// A named constant, with its name and sort as the payload. The encoder gives it fresh
202 /// variables, one per bit.
203 symbol: SymbolExpr,
204 /// A function application, with the function and its arguments as the payload. Its sort is the
205 /// function's result sort.
206 apply: ApplyExpr,
207 /// A Boolean constant. SMT-LIB writes it `true` or `false`.
208 bool: bool,
209 /// An integer constant, a signed 128-bit value. The bit-vector encoder refuses it.
210 int: i128,
211 /// A bit-vector constant, with its value and width as the payload. SMT-LIB writes it
212 /// `(_ bvV W)`.
213 bitvec: BitVecExpr,
214 /// The negation of one Boolean operand.
215 not: Term,
216 /// The conjunction of any number of Boolean operands. With no operands it is true. SMT-LIB
217 /// writes it `and`.
218 and_: []const Term,
219 /// The disjunction of any number of Boolean operands. With no operands it is false. SMT-LIB
220 /// writes it `or`.
221 or_: []const Term,
222 /// `lhs` implies `rhs`, both Boolean. SMT-LIB writes it `=>`.
223 implies: BinaryOperands,
224 /// `lhs` equals `rhs`, a Boolean term over two operands of one sort. Two arrays are equal when
225 /// every cell is equal. SMT-LIB writes it `=`.
226 eq: BinaryOperands,
227 /// True when all operands differ from one another, over operands of one sort. The bit-vector
228 /// encoder refuses it.
229 distinct: []const Term,
230 /// The integer sum of any number of integer operands. SMT-LIB writes it `+`. The bit-vector
231 /// encoder refuses it.
232 add: []const Term,
233 /// The integer product of any number of integer operands. SMT-LIB writes it `*`. The bit-vector
234 /// encoder refuses it.
235 mul: []const Term,
236 /// `lhs` is at most `rhs`, as integers. SMT-LIB writes it `<=`. The bit-vector encoder refuses
237 /// it.
238 le: BinaryOperands,
239 /// `lhs` is less than `rhs`, as integers. SMT-LIB writes it `<`. The bit-vector encoder refuses
240 /// it.
241 lt: BinaryOperands,
242 /// `lhs` is at least `rhs`, as integers. SMT-LIB writes it `>=`. The bit-vector encoder refuses
243 /// it.
244 ge: BinaryOperands,
245 /// `lhs` is greater than `rhs`, as integers. SMT-LIB writes it `>`. The bit-vector encoder
246 /// refuses it.
247 gt: BinaryOperands,
248 /// `lhs` is at most `rhs`, as unsigned bit-vectors of one width.
249 bvule: BinaryOperands,
250 /// `lhs` is less than `rhs`, as unsigned bit-vectors of one width.
251 bvult: BinaryOperands,
252 /// `lhs` is at most `rhs`, as two's-complement bit-vectors of one width.
253 bvsle: BinaryOperands,
254 /// `lhs` is less than `rhs`, as two's-complement bit-vectors of one width.
255 bvslt: BinaryOperands,
256 /// True when the unsigned sum of `lhs` and `rhs` does not fit their width.
257 bvuaddo: BinaryOperands,
258 /// True when the two's-complement sum of `lhs` and `rhs` does not fit their width: both have
259 /// one sign and the sum has the other.
260 bvsaddo: BinaryOperands,
261 /// True when the two's-complement difference `lhs` minus `rhs` does not fit their width.
262 bvssubo: BinaryOperands,
263 /// True when the unsigned product of `lhs` and `rhs` does not fit their width.
264 bvumulo: BinaryOperands,
265 /// True when the two's-complement product of `lhs` and `rhs` does not fit their width.
266 bvsmulo: BinaryOperands,
267 /// The bitwise complement of one bit-vector operand, of the same width.
268 bvnot: Term,
269 /// The bitwise and of two bit-vectors of one width.
270 bvand: BinaryOperands,
271 /// The bitwise or of two bit-vectors of one width.
272 bvor: BinaryOperands,
273 /// The bitwise exclusive or of two bit-vectors of one width.
274 bvxor: BinaryOperands,
275 /// `lhs` shifted toward its most significant bit by the value of `rhs`, with zeros shifted in,
276 /// over two bit-vectors of one width. A shift amount at or above the width gives zero.
277 bvshl: BinaryOperands,
278 /// `lhs` shifted toward its least significant bit by the value of `rhs`, with zeros shifted in.
279 /// A shift amount at or above the width gives zero.
280 bvlshr: BinaryOperands,
281 /// `lhs` shifted toward its least significant bit by the value of `rhs`, with copies of its
282 /// sign bit shifted in. A shift amount at or above the width fills every bit with the sign bit.
283 bvashr: BinaryOperands,
284 /// The unsigned quotient of `lhs` by `rhs`, rounded down. Division by zero gives all ones.
285 bvudiv: BinaryOperands,
286 /// The unsigned remainder of `lhs` by `rhs`. The remainder by zero is `lhs`.
287 bvurem: BinaryOperands,
288 /// The two's-complement quotient of `lhs` by `rhs`, rounded toward zero. Division by zero gives
289 /// 1 for a negative `lhs` and all ones otherwise.
290 bvsdiv: BinaryOperands,
291 /// The two's-complement remainder of `lhs` by `rhs`, with the sign of `lhs`. The remainder by
292 /// zero is `lhs`.
293 bvsrem: BinaryOperands,
294 /// The two's-complement modulo of `lhs` by `rhs`, with the sign of `rhs`. The modulo by zero is
295 /// `lhs`.
296 bvsmod: BinaryOperands,
297 /// The element of an array at an index, a bit-vector of the element width. The index has the
298 /// array's index width. SMT-LIB writes it `select`.
299 array_select: ArraySelectExpr,
300 /// An array equal to its operand everywhere except at one index, which holds the new element.
301 /// The term's sort is the operand's array sort. SMT-LIB writes it `store`.
302 array_store: ArrayStoreExpr,
303 /// The bits of `lhs` above the bits of `rhs`, one bit-vector as wide as the two together.
304 /// SMT-LIB writes it `concat`.
305 bvconcat: BinaryOperands,
306 /// The bits from position `high` down to position `low` of one bit-vector, both included, so
307 /// the result has `high - low + 1` bits. SMT-LIB writes it `((_ extract high low) x)`.
308 bvextract: BitVecExtractExpr,
309 /// A bit-vector widened by `extra` zero bits above its most significant bit. SMT-LIB writes it
310 /// `((_ zero_extend extra) x)`.
311 bvzeroext: BitVecExtendExpr,
312 /// A bit-vector widened by `extra` copies of its sign bit. SMT-LIB writes it
313 /// `((_ sign_extend extra) x)`.
314 bvsignext: BitVecExtendExpr,
315 /// A bit-vector rotated toward its most significant bit by a fixed number of positions, with
316 /// the top bits wrapping to the bottom. SMT-LIB writes it `((_ rotate_left amount) x)`.
317 bvrotl: BitVecRotateExpr,
318 /// A bit-vector rotated toward its least significant bit by a fixed number of positions, with
319 /// the bottom bits wrapping to the top. SMT-LIB writes it `((_ rotate_right amount) x)`.
320 bvrotr: BitVecRotateExpr,
321 /// The sum of two bit-vectors of one width, modulo 2 to the power of the width.
322 bvadd: BinaryOperands,
323 /// The difference `lhs` minus `rhs` of two bit-vectors of one width, modulo 2 to the power of
324 /// the width.
325 bvsub: BinaryOperands,
326 /// The product of two bit-vectors of one width, modulo 2 to the power of the width.
327 bvmul: BinaryOperands,
328 };
329
330 /// One table that owns every term and function declaration it holds. Every formula starts here: a
331 /// caller makes one, builds its terms with the builders, and frees them all at once with `deinit`.
332 /// Each builder appends one term and returns its index. The builders check no sorts, except
333 /// `function` and `apply`, and `sortOf` checks a term's sort when a caller asks. Every builder can
334 /// fail with `error.OutOfMemory`, and a failed builder leaves the table as it was. A `Script`, a
335 /// parser and an encoder borrow the `Context` and have to be freed before it.
336 pub const Context = struct {
337 /// The allocator for every term, name, operand list and declaration. A `Script` over this table
338 /// and the SMT-LIB parser allocate with it too.
339 allocator: std.mem.Allocator,
340 /// Every term in the order it was built: entry i is the term whose index is i. The encoder and
341 /// the SMT-LIB writer read it to walk every named constant.
342 nodes: std.ArrayList(Expr) = .empty,
343 /// Every function declaration in the order it was declared: entry i is the function whose index
344 /// is i.
345 functions: std.ArrayList(FunctionDecl) = .empty,
346
347 /// Returns an empty table that allocates with `allocator`, so a caller makes one before
348 /// building any term. The call allocates nothing.
349 pub fn init(allocator: std.mem.Allocator) Context {
350 return .{ .allocator = allocator };
351 }
352
353 /// Frees every term's name and operand list, every declaration and both tables, so the owner
354 /// calls it once after every `Script`, parser and encoder built over the table is done with its
355 /// terms. Every `Term` and `Function` index from this table is invalid afterward.
356 pub fn deinit(self: *Context) void {
357 for (self.nodes.items) |node| {
358 switch (node) {
359 .symbol => |sym| self.allocator.free(sym.name),
360 .apply => |item| self.allocator.free(item.args),
361 .and_, .or_, .distinct, .add, .mul => |items| self.allocator.free(items),
362 else => {},
363 }
364 }
365 for (self.functions.items) |decl| {
366 self.allocator.free(decl.name);
367 self.allocator.free(decl.params);
368 }
369 self.functions.deinit(self.allocator);
370 self.nodes.deinit(self.allocator);
371 self.* = undefined;
372 }
373
374 /// Appends a named constant of the given sort and returns its term, so code declares each free
375 /// variable of a formula with it, as the SMT-LIB parser does for every `declare-const`. The
376 /// builder copies `name`, so the caller may free its own copy. The builder builds a new term on
377 /// every call, even for a name used before.
378 pub fn symbol(self: *Context, name: []const u8, sort: Sort) !Term {
379 const owned_name = try self.allocator.dupe(u8, name);
380 errdefer self.allocator.free(owned_name);
381 return try self.append(.{ .symbol = .{ .name = owned_name, .sort = sort } });
382 }
383
384 /// Declares a function by name, argument sorts and result sort, and returns its index, so code
385 /// declares each uninterpreted function with it, as the SMT-LIB parser does for every
386 /// `declare-fun`. A second call with the same name and the same sorts returns the first index.
387 /// A second call with the same name and other sorts returns `error.DuplicateFunction`. The
388 /// builder copies `name` and `params`.
389 pub fn function(
390 self: *Context,
391 name: []const u8,
392 params: []const Sort,
393 result: Sort,
394 ) !Function {
395 for (self.functions.items, 0..) |decl, index| {
396 if (!std.mem.eql(u8, decl.name, name)) continue;
397 if (!sortListsEqual(decl.params, params) or !decl.result.eql(result)) {
398 return error.DuplicateFunction;
399 }
400 return @intCast(index);
401 }
402 const owned_name = try self.allocator.dupe(u8, name);
403 errdefer self.allocator.free(owned_name);
404 const owned_params = try self.allocator.dupe(Sort, params);
405 errdefer self.allocator.free(owned_params);
406 const id: Function = @intCast(self.functions.items.len);
407 try self.functions.append(self.allocator, .{
408 .name = owned_name,
409 .params = owned_params,
410 .result = result,
411 });
412 return id;
413 }
414
415 /// Appends the application of the function `function_id` to `args` and returns its term, so
416 /// code applies a declared function to arguments with it. The call returns
417 /// `error.UnknownFunction` for an index past the declarations, `error.FunctionArityMismatch`
418 /// for the wrong number of arguments, and `error.FunctionArgumentSortMismatch` for an argument
419 /// of the wrong sort. The builder computes each argument's sort with `sortOf`, so the call also
420 /// returns the errors of `sortOf` for an argument that has no sort. The builder copies `args`.
421 pub fn apply(self: *Context, function_id: Function, args: []const Term) !Term {
422 if (function_id >= self.functions.items.len) return error.UnknownFunction;
423 const decl = self.functions.items[function_id];
424 if (decl.params.len != args.len) return error.FunctionArityMismatch;
425 for (args, decl.params) |arg, expected| {
426 if (!(try self.sortOf(arg)).eql(expected)) return error.FunctionArgumentSortMismatch;
427 }
428 const owned = try self.allocator.dupe(Term, args);
429 errdefer self.allocator.free(owned);
430 return try self.append(.{ .apply = .{ .function = function_id, .args = owned } });
431 }
432
433 /// Returns the sort of term `id`, checking every operand below it against the sorts its
434 /// operator accepts, so code checks a formula's sorts before encoding or writing, and the
435 /// encoder reads each function argument's sort with it. The call returns `error.TermOutOfRange`
436 /// for an index past the table, `error.SortMismatch` for an operand of the wrong sort,
437 /// `error.InvalidBitVectorRange` for a bad extract range, and the errors of `apply` for a bad
438 /// application. The function allocates nothing, and the call walks the whole term below `id` on
439 /// every call. The recursion has no depth bound, and a term that refers to itself makes the
440 /// call recurse without end.
441 pub fn sortOf(self: *const Context, id: Term) anyerror!Sort {
442 if (id >= self.nodes.items.len) return error.TermOutOfRange;
443 return switch (self.nodes.items[id]) {
444 .symbol => |sym| sym.sort,
445 .apply => |item| try self.sortOfApply(item),
446 .bool => .bool,
447 .int => .int,
448 .bitvec => |value| .{ .bitvec = value.width },
449 .not => |operand| try self.expectBoolResult(operand),
450 .and_, .or_ => |operands| try self.expectBoolList(operands),
451 .implies => |pair| try self.expectBoolPair(pair.lhs, pair.rhs),
452 .eq => |pair| try self.expectSameSortPair(pair.lhs, pair.rhs),
453 .distinct => |operands| try self.expectSameSortList(operands),
454 .add, .mul => |operands| try self.expectIntList(operands),
455 .le => |pair| try self.expectIntPair(pair.lhs, pair.rhs),
456 .lt => |pair| try self.expectIntPair(pair.lhs, pair.rhs),
457 .ge => |pair| try self.expectIntPair(pair.lhs, pair.rhs),
458 .gt => |pair| try self.expectIntPair(pair.lhs, pair.rhs),
459 .bvule => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
460 .bvult => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
461 .bvsle => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
462 .bvslt => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
463 .bvuaddo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
464 .bvsaddo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
465 .bvssubo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
466 .bvumulo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
467 .bvsmulo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),
468 .bvnot => |operand| try self.expectBitVecResult(operand),
469 .bvand => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
470 .bvor => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
471 .bvxor => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
472 .bvshl => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
473 .bvlshr => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
474 .bvashr => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
475 .bvudiv => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
476 .bvurem => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
477 .bvsdiv => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
478 .bvsrem => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
479 .bvsmod => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
480 .bvadd => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
481 .bvsub => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
482 .bvmul => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),
483 .array_select => |item| try self.sortOfArraySelect(item.array, item.index),
484 .array_store => |item| try self.sortOfArrayStore(item.array, item.index, item.value),
485 .bvconcat => |pair| try self.sortOfConcat(pair.lhs, pair.rhs),
486 .bvextract => |item| try self.sortOfExtract(item.operand, item.high, item.low),
487 .bvzeroext => |item| try self.sortOfExtend(item.operand, item.extra),
488 .bvsignext => |item| try self.sortOfExtend(item.operand, item.extra),
489 .bvrotl => |item| try self.expectBitVecResult(item.operand),
490 .bvrotr => |item| try self.expectBitVecResult(item.operand),
491 };
492 }
493
494 /// Appends the constant `value` and returns its term, so code builds the Boolean constants with
495 /// it.
496 pub fn boolValue(self: *Context, value: bool) !Term {
497 return try self.append(.{ .bool = value });
498 }
499
500 /// Appends the integer constant `value` and returns its term, so code builds integer constants
501 /// with it, as the SMT-LIB parser does for every numeral.
502 pub fn intValue(self: *Context, value: i128) !Term {
503 return try self.append(.{ .int = value });
504 }
505
506 /// Appends the constant with bits `value` and width `width` and returns its term, so code
507 /// builds bit-vector constants with it, as the SMT-LIB parser does for every `(_ bvV W)`. The
508 /// builder checks neither the value against the width nor the width. A width above 128 makes
509 /// the encoder panic.
510 pub fn bitvecValue(self: *Context, value: u128, width: u32) !Term {
511 return try self.append(.{ .bitvec = .{ .value = value, .width = width } });
512 }
513
514 /// Appends the negation of `operand` and returns its term, so code negates a Boolean term with
515 /// it.
516 pub fn not(self: *Context, operand: Term) !Term {
517 return try self.append(.{ .not = operand });
518 }
519
520 /// Appends the conjunction of `operands` and returns its term, so code calls it to join Boolean
521 /// terms that must all hold. The builder copies `operands`.
522 pub fn and_(self: *Context, operands: []const Term) !Term {
523 return try self.appendList(.and_, operands);
524 }
525
526 /// Appends the disjunction of `operands` and returns its term, so code calls it to join Boolean
527 /// terms of which one must hold. The builder copies `operands`.
528 pub fn or_(self: *Context, operands: []const Term) !Term {
529 return try self.appendList(.or_, operands);
530 }
531
532 /// Appends `lhs` implies `rhs` and returns its term, so code states that one Boolean term
533 /// implies another with it.
534 pub fn implies(self: *Context, lhs: Term, rhs: Term) !Term {
535 return try self.append(.{ .implies = .{ .lhs = lhs, .rhs = rhs } });
536 }
537
538 /// Appends `lhs` equals `rhs` and returns its term, so code calls it to state that two terms
539 /// are equal.
540 pub fn eq(self: *Context, lhs: Term, rhs: Term) !Term {
541 return try self.append(.{ .eq = .{ .lhs = lhs, .rhs = rhs } });
542 }
543
544 /// Appends the claim that `operands` all differ and returns its term, so code states that terms
545 /// all differ with it. The builder copies `operands`. The bit-vector encoder refuses the term.
546 pub fn distinct(self: *Context, operands: []const Term) !Term {
547 return try self.appendList(.distinct, operands);
548 }
549
550 /// Appends the integer sum of `operands` and returns its term, so code adds integer terms with
551 /// it. The builder copies `operands`. The bit-vector encoder refuses the term.
552 pub fn add(self: *Context, operands: []const Term) !Term {
553 return try self.appendList(.add, operands);
554 }
555
556 /// Appends the integer product of `operands` and returns its term, so code multiplies integer
557 /// terms with it. The builder copies `operands`. The bit-vector encoder refuses the term.
558 pub fn mul(self: *Context, operands: []const Term) !Term {
559 return try self.appendList(.mul, operands);
560 }
561
562 /// Appends the two-operand term of kind `tag` over `lhs` and `rhs` and returns its term, so the
563 /// SMT-LIB parser calls it with the tag of each two-operand operator it reads, and one call
564 /// covers every such operator. The parameter `tag` names a kind whose payload is
565 /// `BinaryOperands`, or `.array_select`, which the builder builds with `arraySelect`. Any other
566 /// tag is a compile error.
567 pub fn binary(self: *Context, comptime tag: std.meta.Tag(Expr), lhs: Term, rhs: Term) !Term {
568 return switch (tag) {
569 .implies,
570 .eq,
571 .le,
572 .lt,
573 .ge,
574 .gt,
575 .bvule,
576 .bvult,
577 .bvsle,
578 .bvslt,
579 .bvuaddo,
580 .bvsaddo,
581 .bvssubo,
582 .bvumulo,
583 .bvsmulo,
584 .bvand,
585 .bvor,
586 .bvxor,
587 .bvshl,
588 .bvlshr,
589 .bvashr,
590 .bvudiv,
591 .bvurem,
592 .bvsdiv,
593 .bvsrem,
594 .bvsmod,
595 .bvconcat,
596 .bvadd,
597 .bvsub,
598 .bvmul,
599 => try self.appendPair(tag, lhs, rhs),
600 .array_select => try self.arraySelect(lhs, rhs),
601 else => unreachable,
602 };
603 }
604
605 /// Appends `lhs` at most `rhs`, as integers, and returns its term, so code compares integer
606 /// terms with it. The bit-vector encoder refuses the term.
607 pub fn le(self: *Context, lhs: Term, rhs: Term) !Term {
608 return try self.append(.{ .le = .{ .lhs = lhs, .rhs = rhs } });
609 }
610
611 /// Appends `lhs` less than `rhs`, as integers, and returns its term, so code compares integer
612 /// terms with it. The bit-vector encoder refuses the term.
613 pub fn lt(self: *Context, lhs: Term, rhs: Term) !Term {
614 return try self.append(.{ .lt = .{ .lhs = lhs, .rhs = rhs } });
615 }
616
617 /// Appends `lhs` at least `rhs`, as integers, and returns its term, so code compares integer
618 /// terms with it. The bit-vector encoder refuses the term.
619 pub fn ge(self: *Context, lhs: Term, rhs: Term) !Term {
620 return try self.append(.{ .ge = .{ .lhs = lhs, .rhs = rhs } });
621 }
622
623 /// Appends `lhs` greater than `rhs`, as integers, and returns its term, so code compares
624 /// integer terms with it. The bit-vector encoder refuses the term.
625 pub fn gt(self: *Context, lhs: Term, rhs: Term) !Term {
626 return try self.append(.{ .gt = .{ .lhs = lhs, .rhs = rhs } });
627 }
628
629 /// Appends `lhs` at most `rhs`, as unsigned bit-vectors, and returns its term, so code compares
630 /// bit-vectors as unsigned numbers with it.
631 pub fn bvule(self: *Context, lhs: Term, rhs: Term) !Term {
632 return try self.append(.{ .bvule = .{ .lhs = lhs, .rhs = rhs } });
633 }
634
635 /// Appends `lhs` less than `rhs`, as unsigned bit-vectors, and returns its term, so code
636 /// compares bit-vectors as unsigned numbers with it, as the SMT-LIB round-trip test does.
637 pub fn bvult(self: *Context, lhs: Term, rhs: Term) !Term {
638 return try self.append(.{ .bvult = .{ .lhs = lhs, .rhs = rhs } });
639 }
640
641 /// Appends `lhs` at most `rhs`, as two's-complement bit-vectors, and returns its term, so code
642 /// compares bit-vectors as two's-complement numbers with it.
643 pub fn bvsle(self: *Context, lhs: Term, rhs: Term) !Term {
644 return try self.append(.{ .bvsle = .{ .lhs = lhs, .rhs = rhs } });
645 }
646
647 /// Appends `lhs` less than `rhs`, as two's-complement bit-vectors, and returns its term, so
648 /// code compares bit-vectors as two's-complement numbers with it.
649 pub fn bvslt(self: *Context, lhs: Term, rhs: Term) !Term {
650 return try self.append(.{ .bvslt = .{ .lhs = lhs, .rhs = rhs } });
651 }
652
653 /// Appends the claim that the unsigned sum of `lhs` and `rhs` overflows their width and returns
654 /// its term. Code asks with it whether an unsigned addition can overflow.
655 pub fn bvuaddo(self: *Context, lhs: Term, rhs: Term) !Term {
656 return try self.append(.{ .bvuaddo = .{ .lhs = lhs, .rhs = rhs } });
657 }
658
659 /// Appends the claim that the two's-complement sum of `lhs` and `rhs` overflows their width and
660 /// returns its term. Code asks with it whether a two's-complement addition can overflow.
661 pub fn bvsaddo(self: *Context, lhs: Term, rhs: Term) !Term {
662 return try self.append(.{ .bvsaddo = .{ .lhs = lhs, .rhs = rhs } });
663 }
664
665 /// Appends the claim that the two's-complement difference `lhs` minus `rhs` overflows their
666 /// width and returns its term. Code asks with it whether a two's-complement subtraction can
667 /// overflow.
668 pub fn bvssubo(self: *Context, lhs: Term, rhs: Term) !Term {
669 return try self.append(.{ .bvssubo = .{ .lhs = lhs, .rhs = rhs } });
670 }
671
672 /// Appends the claim that the unsigned product of `lhs` and `rhs` overflows their width and
673 /// returns its term. Code asks with it whether an unsigned multiplication can overflow.
674 pub fn bvumulo(self: *Context, lhs: Term, rhs: Term) !Term {
675 return try self.append(.{ .bvumulo = .{ .lhs = lhs, .rhs = rhs } });
676 }
677
678 /// Appends the claim that the two's-complement product of `lhs` and `rhs` overflows their width
679 /// and returns its term. Code asks with it whether a two's-complement multiplication can
680 /// overflow.
681 pub fn bvsmulo(self: *Context, lhs: Term, rhs: Term) !Term {
682 return try self.append(.{ .bvsmulo = .{ .lhs = lhs, .rhs = rhs } });
683 }
684
685 /// Appends the bitwise complement of `operand` and returns its term. Code complements every bit
686 /// of a bit-vector with it.
687 pub fn bvnot(self: *Context, operand: Term) !Term {
688 return try self.append(.{ .bvnot = operand });
689 }
690
691 /// Appends the bitwise and of `lhs` and `rhs` and returns its term. Code masks bit-vectors with
692 /// it.
693 pub fn bvand(self: *Context, lhs: Term, rhs: Term) !Term {
694 return try self.append(.{ .bvand = .{ .lhs = lhs, .rhs = rhs } });
695 }
696
697 /// Appends the bitwise or of `lhs` and `rhs` and returns its term. Code sets bits of a
698 /// bit-vector with it.
699 pub fn bvor(self: *Context, lhs: Term, rhs: Term) !Term {
700 return try self.append(.{ .bvor = .{ .lhs = lhs, .rhs = rhs } });
701 }
702
703 /// Appends the bitwise exclusive or of `lhs` and `rhs` and returns its term. Code flips bits of
704 /// a bit-vector with it.
705 pub fn bvxor(self: *Context, lhs: Term, rhs: Term) !Term {
706 return try self.append(.{ .bvxor = .{ .lhs = lhs, .rhs = rhs } });
707 }
708
709 /// Appends `lhs` shifted toward its most significant bit by the value of `rhs` and returns its
710 /// term. Code shifts a bit-vector left with it.
711 pub fn bvshl(self: *Context, lhs: Term, rhs: Term) !Term {
712 return try self.append(.{ .bvshl = .{ .lhs = lhs, .rhs = rhs } });
713 }
714
715 /// Appends `lhs` shifted toward its least significant bit by the value of `rhs`, with zeros
716 /// shifted in, and returns its term. Code shifts with it a bit-vector right with zero fill.
717 pub fn bvlshr(self: *Context, lhs: Term, rhs: Term) !Term {
718 return try self.append(.{ .bvlshr = .{ .lhs = lhs, .rhs = rhs } });
719 }
720
721 /// Appends `lhs` shifted toward its least significant bit by the value of `rhs`, with copies of
722 /// its sign bit shifted in, and returns its term. Code shifts a two's-complement bit-vector
723 /// right with it.
724 pub fn bvashr(self: *Context, lhs: Term, rhs: Term) !Term {
725 return try self.append(.{ .bvashr = .{ .lhs = lhs, .rhs = rhs } });
726 }
727
728 /// Appends the unsigned quotient of `lhs` by `rhs` and returns its term. Code divides
729 /// bit-vectors as unsigned numbers with it.
730 pub fn bvudiv(self: *Context, lhs: Term, rhs: Term) !Term {
731 return try self.append(.{ .bvudiv = .{ .lhs = lhs, .rhs = rhs } });
732 }
733
734 /// Appends the unsigned remainder of `lhs` by `rhs` and returns its term. Code takes the
735 /// unsigned remainder of bit-vectors with it.
736 pub fn bvurem(self: *Context, lhs: Term, rhs: Term) !Term {
737 return try self.append(.{ .bvurem = .{ .lhs = lhs, .rhs = rhs } });
738 }
739
740 /// Appends the two's-complement quotient of `lhs` by `rhs`, rounded toward zero, and returns
741 /// its term. Code divides bit-vectors as two's-complement numbers with it.
742 pub fn bvsdiv(self: *Context, lhs: Term, rhs: Term) !Term {
743 return try self.append(.{ .bvsdiv = .{ .lhs = lhs, .rhs = rhs } });
744 }
745
746 /// Appends the remainder of `lhs` by `rhs` with the sign of `lhs` and returns its term. Code
747 /// takes the two's-complement remainder of bit-vectors with it.
748 pub fn bvsrem(self: *Context, lhs: Term, rhs: Term) !Term {
749 return try self.append(.{ .bvsrem = .{ .lhs = lhs, .rhs = rhs } });
750 }
751
752 /// Appends the modulo of `lhs` by `rhs` with the sign of `rhs` and returns its term. Code takes
753 /// the two's-complement modulo of bit-vectors with it.
754 pub fn bvsmod(self: *Context, lhs: Term, rhs: Term) !Term {
755 return try self.append(.{ .bvsmod = .{ .lhs = lhs, .rhs = rhs } });
756 }
757
758 /// Appends the element of `array` at `index` and returns its term. Code reads an array at an
759 /// index with it.
760 pub fn arraySelect(self: *Context, array: Term, index: Term) !Term {
761 return try self.append(.{ .array_select = .{ .array = array, .index = index } });
762 }
763
764 /// Appends the array equal to `array` except that `index` holds `value`, and returns its term.
765 /// Code writes an element into an array with it.
766 pub fn arrayStore(self: *Context, array: Term, index: Term, value: Term) !Term {
767 return try self.append(.{ .array_store = .{
768 .array = array,
769 .index = index,
770 .value = value,
771 } });
772 }
773
774 /// Appends the bits of `lhs` above the bits of `rhs` and returns its term. Code joins two
775 /// bit-vectors into a wider one with it.
776 pub fn bvconcat(self: *Context, lhs: Term, rhs: Term) !Term {
777 return try self.append(.{ .bvconcat = .{ .lhs = lhs, .rhs = rhs } });
778 }
779
780 /// Appends the bits from position `high` down to position `low` of `operand`, both included,
781 /// and returns its term. Code takes a range of bits from a bit-vector with it. It checks no
782 /// range: `sortOf` and the encoder report `InvalidBitVectorRange` when `low` is above `high` or
783 /// `high` is at or above the width.
784 pub fn bvextract(self: *Context, operand: Term, high: u32, low: u32) !Term {
785 return try self.append(.{ .bvextract = .{ .operand = operand, .high = high, .low = low } });
786 }
787
788 /// Appends `operand` widened by `extra` zero bits above its most significant bit and returns
789 /// its term. Code widens an unsigned bit-vector with it.
790 pub fn bvzeroext(self: *Context, operand: Term, extra: u32) !Term {
791 return try self.append(.{ .bvzeroext = .{ .operand = operand, .extra = extra } });
792 }
793
794 /// Appends `operand` widened by `extra` copies of its sign bit and returns its term. Code
795 /// widens a two's-complement bit-vector with it.
796 pub fn bvsignext(self: *Context, operand: Term, extra: u32) !Term {
797 return try self.append(.{ .bvsignext = .{ .operand = operand, .extra = extra } });
798 }
799
800 /// Appends `operand` rotated toward its most significant bit by `amount` positions and returns
801 /// its term. Code rotates a bit-vector left by a fixed amount with it.
802 pub fn bvrotl(self: *Context, operand: Term, amount: u32) !Term {
803 return try self.append(.{ .bvrotl = .{ .operand = operand, .amount = amount } });
804 }
805
806 /// Appends `operand` rotated toward its least significant bit by `amount` positions and returns
807 /// its term. Code rotates a bit-vector right by a fixed amount with it.
808 pub fn bvrotr(self: *Context, operand: Term, amount: u32) !Term {
809 return try self.append(.{ .bvrotr = .{ .operand = operand, .amount = amount } });
810 }
811
812 /// Appends the sum of `lhs` and `rhs`, modulo 2 to the power of their width, and returns its
813 /// term. Code adds bit-vectors with it.
814 pub fn bvadd(self: *Context, lhs: Term, rhs: Term) !Term {
815 return try self.append(.{ .bvadd = .{ .lhs = lhs, .rhs = rhs } });
816 }
817
818 /// Appends `lhs` minus `rhs`, modulo 2 to the power of their width, and returns its term. Code
819 /// subtracts bit-vectors with it.
820 pub fn bvsub(self: *Context, lhs: Term, rhs: Term) !Term {
821 return try self.append(.{ .bvsub = .{ .lhs = lhs, .rhs = rhs } });
822 }
823
824 /// Appends the product of `lhs` and `rhs`, modulo 2 to the power of their width, and returns
825 /// its term. Code multiplies bit-vectors with it.
826 pub fn bvmul(self: *Context, lhs: Term, rhs: Term) !Term {
827 return try self.append(.{ .bvmul = .{ .lhs = lhs, .rhs = rhs } });
828 }
829
830 fn sortOfApply(self: *const Context, item: ApplyExpr) !Sort {
831 if (item.function >= self.functions.items.len) return error.UnknownFunction;
832 const decl = self.functions.items[item.function];
833 if (decl.params.len != item.args.len) return error.FunctionArityMismatch;
834 for (item.args, decl.params) |arg, expected| {
835 if (!(try self.sortOf(arg)).eql(expected)) return error.FunctionArgumentSortMismatch;
836 }
837 return decl.result;
838 }
839
840 fn expectBoolResult(self: *const Context, operand: Term) !Sort {
841 if (!(try self.sortOf(operand)).eql(.bool)) return error.SortMismatch;
842 return .bool;
843 }
844
845 fn expectBoolPair(self: *const Context, lhs: Term, rhs: Term) !Sort {
846 if (!(try self.sortOf(lhs)).eql(.bool) or !(try self.sortOf(rhs)).eql(.bool)) {
847 return error.SortMismatch;
848 }
849 return .bool;
850 }
851
852 fn expectBoolList(self: *const Context, operands: []const Term) !Sort {
853 for (operands) |operand| {
854 if (!(try self.sortOf(operand)).eql(.bool)) return error.SortMismatch;
855 }
856 return .bool;
857 }
858
859 fn expectIntPair(self: *const Context, lhs: Term, rhs: Term) !Sort {
860 if (!(try self.sortOf(lhs)).eql(.int) or !(try self.sortOf(rhs)).eql(.int)) {
861 return error.SortMismatch;
862 }
863 return .bool;
864 }
865
866 fn expectIntList(self: *const Context, operands: []const Term) !Sort {
867 for (operands) |operand| {
868 if (!(try self.sortOf(operand)).eql(.int)) return error.SortMismatch;
869 }
870 return .int;
871 }
872
873 fn expectSameSortPair(self: *const Context, lhs: Term, rhs: Term) !Sort {
874 if (!(try self.sortOf(lhs)).eql(try self.sortOf(rhs))) return error.SortMismatch;
875 return .bool;
876 }
877
878 fn expectSameSortList(self: *const Context, operands: []const Term) !Sort {
879 if (operands.len == 0) return .bool;
880 const expected = try self.sortOf(operands[0]);
881 for (operands[1..]) |operand| {
882 if (!(try self.sortOf(operand)).eql(expected)) return error.SortMismatch;
883 }
884 return .bool;
885 }
886
887 fn expectBitVecPair(self: *const Context, lhs: Term, rhs: Term) !Sort {
888 _ = try self.expectBitVecPairResult(lhs, rhs);
889 return .bool;
890 }
891
892 fn expectBitVecResult(self: *const Context, operand: Term) !Sort {
893 return switch (try self.sortOf(operand)) {
894 .bitvec => |width| .{ .bitvec = width },
895 else => error.SortMismatch,
896 };
897 }
898
899 fn expectBitVecPairResult(self: *const Context, lhs: Term, rhs: Term) !Sort {
900 return switch (try self.sortOf(lhs)) {
901 .bitvec => |lhs_width| switch (try self.sortOf(rhs)) {
902 .bitvec => |rhs_width| {
903 if (lhs_width != rhs_width) return error.SortMismatch;
904 return .{ .bitvec = lhs_width };
905 },
906 else => error.SortMismatch,
907 },
908 else => error.SortMismatch,
909 };
910 }
911
912 fn sortOfArraySelect(self: *const Context, array: Term, index: Term) !Sort {
913 const array_sort = try self.sortOf(array);
914 const index_sort = try self.sortOf(index);
915 return switch (array_sort) {
916 .array => |shape| switch (index_sort) {
917 .bitvec => |width| {
918 if (width != shape.index_width) return error.SortMismatch;
919 return .{ .bitvec = shape.element_width };
920 },
921 else => error.SortMismatch,
922 },
923 else => error.SortMismatch,
924 };
925 }
926
927 fn sortOfArrayStore(self: *const Context, array: Term, index: Term, value: Term) !Sort {
928 const array_sort = try self.sortOf(array);
929 const index_sort = try self.sortOf(index);
930 const value_sort = try self.sortOf(value);
931 return switch (array_sort) {
932 .array => |shape| switch (index_sort) {
933 .bitvec => |index_width| switch (value_sort) {
934 .bitvec => |element_width| {
935 if (index_width != shape.index_width or
936 element_width != shape.element_width)
937 {
938 return error.SortMismatch;
939 }
940 return array_sort;
941 },
942 else => error.SortMismatch,
943 },
944 else => error.SortMismatch,
945 },
946 else => error.SortMismatch,
947 };
948 }
949
950 fn sortOfConcat(self: *const Context, lhs: Term, rhs: Term) !Sort {
951 return switch (try self.sortOf(lhs)) {
952 .bitvec => |lhs_width| switch (try self.sortOf(rhs)) {
953 .bitvec => |rhs_width| .{ .bitvec = try std.math.add(u32, lhs_width, rhs_width) },
954 else => error.SortMismatch,
955 },
956 else => error.SortMismatch,
957 };
958 }
959
960 fn sortOfExtract(self: *const Context, operand: Term, high: u32, low: u32) !Sort {
961 return switch (try self.sortOf(operand)) {
962 .bitvec => |width| {
963 if (low > high or high >= width) return error.InvalidBitVectorRange;
964 return .{ .bitvec = high - low + 1 };
965 },
966 else => error.SortMismatch,
967 };
968 }
969
970 fn sortOfExtend(self: *const Context, operand: Term, extra: u32) !Sort {
971 return switch (try self.sortOf(operand)) {
972 .bitvec => |width| .{ .bitvec = try std.math.add(u32, width, extra) },
973 else => error.SortMismatch,
974 };
975 }
976
977 fn append(self: *Context, expr: Expr) !Term {
978 const id: Term = @intCast(self.nodes.items.len);
979 try self.nodes.append(self.allocator, expr);
980 return id;
981 }
982
983 fn appendPair(self: *Context, comptime tag: std.meta.Tag(Expr), lhs: Term, rhs: Term) !Term {
984 return try self.append(@unionInit(Expr, @tagName(tag), .{ .lhs = lhs, .rhs = rhs }));
985 }
986
987 fn appendList(self: *Context, comptime tag: std.meta.Tag(Expr), operands: []const Term) !Term {
988 const owned = try self.allocator.dupe(Term, operands);
989 errdefer self.allocator.free(owned);
990 return switch (tag) {
991 .and_ => try self.append(.{ .and_ = owned }),
992 .or_ => try self.append(.{ .or_ = owned }),
993 .distinct => try self.append(.{ .distinct = owned }),
994 .add => try self.append(.{ .add = owned }),
995 .mul => try self.append(.{ .mul = owned }),
996 else => unreachable,
997 };
998 }
999 };
1000
1001 fn sortListsEqual(lhs: []const Sort, rhs: []const Sort) bool {
1002 if (lhs.len != rhs.len) return false;
1003 for (lhs, rhs) |left, right| {
1004 if (!left.eql(right)) return false;
1005 }
1006 return true;
1007 }
1008
1009 /// A logic name and the list of terms asserted over one `Context`. `smtlib.parseScript` returns
1010 /// one, `smtlib.writeScript` prints one, and code that solves a script asserts each of its terms
1011 /// with the encoder. It borrows the `Context` and allocates its list with the `Context`'s
1012 /// allocator.
1013 pub const Script = struct {
1014 /// The `Context` whose terms the script asserts.
1015 ctx: *Context,
1016 /// The logic name, such as `QF_BV`, that `set-logic` gives. The script borrows it: a script
1017 /// from `smtlib.parseScript` points into the parsed text, which has to outlive the script.
1018 logic: []const u8,
1019 /// The asserted terms in the order they were asserted.
1020 assertions: std.ArrayList(Term) = .empty,
1021
1022 /// Returns a script over `ctx` with logic `logic` and no assertions. Code makes an empty script
1023 /// before asserting terms, as the SMT-LIB writer's tests do. It copies neither and allocates
1024 /// nothing.
1025 pub fn init(ctx: *Context, logic: []const u8) Script {
1026 return .{ .ctx = ctx, .logic = logic };
1027 }
1028
1029 /// Frees the list of assertions and leaves the terms to the `Context`. The owner calls it
1030 /// before freeing the `Context`.
1031 pub fn deinit(self: *Script) void {
1032 self.assertions.deinit(self.ctx.allocator);
1033 self.* = undefined;
1034 }
1035
1036 /// Appends `assertion` to the list. Code adds one assertion to a script with it. It checks
1037 /// nothing, including whether the term is Boolean.
1038 pub fn assertTerm(self: *Script, assertion: Term) !void {
1039 try self.assertions.append(self.ctx.allocator, assertion);
1040 }
1041 };
1042
1043 test "term context stores structured arithmetic expression" {
1044 var ctx = Context.init(std.testing.allocator);
1045 defer ctx.deinit();
1046 const x = try ctx.symbol("x", .int);
1047 const one = try ctx.intValue(1);
1048 const sum = try ctx.add(&.{ x, one });
1049 const zero = try ctx.intValue(0);
1050 _ = try ctx.gt(sum, zero);
1051 try std.testing.expectEqual(@as(usize, 5), ctx.nodes.items.len);
1052 }
1053
1054 test "term context stores function applications" {
1055 var ctx = Context.init(std.testing.allocator);
1056 defer ctx.deinit();
1057 const bv4 = Sort{ .bitvec = 4 };
1058 const x = try ctx.symbol("x", bv4);
1059 const y = try ctx.symbol("y", bv4);
1060 const flag = try ctx.symbol("flag", .bool);
1061 const f = try ctx.function("f", &.{bv4}, bv4);
1062 const fx = try ctx.apply(f, &.{x});
1063 _ = try ctx.apply(f, &.{y});
1064 try std.testing.expectEqual(@as(usize, 1), ctx.functions.items.len);
1065 try std.testing.expectEqual(@as(usize, 5), ctx.nodes.items.len);
1066 try std.testing.expect((try ctx.sortOf(fx)).eql(bv4));
1067 try std.testing.expectEqual(f, try ctx.function("f", &.{bv4}, bv4));
1068 try std.testing.expectError(error.DuplicateFunction, ctx.function("f", &.{bv4}, .bool));
1069 try std.testing.expectError(error.FunctionArgumentSortMismatch, ctx.apply(f, &.{flag}));
1070 }
1071
1072 test "term context infers composite sorts" {
1073 var ctx = Context.init(std.testing.allocator);
1074 defer ctx.deinit();
1075 const bv4 = Sort{ .bitvec = 4 };
1076 const high = try ctx.symbol("high", bv4);
1077 const low = try ctx.symbol("low", bv4);
1078 const word = try ctx.bvconcat(high, low);
1079 const upper = try ctx.bvextract(word, 7, 4);
1080 const lower = try ctx.bvextract(word, 3, 0);
1081 const memory = try ctx.symbol("memory", .{ .array = .{
1082 .index_width = 2,
1083 .element_width = 4,
1084 } });
1085 const index = try ctx.symbol("index", .{ .bitvec = 2 });
1086 const read = try ctx.arraySelect(memory, index);
1087 try std.testing.expect((try ctx.sortOf(word)).eql(.{ .bitvec = 8 }));
1088 try std.testing.expect((try ctx.sortOf(upper)).eql(bv4));
1089 try std.testing.expect((try ctx.sortOf(lower)).eql(bv4));
1090 try std.testing.expect((try ctx.sortOf(try ctx.eq(upper, lower))).eql(.bool));
1091 try std.testing.expect((try ctx.sortOf(read)).eql(bv4));
1092 }
1093
1094 test "term context stores bit-vector overflow predicates" {
1095 var ctx = Context.init(std.testing.allocator);
1096 defer ctx.deinit();
1097 const x = try ctx.symbol("x", .{ .bitvec = 8 });
1098 const y = try ctx.symbol("y", .{ .bitvec = 8 });
1099 _ = try ctx.bvuaddo(x, y);
1100 _ = try ctx.bvsaddo(x, y);
1101 _ = try ctx.bvssubo(x, y);
1102 _ = try ctx.bvumulo(x, y);
1103 _ = try ctx.bvsmulo(x, y);
1104 try std.testing.expectEqual(@as(usize, 7), ctx.nodes.items.len);
1105 }
1106
1107 test "term context stores signed bit-vector comparisons" {
1108 var ctx = Context.init(std.testing.allocator);
1109 defer ctx.deinit();
1110 const x = try ctx.symbol("x", .{ .bitvec = 8 });
1111 const y = try ctx.symbol("y", .{ .bitvec = 8 });
1112 const difference = try ctx.bvsub(x, y);
1113 _ = try ctx.bvslt(difference, y);
1114 _ = try ctx.bvsle(x, y);
1115 try std.testing.expect((try ctx.sortOf(difference)).eql(.{ .bitvec = 8 }));
1116 try std.testing.expectEqual(@as(usize, 5), ctx.nodes.items.len);
1117 }
1118
1119 test "term context stores bit-vector bitwise operators" {
1120 var ctx = Context.init(std.testing.allocator);
1121 defer ctx.deinit();
1122 const x = try ctx.symbol("x", .{ .bitvec = 8 });
1123 const y = try ctx.symbol("y", .{ .bitvec = 8 });
1124 _ = try ctx.bvnot(x);
1125 _ = try ctx.bvand(x, y);
1126 _ = try ctx.bvor(x, y);
1127 _ = try ctx.bvxor(x, y);
1128 try std.testing.expectEqual(@as(usize, 6), ctx.nodes.items.len);
1129 }
1130
1131 test "term context stores bit-vector shift operators" {
1132 var ctx = Context.init(std.testing.allocator);
1133 defer ctx.deinit();
1134 const x = try ctx.symbol("x", .{ .bitvec = 8 });
1135 const amount = try ctx.symbol("amount", .{ .bitvec = 8 });
1136 _ = try ctx.bvshl(x, amount);
1137 _ = try ctx.bvlshr(x, amount);
1138 _ = try ctx.bvashr(x, amount);
1139 _ = try ctx.bvudiv(x, amount);
1140 _ = try ctx.bvurem(x, amount);
1141 _ = try ctx.bvsdiv(x, amount);
1142 _ = try ctx.bvsrem(x, amount);
1143 _ = try ctx.bvsmod(x, amount);
1144 try std.testing.expectEqual(@as(usize, 10), ctx.nodes.items.len);
1145 }
1146
1147 test "term context stores bit-vector width-changing operators" {
1148 var ctx = Context.init(std.testing.allocator);
1149 defer ctx.deinit();
1150 const high = try ctx.symbol("high", .{ .bitvec = 4 });
1151 const low = try ctx.symbol("low", .{ .bitvec = 4 });
1152 const word = try ctx.bvconcat(high, low);
1153 _ = try ctx.bvextract(word, 7, 4);
1154 _ = try ctx.bvzeroext(high, 4);
1155 _ = try ctx.bvsignext(low, 4);
1156 try std.testing.expectEqual(@as(usize, 6), ctx.nodes.items.len);
1157 }
1158
1159 test "term context stores bit-vector rotate operators" {
1160 var ctx = Context.init(std.testing.allocator);
1161 defer ctx.deinit();
1162 const x = try ctx.symbol("x", .{ .bitvec = 8 });
1163 _ = try ctx.bvrotl(x, 3);
1164 _ = try ctx.bvrotr(x, 5);
1165 try std.testing.expectEqual(@as(usize, 3), ctx.nodes.items.len);
1166 }
1167
1168 test "term context stores finite bit-vector array operators" {
1169 var ctx = Context.init(std.testing.allocator);
1170 defer ctx.deinit();
1171 const memory = try ctx.symbol("memory", .{ .array = .{
1172 .index_width = 2,
1173 .element_width = 4,
1174 } });
1175 const index = try ctx.symbol("index", .{ .bitvec = 2 });
1176 const value = try ctx.symbol("value", .{ .bitvec = 4 });
1177 const written = try ctx.arrayStore(memory, index, value);
1178 _ = try ctx.arraySelect(written, index);
1179 try std.testing.expectEqual(@as(usize, 5), ctx.nodes.items.len);
1180 }