346 lines
11 KiB
Rust
346 lines
11 KiB
Rust
mod tests;
|
|
|
|
#[derive(Debug, Clone, Copy, PartialEq)]
|
|
pub enum Token {
|
|
Negation,
|
|
Conjunction,
|
|
Disjunction,
|
|
ExclusiveDisjunction,
|
|
MaterialCondition,
|
|
LogicalEquivalence,
|
|
}
|
|
|
|
#[derive(Debug, Clone, PartialEq)]
|
|
pub enum Node<T>
|
|
where
|
|
T: Clone + std::fmt::Debug,
|
|
{
|
|
Leaf(T),
|
|
Unary {
|
|
operator: Token,
|
|
operand: Box<Node<T>>,
|
|
},
|
|
Binary {
|
|
operator: Token,
|
|
lhs: Box<Node<T>>,
|
|
rhs: Box<Node<T>>,
|
|
},
|
|
}
|
|
|
|
impl<T> Node<T>
|
|
where
|
|
T: Clone + std::fmt::Debug,
|
|
{
|
|
fn negation_conjunction_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
|
|
Node::Binary {
|
|
operator: Token::Disjunction,
|
|
lhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*lhs.clone()),
|
|
}),
|
|
rhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*rhs.clone()),
|
|
}),
|
|
}
|
|
}
|
|
|
|
fn negation_disjunction_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
|
|
Node::Binary {
|
|
operator: Token::Conjunction,
|
|
lhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*lhs.clone()),
|
|
}),
|
|
rhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*rhs.clone()),
|
|
}),
|
|
}
|
|
}
|
|
|
|
fn negation_material_condition_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
|
|
Node::Binary {
|
|
operator: Token::Conjunction,
|
|
lhs: Box::new(*lhs.clone()),
|
|
rhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*rhs.clone()),
|
|
}),
|
|
}
|
|
}
|
|
|
|
fn material_condition_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
|
|
Node::Binary {
|
|
operator: Token::Disjunction,
|
|
lhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*lhs.clone()),
|
|
}),
|
|
rhs: Box::new(*rhs.clone()),
|
|
}
|
|
}
|
|
|
|
fn negation_exclusive_disjunction_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
|
|
Node::Binary {
|
|
operator: Token::Disjunction,
|
|
lhs: Box::new(Node::Binary {
|
|
operator: Token::Conjunction,
|
|
lhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*lhs.clone()),
|
|
}),
|
|
rhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*rhs.clone()),
|
|
}),
|
|
}),
|
|
rhs: Box::new(Node::Binary {
|
|
operator: Token::Conjunction,
|
|
lhs: Box::new(*lhs.clone()),
|
|
rhs: Box::new(*rhs.clone()),
|
|
}),
|
|
}
|
|
}
|
|
|
|
fn exclusive_disjunction_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
|
|
Node::Binary {
|
|
operator: Token::Conjunction,
|
|
lhs: Box::new(Node::Binary {
|
|
operator: Token::Disjunction,
|
|
lhs: Box::new(*lhs.clone()),
|
|
rhs: Box::new(*rhs.clone()),
|
|
}),
|
|
rhs: Box::new(Node::Binary {
|
|
operator: Token::Disjunction,
|
|
lhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*lhs.clone()),
|
|
}),
|
|
rhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*rhs.clone()),
|
|
}),
|
|
}),
|
|
}
|
|
}
|
|
|
|
fn logical_equivalence_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
|
|
Node::Binary {
|
|
operator: Token::Conjunction,
|
|
lhs: Box::new(Node::Binary {
|
|
operator: Token::Disjunction,
|
|
lhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*lhs.clone()),
|
|
}),
|
|
rhs: Box::new(*rhs.clone()),
|
|
}),
|
|
rhs: Box::new(Node::Binary {
|
|
operator: Token::Disjunction,
|
|
lhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*rhs.clone()),
|
|
}),
|
|
rhs: Box::new(*lhs.clone()),
|
|
}),
|
|
}
|
|
}
|
|
|
|
fn negation_logical_equivalence_to_nnf(lhs: &Box<Node<T>>, rhs: &Box<Node<T>>) -> Node<T> {
|
|
Node::Binary {
|
|
operator: Token::Disjunction,
|
|
lhs: Box::new(Node::Binary {
|
|
operator: Token::Conjunction,
|
|
lhs: Box::new(*lhs.clone()),
|
|
rhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*rhs.clone()),
|
|
}),
|
|
}),
|
|
rhs: Box::new(Node::Binary {
|
|
operator: Token::Conjunction,
|
|
lhs: Box::new(*rhs.clone()),
|
|
rhs: Box::new(Node::Unary {
|
|
operator: Token::Negation,
|
|
operand: Box::new(*lhs.clone()),
|
|
}),
|
|
}),
|
|
}
|
|
}
|
|
|
|
pub fn simplify(&mut self) {
|
|
match self {
|
|
Node::Unary { operator, operand } if *operator == Token::Negation => match &**operand {
|
|
Node::Unary {
|
|
operator: inner_op,
|
|
operand: inner_operand,
|
|
} if *inner_op == Token::Negation => {
|
|
*self = *inner_operand.clone();
|
|
self.simplify();
|
|
}
|
|
Node::Binary {
|
|
operator: inner_op,
|
|
lhs: inner_lhs,
|
|
rhs: inner_rhs,
|
|
} => {
|
|
*self = match *inner_op {
|
|
Token::Conjunction => {
|
|
Self::negation_conjunction_to_nnf(inner_lhs, inner_rhs)
|
|
}
|
|
Token::Disjunction => {
|
|
Self::negation_disjunction_to_nnf(inner_lhs, inner_rhs)
|
|
}
|
|
Token::ExclusiveDisjunction => {
|
|
Self::negation_exclusive_disjunction_to_nnf(inner_lhs, inner_rhs)
|
|
}
|
|
Token::LogicalEquivalence => {
|
|
Self::negation_logical_equivalence_to_nnf(inner_lhs, inner_rhs)
|
|
}
|
|
Token::MaterialCondition => {
|
|
Self::negation_material_condition_to_nnf(inner_lhs, inner_rhs)
|
|
}
|
|
_ => unreachable!(),
|
|
};
|
|
self.simplify();
|
|
}
|
|
_ => (),
|
|
},
|
|
Node::Binary {
|
|
operator, lhs, rhs, ..
|
|
} => {
|
|
if let Some(node) = match *operator {
|
|
Token::ExclusiveDisjunction => {
|
|
Some(Self::exclusive_disjunction_to_nnf(lhs, rhs))
|
|
}
|
|
Token::LogicalEquivalence => Some(Self::logical_equivalence_to_nnf(lhs, rhs)),
|
|
Token::MaterialCondition => Some(Self::material_condition_to_nnf(lhs, rhs)),
|
|
_ => None,
|
|
} {
|
|
*self = node.clone();
|
|
self.simplify();
|
|
} else {
|
|
lhs.simplify();
|
|
rhs.simplify();
|
|
}
|
|
}
|
|
_ => (),
|
|
}
|
|
}
|
|
}
|
|
|
|
impl Node<bool> {
|
|
pub fn parse_formula(formula: &str) -> Node<bool> {
|
|
let mut stack = vec![];
|
|
for c in formula.chars() {
|
|
match c {
|
|
'0' => stack.push(Node::Leaf(false)),
|
|
'1' => stack.push(Node::Leaf(true)),
|
|
'!' => add_unary_node(&mut stack, Token::Negation),
|
|
'&' => add_binary_node(&mut stack, Token::Conjunction),
|
|
'|' => add_binary_node(&mut stack, Token::Disjunction),
|
|
'^' => add_binary_node(&mut stack, Token::ExclusiveDisjunction),
|
|
'>' => add_binary_node(&mut stack, Token::MaterialCondition),
|
|
'=' => add_binary_node(&mut stack, Token::LogicalEquivalence),
|
|
_ => panic!("Error: {} is not a valid character", c),
|
|
}
|
|
}
|
|
stack.pop().unwrap()
|
|
}
|
|
|
|
pub fn ast_to_formula(ast: &Node<bool>) -> String {
|
|
let mut str = String::from("");
|
|
match ast {
|
|
Node::Unary { operator, operand } => {
|
|
str.push_str(Self::ast_to_formula(operand).as_str());
|
|
str.push(token_to_char(*operator));
|
|
}
|
|
Node::Binary { operator, lhs, rhs } => {
|
|
str.push_str(Self::ast_to_formula(lhs).as_str());
|
|
str.push_str(Self::ast_to_formula(rhs).as_str());
|
|
str.push(token_to_char(*operator));
|
|
}
|
|
Node::Leaf(b) => str.push(bool_to_char(*b)),
|
|
};
|
|
str
|
|
}
|
|
}
|
|
|
|
impl Node<char> {
|
|
pub fn parse_formula(formula: &str) -> Node<char> {
|
|
let mut stack = vec![];
|
|
for c in formula.chars() {
|
|
match c {
|
|
'A'..='Z' => stack.push(Node::Leaf(c)),
|
|
'!' => add_unary_node(&mut stack, Token::Negation),
|
|
'&' => add_binary_node(&mut stack, Token::Conjunction),
|
|
'|' => add_binary_node(&mut stack, Token::Disjunction),
|
|
'^' => add_binary_node(&mut stack, Token::ExclusiveDisjunction),
|
|
'>' => add_binary_node(&mut stack, Token::MaterialCondition),
|
|
'=' => add_binary_node(&mut stack, Token::LogicalEquivalence),
|
|
_ => panic!("Error: {} is not a valid character", c),
|
|
}
|
|
}
|
|
stack.pop().unwrap()
|
|
}
|
|
|
|
pub fn ast_to_formula(ast: &Node<char>) -> String {
|
|
let mut str = String::from("");
|
|
match ast {
|
|
Node::Unary { operator, operand } => {
|
|
str.push_str(Self::ast_to_formula(operand).as_str());
|
|
str.push(token_to_char(*operator));
|
|
}
|
|
Node::Binary { operator, lhs, rhs } => {
|
|
str.push_str(Self::ast_to_formula(lhs).as_str());
|
|
str.push_str(Self::ast_to_formula(rhs).as_str());
|
|
str.push(token_to_char(*operator));
|
|
}
|
|
Node::Leaf(c) => str.push(*c),
|
|
};
|
|
str
|
|
}
|
|
}
|
|
|
|
pub fn add_unary_node<T>(stack: &mut Vec<Node<T>>, token: Token)
|
|
where
|
|
T: Clone + std::fmt::Debug,
|
|
{
|
|
let operand = Box::new(stack.pop().unwrap());
|
|
stack.push(Node::Unary {
|
|
operator: token,
|
|
operand,
|
|
});
|
|
}
|
|
|
|
pub fn add_binary_node<T>(stack: &mut Vec<Node<T>>, token: Token)
|
|
where
|
|
T: Clone + std::fmt::Debug,
|
|
{
|
|
let rhs = Box::new(stack.pop().unwrap());
|
|
let lhs = Box::new(stack.pop().unwrap());
|
|
stack.push(Node::Binary {
|
|
operator: token,
|
|
lhs,
|
|
rhs,
|
|
});
|
|
}
|
|
|
|
fn bool_to_char(b: bool) -> char {
|
|
match b {
|
|
false => '0',
|
|
true => '1',
|
|
}
|
|
}
|
|
|
|
fn token_to_char(token: Token) -> char {
|
|
match token {
|
|
Token::Negation => '!',
|
|
Token::Conjunction => '&',
|
|
Token::Disjunction => '|',
|
|
Token::ExclusiveDisjunction => '^',
|
|
Token::MaterialCondition => '>',
|
|
Token::LogicalEquivalence => '=',
|
|
}
|
|
}
|