tiny.smt.smtlib.parse.sort

1pub const sort = @import("sort.zig");

1//! Reads an SMT-LIB sort, or a parenthesized list of sorts, because every declaration gives the2//! sort of a constant or the argument and result sorts of a function.3//!4//! The reader accepts the Boolean sort `Bool`, the integer sort `Int`, the bit-vector sort5//! `(_ BitVec n)` and the array sort `(Array I E)`. The index sort `I` and the element sort `E` of6//! an array are each a bit-vector sort `(_ BitVec n)`.7const std = @import("std");8const smt = @import("../../root.zig");910const errors = @import("error.zig");11const state = @import("state.zig");12const token = @import("token.zig");1314const Error = errors.Error;15const ParseError = errors.ParseError;16const Parser = state.Parser;17const term = smt.term;1819/// Reads one sort and returns it. The command reader calls it for the sort of each declaration. The20/// call returns `ExpectedSort` for any other sort, arrays over other sorts included, and21/// `InvalidNumber` for a width other than a decimal 32-bit unsigned number. The function accepts22/// any width, 0 included.23pub fn parse(parser: *Parser) Error!term.Sort {24    if (token.peekLeft(parser)) {25        try token.expectLeft(parser);26        const head = try token.atom(parser);27        if (std.mem.eql(u8, head, "_")) {28            const kind = try token.atom(parser);29            if (!std.mem.eql(u8, kind, "BitVec")) return ParseError.ExpectedSort;30            const width = std.fmt.parseInt(u32, try token.atom(parser), 10) catch return ParseError.InvalidNumber;31            try token.expectRight(parser);32            return .{ .bitvec = width };33        }34        if (std.mem.eql(u8, head, "Array")) {35            const index = try parse(parser);36            const element = try parse(parser);37            try token.expectRight(parser);38            const index_width = switch (index) {39                .bitvec => |width| width,40                else => return ParseError.ExpectedSort,41            };42            const element_width = switch (element) {43                .bitvec => |width| width,44                else => return ParseError.ExpectedSort,45            };46            return .{ .array = .{ .index_width = index_width, .element_width = element_width } };47        }48        return ParseError.ExpectedSort;49    }50    const sort = try token.atom(parser);51    if (std.mem.eql(u8, sort, "Bool")) return .bool;52    if (std.mem.eql(u8, sort, "Int")) return .int;53    return ParseError.ExpectedSort;54}5556/// Reads a parenthesized list of sorts, possibly empty, and returns them as a slice. The command57/// reader calls it for the argument sorts of `declare-fun`. The slice is allocated with the58/// `Context`'s allocator, and the caller frees it. The call returns `ExpectedList` when the list59/// does not open with a parenthesis, and the errors of reading one sort.60pub fn list(parser: *Parser) Error![]term.Sort {61    try token.expectLeft(parser);62    var sorts: std.ArrayList(term.Sort) = .empty;63    errdefer sorts.deinit(parser.ctx.allocator);64    while (!token.peekRight(parser)) {65        try sorts.append(parser.ctx.allocator, try parse(parser));66    }67    try token.expectRight(parser);68    return try sorts.toOwnedSlice(parser.ctx.allocator);69}