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

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! Reads the commands of an SMT-LIB script in order and collects its logic and assertions. Each
 2 //! command either declares a name that later terms use or asserts a formula, so the commands are
 3 //! read in order and each declaration is known before the terms after it. The reader accepts five
 4 //! commands and refuses every other with `UnsupportedCommand`.
 5 const std = @import("std");
 6 const smt = @import("../../root.zig");
 7 
 8 const errors = @import("error.zig");
 9 const sort = @import("sort.zig");
10 const state = @import("state.zig");
11 const term_parser = @import("term.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 every command of the parser's text and returns a `Script` over the parser's `Context` with
20 /// 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 one
22 /// does. `declare-const` adds a constant and `declare-fun` a function to the `Context`, and both
23 /// record the name for the terms that follow. `assert` reads a term and appends it to the
24 /// assertions, and `check-sat` is read and ignored. It returns `DuplicateSymbol` for a name
25 /// declared twice in the script, and `UnsupportedCommand` for any other command. It checks no
26 /// sorts: an `assert` of a non-Boolean term is accepted. The logic name and the recorded names
27 /// borrow the parser's text. On an error it frees the assertion list, and the terms already built
28 /// stay in the `Context`.
29 pub 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 }