tiny.smt.smtlib.parse

1//! Reads SMT-LIB text into terms, one command at a time. A caller needs one call that turns a whole2//! script into terms and a list of assertions.3//!4//! The reader reads tokens with `token`, sorts with `sort`, terms with `term` and commands with5//! `script`, all over one parser state (`Parser`) from `state`. It descends one call per6//! parenthesis, with no depth bound.7const smt = @import("../../root.zig");89pub const errors = @import("error.zig");10pub const script = @import("script.zig");11pub const sort = @import("sort.zig");12pub const state = @import("state.zig");13pub const term = @import("term.zig");14pub const token = @import("token.zig");1516const smt_term = smt.term;1718pub const Error = errors.Error;19pub const ParseError = errors.ParseError;20pub const Parser = state.Parser;2122/// Reads the script `source`, adds its constants, functions and terms to `ctx`, and returns a23/// `Script` over `ctx` with the script's logic and assertions. The caller loads an SMT-LIB script24/// with it, then solves the assertions of the returned `Script`. The returned `Script` borrows its25/// logic name from `source`, so `source` has to outlive it. The caller owns the `Script` and frees26/// it with `Script.deinit` before freeing `ctx`. The logic is `ALL` when the script has no27/// `set-logic`. On an error the terms already built stay in `ctx`. Each call starts with no28/// declared names, so a second script read into the same `ctx` cannot refer to the constants of the29/// first. It returns the `ParseError` tags, the errors of the `Context` builders and30/// `error.OutOfMemory`, under the error set `Error`, which is `anyerror`.31pub fn parseScript(ctx: *smt_term.Context, source: []const u8) Error!smt_term.Script {32    var parser = Parser.init(ctx, source);33    defer parser.deinit();34    return try script.parse(&parser);35}

1pub const parse = @import("parse/root.zig");