lib/smt/src/smtlib/parse/term.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! Reads one SMT-LIB term and builds it in a `Context`. A script's formulas use the operators of
2 //! different theories, so the reader has to map each operator name to the term it builds. A table
3 //! maps each supported SMT-LIB operator name to its term kind. Every two-operand operator takes
4 //! exactly two operands, so a chained `(= a b c)` fails. The reader refuses `let`, `ite`, `xor`,
5 //! `-`, `bvneg`, the `#b` and `#x` literals and quoted symbols. It descends one call per
6 //! parenthesis, with no depth bound.
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 const ExprTag = std.meta.Tag(term.Expr);
19
20 const Operation = union(enum) {
21 unary: ExprTag,
22 binary: ExprTag,
23 ternary: ExprTag,
24 nary: ExprTag,
25 };
26
27 const OperationEntry = struct {
28 name: []const u8,
29 operation: Operation,
30 };
31
32 const operations = [_]OperationEntry{
33 .{ .name = "not", .operation = .{ .unary = .not } },
34 .{ .name = "=>", .operation = .{ .binary = .implies } },
35 .{ .name = "=", .operation = .{ .binary = .eq } },
36 .{ .name = "<=", .operation = .{ .binary = .le } },
37 .{ .name = "<", .operation = .{ .binary = .lt } },
38 .{ .name = ">=", .operation = .{ .binary = .ge } },
39 .{ .name = ">", .operation = .{ .binary = .gt } },
40 .{ .name = "bvule", .operation = .{ .binary = .bvule } },
41 .{ .name = "bvult", .operation = .{ .binary = .bvult } },
42 .{ .name = "bvsle", .operation = .{ .binary = .bvsle } },
43 .{ .name = "bvslt", .operation = .{ .binary = .bvslt } },
44 .{ .name = "bvuaddo", .operation = .{ .binary = .bvuaddo } },
45 .{ .name = "bvsaddo", .operation = .{ .binary = .bvsaddo } },
46 .{ .name = "bvssubo", .operation = .{ .binary = .bvssubo } },
47 .{ .name = "bvumulo", .operation = .{ .binary = .bvumulo } },
48 .{ .name = "bvsmulo", .operation = .{ .binary = .bvsmulo } },
49 .{ .name = "bvnot", .operation = .{ .unary = .bvnot } },
50 .{ .name = "bvand", .operation = .{ .binary = .bvand } },
51 .{ .name = "bvor", .operation = .{ .binary = .bvor } },
52 .{ .name = "bvxor", .operation = .{ .binary = .bvxor } },
53 .{ .name = "bvshl", .operation = .{ .binary = .bvshl } },
54 .{ .name = "bvlshr", .operation = .{ .binary = .bvlshr } },
55 .{ .name = "bvashr", .operation = .{ .binary = .bvashr } },
56 .{ .name = "bvudiv", .operation = .{ .binary = .bvudiv } },
57 .{ .name = "bvurem", .operation = .{ .binary = .bvurem } },
58 .{ .name = "bvsdiv", .operation = .{ .binary = .bvsdiv } },
59 .{ .name = "bvsrem", .operation = .{ .binary = .bvsrem } },
60 .{ .name = "bvsmod", .operation = .{ .binary = .bvsmod } },
61 .{ .name = "select", .operation = .{ .binary = .array_select } },
62 .{ .name = "store", .operation = .{ .ternary = .array_store } },
63 .{ .name = "concat", .operation = .{ .binary = .bvconcat } },
64 .{ .name = "bvadd", .operation = .{ .binary = .bvadd } },
65 .{ .name = "bvsub", .operation = .{ .binary = .bvsub } },
66 .{ .name = "bvmul", .operation = .{ .binary = .bvmul } },
67 .{ .name = "and", .operation = .{ .nary = .and_ } },
68 .{ .name = "or", .operation = .{ .nary = .or_ } },
69 .{ .name = "distinct", .operation = .{ .nary = .distinct } },
70 .{ .name = "+", .operation = .{ .nary = .add } },
71 .{ .name = "*", .operation = .{ .nary = .mul } },
72 };
73
74 /// Reads one term at the parser's position, builds it in the parser's `Context` and returns it. The
75 /// command reader calls it for the term of each `assert`. An atom is `true`, `false`, an integer,
76 /// the name of a function with no arguments, or the name of a declared constant. An integer is a
77 /// decimal numeral with an optional leading `-`. A list is `(_ bvV W)` for a bit-vector constant,
78 /// an indexed operator such as `((_ extract high low) x)`, a supported operator applied to its
79 /// operands, or a declared function applied to its arguments. It returns `UnknownSymbol` for an
80 /// undeclared name, `UnsupportedTerm` for an unsupported operator, `InvalidNumber` for a malformed
81 /// number, and the errors of the `Context` builders, such as `FunctionArityMismatch`. It checks no
82 /// sorts except the arguments of a function application.
83 pub fn parse(parser: *Parser) Error!term.Term {
84 if (!token.peekLeft(parser)) {
85 const item = try token.atom(parser);
86 if (std.mem.eql(u8, item, "true")) return try parser.ctx.boolValue(true);
87 if (std.mem.eql(u8, item, "false")) return try parser.ctx.boolValue(false);
88 if (parseInteger(item)) |value| return try parser.ctx.intValue(value);
89 if (parser.functions.get(item)) |function_id| return try parser.ctx.apply(function_id, &.{});
90 return parser.symbols.get(item) orelse ParseError.UnknownSymbol;
91 }
92 try token.expectLeft(parser);
93 if (token.peekLeft(parser)) return try parseIndexed(parser);
94 const op = try token.atom(parser);
95 if (std.mem.eql(u8, op, "_")) {
96 const value_atom = try token.atom(parser);
97 if (!std.mem.startsWith(u8, value_atom, "bv")) return ParseError.UnsupportedTerm;
98 const value = std.fmt.parseInt(u128, value_atom[2..], 10) catch return ParseError.InvalidNumber;
99 const width = std.fmt.parseInt(u32, try token.atom(parser), 10) catch return ParseError.InvalidNumber;
100 try token.expectRight(parser);
101 return try parser.ctx.bitvecValue(value, width);
102 }
103 inline for (operations) |entry| {
104 if (std.mem.eql(u8, op, entry.name)) return try parseOperation(parser, entry.operation);
105 }
106 if (parser.functions.get(op)) |function_id| return try parseApply(parser, function_id);
107 return ParseError.UnsupportedTerm;
108 }
109
110 fn parseOperation(parser: *Parser, comptime operation: Operation) Error!term.Term {
111 return switch (operation) {
112 .unary => |tag| try parseUnary(parser, tag),
113 .binary => |tag| try parseBinary(parser, tag),
114 .ternary => |tag| try parseTernary(parser, tag),
115 .nary => |tag| try parseNary(parser, tag),
116 };
117 }
118
119 fn parseIndexed(parser: *Parser) Error!term.Term {
120 try token.expectLeft(parser);
121 const underscore = try token.atom(parser);
122 if (!std.mem.eql(u8, underscore, "_")) return ParseError.UnsupportedTerm;
123 const op = try token.atom(parser);
124 if (std.mem.eql(u8, op, "extract")) {
125 const high = std.fmt.parseInt(u32, try token.atom(parser), 10) catch return ParseError.InvalidNumber;
126 const low = std.fmt.parseInt(u32, try token.atom(parser), 10) catch return ParseError.InvalidNumber;
127 try token.expectRight(parser);
128 const operand = try parse(parser);
129 try token.expectRight(parser);
130 return try parser.ctx.bvextract(operand, high, low);
131 }
132 if (std.mem.eql(u8, op, "zero_extend")) {
133 const extra = std.fmt.parseInt(u32, try token.atom(parser), 10) catch return ParseError.InvalidNumber;
134 try token.expectRight(parser);
135 const operand = try parse(parser);
136 try token.expectRight(parser);
137 return try parser.ctx.bvzeroext(operand, extra);
138 }
139 if (std.mem.eql(u8, op, "sign_extend")) {
140 const extra = std.fmt.parseInt(u32, try token.atom(parser), 10) catch return ParseError.InvalidNumber;
141 try token.expectRight(parser);
142 const operand = try parse(parser);
143 try token.expectRight(parser);
144 return try parser.ctx.bvsignext(operand, extra);
145 }
146 if (std.mem.eql(u8, op, "rotate_left")) {
147 const amount = std.fmt.parseInt(u32, try token.atom(parser), 10) catch return ParseError.InvalidNumber;
148 try token.expectRight(parser);
149 const operand = try parse(parser);
150 try token.expectRight(parser);
151 return try parser.ctx.bvrotl(operand, amount);
152 }
153 if (std.mem.eql(u8, op, "rotate_right")) {
154 const amount = std.fmt.parseInt(u32, try token.atom(parser), 10) catch return ParseError.InvalidNumber;
155 try token.expectRight(parser);
156 const operand = try parse(parser);
157 try token.expectRight(parser);
158 return try parser.ctx.bvrotr(operand, amount);
159 }
160 return ParseError.UnsupportedTerm;
161 }
162
163 fn parseUnary(parser: *Parser, comptime tag: std.meta.Tag(term.Expr)) Error!term.Term {
164 const operand = try parse(parser);
165 try token.expectRight(parser);
166 return switch (tag) {
167 .not => try parser.ctx.not(operand),
168 .bvnot => try parser.ctx.bvnot(operand),
169 else => unreachable,
170 };
171 }
172
173 fn parseBinary(parser: *Parser, comptime tag: std.meta.Tag(term.Expr)) Error!term.Term {
174 const lhs = try parse(parser);
175 const rhs = try parse(parser);
176 try token.expectRight(parser);
177 return try parser.ctx.binary(tag, lhs, rhs);
178 }
179
180 fn parseTernary(parser: *Parser, comptime tag: std.meta.Tag(term.Expr)) Error!term.Term {
181 const first = try parse(parser);
182 const second = try parse(parser);
183 const third = try parse(parser);
184 try token.expectRight(parser);
185 return switch (tag) {
186 .array_store => try parser.ctx.arrayStore(first, second, third),
187 else => unreachable,
188 };
189 }
190
191 fn parseNary(parser: *Parser, comptime tag: std.meta.Tag(term.Expr)) Error!term.Term {
192 var operands: std.ArrayList(term.Term) = .empty;
193 defer operands.deinit(parser.ctx.allocator);
194 while (!token.peekRight(parser)) {
195 try operands.append(parser.ctx.allocator, try parse(parser));
196 }
197 try token.expectRight(parser);
198 return switch (tag) {
199 .and_ => try parser.ctx.and_(operands.items),
200 .or_ => try parser.ctx.or_(operands.items),
201 .distinct => try parser.ctx.distinct(operands.items),
202 .add => try parser.ctx.add(operands.items),
203 .mul => try parser.ctx.mul(operands.items),
204 else => unreachable,
205 };
206 }
207
208 fn parseApply(parser: *Parser, function: term.Function) Error!term.Term {
209 var operands: std.ArrayList(term.Term) = .empty;
210 defer operands.deinit(parser.ctx.allocator);
211 while (!token.peekRight(parser)) {
212 try operands.append(parser.ctx.allocator, try parse(parser));
213 }
214 try token.expectRight(parser);
215 return try parser.ctx.apply(function, operands.items);
216 }
217
218 fn parseInteger(text: []const u8) ?i128 {
219 if (text.len == 0) return null;
220 if (text[0] == '-' and text.len == 1) return null;
221 if (text[0] != '-' and (text[0] < '0' or text[0] > '9')) return null;
222 return std.fmt.parseInt(i128, text, 10) catch null;
223 }