rust_formal_verification/formulas/
literal.rs

1// ************************************************************************************************
2// use
3// ************************************************************************************************
4
5use std::{fmt, ops::Not};
6
7// ************************************************************************************************
8// type alias
9// ************************************************************************************************
10
11/// This is the type that the literal
12pub type VariableType = u32;
13
14// ************************************************************************************************
15// struct
16// ************************************************************************************************
17
18#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Copy)]
19pub struct Literal {
20    literal_number: VariableType,
21}
22
23// ************************************************************************************************
24// impl
25// ************************************************************************************************
26
27impl Literal {
28    pub fn new(number: VariableType) -> Self {
29        debug_assert!(number > 0, "Literal number may not be zero.");
30        debug_assert!(
31            number <= (VariableType::MAX >> 1),
32            "Literal number is too big."
33        );
34        Self {
35            literal_number: (number << 1),
36        }
37    }
38
39    pub fn negate_if_true(&self, is_negated: bool) -> Self {
40        if is_negated {
41            !self.to_owned()
42        } else {
43            self.to_owned()
44        }
45    }
46
47    pub fn get_number(&self) -> VariableType {
48        self.literal_number >> 1
49    }
50
51    pub fn is_negated(&self) -> bool {
52        (self.literal_number % 2) == 1
53    }
54}
55
56// ************************************************************************************************
57// negation
58// ************************************************************************************************
59
60impl Not for Literal {
61    type Output = Self;
62
63    fn not(self) -> Self::Output {
64        Self::Output {
65            literal_number: self.literal_number ^ 1,
66        }
67    }
68}
69
70// ************************************************************************************************
71// printing
72// ************************************************************************************************
73
74impl fmt::Display for Literal {
75    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
76        if self.is_negated() {
77            write!(f, "-{}", self.get_number())
78        } else {
79            write!(f, "{}", self.get_number())
80        }
81    }
82}
rust_formal_verification/formulas/literal.rs

rust_formal_verification/formulas/
literal.rs
