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

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! Reads SMT-LIB text into terms, one command at a time. A caller needs one call that turns a whole
 2 //! script into terms and a list of assertions.
 3 //!
 4 //! The reader reads tokens with `token`, sorts with `sort`, terms with `term` and commands with
 5 //! `script`, all over one parser state (`Parser`) from `state`. It descends one call per
 6 //! parenthesis, with no depth bound.
 7 const smt = @import("../../root.zig");
 8 
 9 pub const errors = @import("error.zig");
10 pub const script = @import("script.zig");
11 pub const sort = @import("sort.zig");
12 pub const state = @import("state.zig");
13 pub const term = @import("term.zig");
14 pub const token = @import("token.zig");
15 
16 const smt_term = smt.term;
17 
18 pub const Error = errors.Error;
19 pub const ParseError = errors.ParseError;
20 pub const Parser = state.Parser;
21 
22 /// Reads the script `source`, adds its constants, functions and terms to `ctx`, and returns a
23 /// `Script` over `ctx` with the script's logic and assertions. The caller loads an SMT-LIB script
24 /// with it, then solves the assertions of the returned `Script`. The returned `Script` borrows its
25 /// logic name from `source`, so `source` has to outlive it. The caller owns the `Script` and frees
26 /// it with `Script.deinit` before freeing `ctx`. The logic is `ALL` when the script has no
27 /// `set-logic`. On an error the terms already built stay in `ctx`. Each call starts with no
28 /// declared names, so a second script read into the same `ctx` cannot refer to the constants of the
29 /// first. It returns the `ParseError` tags, the errors of the `Context` builders and
30 /// `error.OutOfMemory`, under the error set `Error`, which is `anyerror`.
31 pub 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 }