tiny.smt.Context

1/// One table that owns every term and function declaration it holds. Every formula starts here: a2/// caller makes one, builds its terms with the builders, and frees them all at once with `deinit`.3/// Each builder appends one term and returns its index. The builders check no sorts, except4/// `function` and `apply`, and `sortOf` checks a term's sort when a caller asks. Every builder can5/// fail with `error.OutOfMemory`, and a failed builder leaves the table as it was. A `Script`, a6/// parser and an encoder borrow the `Context` and have to be freed before it.7pub const Context = struct {8    /// The allocator for every term, name, operand list and declaration. A `Script` over this table9    /// and the SMT-LIB parser allocate with it too.10    allocator: std.mem.Allocator,11    /// Every term in the order it was built: entry i is the term whose index is i. The encoder and12    /// the SMT-LIB writer read it to walk every named constant.13    nodes: std.ArrayList(Expr) = .empty,14    /// Every function declaration in the order it was declared: entry i is the function whose index15    /// is i.16    functions: std.ArrayList(FunctionDecl) = .empty,1718    /// Returns an empty table that allocates with `allocator`, so a caller makes one before19    /// building any term. The call allocates nothing.20    pub fn init(allocator: std.mem.Allocator) Context {21        return .{ .allocator = allocator };22    }2324    /// Frees every term's name and operand list, every declaration and both tables, so the owner25    /// calls it once after every `Script`, parser and encoder built over the table is done with its26    /// terms. Every `Term` and `Function` index from this table is invalid afterward.27    pub fn deinit(self: *Context) void {28        for (self.nodes.items) |node| {29            switch (node) {30                .symbol => |sym| self.allocator.free(sym.name),31                .apply => |item| self.allocator.free(item.args),32                .and_, .or_, .distinct, .add, .mul => |items| self.allocator.free(items),33                else => {},34            }35        }36        for (self.functions.items) |decl| {37            self.allocator.free(decl.name);38            self.allocator.free(decl.params);39        }40        self.functions.deinit(self.allocator);41        self.nodes.deinit(self.allocator);42        self.* = undefined;43    }4445    /// Appends a named constant of the given sort and returns its term, so code declares each free46    /// variable of a formula with it, as the SMT-LIB parser does for every `declare-const`. The47    /// builder copies `name`, so the caller may free its own copy. The builder builds a new term on48    /// every call, even for a name used before.49    pub fn symbol(self: *Context, name: []const u8, sort: Sort) !Term {50        const owned_name = try self.allocator.dupe(u8, name);51        errdefer self.allocator.free(owned_name);52        return try self.append(.{ .symbol = .{ .name = owned_name, .sort = sort } });53    }5455    /// Declares a function by name, argument sorts and result sort, and returns its index, so code56    /// declares each uninterpreted function with it, as the SMT-LIB parser does for every57    /// `declare-fun`. A second call with the same name and the same sorts returns the first index.58    /// A second call with the same name and other sorts returns `error.DuplicateFunction`. The59    /// builder copies `name` and `params`.60    pub fn function(61        self: *Context,62        name: []const u8,63        params: []const Sort,64        result: Sort,65    ) !Function {66        for (self.functions.items, 0..) |decl, index| {67            if (!std.mem.eql(u8, decl.name, name)) continue;68            if (!sortListsEqual(decl.params, params) or !decl.result.eql(result)) {69                return error.DuplicateFunction;70            }71            return @intCast(index);72        }73        const owned_name = try self.allocator.dupe(u8, name);74        errdefer self.allocator.free(owned_name);75        const owned_params = try self.allocator.dupe(Sort, params);76        errdefer self.allocator.free(owned_params);77        const id: Function = @intCast(self.functions.items.len);78        try self.functions.append(self.allocator, .{79            .name = owned_name,80            .params = owned_params,81            .result = result,82        });83        return id;84    }8586    /// Appends the application of the function `function_id` to `args` and returns its term, so87    /// code applies a declared function to arguments with it. The call returns88    /// `error.UnknownFunction` for an index past the declarations, `error.FunctionArityMismatch`89    /// for the wrong number of arguments, and `error.FunctionArgumentSortMismatch` for an argument90    /// of the wrong sort. The builder computes each argument's sort with `sortOf`, so the call also91    /// returns the errors of `sortOf` for an argument that has no sort. The builder copies `args`.92    pub fn apply(self: *Context, function_id: Function, args: []const Term) !Term {93        if (function_id >= self.functions.items.len) return error.UnknownFunction;94        const decl = self.functions.items[function_id];95        if (decl.params.len != args.len) return error.FunctionArityMismatch;96        for (args, decl.params) |arg, expected| {97            if (!(try self.sortOf(arg)).eql(expected)) return error.FunctionArgumentSortMismatch;98        }99        const owned = try self.allocator.dupe(Term, args);100        errdefer self.allocator.free(owned);101        return try self.append(.{ .apply = .{ .function = function_id, .args = owned } });102    }103104    /// Returns the sort of term `id`, checking every operand below it against the sorts its105    /// operator accepts, so code checks a formula's sorts before encoding or writing, and the106    /// encoder reads each function argument's sort with it. The call returns `error.TermOutOfRange`107    /// for an index past the table, `error.SortMismatch` for an operand of the wrong sort,108    /// `error.InvalidBitVectorRange` for a bad extract range, and the errors of `apply` for a bad109    /// application. The function allocates nothing, and the call walks the whole term below `id` on110    /// every call. The recursion has no depth bound, and a term that refers to itself makes the111    /// call recurse without end.112    pub fn sortOf(self: *const Context, id: Term) anyerror!Sort {113        if (id >= self.nodes.items.len) return error.TermOutOfRange;114        return switch (self.nodes.items[id]) {115            .symbol => |sym| sym.sort,116            .apply => |item| try self.sortOfApply(item),117            .bool => .bool,118            .int => .int,119            .bitvec => |value| .{ .bitvec = value.width },120            .not => |operand| try self.expectBoolResult(operand),121            .and_, .or_ => |operands| try self.expectBoolList(operands),122            .implies => |pair| try self.expectBoolPair(pair.lhs, pair.rhs),123            .eq => |pair| try self.expectSameSortPair(pair.lhs, pair.rhs),124            .distinct => |operands| try self.expectSameSortList(operands),125            .add, .mul => |operands| try self.expectIntList(operands),126            .le => |pair| try self.expectIntPair(pair.lhs, pair.rhs),127            .lt => |pair| try self.expectIntPair(pair.lhs, pair.rhs),128            .ge => |pair| try self.expectIntPair(pair.lhs, pair.rhs),129            .gt => |pair| try self.expectIntPair(pair.lhs, pair.rhs),130            .bvule => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),131            .bvult => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),132            .bvsle => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),133            .bvslt => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),134            .bvuaddo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),135            .bvsaddo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),136            .bvssubo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),137            .bvumulo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),138            .bvsmulo => |pair| try self.expectBitVecPair(pair.lhs, pair.rhs),139            .bvnot => |operand| try self.expectBitVecResult(operand),140            .bvand => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),141            .bvor => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),142            .bvxor => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),143            .bvshl => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),144            .bvlshr => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),145            .bvashr => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),146            .bvudiv => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),147            .bvurem => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),148            .bvsdiv => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),149            .bvsrem => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),150            .bvsmod => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),151            .bvadd => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),152            .bvsub => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),153            .bvmul => |pair| try self.expectBitVecPairResult(pair.lhs, pair.rhs),154            .array_select => |item| try self.sortOfArraySelect(item.array, item.index),155            .array_store => |item| try self.sortOfArrayStore(item.array, item.index, item.value),156            .bvconcat => |pair| try self.sortOfConcat(pair.lhs, pair.rhs),157            .bvextract => |item| try self.sortOfExtract(item.operand, item.high, item.low),158            .bvzeroext => |item| try self.sortOfExtend(item.operand, item.extra),159            .bvsignext => |item| try self.sortOfExtend(item.operand, item.extra),160            .bvrotl => |item| try self.expectBitVecResult(item.operand),161            .bvrotr => |item| try self.expectBitVecResult(item.operand),162        };163    }164165    /// Appends the constant `value` and returns its term, so code builds the Boolean constants with166    /// it.167    pub fn boolValue(self: *Context, value: bool) !Term {168        return try self.append(.{ .bool = value });169    }170171    /// Appends the integer constant `value` and returns its term, so code builds integer constants172    /// with it, as the SMT-LIB parser does for every numeral.173    pub fn intValue(self: *Context, value: i128) !Term {174        return try self.append(.{ .int = value });175    }176177    /// Appends the constant with bits `value` and width `width` and returns its term, so code178    /// builds bit-vector constants with it, as the SMT-LIB parser does for every `(_ bvV W)`. The179    /// builder checks neither the value against the width nor the width. A width above 128 makes180    /// the encoder panic.181    pub fn bitvecValue(self: *Context, value: u128, width: u32) !Term {182        return try self.append(.{ .bitvec = .{ .value = value, .width = width } });183    }184185    /// Appends the negation of `operand` and returns its term, so code negates a Boolean term with186    /// it.187    pub fn not(self: *Context, operand: Term) !Term {188        return try self.append(.{ .not = operand });189    }190191    /// Appends the conjunction of `operands` and returns its term, so code calls it to join Boolean192    /// terms that must all hold. The builder copies `operands`.193    pub fn and_(self: *Context, operands: []const Term) !Term {194        return try self.appendList(.and_, operands);195    }196197    /// Appends the disjunction of `operands` and returns its term, so code calls it to join Boolean198    /// terms of which one must hold. The builder copies `operands`.199    pub fn or_(self: *Context, operands: []const Term) !Term {200        return try self.appendList(.or_, operands);201    }202203    /// Appends `lhs` implies `rhs` and returns its term, so code states that one Boolean term204    /// implies another with it.205    pub fn implies(self: *Context, lhs: Term, rhs: Term) !Term {206        return try self.append(.{ .implies = .{ .lhs = lhs, .rhs = rhs } });207    }208209    /// Appends `lhs` equals `rhs` and returns its term, so code calls it to state that two terms210    /// are equal.211    pub fn eq(self: *Context, lhs: Term, rhs: Term) !Term {212        return try self.append(.{ .eq = .{ .lhs = lhs, .rhs = rhs } });213    }214215    /// Appends the claim that `operands` all differ and returns its term, so code states that terms216    /// all differ with it. The builder copies `operands`. The bit-vector encoder refuses the term.217    pub fn distinct(self: *Context, operands: []const Term) !Term {218        return try self.appendList(.distinct, operands);219    }220221    /// Appends the integer sum of `operands` and returns its term, so code adds integer terms with222    /// it. The builder copies `operands`. The bit-vector encoder refuses the term.223    pub fn add(self: *Context, operands: []const Term) !Term {224        return try self.appendList(.add, operands);225    }226227    /// Appends the integer product of `operands` and returns its term, so code multiplies integer228    /// terms with it. The builder copies `operands`. The bit-vector encoder refuses the term.229    pub fn mul(self: *Context, operands: []const Term) !Term {230        return try self.appendList(.mul, operands);231    }232233    /// Appends the two-operand term of kind `tag` over `lhs` and `rhs` and returns its term, so the234    /// SMT-LIB parser calls it with the tag of each two-operand operator it reads, and one call235    /// covers every such operator. The parameter `tag` names a kind whose payload is236    /// `BinaryOperands`, or `.array_select`, which the builder builds with `arraySelect`. Any other237    /// tag is a compile error.238    pub fn binary(self: *Context, comptime tag: std.meta.Tag(Expr), lhs: Term, rhs: Term) !Term {239        return switch (tag) {240            .implies,241            .eq,242            .le,243            .lt,244            .ge,245            .gt,246            .bvule,247            .bvult,248            .bvsle,249            .bvslt,250            .bvuaddo,251            .bvsaddo,252            .bvssubo,253            .bvumulo,254            .bvsmulo,255            .bvand,256            .bvor,257            .bvxor,258            .bvshl,259            .bvlshr,260            .bvashr,261            .bvudiv,262            .bvurem,263            .bvsdiv,264            .bvsrem,265            .bvsmod,266            .bvconcat,267            .bvadd,268            .bvsub,269            .bvmul,270            => try self.appendPair(tag, lhs, rhs),271            .array_select => try self.arraySelect(lhs, rhs),272            else => unreachable,273        };274    }275276    /// Appends `lhs` at most `rhs`, as integers, and returns its term, so code compares integer277    /// terms with it. The bit-vector encoder refuses the term.278    pub fn le(self: *Context, lhs: Term, rhs: Term) !Term {279        return try self.append(.{ .le = .{ .lhs = lhs, .rhs = rhs } });280    }281282    /// Appends `lhs` less than `rhs`, as integers, and returns its term, so code compares integer283    /// terms with it. The bit-vector encoder refuses the term.284    pub fn lt(self: *Context, lhs: Term, rhs: Term) !Term {285        return try self.append(.{ .lt = .{ .lhs = lhs, .rhs = rhs } });286    }287288    /// Appends `lhs` at least `rhs`, as integers, and returns its term, so code compares integer289    /// terms with it. The bit-vector encoder refuses the term.290    pub fn ge(self: *Context, lhs: Term, rhs: Term) !Term {291        return try self.append(.{ .ge = .{ .lhs = lhs, .rhs = rhs } });292    }293294    /// Appends `lhs` greater than `rhs`, as integers, and returns its term, so code compares295    /// integer terms with it. The bit-vector encoder refuses the term.296    pub fn gt(self: *Context, lhs: Term, rhs: Term) !Term {297        return try self.append(.{ .gt = .{ .lhs = lhs, .rhs = rhs } });298    }299300    /// Appends `lhs` at most `rhs`, as unsigned bit-vectors, and returns its term, so code compares301    /// bit-vectors as unsigned numbers with it.302    pub fn bvule(self: *Context, lhs: Term, rhs: Term) !Term {303        return try self.append(.{ .bvule = .{ .lhs = lhs, .rhs = rhs } });304    }305306    /// Appends `lhs` less than `rhs`, as unsigned bit-vectors, and returns its term, so code307    /// compares bit-vectors as unsigned numbers with it, as the SMT-LIB round-trip test does.308    pub fn bvult(self: *Context, lhs: Term, rhs: Term) !Term {309        return try self.append(.{ .bvult = .{ .lhs = lhs, .rhs = rhs } });310    }311312    /// Appends `lhs` at most `rhs`, as two's-complement bit-vectors, and returns its term, so code313    /// compares bit-vectors as two's-complement numbers with it.314    pub fn bvsle(self: *Context, lhs: Term, rhs: Term) !Term {315        return try self.append(.{ .bvsle = .{ .lhs = lhs, .rhs = rhs } });316    }317318    /// Appends `lhs` less than `rhs`, as two's-complement bit-vectors, and returns its term, so319    /// code compares bit-vectors as two's-complement numbers with it.320    pub fn bvslt(self: *Context, lhs: Term, rhs: Term) !Term {321        return try self.append(.{ .bvslt = .{ .lhs = lhs, .rhs = rhs } });322    }323324    /// Appends the claim that the unsigned sum of `lhs` and `rhs` overflows their width and returns325    /// its term. Code asks with it whether an unsigned addition can overflow.326    pub fn bvuaddo(self: *Context, lhs: Term, rhs: Term) !Term {327        return try self.append(.{ .bvuaddo = .{ .lhs = lhs, .rhs = rhs } });328    }329330    /// Appends the claim that the two's-complement sum of `lhs` and `rhs` overflows their width and331    /// returns its term. Code asks with it whether a two's-complement addition can overflow.332    pub fn bvsaddo(self: *Context, lhs: Term, rhs: Term) !Term {333        return try self.append(.{ .bvsaddo = .{ .lhs = lhs, .rhs = rhs } });334    }335336    /// Appends the claim that the two's-complement difference `lhs` minus `rhs` overflows their337    /// width and returns its term. Code asks with it whether a two's-complement subtraction can338    /// overflow.339    pub fn bvssubo(self: *Context, lhs: Term, rhs: Term) !Term {340        return try self.append(.{ .bvssubo = .{ .lhs = lhs, .rhs = rhs } });341    }342343    /// Appends the claim that the unsigned product of `lhs` and `rhs` overflows their width and344    /// returns its term. Code asks with it whether an unsigned multiplication can overflow.345    pub fn bvumulo(self: *Context, lhs: Term, rhs: Term) !Term {346        return try self.append(.{ .bvumulo = .{ .lhs = lhs, .rhs = rhs } });347    }348349    /// Appends the claim that the two's-complement product of `lhs` and `rhs` overflows their width350    /// and returns its term. Code asks with it whether a two's-complement multiplication can351    /// overflow.352    pub fn bvsmulo(self: *Context, lhs: Term, rhs: Term) !Term {353        return try self.append(.{ .bvsmulo = .{ .lhs = lhs, .rhs = rhs } });354    }355356    /// Appends the bitwise complement of `operand` and returns its term. Code complements every bit357    /// of a bit-vector with it.358    pub fn bvnot(self: *Context, operand: Term) !Term {359        return try self.append(.{ .bvnot = operand });360    }361362    /// Appends the bitwise and of `lhs` and `rhs` and returns its term. Code masks bit-vectors with363    /// it.364    pub fn bvand(self: *Context, lhs: Term, rhs: Term) !Term {365        return try self.append(.{ .bvand = .{ .lhs = lhs, .rhs = rhs } });366    }367368    /// Appends the bitwise or of `lhs` and `rhs` and returns its term. Code sets bits of a369    /// bit-vector with it.370    pub fn bvor(self: *Context, lhs: Term, rhs: Term) !Term {371        return try self.append(.{ .bvor = .{ .lhs = lhs, .rhs = rhs } });372    }373374    /// Appends the bitwise exclusive or of `lhs` and `rhs` and returns its term. Code flips bits of375    /// a bit-vector with it.376    pub fn bvxor(self: *Context, lhs: Term, rhs: Term) !Term {377        return try self.append(.{ .bvxor = .{ .lhs = lhs, .rhs = rhs } });378    }379380    /// Appends `lhs` shifted toward its most significant bit by the value of `rhs` and returns its381    /// term. Code shifts a bit-vector left with it.382    pub fn bvshl(self: *Context, lhs: Term, rhs: Term) !Term {383        return try self.append(.{ .bvshl = .{ .lhs = lhs, .rhs = rhs } });384    }385386    /// Appends `lhs` shifted toward its least significant bit by the value of `rhs`, with zeros387    /// shifted in, and returns its term. Code shifts with it a bit-vector right with zero fill.388    pub fn bvlshr(self: *Context, lhs: Term, rhs: Term) !Term {389        return try self.append(.{ .bvlshr = .{ .lhs = lhs, .rhs = rhs } });390    }391392    /// Appends `lhs` shifted toward its least significant bit by the value of `rhs`, with copies of393    /// its sign bit shifted in, and returns its term. Code shifts a two's-complement bit-vector394    /// right with it.395    pub fn bvashr(self: *Context, lhs: Term, rhs: Term) !Term {396        return try self.append(.{ .bvashr = .{ .lhs = lhs, .rhs = rhs } });397    }398399    /// Appends the unsigned quotient of `lhs` by `rhs` and returns its term. Code divides400    /// bit-vectors as unsigned numbers with it.401    pub fn bvudiv(self: *Context, lhs: Term, rhs: Term) !Term {402        return try self.append(.{ .bvudiv = .{ .lhs = lhs, .rhs = rhs } });403    }404405    /// Appends the unsigned remainder of `lhs` by `rhs` and returns its term. Code takes the406    /// unsigned remainder of bit-vectors with it.407    pub fn bvurem(self: *Context, lhs: Term, rhs: Term) !Term {408        return try self.append(.{ .bvurem = .{ .lhs = lhs, .rhs = rhs } });409    }410411    /// Appends the two's-complement quotient of `lhs` by `rhs`, rounded toward zero, and returns412    /// its term. Code divides bit-vectors as two's-complement numbers with it.413    pub fn bvsdiv(self: *Context, lhs: Term, rhs: Term) !Term {414        return try self.append(.{ .bvsdiv = .{ .lhs = lhs, .rhs = rhs } });415    }416417    /// Appends the remainder of `lhs` by `rhs` with the sign of `lhs` and returns its term. Code418    /// takes the two's-complement remainder of bit-vectors with it.419    pub fn bvsrem(self: *Context, lhs: Term, rhs: Term) !Term {420        return try self.append(.{ .bvsrem = .{ .lhs = lhs, .rhs = rhs } });421    }422423    /// Appends the modulo of `lhs` by `rhs` with the sign of `rhs` and returns its term. Code takes424    /// the two's-complement modulo of bit-vectors with it.425    pub fn bvsmod(self: *Context, lhs: Term, rhs: Term) !Term {426        return try self.append(.{ .bvsmod = .{ .lhs = lhs, .rhs = rhs } });427    }428429    /// Appends the element of `array` at `index` and returns its term. Code reads an array at an430    /// index with it.431    pub fn arraySelect(self: *Context, array: Term, index: Term) !Term {432        return try self.append(.{ .array_select = .{ .array = array, .index = index } });433    }434435    /// Appends the array equal to `array` except that `index` holds `value`, and returns its term.436    /// Code writes an element into an array with it.437    pub fn arrayStore(self: *Context, array: Term, index: Term, value: Term) !Term {438        return try self.append(.{ .array_store = .{439            .array = array,440            .index = index,441            .value = value,442        } });443    }444445    /// Appends the bits of `lhs` above the bits of `rhs` and returns its term. Code joins two446    /// bit-vectors into a wider one with it.447    pub fn bvconcat(self: *Context, lhs: Term, rhs: Term) !Term {448        return try self.append(.{ .bvconcat = .{ .lhs = lhs, .rhs = rhs } });449    }450451    /// Appends the bits from position `high` down to position `low` of `operand`, both included,452    /// and returns its term. Code takes a range of bits from a bit-vector with it. It checks no453    /// range: `sortOf` and the encoder report `InvalidBitVectorRange` when `low` is above `high` or454    /// `high` is at or above the width.455    pub fn bvextract(self: *Context, operand: Term, high: u32, low: u32) !Term {456        return try self.append(.{ .bvextract = .{ .operand = operand, .high = high, .low = low } });457    }458459    /// Appends `operand` widened by `extra` zero bits above its most significant bit and returns460    /// its term. Code widens an unsigned bit-vector with it.461    pub fn bvzeroext(self: *Context, operand: Term, extra: u32) !Term {462        return try self.append(.{ .bvzeroext = .{ .operand = operand, .extra = extra } });463    }464465    /// Appends `operand` widened by `extra` copies of its sign bit and returns its term. Code466    /// widens a two's-complement bit-vector with it.467    pub fn bvsignext(self: *Context, operand: Term, extra: u32) !Term {468        return try self.append(.{ .bvsignext = .{ .operand = operand, .extra = extra } });469    }470471    /// Appends `operand` rotated toward its most significant bit by `amount` positions and returns472    /// its term. Code rotates a bit-vector left by a fixed amount with it.473    pub fn bvrotl(self: *Context, operand: Term, amount: u32) !Term {474        return try self.append(.{ .bvrotl = .{ .operand = operand, .amount = amount } });475    }476477    /// Appends `operand` rotated toward its least significant bit by `amount` positions and returns478    /// its term. Code rotates a bit-vector right by a fixed amount with it.479    pub fn bvrotr(self: *Context, operand: Term, amount: u32) !Term {480        return try self.append(.{ .bvrotr = .{ .operand = operand, .amount = amount } });481    }482483    /// Appends the sum of `lhs` and `rhs`, modulo 2 to the power of their width, and returns its484    /// term. Code adds bit-vectors with it.485    pub fn bvadd(self: *Context, lhs: Term, rhs: Term) !Term {486        return try self.append(.{ .bvadd = .{ .lhs = lhs, .rhs = rhs } });487    }488489    /// Appends `lhs` minus `rhs`, modulo 2 to the power of their width, and returns its term. Code490    /// subtracts bit-vectors with it.491    pub fn bvsub(self: *Context, lhs: Term, rhs: Term) !Term {492        return try self.append(.{ .bvsub = .{ .lhs = lhs, .rhs = rhs } });493    }494495    /// Appends the product of `lhs` and `rhs`, modulo 2 to the power of their width, and returns496    /// its term. Code multiplies bit-vectors with it.497    pub fn bvmul(self: *Context, lhs: Term, rhs: Term) !Term {498        return try self.append(.{ .bvmul = .{ .lhs = lhs, .rhs = rhs } });499    }500501    fn sortOfApply(self: *const Context, item: ApplyExpr) !Sort {502        if (item.function >= self.functions.items.len) return error.UnknownFunction;503        const decl = self.functions.items[item.function];504        if (decl.params.len != item.args.len) return error.FunctionArityMismatch;505        for (item.args, decl.params) |arg, expected| {506            if (!(try self.sortOf(arg)).eql(expected)) return error.FunctionArgumentSortMismatch;507        }508        return decl.result;509    }510511    fn expectBoolResult(self: *const Context, operand: Term) !Sort {512        if (!(try self.sortOf(operand)).eql(.bool)) return error.SortMismatch;513        return .bool;514    }515516    fn expectBoolPair(self: *const Context, lhs: Term, rhs: Term) !Sort {517        if (!(try self.sortOf(lhs)).eql(.bool) or !(try self.sortOf(rhs)).eql(.bool)) {518            return error.SortMismatch;519        }520        return .bool;521    }522523    fn expectBoolList(self: *const Context, operands: []const Term) !Sort {524        for (operands) |operand| {525            if (!(try self.sortOf(operand)).eql(.bool)) return error.SortMismatch;526        }527        return .bool;528    }529530    fn expectIntPair(self: *const Context, lhs: Term, rhs: Term) !Sort {531        if (!(try self.sortOf(lhs)).eql(.int) or !(try self.sortOf(rhs)).eql(.int)) {532            return error.SortMismatch;533        }534        return .bool;535    }536537    fn expectIntList(self: *const Context, operands: []const Term) !Sort {538        for (operands) |operand| {539            if (!(try self.sortOf(operand)).eql(.int)) return error.SortMismatch;540        }541        return .int;542    }543544    fn expectSameSortPair(self: *const Context, lhs: Term, rhs: Term) !Sort {545        if (!(try self.sortOf(lhs)).eql(try self.sortOf(rhs))) return error.SortMismatch;546        return .bool;547    }548549    fn expectSameSortList(self: *const Context, operands: []const Term) !Sort {550        if (operands.len == 0) return .bool;551        const expected = try self.sortOf(operands[0]);552        for (operands[1..]) |operand| {553            if (!(try self.sortOf(operand)).eql(expected)) return error.SortMismatch;554        }555        return .bool;556    }557558    fn expectBitVecPair(self: *const Context, lhs: Term, rhs: Term) !Sort {559        _ = try self.expectBitVecPairResult(lhs, rhs);560        return .bool;561    }562563    fn expectBitVecResult(self: *const Context, operand: Term) !Sort {564        return switch (try self.sortOf(operand)) {565            .bitvec => |width| .{ .bitvec = width },566            else => error.SortMismatch,567        };568    }569570    fn expectBitVecPairResult(self: *const Context, lhs: Term, rhs: Term) !Sort {571        return switch (try self.sortOf(lhs)) {572            .bitvec => |lhs_width| switch (try self.sortOf(rhs)) {573                .bitvec => |rhs_width| {574                    if (lhs_width != rhs_width) return error.SortMismatch;575                    return .{ .bitvec = lhs_width };576                },577                else => error.SortMismatch,578            },579            else => error.SortMismatch,580        };581    }582583    fn sortOfArraySelect(self: *const Context, array: Term, index: Term) !Sort {584        const array_sort = try self.sortOf(array);585        const index_sort = try self.sortOf(index);586        return switch (array_sort) {587            .array => |shape| switch (index_sort) {588                .bitvec => |width| {589                    if (width != shape.index_width) return error.SortMismatch;590                    return .{ .bitvec = shape.element_width };591                },592                else => error.SortMismatch,593            },594            else => error.SortMismatch,595        };596    }597598    fn sortOfArrayStore(self: *const Context, array: Term, index: Term, value: Term) !Sort {599        const array_sort = try self.sortOf(array);600        const index_sort = try self.sortOf(index);601        const value_sort = try self.sortOf(value);602        return switch (array_sort) {603            .array => |shape| switch (index_sort) {604                .bitvec => |index_width| switch (value_sort) {605                    .bitvec => |element_width| {606                        if (index_width != shape.index_width or607                            element_width != shape.element_width)608                        {609                            return error.SortMismatch;610                        }611                        return array_sort;612                    },613                    else => error.SortMismatch,614                },615                else => error.SortMismatch,616            },617            else => error.SortMismatch,618        };619    }620621    fn sortOfConcat(self: *const Context, lhs: Term, rhs: Term) !Sort {622        return switch (try self.sortOf(lhs)) {623            .bitvec => |lhs_width| switch (try self.sortOf(rhs)) {624                .bitvec => |rhs_width| .{ .bitvec = try std.math.add(u32, lhs_width, rhs_width) },625                else => error.SortMismatch,626            },627            else => error.SortMismatch,628        };629    }630631    fn sortOfExtract(self: *const Context, operand: Term, high: u32, low: u32) !Sort {632        return switch (try self.sortOf(operand)) {633            .bitvec => |width| {634                if (low > high or high >= width) return error.InvalidBitVectorRange;635                return .{ .bitvec = high - low + 1 };636            },637            else => error.SortMismatch,638        };639    }640641    fn sortOfExtend(self: *const Context, operand: Term, extra: u32) !Sort {642        return switch (try self.sortOf(operand)) {643            .bitvec => |width| .{ .bitvec = try std.math.add(u32, width, extra) },644            else => error.SortMismatch,645        };646    }647648    fn append(self: *Context, expr: Expr) !Term {649        const id: Term = @intCast(self.nodes.items.len);650        try self.nodes.append(self.allocator, expr);651        return id;652    }653654    fn appendPair(self: *Context, comptime tag: std.meta.Tag(Expr), lhs: Term, rhs: Term) !Term {655        return try self.append(@unionInit(Expr, @tagName(tag), .{ .lhs = lhs, .rhs = rhs }));656    }657658    fn appendList(self: *Context, comptime tag: std.meta.Tag(Expr), operands: []const Term) !Term {659        const owned = try self.allocator.dupe(Term, operands);660        errdefer self.allocator.free(owned);661        return switch (tag) {662            .and_ => try self.append(.{ .and_ = owned }),663            .or_ => try self.append(.{ .or_ = owned }),664            .distinct => try self.append(.{ .distinct = owned }),665            .add => try self.append(.{ .add = owned }),666            .mul => try self.append(.{ .mul = owned }),667            else => unreachable,668        };669    }670};

1pub const Context = term.Context;