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

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 //! The errors of the SMT-LIB reader. A caller that refuses a script needs to tell a malformed text
 2 //! from a well-formed script that uses something unsupported by the reader. The reader's functions
 3 //! 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 script
 6 /// was refused switches on these tags.
 7 pub 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 here
13     /// because `=` takes two operands.
14     ExpectedRightParen,
15     /// A sort is other than `Bool`, `Int`, `(_ BitVec n)` or an `Array` from one bit-vector sort to
16     /// 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 an
21     /// integer.
22     UnknownSymbol,
23     /// A `declare-const` or `declare-fun` names a constant or function the same script already
24     /// 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 indexed
30     /// form other than `(_ bvV W)`, `extract`, `zero_extend`, `sign_extend`, `rotate_left` and
31     /// `rotate_right`.
32     UnsupportedTerm,
33     /// A width, a bit index, a count or a bit-vector value is other than a decimal number that fits
34     /// its type.
35     InvalidNumber,
36 };
37 
38 /// The error set of the reader's functions: any error. Every function of the reader returns it, so
39 /// 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`, and
41 /// `error.OutOfMemory`. Because it is `anyerror`, the compiler cannot list the errors a call
42 /// returns.
43 pub const Error = anyerror;