tiny.smt.smtlib.parse.term

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

1//! Reads one SMT-LIB term and builds it in a `Context`. A script's formulas use the operators of2//! different theories, so the reader has to map each operator name to the term it builds. A table3//! maps each supported SMT-LIB operator name to its term kind. Every two-operand operator takes4//! 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 per6//! parenthesis, with no depth bound.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;18const ExprTag = std.meta.Tag(term.Expr);1920const Operation = union(enum) {21    unary: ExprTag,22    binary: ExprTag,23    ternary: ExprTag,24    nary: ExprTag,25};2627const OperationEntry = struct {28    name: []const u8,29    operation: Operation,30};3132const 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};7374/// Reads one term at the parser's position, builds it in the parser's `Context` and returns it. The75/// 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 a77/// 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 its79/// operands, or a declared function applied to its arguments. It returns `UnknownSymbol` for an80/// undeclared name, `UnsupportedTerm` for an unsupported operator, `InvalidNumber` for a malformed81/// number, and the errors of the `Context` builders, such as `FunctionArityMismatch`. It checks no82/// sorts except the arguments of a function application.83pub 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}109110fn 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}118119fn 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}162163fn 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}172173fn 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}179180fn 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}190191fn 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}207208fn 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}217218fn 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}