lib/smt/src/smtlib/root.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! Reads SMT-LIB scripts into terms and writes terms back as SMT-LIB text. A caller needs to load a
 2 //! formula another tool wrote, and to hand a formula it built to another solver. The caller also
 3 //! 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 a
 6 //! sequence of parenthesized commands that set a logic, declare constants and functions, assert
 7 //! formulas and ask for satisfiability. The reader and the writer use its syntax and its operator
 8 //! names.
 9 //!
10 //! The reader accepts five commands, `set-logic`, `declare-const`, `declare-fun`, `assert`, and
11 //! `check-sat`, and the sorts `Bool`, `Int`, `(_ BitVec n)`, and arrays from bit-vectors to
12 //! 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 reads
14 //! back as the same formula, except for `distinct` with one operand, `+` and `*` with none, and
15 //! constants that share a name. The writer prints a negative integer as `-5`, which this reader
16 //! accepts and standard SMT-LIB readers refuse, since SMT-LIB writes it `(- 5)`. The reader lives
17 //! in `parse` and the writer in `write`, and `parseScript`, `writeScript`, `writeTerm`, `Error`,
18 //! and `ParseError` are re-exported here.
19 pub const parse = @import("parse/root.zig");
20 pub const write = @import("write.zig");
21 
22 pub const Error = parse.Error;
23 pub const ParseError = parse.ParseError;
24 pub const parseScript = parse.parseScript;
25 pub const writeScript = write.writeScript;
26 pub const writeTerm = write.writeTerm;