Skip to documentation
SLOP

tiny.smt.Script

Reference tiny.smt Script

Defined in term.

A logic name and the list of terms asserted over one Context.

API (6)

Actions

Public operations.

Fields and members

Public fields and members.

No direct callersNo direct callstermScript
Static calls · unresolved targets: unknown · external targets: unknown.

Source

Source: lib/smt/src/term.zig:1013

zig
/// A logic name and the list of terms asserted over one `Context`. `smtlib.parseScript` returns/// one, `smtlib.writeScript` prints one, and code that solves a script asserts each of its terms/// with the encoder. It borrows the `Context` and allocates its list with the `Context`'s/// allocator.pub const Script = struct {    /// The `Context` whose terms the script asserts.    ctx: *Context,    /// The logic name, such as `QF_BV`, that `set-logic` gives. The script borrows it: a script    /// from `smtlib.parseScript` points into the parsed text, which has to outlive the script.    logic: []const u8,    /// The asserted terms in the order they were asserted.    assertions: std.ArrayList(Term) = .empty,    /// Returns a script over `ctx` with logic `logic` and no assertions. Code makes an empty script    /// before asserting terms, as the SMT-LIB writer's tests do. It copies neither and allocates    /// nothing.    pub fn init(ctx: *Context, logic: []const u8) Script {        return .{ .ctx = ctx, .logic = logic };    }    /// Frees the list of assertions and leaves the terms to the `Context`. The owner calls it    /// before freeing the `Context`.    pub fn deinit(self: *Script) void {        self.assertions.deinit(self.ctx.allocator);        self.* = undefined;    }    /// Appends `assertion` to the list. Code adds one assertion to a script with it. It checks    /// nothing, including whether the term is Boolean.    pub fn assertTerm(self: *Script, assertion: Term) !void {        try self.assertions.append(self.ctx.allocator, assertion);    }};

Source: lib/smt/src/root.zig:120

zig
pub const Script = term.Script;
Called byCallsNo direct callssmtlib.parse.scriptparsetest sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...+8 moreScriptassertTerm
Static calls · unresolved targets: 1 · external targets: 0.
Called byCallsNo direct callssmtlib.parse.scriptparsetest sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...+8 moreScriptdeinit
Static calls · unresolved targets: 0 · external targets: 1.
Called byCallsNo direct callssmtlib.parse.scriptparsetest sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...test sourcelib.smt.src.smtlib.testtest: SMT-LIB parser rereads bit-vect...+8 moreScriptinit
Static calls · unresolved targets: 0 · external targets: 0.

Complete caller list for Script.assertTerm

13 direct callers.

Complete caller list for Script.deinit

13 direct callers.

Complete caller list for Script.init

13 direct callers.

Audit

Definitions4
Public names8
Members3
Version26.7.0
Revisiondaab053ee433