boolean_circuit/
literal.rs

1use std::rc::Rc;
2
3use itertools::Itertools;
4
5/// A positive or negated variable identified by its name.
6///
7/// Cloning is efficient because the name is shared.
8#[derive(Clone, Debug, Hash, PartialEq, Eq)]
9pub enum Literal {
10    Pos(Rc<String>),
11    Neg(Rc<String>),
12}
13
14impl Literal {
15    /// Returns the name of the variable.
16    pub fn var(&self) -> &str {
17        match self {
18            Literal::Pos(name) | Literal::Neg(name) => name.as_str(),
19        }
20    }
21
22    /// Returns true if the literal is negated, false otherwise.
23    pub fn is_negated(&self) -> bool {
24        match self {
25            Literal::Pos(_) => false,
26            Literal::Neg(_) => true,
27        }
28    }
29}
30
31/// Formats a clause in human-readable form.
32pub fn clause_to_string(clause: &[Literal]) -> String {
33    clause.iter().format(" v ").to_string()
34}
35
36impl From<&str> for Literal {
37    fn from(name: &str) -> Literal {
38        Literal::Pos(Rc::new(name.to_string()))
39    }
40}
41
42impl std::ops::Not for &Literal {
43    type Output = Literal;
44
45    fn not(self) -> Literal {
46        !self.clone()
47    }
48}
49
50impl std::ops::Not for Literal {
51    type Output = Literal;
52
53    fn not(self) -> Literal {
54        match self {
55            Literal::Pos(name) => Literal::Neg(name),
56            Literal::Neg(name) => Literal::Pos(name),
57        }
58    }
59}
60
61impl std::fmt::Display for Literal {
62    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
63        match self {
64            Literal::Pos(name) => write!(f, "{name}"),
65            Literal::Neg(name) => write!(f, "-{name}"),
66        }
67    }
68}