tiny.smt.smtlib

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

1//! Reads SMT-LIB scripts into terms and writes terms back as SMT-LIB text. A caller needs to load a2//! formula another tool wrote, and to hand a formula it built to another solver. The caller also3//! needs a script it wrote to read back as the same formula.4//!5//! [SMT-LIB](https://smt-lib.org/) is the standard text language of SMT solvers: a script is a6//! sequence of parenthesized commands that set a logic, declare constants and functions, assert7//! formulas and ask for satisfiability. The reader and the writer use its syntax and its operator8//! names.9//!10//! The reader accepts five commands, `set-logic`, `declare-const`, `declare-fun`, `assert`, and11//! `check-sat`, and the sorts `Bool`, `Int`, `(_ BitVec n)`, and arrays from bit-vectors to12//! bit-vectors. The reader refuses forms that common SMT-LIB benchmarks use: `let`, `ite`, `xor`,13//! `-`, `bvneg`, the `#b` and `#x` literals, and quoted symbols. A script the writer prints reads14//! back as the same formula, except for `distinct` with one operand, `+` and `*` with none, and15//! constants that share a name. The writer prints a negative integer as `-5`, which this reader16//! accepts and standard SMT-LIB readers refuse, since SMT-LIB writes it `(- 5)`. The reader lives17//! in `parse` and the writer in `write`, and `parseScript`, `writeScript`, `writeTerm`, `Error`,18//! and `ParseError` are re-exported here.19pub const parse = @import("parse/root.zig");20pub const write = @import("write.zig");2122pub const Error = parse.Error;23pub const ParseError = parse.ParseError;24pub const parseScript = parse.parseScript;25pub const writeScript = write.writeScript;26pub const writeTerm = write.writeTerm;