tiny.smt.smtlib.parse.script

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

1//! Reads the commands of an SMT-LIB script in order and collects its logic and assertions. Each2//! command either declares a name that later terms use or asserts a formula, so the commands are3//! read in order and each declaration is known before the terms after it. The reader accepts five4//! commands and refuses every other with `UnsupportedCommand`.5const std = @import("std");6const smt = @import("../../root.zig");78const errors = @import("error.zig");9const sort = @import("sort.zig");10const state = @import("state.zig");11const term_parser = @import("term.zig");12const token = @import("token.zig");1314const Error = errors.Error;15const ParseError = errors.ParseError;16const Parser = state.Parser;17const term = smt.term;1819/// Reads every command of the parser's text and returns a `Script` over the parser's `Context` with20/// the script's logic and assertions. `parseScript` calls it, and code that builds its own `Parser`21/// calls it to read a script with that state. `set-logic` sets the logic, which is `ALL` until one22/// does. `declare-const` adds a constant and `declare-fun` a function to the `Context`, and both23/// record the name for the terms that follow. `assert` reads a term and appends it to the24/// assertions, and `check-sat` is read and ignored. It returns `DuplicateSymbol` for a name25/// declared twice in the script, and `UnsupportedCommand` for any other command. It checks no26/// sorts: an `assert` of a non-Boolean term is accepted. The logic name and the recorded names27/// borrow the parser's text. On an error it frees the assertion list, and the terms already built28/// stay in the `Context`.29pub fn parse(parser: *Parser) Error!term.Script {30    var parsed = term.Script.init(parser.ctx, "ALL");31    errdefer parsed.deinit();32    while (token.skipSpace(parser)) {33        try token.expectLeft(parser);34        const command = try token.atom(parser);35        if (std.mem.eql(u8, command, "set-logic")) {36            parsed.logic = try token.atom(parser);37            try token.expectRight(parser);38        } else if (std.mem.eql(u8, command, "declare-const")) {39            const name = try token.atom(parser);40            if (parser.symbols.contains(name) or parser.functions.contains(name)) return ParseError.DuplicateSymbol;41            const symbol_sort = try sort.parse(parser);42            const symbol = try parser.ctx.symbol(name, symbol_sort);43            try parser.symbols.put(name, symbol);44            try token.expectRight(parser);45        } else if (std.mem.eql(u8, command, "declare-fun")) {46            const name = try token.atom(parser);47            if (parser.symbols.contains(name) or parser.functions.contains(name)) return ParseError.DuplicateSymbol;48            const params = try sort.list(parser);49            defer parser.ctx.allocator.free(params);50            const result = try sort.parse(parser);51            const function = try parser.ctx.function(name, params, result);52            try parser.functions.put(name, function);53            try token.expectRight(parser);54        } else if (std.mem.eql(u8, command, "assert")) {55            try parsed.assertTerm(try term_parser.parse(parser));56            try token.expectRight(parser);57        } else if (std.mem.eql(u8, command, "check-sat")) {58            try token.expectRight(parser);59        } else {60            return ParseError.UnsupportedCommand;61        }62    }63    return parsed;64}