tiny.smt.Sort

1/// The sort of a term: Boolean, integer, a bit-vector of a given width, or an array from2/// bit-vectors to bit-vectors. Code declares every constant and function with a sort, and `sortOf`3/// returns one for every term.4pub const Sort = union(enum) {5    /// The Boolean sort. SMT-LIB writes it `Bool`.6    bool,7    /// The sort of mathematical integers. SMT-LIB writes it `Int`. The bit-vector encoder refuses8    /// terms of this sort with `UnsupportedTerm`.9    int,10    /// A bit-vector sort, with its width in bits as the payload. SMT-LIB writes it `(_ BitVec n)`.11    /// Any width is accepted, 0 and widths above 128 included. A bit-vector constant wider than 12812    /// bits makes the encoder panic. A named constant wider than 128 bits encodes, and13    /// `Encoder.model` returns `ModelValueTooWide` for it.14    bitvec: u32,15    /// An array sort, with its index and element widths as the payload. SMT-LIB writes it16    /// `(Array (_ BitVec i) (_ BitVec e))`.17    array: ArraySort,1819    /// Writes the sort in SMT-LIB syntax: `Bool`, `Int`, `(_ BitVec n)` or20    /// `(Array (_ BitVec i) (_ BitVec e))`. The SMT-LIB writer calls it to print the sort of every21    /// declaration. The function returns only the writer's errors.22    pub fn write(self: Sort, writer: *std.Io.Writer) std.Io.Writer.Error!void {23        switch (self) {24            .bool => try writer.writeAll("Bool"),25            .int => try writer.writeAll("Int"),26            .bitvec => |width| try writer.print("(_ BitVec {d})", .{width}),27            .array => |array| try writer.print(28                "(Array (_ BitVec {d}) (_ BitVec {d}))",29                .{ array.index_width, array.element_width },30            ),31        }32    }3334    /// Returns true when the two sorts have the same kind and the same widths. `sortOf` and35    /// `function` call it to compare the sort an operator needs with the sort it got.36    pub fn eql(self: Sort, other: Sort) bool {37        return std.meta.eql(self, other);38    }39};

1pub const Sort = term.Sort;