machine-check-hw 0.7.1

System crate for machine-check for verification of BTOR2 files
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

use btor2rs::{
    id::{Nid, Sid},
    sort::{Bitvec, Sort},
};

use crate::translate::btor2::Error;

use super::NodeTranslator;

impl NodeTranslator<'_> {
    pub(super) fn get_sort(&self, sid: Sid) -> Result<&Sort, Error> {
        self.translator
            .btor2
            .sorts
            .get(&sid)
            .ok_or(Error::InvalidSort(sid))
    }

    pub(super) fn get_bitvec(&self, sid: Sid) -> Result<&Bitvec, Error> {
        let sort = self.get_sort(sid)?;
        let Sort::Bitvec(bitvec) = sort else {
            return Err(Error::ExpectBitvecSort(sid));
        };
        Ok(bitvec)
    }

    pub(super) fn get_nid_bitvec(&self, nid: Nid) -> Result<&Bitvec, Error> {
        let node = self
            .translator
            .btor2
            .nodes
            .get(&nid)
            .ok_or(Error::InvalidNode(nid))?;
        let sid = node.get_result_sid().ok_or(Error::UnknownNodeSort(nid))?;
        self.get_bitvec(sid)
    }
}