rust_formal_verification/formulas/
cube.rs

1// ************************************************************************************************
2// use
3// ************************************************************************************************
4
5use super::{Clause, CNF};
6use crate::formulas::Literal;
7use std::fmt;
8use std::hash::Hash;
9use std::ops::Not;
10
11// ************************************************************************************************
12// struct
13// ************************************************************************************************
14
15#[derive(Eq, PartialEq, Clone, Hash, PartialOrd, Ord)]
16pub struct Cube {
17    literals: Vec<Literal>,
18}
19
20// ************************************************************************************************
21// impl
22// ************************************************************************************************
23
24impl Cube {
25    pub fn new(literals: &[Literal]) -> Self {
26        let mut sorted = literals.to_owned();
27        sorted.sort();
28        Self { literals: sorted }
29    }
30
31    pub fn len(&self) -> usize {
32        self.literals.len()
33    }
34
35    pub fn is_empty(&self) -> bool {
36        self.literals.is_empty()
37    }
38
39    pub fn iter(&self) -> impl Iterator<Item = &Literal> {
40        self.literals.iter()
41    }
42
43    pub fn to_cnf(&self) -> CNF {
44        let mut cnf = CNF::new();
45        for lit in self.literals.iter() {
46            cnf.add_clause(&Clause::new(&[lit.to_owned()]));
47        }
48        cnf
49    }
50}
51
52// ************************************************************************************************
53// negation
54// ************************************************************************************************
55
56impl Not for Cube {
57    type Output = Clause;
58
59    fn not(self) -> Self::Output {
60        let mut literals = Vec::new();
61        for lit in self.iter() {
62            literals.push(!lit.to_owned());
63        }
64        Clause::new(&literals)
65    }
66}
67
68// ************************************************************************************************
69// printing
70// ************************************************************************************************
71
72impl fmt::Display for Cube {
73    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
74        let cnf = self.to_cnf();
75        write!(f, "{}", cnf)
76    }
77}
rust_formal_verification/formulas/cube.rs

rust_formal_verification/formulas/
cube.rs
