smt_scope/
error.rs

1use core::fmt;
2use std::{collections::TryReserveError, num};
3
4use ::num::bigint;
5use lasso::LassoError;
6#[cfg(feature = "mem_dbg")]
7use mem_dbg::{MemDbg, MemSize};
8use nonmax::ParseIntError;
9
10use crate::items::{Blame, ENodeIdx, Fingerprint, QuantIdx, TermId, TermIdx};
11
12pub type Result<T> = std::result::Result<T, Error>;
13pub type FResult<T> = std::result::Result<T, FatalError>;
14
15#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
16#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
17#[derive(Debug, Clone, Copy, PartialEq, Eq)]
18pub enum Either<T, U> {
19    Left(T),
20    Right(U),
21}
22impl<T, U> Either<T, U> {
23    pub fn into_result(self) -> std::result::Result<T, U> {
24        match self {
25            Self::Left(t) => Ok(t),
26            Self::Right(u) => Err(u),
27        }
28    }
29}
30
31#[derive(Debug)]
32pub enum Error {
33    UnknownLine(String),
34    UnexpectedNewline,
35    ExpectedNewline(String),
36    UnexpectedEnd,
37
38    // Version
39    InvalidVersion(semver::Error),
40
41    // Id parsing
42    InvalidIdNumber(ParseIntError),
43    InvalidIdHash(String),
44    UnknownId(TermId),
45
46    // Var parsing
47    InvalidVar(ParseIntError),
48
49    // Meaning parsing
50    ParseBigUintError(bigint::ParseBigIntError),
51    ParseError(String),
52
53    // Quantifier
54    VarNamesListInconsistent, // attach var names
55    VarNamesNoBar,
56    InvalidVarNum(ParseIntError),
57    UnknownQuantifierIdx(TermIdx),
58    NonNullLambdaName(String),
59    InvalidQVarInteger(ParseIntError),
60    NewMatchOnLambda(QuantIdx),
61    UnknownPatternIdx(TermIdx),
62    SubpatTooFewBlame(usize),
63    // Z3 ISSUE: https://github.com/viperproject/smt-scope/issues/63
64    SubpatNoBlame(Vec<TermIdx>),
65
66    // Inst discovered
67    /// theory-solving non-rewrite axiom should blame valid enodes
68    NonRewriteAxiomInvalidEnode(TermIdx),
69    /// theory-solving rewrite axiom should only have one term
70    RewriteAxiomMultipleTerms1(TermIdx),
71    RewriteAxiomMultipleTerms2(Vec<Blame>),
72    UnknownInstMethod(String),
73
74    // Instance
75    UnmatchedEndOfInstance,
76
77    TupleMissingParens,
78    UnequalTupleForms(u8, u8),
79
80    // Fingerprint
81    InvalidFingerprint(num::ParseIntError),
82    UnknownFingerprint(Fingerprint),
83
84    // Enode
85    UnknownEnode(TermIdx),
86    InvalidGeneration(ParseIntError),
87    EnodeRootMismatch(ENodeIdx, ENodeIdx),
88
89    // Equality
90    UnknownEqLit,
91
92    // Stack
93    StackFrameNotPushed,
94    PopConflictMismatch,
95    InvalidFrameInteger(num::ParseIntError),
96
97    // CDCL
98    NoConflict,
99    BoolLiteral,
100    BoolLiteralNotP,
101    InvalidBoolLiteral(num::ParseIntError),
102    UnknownJustification(String),
103    MissingColonJustification,
104    InvalidTheoryId(num::ParseIntError),
105
106    Allocation(TryReserveError),
107    Lasso(LassoError),
108
109    /// Unused, kept for debugging to see error line instead of simply panicking
110    /// at `debug_assert`.
111    Debug,
112}
113
114impl From<semver::Error> for Error {
115    fn from(err: semver::Error) -> Self {
116        Self::InvalidVersion(err)
117    }
118}
119
120impl From<TryReserveError> for Error {
121    fn from(err: TryReserveError) -> Self {
122        Self::Allocation(err)
123    }
124}
125
126impl From<LassoError> for Error {
127    fn from(value: LassoError) -> Self {
128        Self::Lasso(value)
129    }
130}
131
132impl Error {
133    pub fn is_oom(&self) -> bool {
134        matches!(self, Self::Allocation(_) | Self::Lasso(_))
135    }
136
137    pub fn as_fatal(self) -> Option<FatalError> {
138        match self {
139            Self::Allocation(alloc) => Some(FatalError::Allocation(alloc)),
140            Self::Lasso(lasso) => Some(FatalError::Lasso(lasso)),
141            _ => None,
142        }
143    }
144}
145
146#[derive(Debug, Clone)]
147pub enum FatalError {
148    Allocation(TryReserveError),
149    Lasso(LassoError),
150    Io(std::rc::Rc<std::io::Error>),
151}
152
153impl From<std::io::Error> for FatalError {
154    fn from(err: std::io::Error) -> Self {
155        Self::Io(std::rc::Rc::new(err))
156    }
157}
158
159impl fmt::Display for FatalError {
160    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
161        match self {
162            Self::Allocation(alloc) => write!(f, "Allocation error: {alloc}"),
163            Self::Lasso(lasso) => write!(f, "String interning error: {lasso}"),
164            Self::Io(err) => write!(f, "IO error: {err}"),
165        }
166    }
167}
smt_scope/error.rs

smt_scope/
error.rs
