fix: add XOR removal

leogaudin · Aug 31, 2024 · 1411e33 · 1411e33
1 parent 360351e
commit 1411e33
Show file tree

Hide file tree

Showing 2 changed files with 40 additions and 4 deletions.
diff --git a/src/ex05.rs b/src/ex05.rs
@@ -6,7 +6,7 @@
 
 use crate::tree::{create_tree, tree_to_rpn, NodeValue, TreeNode, TreeNodeRef};
 
-pub fn remove_double_negation(node: TreeNodeRef) -> TreeNodeRef {
+fn remove_double_negation(node: TreeNodeRef) -> TreeNodeRef {
     let node = node.borrow();
     match node.get_val() {
         Some(NodeValue::Operator('!')) => {
@@ -31,7 +31,7 @@ pub fn remove_double_negation(node: TreeNodeRef) -> TreeNodeRef {
 	}
 }
 
-pub fn remove_equivalence(node: TreeNodeRef) -> TreeNodeRef {
+fn remove_equivalence(node: TreeNodeRef) -> TreeNodeRef {
 	let node = node.borrow();
 	match node.get_val() {
 		Some(NodeValue::Operator('=')) => {
@@ -70,7 +70,7 @@ pub fn remove_equivalence(node: TreeNodeRef) -> TreeNodeRef {
 	}
 }
 
-pub fn remove_de_morgan(node: TreeNodeRef) -> TreeNodeRef {
+fn remove_de_morgan(node: TreeNodeRef) -> TreeNodeRef {
 	let node = node.borrow();
 	match node.get_val() {
 		Some(NodeValue::Operator('!')) => {
@@ -121,7 +121,7 @@ pub fn remove_de_morgan(node: TreeNodeRef) -> TreeNodeRef {
 	}
 }
 
-pub fn remove_material_condition(node: TreeNodeRef) -> TreeNodeRef {
+fn remove_material_condition(node: TreeNodeRef) -> TreeNodeRef {
 	let node = node.borrow();
 	match node.get_val() {
 		Some(NodeValue::Operator('>')) => {
@@ -150,7 +150,39 @@ pub fn remove_material_condition(node: TreeNodeRef) -> TreeNodeRef {
 	}
 }
 
+fn remove_xor(node: TreeNodeRef) -> TreeNodeRef {
+	let node = node.borrow();
+	match node.get_val() {
+		Some(NodeValue::Operator('^')) => {
+			let left: TreeNodeRef = remove_xor(node.get_left().unwrap());
+			let right: TreeNodeRef = remove_xor(node.get_right().unwrap());
+			let equal: TreeNodeRef = TreeNode::new_with_children(
+				NodeValue::Operator('='),
+				left,
+				right
+			);
+			let new_node: TreeNodeRef = TreeNode::new_from(
+				NodeValue::Operator('!')
+			);
+			new_node.borrow_mut().set_left(equal);
+			return new_node;
+		}
+		Some(NodeValue::Value(_)) | Some(NodeValue::Variable(_)) => return node.clone(),
+		_ => {
+			let new_node: TreeNodeRef = TreeNode::new_from(node.get_val().unwrap());
+			if let Some(left) = node.get_left() {
+				new_node.borrow_mut().set_left(remove_xor(left));
+			}
+			if let Some(right) = node.get_right() {
+				new_node.borrow_mut().set_right(remove_xor(right));
+			}
+			return new_node;
+		}
+	}
+}
+
 pub fn tree_to_nnf(tree: TreeNodeRef) -> TreeNodeRef {
+	let tree: TreeNodeRef = remove_xor(tree);
 	let tree: TreeNodeRef = remove_equivalence(tree);
 	let tree: TreeNodeRef = remove_material_condition(tree);
 	let tree: TreeNodeRef = remove_de_morgan(tree);

diff --git a/src/main.rs b/src/main.rs
@@ -200,6 +200,7 @@ fn main() {
 		"AB&CD&|EF&|",
 		"AB&CD&|EF&|GH&|",
 		"AB&CD&|EF&|GH&|IJ&|",
+		"AA!^BB!^^",
 	];
 
 	for formula in formulas {
@@ -229,14 +230,17 @@ fn main() {
 		);
 		println!();
 	}
+
 	println!("\n{}", "EX07 - SAT".bold());
+	let large = conjunctive_normal_form("AA!^BB!^^");
 	let formulas = [
 		("AB|", true),
 		("AB&", true),
 		("AA!&", false),
 		("AA^", false),
 		("AA!&BB!&|", false),
 		("AA!^BB!^^", false),
+		(large.as_str(), false),
 	];
 
 	for formula in formulas {