btor2rs 0.1.0

Safe-Rust Btor2 parser
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

use thiserror::Error;

use crate::{Btor2, Nid, Node, Sid, Sort};

impl Btor2 {
    pub(crate) fn parse_line(&mut self, line: &str) -> Result<(), LineError> {
        if line.starts_with(';') {
            // comment
            return Ok(());
        }

        let mut split = line.split_whitespace();
        let Some(id) = split.next() else {
            // empty line
            return Ok(());
        };

        let second = split.next().ok_or(LineError::MissingSecondSymbol)?;

        if second == "sort" {
            let sort = Sort::parse(split)?;
            let sid = Sid::try_from_str(id)?;
            if self.sorts.insert(sid, sort).is_some() {
                return Err(LineError::DuplicateSid(sid));
            }
            return Ok(());
        }
        if let Some(node) = Node::try_parse(second, split)? {
            let nid = Nid::try_from_str(id)?;
            if self.nodes.insert(nid, node).is_some() {
                return Err(LineError::DuplicateNid(nid));
            }
            return Ok(());
        }

        Err(LineError::InvalidLine)
    }
}

#[derive(Error, Debug, Clone)]
pub(crate) enum LineError {
    // missing
    #[error("Missing second symbol")]
    MissingSecondSymbol,
    #[error("Missing constant")]
    MissingConstant,
    #[error("Missing number")]
    MissingNumber,
    #[error("Missing sort id")]
    MissingSid,
    #[error("Missing node id")]
    MissingNid,
    #[error("Missing right-side node id")]
    MissingRnid,
    #[error("Missing sort type")]
    MissingSortType,
    #[error("Missing bitvec length")]
    MissingBitvecLength,

    // invalid
    #[error("Invalid line")]
    InvalidLine,
    #[error("Invalid number {0:?}")]
    InvalidNumber(String),
    #[error("Invalid sort id {0:?}")]
    InvalidSid(String),
    #[error("Invalid node id {0:?}")]
    InvalidNid(String),
    #[error("Invalid right-side node id {0:?}")]
    InvalidRnid(String),
    #[error("Invalid slice with upper bit lower than lower bit")]
    InvalidSlice,
    #[error("Invalid sort type")]
    InvalidSortType,
    #[error("Invalid bitvec length")]
    InvalidBitvecLength,

    // duplicate
    #[error("Duplicate sort id {0}")]
    DuplicateSid(Sid),
    #[error("Duplicate node id {0}")]
    DuplicateNid(Nid),
}