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

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! The state one reading of an SMT-LIB text carries from call to call. A term can name any constant
 2 //! or function declared earlier in the script, so the reader keeps the declared names while it
 3 //! reads. The state (`Parser`) holds the text, the position in it, and two hash maps from declared
 4 //! names to constants and to functions.
 5 const std = @import("std");
 6 const smt = @import("../../root.zig");
 7 
 8 const term = smt.term;
 9 
10 /// The state of one reading: the `Context` the terms go into, the text, the position in it, and the
11 /// constants and functions declared so far. Code that reads a script with the reader's parts builds
12 /// one, as `parseScript` does. It borrows the `Context` and the text, and its hash maps allocate
13 /// with the `Context`'s allocator. The hash-map keys are slices of the text, so the text has to
14 /// outlive the state.
15 pub const Parser = struct {
16     ctx: *term.Context,
17     source: []const u8,
18     pos: usize = 0,
19     symbols: std.StringHashMap(term.Term),
20     functions: std.StringHashMap(term.Function),
21 
22     /// Returns a state over `ctx` and `source` at position 0 with no declared names. Code calls it
23     /// once before reading. It allocates nothing.
24     pub fn init(ctx: *term.Context, source: []const u8) Parser {
25         return .{
26             .ctx = ctx,
27             .source = source,
28             .symbols = std.StringHashMap(term.Term).init(ctx.allocator),
29             .functions = std.StringHashMap(term.Function).init(ctx.allocator),
30         };
31     }
32 
33     /// Frees the two hash maps. Code calls it once when done reading. The terms and the `Script`
34     /// the reading built stay valid.
35     pub fn deinit(self: *Parser) void {
36         self.functions.deinit();
37         self.symbols.deinit();
38     }
39 };