tiny.smt.smtlib.parse.state

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

1//! The state one reading of an SMT-LIB text carries from call to call. A term can name any constant2//! or function declared earlier in the script, so the reader keeps the declared names while it3//! reads. The state (`Parser`) holds the text, the position in it, and two hash maps from declared4//! names to constants and to functions.5const std = @import("std");6const smt = @import("../../root.zig");78const term = smt.term;910/// The state of one reading: the `Context` the terms go into, the text, the position in it, and the11/// constants and functions declared so far. Code that reads a script with the reader's parts builds12/// one, as `parseScript` does. It borrows the `Context` and the text, and its hash maps allocate13/// with the `Context`'s allocator. The hash-map keys are slices of the text, so the text has to14/// outlive the state.15pub 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),2122    /// Returns a state over `ctx` and `source` at position 0 with no declared names. Code calls it23    /// 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    }3233    /// 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};