rust_formal_verification/formulas/
clause.rs

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

rust_formal_verification/formulas/
clause.rs
