1 
use crate::ast::Expression;
2 
use polyquine::Quine;
3 
use serde::Deserialize;
4 
use serde::Serialize;
5 
use std::fmt;
6 
use uniplate::Uniplate;
7 

            

        

            

                8
            

            

                
            

            

                
#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate, Quine)]

            

        

            

                9
            

            

                
            

            

                
pub struct CnfClause {

            

        

            

                10
            

            

                
            

            

                
    // This represents a cnf clause in its simplest form, it should only contain literals

            

        

            

                11
            

            

                
            

            

                
    literals: Vec<Expression>,

            

        

            

                12
            

            

                
            

            

                
}

            

        

            

                13
            

            

                
            

            

                

            

        

            

                14
            

            

                
            

            

                
impl CnfClause {

            

        

            

                15
            

            

                
            

            

                
    pub fn new(literals: Vec<Expression>) -> Self {

            

        

            

                16
            

            

                
            

            

                
        CnfClause { literals }

            

        

            

                17
            

            

                
            

            

                
    }

            

        

            

                18
            

            

                
            

            

                

            

        

            

                19
            

            

                
            

            

                
    // Expose an iterator for the vector

            

        

            

                20
            

            

                
            

            

                
    pub fn iter(&self) -> impl Iterator<Item = &Expression> {

            

        

            

                21
            

            

                
            

            

                
        self.literals.iter()

            

        

            

                22
            

            

                
            

            

                
    }

            

        

            

                23
            

            

                
            

            

                

            

        

            

                24
            

            

                
            

            

                
    pub fn literals(&self) -> &Vec<Expression> {

            

        

            

                25
            

            

                
            

            

                
        &self.literals

            

        

            

                26
            

            

                
            

            

                
    }

            

        

            

                27
            

            

                
            

            

                
}

            

        

            

                28
            

            

                
            

            

                

            

        

            

                29
            

            

                
            

            

                
impl fmt::Display for CnfClause {

            

        

            

                30
            

            

                
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

            

        

            

                31
            

            

                
            

            

                
        // Print the contents of the valid_variants vector

            

        

            

                32
            

            

                
            

            

                
        write!(f, "(")?;

            

        

            

                33
            

            

                
            

            

                
        for (i, lit) in self.literals.iter().enumerate() {

            

        

            

                34
            

            

                
            

            

                
            if i > 0 {

            

        

            

                35
            

            

                
            

            

                
                write!(f, " \\/ ")?; // Add a comma between elements

            

        

            

                36
            

            

                
            

            

                
            }

            

        

            

                37
            

            

                
            

            

                
            match lit {

            

        

            

                38
            

            

                
            

            

                
                Expression::Not(_, var) => write!(f, "¬{}", var.as_ref())?,

            

        

            

                39
            

            

                
            

            

                
                Expression::Atomic(_, _) => write!(f, "{lit}")?,

            

        

            

                40
            

            

                
            

            

                
                _ => panic!("This expression type should not appear in a CnfClause"),

            

        

            

                41
            

            

                
            

            

                
            }

            

        

            

                42
            

            

                
            

            

                
        }

            

        

            

                43
            

            

                
            

            

                
        write!(f, ")") // Close the vector representation

            

        

            

                44
            

            

                
            

            

                
    }

            

        

            

                45
            

            

                
            

            

                
}