tiny.smt.smtlib.parse.errors

1//! The errors of the SMT-LIB reader. A caller that refuses a script needs to tell a malformed text2//! from a well-formed script that uses something unsupported by the reader. The reader's functions3//! return `Error`, which is `anyerror`, so the `Context` builders' errors and `error.OutOfMemory`4//! pass through beside the tags of `ParseError`.5/// The errors the reader returns for unreadable or unsupported text. Code that reports why a script6/// was refused switches on these tags.7pub const ParseError = error{8    /// An atom was due, and the text ended or a parenthesis came.9    ExpectedAtom,10    /// An opening parenthesis was due.11    ExpectedList,12    /// A closing parenthesis was due, as after an operator's last operand: `(= a b c)` fails here13    /// because `=` takes two operands.14    ExpectedRightParen,15    /// A sort is other than `Bool`, `Int`, `(_ BitVec n)` or an `Array` from one bit-vector sort to16    /// another.17    ExpectedSort,18    /// No function of the reader returns it.19    ExpectedCommand,20    /// An atom names an undeclared constant or function and is other than `true`, `false` or an21    /// integer.22    UnknownSymbol,23    /// A `declare-const` or `declare-fun` names a constant or function the same script already24    /// declared.25    DuplicateSymbol,26    /// A command other than `set-logic`, `declare-const`, `declare-fun`, `assert` and `check-sat`,27    /// such as `set-option` or `get-model`.28    UnsupportedCommand,29    /// A term whose operator is unsupported by the reader, such as `let` or `ite`, or an indexed30    /// form other than `(_ bvV W)`, `extract`, `zero_extend`, `sign_extend`, `rotate_left` and31    /// `rotate_right`.32    UnsupportedTerm,33    /// A width, a bit index, a count or a bit-vector value is other than a decimal number that fits34    /// its type.35    InvalidNumber,36};3738/// The error set of the reader's functions: any error. Every function of the reader returns it, so39/// a caller's own error set has to absorb it. It covers `ParseError`, the errors of the `Context`40/// builders, such as `DuplicateFunction` and `FunctionArgumentSortMismatch`, and41/// `error.OutOfMemory`. Because it is `anyerror`, the compiler cannot list the errors a call42/// returns.43pub const Error = anyerror;

1pub const errors = @import("error.zig");