lib/smt/src/smtlib/parse/sort.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! Reads an SMT-LIB sort, or a parenthesized list of sorts, because every declaration gives the
 2 //! 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 sort
 5 //! `(_ BitVec n)` and the array sort `(Array I E)`. The index sort `I` and the element sort `E` of
 6 //! an array are each a bit-vector sort `(_ BitVec n)`.
 7 const std = @import("std");
 8 const smt = @import("../../root.zig");
 9 
10 const errors = @import("error.zig");
11 const state = @import("state.zig");
12 const token = @import("token.zig");
13 
14 const Error = errors.Error;
15 const ParseError = errors.ParseError;
16 const Parser = state.Parser;
17 const term = smt.term;
18 
19 /// Reads one sort and returns it. The command reader calls it for the sort of each declaration. The
20 /// call returns `ExpectedSort` for any other sort, arrays over other sorts included, and
21 /// `InvalidNumber` for a width other than a decimal 32-bit unsigned number. The function accepts
22 /// any width, 0 included.
23 pub 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 }
55 
56 /// Reads a parenthesized list of sorts, possibly empty, and returns them as a slice. The command
57 /// reader calls it for the argument sorts of `declare-fun`. The slice is allocated with the
58 /// `Context`'s allocator, and the caller frees it. The call returns `ExpectedList` when the list
59 /// does not open with a parenthesis, and the errors of reading one sort.
60 pub 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 }