mck 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

use std::marker::PhantomData;

use serde::{Deserialize, Serialize};

use crate::{
    abstr::{combination::DomainCombination, three_valued::RThreeValuedBitvector},
    misc::RBound,
};

use super::three_valued::RMarkBitvector;

mod meta;
mod ops;
mod support;

// TODO: remove equality in favour of meta-equality
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub struct RCombinedMark<D: DomainCombination<RBound, Left = RThreeValuedBitvector>>(
    pub(super) RMarkBitvector,
    PhantomData<D>,
);