From d1e15ce8a9d99de5af9189cbf55a0b2252000258 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 22:23:23 +0100 Subject: [PATCH 01/12] Add evaluate_comparisons simplification --- src/simplifying/fol/ht.rs | 89 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 86 insertions(+), 3 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 31207bcc..fb0d50d3 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -3,7 +3,9 @@ use crate::{ apply::Apply as _, unbox::{fol::UnboxedFormula, Unbox as _}, }, - syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Theory}, + syntax_tree::fol::{ + AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Relation, Theory, + }, }; pub fn simplify(theory: Theory) -> Theory { @@ -14,6 +16,7 @@ pub fn simplify(theory: Theory) -> Theory { fn simplify_formula(formula: Formula) -> Formula { formula.apply_all(&mut vec![ + Box::new(evaluate_comparisons), Box::new(remove_identities), Box::new(remove_annihilations), Box::new(remove_idempotences), @@ -21,6 +24,56 @@ fn simplify_formula(formula: Formula) -> Formula { ]) } +fn evaluate_comparisons(formula: Formula) -> Formula { + // Evaluate comparisons between structurally equal terms + // e.g. T = T => #true + // e.g. T != T => #false + // e.g. T1 = T2 = T3 => T1 = T2 and T2 = T3 (side effect) + + match formula { + Formula::AtomicFormula(AtomicFormula::Comparison(Comparison { term, guards })) => { + let mut formulas = vec![]; + + let mut lhs = term; + for Guard { + relation, + term: rhs, + } in guards + { + formulas.push(Formula::AtomicFormula(if lhs == rhs { + match relation { + // T = T => #true + // T >= T => #true + // T <= T => #true + Relation::Equal | Relation::GreaterEqual | Relation::LessEqual => { + AtomicFormula::Truth + } + // T != T => #false + // T > T => #false + // T < T => #false + Relation::NotEqual | Relation::Greater | Relation::Less => { + AtomicFormula::Falsity + } + } + } else { + AtomicFormula::Comparison(Comparison { + term: lhs, + guards: vec![Guard { + relation, + term: rhs.clone(), + }], + }) + })); + + lhs = rhs; + } + + Formula::conjoin(formulas) + } + x => x, + } +} + fn remove_identities(formula: Formula) -> Formula { // Remove identities // e.g. F op E => F @@ -142,8 +195,8 @@ pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula { mod tests { use { super::{ - join_nested_quantifiers, remove_annihilations, remove_idempotences, remove_identities, - simplify_formula, + evaluate_comparisons, join_nested_quantifiers, + remove_annihilations, remove_idempotences, remove_identities, simplify_formula, }, crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, }; @@ -161,6 +214,36 @@ mod tests { } } + #[test] + fn test_evaluate_comparisons() { + for (src, target) in [ + ("X = X", "#true"), + ("X = Y", "X = Y"), + ("X != X", "#false"), + ("X != Y", "X != Y"), + ("X > X", "#false"), + ("X > Y", "X > Y"), + ("X < X", "#false"), + ("X < Y", "X < Y"), + ("X >= X", "#true"), + ("X >= Y", "X >= Y"), + ("X <= X", "#true"), + ("X <= Y", "X <= Y"), + ("X$i + 1 = X$i + 1", "#true"), + ("X$i + 1 + 1 = X$i + 2", "X$i + 1 + 1 = X$i + 2"), + ("X = X = Y", "#true and X = Y"), + ("X != X = Y", "#false and X = Y"), + ("X = Y = Z", "X = Y and Y = Z"), + ] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut evaluate_comparisons), + target.parse().unwrap() + ) + } + } + #[test] fn test_remove_identities() { for (src, target) in [ From 346eb08c431418ef6370e79749b44172fadc120a Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 22:41:04 +0100 Subject: [PATCH 02/12] Add apply_definitions simplification --- src/simplifying/fol/ht.rs | 76 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 73 insertions(+), 3 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index fb0d50d3..78959e0a 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -5,6 +5,7 @@ use crate::{ }, syntax_tree::fol::{ AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Relation, Theory, + UnaryConnective, }, }; @@ -17,6 +18,7 @@ pub fn simplify(theory: Theory) -> Theory { fn simplify_formula(formula: Formula) -> Formula { formula.apply_all(&mut vec![ Box::new(evaluate_comparisons), + Box::new(apply_definitions), Box::new(remove_identities), Box::new(remove_annihilations), Box::new(remove_idempotences), @@ -74,6 +76,55 @@ fn evaluate_comparisons(formula: Formula) -> Formula { } } +fn apply_definitions(formula: Formula) -> Formula { + // Apply definitions + // e.g. not F => F -> #false + // e.g. F <- G => G -> F + // e.g. F <-> G => (F -> G) and (G -> F) + + match formula.unbox() { + // not F => F -> #false + UnboxedFormula::UnaryFormula { + connective: UnaryConnective::Negation, + formula, + } => Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: formula.into(), + rhs: Formula::AtomicFormula(AtomicFormula::Falsity).into(), + }, + + // F <- G => G -> F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::ReverseImplication, + lhs, + rhs, + } => Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: rhs.into(), + rhs: lhs.into(), + }, + + // F <-> G => (F -> G) and (G -> F) + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Equivalence, + lhs, + rhs, + } => Formula::conjoin([ + Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: lhs.clone().into(), + rhs: rhs.clone().into(), + }, + Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: rhs.into(), + rhs: lhs.into(), + }, + ]), + x => x.rebox(), + } +} + fn remove_identities(formula: Formula) -> Formula { // Remove identities // e.g. F op E => F @@ -195,10 +246,13 @@ pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula { mod tests { use { super::{ - evaluate_comparisons, join_nested_quantifiers, - remove_annihilations, remove_idempotences, remove_identities, simplify_formula, + evaluate_comparisons, join_nested_quantifiers, remove_annihilations, + remove_idempotences, remove_identities, simplify_formula, + }, + crate::{ + convenience::apply::Apply as _, simplifying::fol::ht::apply_definitions, + syntax_tree::fol::Formula, }, - crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, }; #[test] @@ -244,6 +298,22 @@ mod tests { } } + #[test] + fn test_apply_definitions() { + for (src, target) in [ + ("not f", "f -> #false"), + ("f <- g", "g -> f"), + ("f <-> g", "(f -> g) and (g -> f)"), + ] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut apply_definitions), + target.parse().unwrap() + ) + } + } + #[test] fn test_remove_identities() { for (src, target) in [ From 1dddd538ee32b300c0ff8bd489f35040655f8677 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 22:57:10 +0100 Subject: [PATCH 03/12] Amend the remove_identities simplification with rules for implications --- src/simplifying/fol/ht.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 78959e0a..79c7e695 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -158,6 +158,13 @@ fn remove_identities(formula: Formula) -> Formula { rhs, } => rhs, + // #true -> F => F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: Formula::AtomicFormula(AtomicFormula::Truth), + rhs, + } => rhs, + x => x.rebox(), } } @@ -321,6 +328,7 @@ mod tests { ("a and #true", "a"), ("#false or a", "a"), ("a or #false", "a"), + ("#true -> a", "a"), ] { assert_eq!( src.parse::() From b86a15437586a9d77087c5992a2380ceab5c9b70 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 23:07:13 +0100 Subject: [PATCH 04/12] Amend the remove_annihilations simplification with rules for implications --- src/simplifying/fol/ht.rs | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 79c7e695..5904c032 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -202,6 +202,27 @@ fn remove_annihilations(formula: Formula) -> Formula { rhs: _, } => lhs, + // F -> #true => #true + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: _, + rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Truth), + } => rhs, + + // #false -> F => #true + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: Formula::AtomicFormula(AtomicFormula::Falsity), + rhs: _, + } => Formula::AtomicFormula(AtomicFormula::Truth), + + // F -> F => #true + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs, + rhs, + } if lhs == rhs => Formula::AtomicFormula(AtomicFormula::Truth), + x => x.rebox(), } } @@ -346,6 +367,9 @@ mod tests { ("a or #true", "#true"), ("#false and a", "#false"), ("a and #false", "#false"), + ("a -> #true", "#true"), + ("#false -> a", "#true"), + ("a -> a", "#true"), ] { assert_eq!( src.parse::() From 7cbb05c863b24454d5c098ef1f85d68544f5293c Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 20 Nov 2024 19:41:23 +0100 Subject: [PATCH 05/12] Add remove_orphaned_variables simplification --- src/simplifying/fol/ht.rs | 59 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 56 insertions(+), 3 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 5904c032..569d08f3 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -4,8 +4,8 @@ use crate::{ unbox::{fol::UnboxedFormula, Unbox as _}, }, syntax_tree::fol::{ - AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Relation, Theory, - UnaryConnective, + AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Quantification, Relation, + Theory, UnaryConnective, }, }; @@ -22,6 +22,7 @@ fn simplify_formula(formula: Formula) -> Formula { Box::new(remove_identities), Box::new(remove_annihilations), Box::new(remove_idempotences), + Box::new(remove_orphaned_variables), Box::new(join_nested_quantifiers), ]) } @@ -244,6 +245,39 @@ fn remove_idempotences(formula: Formula) -> Formula { } } +fn remove_orphaned_variables(formula: Formula) -> Formula { + // Remove orphaned variables in quantification + // e.g. q X Y F(X) => q X F(X) + + match formula { + // forall X Y F(X) => forall X F(X) + // exists X Y F(X) => exists X F(X) + Formula::QuantifiedFormula { + quantification: + Quantification { + quantifier, + variables, + }, + formula, + } => { + let free_variables = formula.free_variables(); + let variables = variables + .into_iter() + .filter(|v| free_variables.contains(v)) + .collect(); + + Formula::QuantifiedFormula { + quantification: Quantification { + quantifier, + variables, + }, + formula, + } + } + x => x, + } +} + pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula { // Remove nested quantifiers // e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y) @@ -275,7 +309,7 @@ mod tests { use { super::{ evaluate_comparisons, join_nested_quantifiers, remove_annihilations, - remove_idempotences, remove_identities, simplify_formula, + remove_idempotences, remove_identities, remove_orphaned_variables, simplify_formula, }, crate::{ convenience::apply::Apply as _, simplifying::fol::ht::apply_definitions, @@ -288,6 +322,9 @@ mod tests { for (src, target) in [ ("#true and #true and a", "a"), ("#true and (#true and a)", "a"), + ("forall X a", "a"), + ("X = X and a", "a"), + ("forall X (X = X)", "#true"), ] { assert_eq!( simplify_formula(src.parse().unwrap()), @@ -392,6 +429,22 @@ mod tests { } } + #[test] + fn test_remove_orphaned_variables() { + for (src, target) in [ + ("forall X Y Z (X = X)", "forall X (X = X)"), + ("exists X Y (X = Y)", "exists X Y (X = Y)"), + ("exists X Y Z (X = Y)", "exists X Y (X = Y)"), + ] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut remove_orphaned_variables), + target.parse().unwrap() + ) + } + } + #[test] fn test_join_nested_quantifiers() { for (src, target) in [ From 0f5604c790b32495517d8fc81fa15b8bd84f5c6f Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 23:18:22 +0100 Subject: [PATCH 06/12] Add remove_empty_quantifications simplification --- src/simplifying/fol/ht.rs | 42 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 569d08f3..8689f498 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -23,6 +23,7 @@ fn simplify_formula(formula: Formula) -> Formula { Box::new(remove_annihilations), Box::new(remove_idempotences), Box::new(remove_orphaned_variables), + Box::new(remove_empty_quantifications), Box::new(join_nested_quantifiers), ]) } @@ -278,6 +279,21 @@ fn remove_orphaned_variables(formula: Formula) -> Formula { } } +fn remove_empty_quantifications(formula: Formula) -> Formula { + // Remove empty quantifiers + // e.g. q F => F + + match formula { + // forall F => F + // exists F => F + Formula::QuantifiedFormula { + quantification, + formula, + } if quantification.variables.is_empty() => *formula, + x => x, + } +} + pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula { // Remove nested quantifiers // e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y) @@ -309,7 +325,8 @@ mod tests { use { super::{ evaluate_comparisons, join_nested_quantifiers, remove_annihilations, - remove_idempotences, remove_identities, remove_orphaned_variables, simplify_formula, + remove_empty_quantifications, remove_idempotences, remove_identities, + remove_orphaned_variables, simplify_formula, }, crate::{ convenience::apply::Apply as _, simplifying::fol::ht::apply_definitions, @@ -445,6 +462,29 @@ mod tests { } } + #[test] + fn test_remove_empty_quantifications() { + use crate::syntax_tree::fol::{Atom, AtomicFormula, Quantification, Quantifier}; + + let src = Formula::QuantifiedFormula { + quantification: Quantification { + quantifier: Quantifier::Forall, + variables: vec![], + }, + formula: Box::new(Formula::AtomicFormula(AtomicFormula::Atom(Atom { + predicate_symbol: "a".into(), + terms: vec![], + }))), + }; + + let target = Formula::AtomicFormula(AtomicFormula::Atom(Atom { + predicate_symbol: "a".into(), + terms: vec![], + })); + + assert_eq!(src.apply(&mut remove_empty_quantifications), target); + } + #[test] fn test_join_nested_quantifiers() { for (src, target) in [ From 568bd5c0574b87ede93928bec88e08839b16e6e4 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 1 Feb 2025 00:25:17 +0100 Subject: [PATCH 07/12] Split apply_definitions --- src/simplifying/fol/ht.rs | 78 ++++++++++++++++++++++++++++----------- 1 file changed, 56 insertions(+), 22 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 8689f498..0236dfee 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -18,7 +18,9 @@ pub fn simplify(theory: Theory) -> Theory { fn simplify_formula(formula: Formula) -> Formula { formula.apply_all(&mut vec![ Box::new(evaluate_comparisons), - Box::new(apply_definitions), + Box::new(apply_negation_definition), + Box::new(apply_reverse_implication_definition), + Box::new(apply_equivalence_definition), Box::new(remove_identities), Box::new(remove_annihilations), Box::new(remove_idempotences), @@ -78,11 +80,9 @@ fn evaluate_comparisons(formula: Formula) -> Formula { } } -fn apply_definitions(formula: Formula) -> Formula { - // Apply definitions +fn apply_negation_definition(formula: Formula) -> Formula { + // Apply the definition for negation // e.g. not F => F -> #false - // e.g. F <- G => G -> F - // e.g. F <-> G => (F -> G) and (G -> F) match formula.unbox() { // not F => F -> #false @@ -95,6 +95,15 @@ fn apply_definitions(formula: Formula) -> Formula { rhs: Formula::AtomicFormula(AtomicFormula::Falsity).into(), }, + x => x.rebox(), + } +} + +fn apply_reverse_implication_definition(formula: Formula) -> Formula { + // Apply the definition for reverse implication + // e.g. F <- G => G -> F + + match formula.unbox() { // F <- G => G -> F UnboxedFormula::BinaryFormula { connective: BinaryConnective::ReverseImplication, @@ -106,6 +115,15 @@ fn apply_definitions(formula: Formula) -> Formula { rhs: lhs.into(), }, + x => x.rebox(), + } +} + +fn apply_equivalence_definition(formula: Formula) -> Formula { + // Apply the definition for equivalence + // e.g. F <-> G => (F -> G) and (G -> F) + + match formula.unbox() { // F <-> G => (F -> G) and (G -> F) UnboxedFormula::BinaryFormula { connective: BinaryConnective::Equivalence, @@ -123,6 +141,7 @@ fn apply_definitions(formula: Formula) -> Formula { rhs: lhs.into(), }, ]), + x => x.rebox(), } } @@ -324,14 +343,12 @@ pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula { mod tests { use { super::{ + apply_equivalence_definition, apply_reverse_implication_definition, apply_negation_definition, evaluate_comparisons, join_nested_quantifiers, remove_annihilations, remove_empty_quantifications, remove_idempotences, remove_identities, remove_orphaned_variables, simplify_formula, }, - crate::{ - convenience::apply::Apply as _, simplifying::fol::ht::apply_definitions, - syntax_tree::fol::Formula, - }, + crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, }; #[test] @@ -381,19 +398,36 @@ mod tests { } #[test] - fn test_apply_definitions() { - for (src, target) in [ - ("not f", "f -> #false"), - ("f <- g", "g -> f"), - ("f <-> g", "(f -> g) and (g -> f)"), - ] { - assert_eq!( - src.parse::() - .unwrap() - .apply(&mut apply_definitions), - target.parse().unwrap() - ) - } + fn test_apply_negation_definitions() { + assert_eq!( + "not f" + .parse::() + .unwrap() + .apply(&mut apply_negation_definition), + "f -> #false".parse().unwrap() + ) + } + + #[test] + fn test_apply_reverse_implication_definitions() { + assert_eq!( + "f <- g" + .parse::() + .unwrap() + .apply(&mut apply_reverse_implication_definition), + "g -> f".parse().unwrap() + ) + } + + #[test] + fn test_apply_equivalence_definitions() { + assert_eq!( + "f <-> g" + .parse::() + .unwrap() + .apply(&mut apply_equivalence_definition), + "(f -> g) and (g -> f)".parse().unwrap() + ) } #[test] From 6f14619ac27426598e57b0b1d02898a79eda76cb Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 1 Feb 2025 01:04:40 +0100 Subject: [PATCH 08/12] Add simplification applying definitions in reverse --- src/simplifying/fol/ht.rs | 112 +++++++++++++++++++++++++++++++++++++- 1 file changed, 111 insertions(+), 1 deletion(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 0236dfee..7d8c04e6 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -99,6 +99,25 @@ fn apply_negation_definition(formula: Formula) -> Formula { } } +fn apply_negation_definition_inverse(formula: Formula) -> Formula { + // Apply the definition for negation in reverse + // e.g. F -> #false => not F + + match formula.unbox() { + // F -> #false => not F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs, + rhs: Formula::AtomicFormula(AtomicFormula::Falsity), + } => Formula::UnaryFormula { + connective: UnaryConnective::Negation, + formula: lhs.into(), + }, + + x => x.rebox(), + } +} + fn apply_reverse_implication_definition(formula: Formula) -> Formula { // Apply the definition for reverse implication // e.g. F <- G => G -> F @@ -119,6 +138,27 @@ fn apply_reverse_implication_definition(formula: Formula) -> Formula { } } +fn apply_reverse_implication_definition_inverse(formula: Formula) -> Formula { + // Apply the definition for reverse implication in reverse + // Yeah, that sounds terrible -- but is actually what happens here... + // e.g. G -> F => F <- G + + match formula.unbox() { + // F -> G => G <- F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs, + rhs, + } => Formula::BinaryFormula { + connective: BinaryConnective::ReverseImplication, + lhs: rhs.into(), + rhs: lhs.into(), + }, + + x => x.rebox(), + } +} + fn apply_equivalence_definition(formula: Formula) -> Formula { // Apply the definition for equivalence // e.g. F <-> G => (F -> G) and (G -> F) @@ -146,6 +186,41 @@ fn apply_equivalence_definition(formula: Formula) -> Formula { } } +fn apply_equivalence_definition_inverse(formula: Formula) -> Formula { + // Apply the definition for equivalence in reverse + // e.g. (F -> G) and (G -> F) => F <-> G + + match formula.unbox() { + // (F -> G) and (G -> F) => F <-> G + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs, + rhs, + } => match (lhs.unbox(), rhs.unbox()) { + ( + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: llhs, + rhs: lrhs, + }, + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: rlhs, + rhs: rrhs, + }, + ) if llhs == rrhs && lrhs == rlhs => Formula::BinaryFormula { + connective: BinaryConnective::Equivalence, + lhs: llhs.into(), + rhs: lrhs.into(), + }, + + (lhs, rhs) => Formula::conjoin([lhs.rebox(), rhs.rebox()]), + }, + + x => x.rebox(), + } +} + fn remove_identities(formula: Formula) -> Formula { // Remove identities // e.g. F op E => F @@ -343,7 +418,9 @@ pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula { mod tests { use { super::{ - apply_equivalence_definition, apply_reverse_implication_definition, apply_negation_definition, + apply_equivalence_definition, apply_equivalence_definition_inverse, + apply_negation_definition, apply_negation_definition_inverse, + apply_reverse_implication_definition, apply_reverse_implication_definition_inverse, evaluate_comparisons, join_nested_quantifiers, remove_annihilations, remove_empty_quantifications, remove_idempotences, remove_identities, remove_orphaned_variables, simplify_formula, @@ -408,6 +485,17 @@ mod tests { ) } + #[test] + fn test_apply_negation_definitions_inverse() { + assert_eq!( + "f -> #false" + .parse::() + .unwrap() + .apply(&mut apply_negation_definition_inverse), + "not f".parse().unwrap() + ) + } + #[test] fn test_apply_reverse_implication_definitions() { assert_eq!( @@ -419,6 +507,17 @@ mod tests { ) } + #[test] + fn test_apply_reverse_implication_definitions_inverse() { + assert_eq!( + "g -> f" + .parse::() + .unwrap() + .apply(&mut apply_reverse_implication_definition_inverse), + "f <- g".parse().unwrap() + ) + } + #[test] fn test_apply_equivalence_definitions() { assert_eq!( @@ -430,6 +529,17 @@ mod tests { ) } + #[test] + fn test_apply_equivalence_definitions_inverse() { + assert_eq!( + "(f -> g) and (g -> f)" + .parse::() + .unwrap() + .apply(&mut apply_equivalence_definition_inverse), + "f <-> g".parse().unwrap() + ) + } + #[test] fn test_remove_identities() { for (src, target) in [ From f176fdcbe06398383cea5f915af7bcbba6e6e466 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 1 Feb 2025 01:06:52 +0100 Subject: [PATCH 09/12] Make simplifications public --- src/simplifying/fol/ht.rs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 7d8c04e6..b62fb8ca 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -15,7 +15,7 @@ pub fn simplify(theory: Theory) -> Theory { } } -fn simplify_formula(formula: Formula) -> Formula { +pub fn simplify_formula(formula: Formula) -> Formula { formula.apply_all(&mut vec![ Box::new(evaluate_comparisons), Box::new(apply_negation_definition), @@ -30,7 +30,7 @@ fn simplify_formula(formula: Formula) -> Formula { ]) } -fn evaluate_comparisons(formula: Formula) -> Formula { +pub fn evaluate_comparisons(formula: Formula) -> Formula { // Evaluate comparisons between structurally equal terms // e.g. T = T => #true // e.g. T != T => #false @@ -80,7 +80,7 @@ fn evaluate_comparisons(formula: Formula) -> Formula { } } -fn apply_negation_definition(formula: Formula) -> Formula { +pub fn apply_negation_definition(formula: Formula) -> Formula { // Apply the definition for negation // e.g. not F => F -> #false @@ -99,7 +99,7 @@ fn apply_negation_definition(formula: Formula) -> Formula { } } -fn apply_negation_definition_inverse(formula: Formula) -> Formula { +pub fn apply_negation_definition_inverse(formula: Formula) -> Formula { // Apply the definition for negation in reverse // e.g. F -> #false => not F @@ -118,7 +118,7 @@ fn apply_negation_definition_inverse(formula: Formula) -> Formula { } } -fn apply_reverse_implication_definition(formula: Formula) -> Formula { +pub fn apply_reverse_implication_definition(formula: Formula) -> Formula { // Apply the definition for reverse implication // e.g. F <- G => G -> F @@ -138,7 +138,7 @@ fn apply_reverse_implication_definition(formula: Formula) -> Formula { } } -fn apply_reverse_implication_definition_inverse(formula: Formula) -> Formula { +pub fn apply_reverse_implication_definition_inverse(formula: Formula) -> Formula { // Apply the definition for reverse implication in reverse // Yeah, that sounds terrible -- but is actually what happens here... // e.g. G -> F => F <- G @@ -159,7 +159,7 @@ fn apply_reverse_implication_definition_inverse(formula: Formula) -> Formula { } } -fn apply_equivalence_definition(formula: Formula) -> Formula { +pub fn apply_equivalence_definition(formula: Formula) -> Formula { // Apply the definition for equivalence // e.g. F <-> G => (F -> G) and (G -> F) @@ -186,7 +186,7 @@ fn apply_equivalence_definition(formula: Formula) -> Formula { } } -fn apply_equivalence_definition_inverse(formula: Formula) -> Formula { +pub fn apply_equivalence_definition_inverse(formula: Formula) -> Formula { // Apply the definition for equivalence in reverse // e.g. (F -> G) and (G -> F) => F <-> G @@ -221,7 +221,7 @@ fn apply_equivalence_definition_inverse(formula: Formula) -> Formula { } } -fn remove_identities(formula: Formula) -> Formula { +pub fn remove_identities(formula: Formula) -> Formula { // Remove identities // e.g. F op E => F @@ -265,7 +265,7 @@ fn remove_identities(formula: Formula) -> Formula { } } -fn remove_annihilations(formula: Formula) -> Formula { +pub fn remove_annihilations(formula: Formula) -> Formula { // Remove annihilations // e.g. F op E => E @@ -323,7 +323,7 @@ fn remove_annihilations(formula: Formula) -> Formula { } } -fn remove_idempotences(formula: Formula) -> Formula { +pub fn remove_idempotences(formula: Formula) -> Formula { // Remove idempotences // e.g. F op F => F @@ -340,7 +340,7 @@ fn remove_idempotences(formula: Formula) -> Formula { } } -fn remove_orphaned_variables(formula: Formula) -> Formula { +pub fn remove_orphaned_variables(formula: Formula) -> Formula { // Remove orphaned variables in quantification // e.g. q X Y F(X) => q X F(X) @@ -373,7 +373,7 @@ fn remove_orphaned_variables(formula: Formula) -> Formula { } } -fn remove_empty_quantifications(formula: Formula) -> Formula { +pub fn remove_empty_quantifications(formula: Formula) -> Formula { // Remove empty quantifiers // e.g. q F => F @@ -388,7 +388,7 @@ fn remove_empty_quantifications(formula: Formula) -> Formula { } } -pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula { +pub fn join_nested_quantifiers(formula: Formula) -> Formula { // Remove nested quantifiers // e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y) From 2e41b3946ee9d3d3d537a60fbd80263a4c738bad Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 1 Feb 2025 01:28:50 +0100 Subject: [PATCH 10/12] Sort simplifications into classic, ht, and intuitionistic --- src/simplifying/fol/ht.rs | 665 +---------------------- src/simplifying/fol/intuitionistic.rs | 665 +++++++++++++++++++++++ src/simplifying/fol/mod.rs | 1 + src/syntax_tree/fol.rs | 2 +- src/verifying/task/strong_equivalence.rs | 4 +- 5 files changed, 672 insertions(+), 665 deletions(-) create mode 100644 src/simplifying/fol/intuitionistic.rs diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index b62fb8ca..c1c68ca3 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -1,665 +1,6 @@ -use crate::{ - convenience::{ - apply::Apply as _, - unbox::{fol::UnboxedFormula, Unbox as _}, - }, - syntax_tree::fol::{ - AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Quantification, Relation, - Theory, UnaryConnective, - }, -}; +use crate::syntax_tree::fol::Theory; pub fn simplify(theory: Theory) -> Theory { - Theory { - formulas: theory.formulas.into_iter().map(simplify_formula).collect(), - } -} - -pub fn simplify_formula(formula: Formula) -> Formula { - formula.apply_all(&mut vec![ - Box::new(evaluate_comparisons), - Box::new(apply_negation_definition), - Box::new(apply_reverse_implication_definition), - Box::new(apply_equivalence_definition), - Box::new(remove_identities), - Box::new(remove_annihilations), - Box::new(remove_idempotences), - Box::new(remove_orphaned_variables), - Box::new(remove_empty_quantifications), - Box::new(join_nested_quantifiers), - ]) -} - -pub fn evaluate_comparisons(formula: Formula) -> Formula { - // Evaluate comparisons between structurally equal terms - // e.g. T = T => #true - // e.g. T != T => #false - // e.g. T1 = T2 = T3 => T1 = T2 and T2 = T3 (side effect) - - match formula { - Formula::AtomicFormula(AtomicFormula::Comparison(Comparison { term, guards })) => { - let mut formulas = vec![]; - - let mut lhs = term; - for Guard { - relation, - term: rhs, - } in guards - { - formulas.push(Formula::AtomicFormula(if lhs == rhs { - match relation { - // T = T => #true - // T >= T => #true - // T <= T => #true - Relation::Equal | Relation::GreaterEqual | Relation::LessEqual => { - AtomicFormula::Truth - } - // T != T => #false - // T > T => #false - // T < T => #false - Relation::NotEqual | Relation::Greater | Relation::Less => { - AtomicFormula::Falsity - } - } - } else { - AtomicFormula::Comparison(Comparison { - term: lhs, - guards: vec![Guard { - relation, - term: rhs.clone(), - }], - }) - })); - - lhs = rhs; - } - - Formula::conjoin(formulas) - } - x => x, - } -} - -pub fn apply_negation_definition(formula: Formula) -> Formula { - // Apply the definition for negation - // e.g. not F => F -> #false - - match formula.unbox() { - // not F => F -> #false - UnboxedFormula::UnaryFormula { - connective: UnaryConnective::Negation, - formula, - } => Formula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: formula.into(), - rhs: Formula::AtomicFormula(AtomicFormula::Falsity).into(), - }, - - x => x.rebox(), - } -} - -pub fn apply_negation_definition_inverse(formula: Formula) -> Formula { - // Apply the definition for negation in reverse - // e.g. F -> #false => not F - - match formula.unbox() { - // F -> #false => not F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs, - rhs: Formula::AtomicFormula(AtomicFormula::Falsity), - } => Formula::UnaryFormula { - connective: UnaryConnective::Negation, - formula: lhs.into(), - }, - - x => x.rebox(), - } -} - -pub fn apply_reverse_implication_definition(formula: Formula) -> Formula { - // Apply the definition for reverse implication - // e.g. F <- G => G -> F - - match formula.unbox() { - // F <- G => G -> F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::ReverseImplication, - lhs, - rhs, - } => Formula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: rhs.into(), - rhs: lhs.into(), - }, - - x => x.rebox(), - } -} - -pub fn apply_reverse_implication_definition_inverse(formula: Formula) -> Formula { - // Apply the definition for reverse implication in reverse - // Yeah, that sounds terrible -- but is actually what happens here... - // e.g. G -> F => F <- G - - match formula.unbox() { - // F -> G => G <- F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs, - rhs, - } => Formula::BinaryFormula { - connective: BinaryConnective::ReverseImplication, - lhs: rhs.into(), - rhs: lhs.into(), - }, - - x => x.rebox(), - } -} - -pub fn apply_equivalence_definition(formula: Formula) -> Formula { - // Apply the definition for equivalence - // e.g. F <-> G => (F -> G) and (G -> F) - - match formula.unbox() { - // F <-> G => (F -> G) and (G -> F) - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Equivalence, - lhs, - rhs, - } => Formula::conjoin([ - Formula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: lhs.clone().into(), - rhs: rhs.clone().into(), - }, - Formula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: rhs.into(), - rhs: lhs.into(), - }, - ]), - - x => x.rebox(), - } -} - -pub fn apply_equivalence_definition_inverse(formula: Formula) -> Formula { - // Apply the definition for equivalence in reverse - // e.g. (F -> G) and (G -> F) => F <-> G - - match formula.unbox() { - // (F -> G) and (G -> F) => F <-> G - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Conjunction, - lhs, - rhs, - } => match (lhs.unbox(), rhs.unbox()) { - ( - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: llhs, - rhs: lrhs, - }, - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: rlhs, - rhs: rrhs, - }, - ) if llhs == rrhs && lrhs == rlhs => Formula::BinaryFormula { - connective: BinaryConnective::Equivalence, - lhs: llhs.into(), - rhs: lrhs.into(), - }, - - (lhs, rhs) => Formula::conjoin([lhs.rebox(), rhs.rebox()]), - }, - - x => x.rebox(), - } -} - -pub fn remove_identities(formula: Formula) -> Formula { - // Remove identities - // e.g. F op E => F - - match formula.unbox() { - // F and #true => F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Conjunction, - lhs, - rhs: Formula::AtomicFormula(AtomicFormula::Truth), - } => lhs, - - // #true and F => F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Conjunction, - lhs: Formula::AtomicFormula(AtomicFormula::Truth), - rhs, - } => rhs, - - // F or #false => F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Disjunction, - lhs, - rhs: Formula::AtomicFormula(AtomicFormula::Falsity), - } => lhs, - - // #false or F => F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Disjunction, - lhs: Formula::AtomicFormula(AtomicFormula::Falsity), - rhs, - } => rhs, - - // #true -> F => F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: Formula::AtomicFormula(AtomicFormula::Truth), - rhs, - } => rhs, - - x => x.rebox(), - } -} - -pub fn remove_annihilations(formula: Formula) -> Formula { - // Remove annihilations - // e.g. F op E => E - - match formula.unbox() { - // F or #true => #true - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Disjunction, - lhs: _, - rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Truth), - } => rhs, - - // #true or F => #true - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Disjunction, - lhs: lhs @ Formula::AtomicFormula(AtomicFormula::Truth), - rhs: _, - } => lhs, - - // F and #false => false - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Conjunction, - lhs: _, - rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Falsity), - } => rhs, - - // #false and F => #false - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Conjunction, - lhs: lhs @ Formula::AtomicFormula(AtomicFormula::Falsity), - rhs: _, - } => lhs, - - // F -> #true => #true - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: _, - rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Truth), - } => rhs, - - // #false -> F => #true - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs: Formula::AtomicFormula(AtomicFormula::Falsity), - rhs: _, - } => Formula::AtomicFormula(AtomicFormula::Truth), - - // F -> F => #true - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Implication, - lhs, - rhs, - } if lhs == rhs => Formula::AtomicFormula(AtomicFormula::Truth), - - x => x.rebox(), - } -} - -pub fn remove_idempotences(formula: Formula) -> Formula { - // Remove idempotences - // e.g. F op F => F - - match formula.unbox() { - // F and F => F - // F or F => F - UnboxedFormula::BinaryFormula { - connective: BinaryConnective::Conjunction | BinaryConnective::Disjunction, - lhs, - rhs, - } if lhs == rhs => lhs, - - x => x.rebox(), - } -} - -pub fn remove_orphaned_variables(formula: Formula) -> Formula { - // Remove orphaned variables in quantification - // e.g. q X Y F(X) => q X F(X) - - match formula { - // forall X Y F(X) => forall X F(X) - // exists X Y F(X) => exists X F(X) - Formula::QuantifiedFormula { - quantification: - Quantification { - quantifier, - variables, - }, - formula, - } => { - let free_variables = formula.free_variables(); - let variables = variables - .into_iter() - .filter(|v| free_variables.contains(v)) - .collect(); - - Formula::QuantifiedFormula { - quantification: Quantification { - quantifier, - variables, - }, - formula, - } - } - x => x, - } -} - -pub fn remove_empty_quantifications(formula: Formula) -> Formula { - // Remove empty quantifiers - // e.g. q F => F - - match formula { - // forall F => F - // exists F => F - Formula::QuantifiedFormula { - quantification, - formula, - } if quantification.variables.is_empty() => *formula, - x => x, - } -} - -pub fn join_nested_quantifiers(formula: Formula) -> Formula { - // Remove nested quantifiers - // e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y) - - match formula.unbox() { - // forall X ( forall Y F(X,Y) ) => forall X Y F(X,Y) - // exists X ( exists Y F(X,Y) ) => exists X Y F(X,Y) - UnboxedFormula::QuantifiedFormula { - quantification: outer_quantification, - formula: - Formula::QuantifiedFormula { - quantification: mut inner_quantification, - formula: inner_formula, - }, - } if outer_quantification.quantifier == inner_quantification.quantifier => { - let mut variables = outer_quantification.variables; - variables.append(&mut inner_quantification.variables); - variables.sort(); - variables.dedup(); - - inner_formula.quantify(outer_quantification.quantifier, variables) - } - x => x.rebox(), - } -} - -#[cfg(test)] -mod tests { - use { - super::{ - apply_equivalence_definition, apply_equivalence_definition_inverse, - apply_negation_definition, apply_negation_definition_inverse, - apply_reverse_implication_definition, apply_reverse_implication_definition_inverse, - evaluate_comparisons, join_nested_quantifiers, remove_annihilations, - remove_empty_quantifications, remove_idempotences, remove_identities, - remove_orphaned_variables, simplify_formula, - }, - crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, - }; - - #[test] - fn test_simplify() { - for (src, target) in [ - ("#true and #true and a", "a"), - ("#true and (#true and a)", "a"), - ("forall X a", "a"), - ("X = X and a", "a"), - ("forall X (X = X)", "#true"), - ] { - assert_eq!( - simplify_formula(src.parse().unwrap()), - target.parse().unwrap() - ) - } - } - - #[test] - fn test_evaluate_comparisons() { - for (src, target) in [ - ("X = X", "#true"), - ("X = Y", "X = Y"), - ("X != X", "#false"), - ("X != Y", "X != Y"), - ("X > X", "#false"), - ("X > Y", "X > Y"), - ("X < X", "#false"), - ("X < Y", "X < Y"), - ("X >= X", "#true"), - ("X >= Y", "X >= Y"), - ("X <= X", "#true"), - ("X <= Y", "X <= Y"), - ("X$i + 1 = X$i + 1", "#true"), - ("X$i + 1 + 1 = X$i + 2", "X$i + 1 + 1 = X$i + 2"), - ("X = X = Y", "#true and X = Y"), - ("X != X = Y", "#false and X = Y"), - ("X = Y = Z", "X = Y and Y = Z"), - ] { - assert_eq!( - src.parse::() - .unwrap() - .apply(&mut evaluate_comparisons), - target.parse().unwrap() - ) - } - } - - #[test] - fn test_apply_negation_definitions() { - assert_eq!( - "not f" - .parse::() - .unwrap() - .apply(&mut apply_negation_definition), - "f -> #false".parse().unwrap() - ) - } - - #[test] - fn test_apply_negation_definitions_inverse() { - assert_eq!( - "f -> #false" - .parse::() - .unwrap() - .apply(&mut apply_negation_definition_inverse), - "not f".parse().unwrap() - ) - } - - #[test] - fn test_apply_reverse_implication_definitions() { - assert_eq!( - "f <- g" - .parse::() - .unwrap() - .apply(&mut apply_reverse_implication_definition), - "g -> f".parse().unwrap() - ) - } - - #[test] - fn test_apply_reverse_implication_definitions_inverse() { - assert_eq!( - "g -> f" - .parse::() - .unwrap() - .apply(&mut apply_reverse_implication_definition_inverse), - "f <- g".parse().unwrap() - ) - } - - #[test] - fn test_apply_equivalence_definitions() { - assert_eq!( - "f <-> g" - .parse::() - .unwrap() - .apply(&mut apply_equivalence_definition), - "(f -> g) and (g -> f)".parse().unwrap() - ) - } - - #[test] - fn test_apply_equivalence_definitions_inverse() { - assert_eq!( - "(f -> g) and (g -> f)" - .parse::() - .unwrap() - .apply(&mut apply_equivalence_definition_inverse), - "f <-> g".parse().unwrap() - ) - } - - #[test] - fn test_remove_identities() { - for (src, target) in [ - ("#true and a", "a"), - ("a and #true", "a"), - ("#false or a", "a"), - ("a or #false", "a"), - ("#true -> a", "a"), - ] { - assert_eq!( - src.parse::() - .unwrap() - .apply(&mut remove_identities), - target.parse().unwrap() - ) - } - } - - #[test] - fn test_remove_annihilations() { - for (src, target) in [ - ("#true or a", "#true"), - ("a or #true", "#true"), - ("#false and a", "#false"), - ("a and #false", "#false"), - ("a -> #true", "#true"), - ("#false -> a", "#true"), - ("a -> a", "#true"), - ] { - assert_eq!( - src.parse::() - .unwrap() - .apply(&mut remove_annihilations), - target.parse().unwrap() - ) - } - } - - #[test] - fn test_remove_idempotences() { - for (src, target) in [("a and a", "a"), ("a or a", "a")] { - assert_eq!( - src.parse::() - .unwrap() - .apply(&mut remove_idempotences), - target.parse().unwrap() - ) - } - } - - #[test] - fn test_remove_orphaned_variables() { - for (src, target) in [ - ("forall X Y Z (X = X)", "forall X (X = X)"), - ("exists X Y (X = Y)", "exists X Y (X = Y)"), - ("exists X Y Z (X = Y)", "exists X Y (X = Y)"), - ] { - assert_eq!( - src.parse::() - .unwrap() - .apply(&mut remove_orphaned_variables), - target.parse().unwrap() - ) - } - } - - #[test] - fn test_remove_empty_quantifications() { - use crate::syntax_tree::fol::{Atom, AtomicFormula, Quantification, Quantifier}; - - let src = Formula::QuantifiedFormula { - quantification: Quantification { - quantifier: Quantifier::Forall, - variables: vec![], - }, - formula: Box::new(Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate_symbol: "a".into(), - terms: vec![], - }))), - }; - - let target = Formula::AtomicFormula(AtomicFormula::Atom(Atom { - predicate_symbol: "a".into(), - terms: vec![], - })); - - assert_eq!(src.apply(&mut remove_empty_quantifications), target); - } - - #[test] - fn test_join_nested_quantifiers() { - for (src, target) in [ - ("exists X (exists Y (X = Y))", "exists X Y (X = Y)"), - ( - "exists X Y ( exists Z ( X < Y and Y < Z ))", - "exists X Y Z ( X < Y and Y < Z )", - ), - ( - "exists X (exists Y (X = Y and q(Y)))", - "exists X Y (X = Y and q(Y))", - ), - ( - "exists X (exists X$i (p(X) -> X$i < 1))", - "exists X X$i (p(X) -> X$i < 1)", - ), - ( - "forall X Y (forall Y Z (p(X,Y) and q(Y,Z)))", - "forall X Y Z (p(X,Y) and q(Y,Z))", - ), - ( - "forall X (forall Y (forall Z (X = Y = Z)))", - "forall X Y Z (X = Y = Z)", - ), - ] { - assert_eq!( - src.parse::() - .unwrap() - .apply(&mut join_nested_quantifiers), - target.parse().unwrap() - ) - } - } + crate::simplifying::fol::intuitionistic::simplify(theory) + // TODO: Add ht simplifications } diff --git a/src/simplifying/fol/intuitionistic.rs b/src/simplifying/fol/intuitionistic.rs new file mode 100644 index 00000000..b62fb8ca --- /dev/null +++ b/src/simplifying/fol/intuitionistic.rs @@ -0,0 +1,665 @@ +use crate::{ + convenience::{ + apply::Apply as _, + unbox::{fol::UnboxedFormula, Unbox as _}, + }, + syntax_tree::fol::{ + AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Quantification, Relation, + Theory, UnaryConnective, + }, +}; + +pub fn simplify(theory: Theory) -> Theory { + Theory { + formulas: theory.formulas.into_iter().map(simplify_formula).collect(), + } +} + +pub fn simplify_formula(formula: Formula) -> Formula { + formula.apply_all(&mut vec![ + Box::new(evaluate_comparisons), + Box::new(apply_negation_definition), + Box::new(apply_reverse_implication_definition), + Box::new(apply_equivalence_definition), + Box::new(remove_identities), + Box::new(remove_annihilations), + Box::new(remove_idempotences), + Box::new(remove_orphaned_variables), + Box::new(remove_empty_quantifications), + Box::new(join_nested_quantifiers), + ]) +} + +pub fn evaluate_comparisons(formula: Formula) -> Formula { + // Evaluate comparisons between structurally equal terms + // e.g. T = T => #true + // e.g. T != T => #false + // e.g. T1 = T2 = T3 => T1 = T2 and T2 = T3 (side effect) + + match formula { + Formula::AtomicFormula(AtomicFormula::Comparison(Comparison { term, guards })) => { + let mut formulas = vec![]; + + let mut lhs = term; + for Guard { + relation, + term: rhs, + } in guards + { + formulas.push(Formula::AtomicFormula(if lhs == rhs { + match relation { + // T = T => #true + // T >= T => #true + // T <= T => #true + Relation::Equal | Relation::GreaterEqual | Relation::LessEqual => { + AtomicFormula::Truth + } + // T != T => #false + // T > T => #false + // T < T => #false + Relation::NotEqual | Relation::Greater | Relation::Less => { + AtomicFormula::Falsity + } + } + } else { + AtomicFormula::Comparison(Comparison { + term: lhs, + guards: vec![Guard { + relation, + term: rhs.clone(), + }], + }) + })); + + lhs = rhs; + } + + Formula::conjoin(formulas) + } + x => x, + } +} + +pub fn apply_negation_definition(formula: Formula) -> Formula { + // Apply the definition for negation + // e.g. not F => F -> #false + + match formula.unbox() { + // not F => F -> #false + UnboxedFormula::UnaryFormula { + connective: UnaryConnective::Negation, + formula, + } => Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: formula.into(), + rhs: Formula::AtomicFormula(AtomicFormula::Falsity).into(), + }, + + x => x.rebox(), + } +} + +pub fn apply_negation_definition_inverse(formula: Formula) -> Formula { + // Apply the definition for negation in reverse + // e.g. F -> #false => not F + + match formula.unbox() { + // F -> #false => not F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs, + rhs: Formula::AtomicFormula(AtomicFormula::Falsity), + } => Formula::UnaryFormula { + connective: UnaryConnective::Negation, + formula: lhs.into(), + }, + + x => x.rebox(), + } +} + +pub fn apply_reverse_implication_definition(formula: Formula) -> Formula { + // Apply the definition for reverse implication + // e.g. F <- G => G -> F + + match formula.unbox() { + // F <- G => G -> F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::ReverseImplication, + lhs, + rhs, + } => Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: rhs.into(), + rhs: lhs.into(), + }, + + x => x.rebox(), + } +} + +pub fn apply_reverse_implication_definition_inverse(formula: Formula) -> Formula { + // Apply the definition for reverse implication in reverse + // Yeah, that sounds terrible -- but is actually what happens here... + // e.g. G -> F => F <- G + + match formula.unbox() { + // F -> G => G <- F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs, + rhs, + } => Formula::BinaryFormula { + connective: BinaryConnective::ReverseImplication, + lhs: rhs.into(), + rhs: lhs.into(), + }, + + x => x.rebox(), + } +} + +pub fn apply_equivalence_definition(formula: Formula) -> Formula { + // Apply the definition for equivalence + // e.g. F <-> G => (F -> G) and (G -> F) + + match formula.unbox() { + // F <-> G => (F -> G) and (G -> F) + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Equivalence, + lhs, + rhs, + } => Formula::conjoin([ + Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: lhs.clone().into(), + rhs: rhs.clone().into(), + }, + Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: rhs.into(), + rhs: lhs.into(), + }, + ]), + + x => x.rebox(), + } +} + +pub fn apply_equivalence_definition_inverse(formula: Formula) -> Formula { + // Apply the definition for equivalence in reverse + // e.g. (F -> G) and (G -> F) => F <-> G + + match formula.unbox() { + // (F -> G) and (G -> F) => F <-> G + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs, + rhs, + } => match (lhs.unbox(), rhs.unbox()) { + ( + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: llhs, + rhs: lrhs, + }, + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: rlhs, + rhs: rrhs, + }, + ) if llhs == rrhs && lrhs == rlhs => Formula::BinaryFormula { + connective: BinaryConnective::Equivalence, + lhs: llhs.into(), + rhs: lrhs.into(), + }, + + (lhs, rhs) => Formula::conjoin([lhs.rebox(), rhs.rebox()]), + }, + + x => x.rebox(), + } +} + +pub fn remove_identities(formula: Formula) -> Formula { + // Remove identities + // e.g. F op E => F + + match formula.unbox() { + // F and #true => F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs, + rhs: Formula::AtomicFormula(AtomicFormula::Truth), + } => lhs, + + // #true and F => F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs: Formula::AtomicFormula(AtomicFormula::Truth), + rhs, + } => rhs, + + // F or #false => F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Disjunction, + lhs, + rhs: Formula::AtomicFormula(AtomicFormula::Falsity), + } => lhs, + + // #false or F => F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Disjunction, + lhs: Formula::AtomicFormula(AtomicFormula::Falsity), + rhs, + } => rhs, + + // #true -> F => F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: Formula::AtomicFormula(AtomicFormula::Truth), + rhs, + } => rhs, + + x => x.rebox(), + } +} + +pub fn remove_annihilations(formula: Formula) -> Formula { + // Remove annihilations + // e.g. F op E => E + + match formula.unbox() { + // F or #true => #true + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Disjunction, + lhs: _, + rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Truth), + } => rhs, + + // #true or F => #true + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Disjunction, + lhs: lhs @ Formula::AtomicFormula(AtomicFormula::Truth), + rhs: _, + } => lhs, + + // F and #false => false + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs: _, + rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Falsity), + } => rhs, + + // #false and F => #false + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs: lhs @ Formula::AtomicFormula(AtomicFormula::Falsity), + rhs: _, + } => lhs, + + // F -> #true => #true + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: _, + rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Truth), + } => rhs, + + // #false -> F => #true + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: Formula::AtomicFormula(AtomicFormula::Falsity), + rhs: _, + } => Formula::AtomicFormula(AtomicFormula::Truth), + + // F -> F => #true + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs, + rhs, + } if lhs == rhs => Formula::AtomicFormula(AtomicFormula::Truth), + + x => x.rebox(), + } +} + +pub fn remove_idempotences(formula: Formula) -> Formula { + // Remove idempotences + // e.g. F op F => F + + match formula.unbox() { + // F and F => F + // F or F => F + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction | BinaryConnective::Disjunction, + lhs, + rhs, + } if lhs == rhs => lhs, + + x => x.rebox(), + } +} + +pub fn remove_orphaned_variables(formula: Formula) -> Formula { + // Remove orphaned variables in quantification + // e.g. q X Y F(X) => q X F(X) + + match formula { + // forall X Y F(X) => forall X F(X) + // exists X Y F(X) => exists X F(X) + Formula::QuantifiedFormula { + quantification: + Quantification { + quantifier, + variables, + }, + formula, + } => { + let free_variables = formula.free_variables(); + let variables = variables + .into_iter() + .filter(|v| free_variables.contains(v)) + .collect(); + + Formula::QuantifiedFormula { + quantification: Quantification { + quantifier, + variables, + }, + formula, + } + } + x => x, + } +} + +pub fn remove_empty_quantifications(formula: Formula) -> Formula { + // Remove empty quantifiers + // e.g. q F => F + + match formula { + // forall F => F + // exists F => F + Formula::QuantifiedFormula { + quantification, + formula, + } if quantification.variables.is_empty() => *formula, + x => x, + } +} + +pub fn join_nested_quantifiers(formula: Formula) -> Formula { + // Remove nested quantifiers + // e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y) + + match formula.unbox() { + // forall X ( forall Y F(X,Y) ) => forall X Y F(X,Y) + // exists X ( exists Y F(X,Y) ) => exists X Y F(X,Y) + UnboxedFormula::QuantifiedFormula { + quantification: outer_quantification, + formula: + Formula::QuantifiedFormula { + quantification: mut inner_quantification, + formula: inner_formula, + }, + } if outer_quantification.quantifier == inner_quantification.quantifier => { + let mut variables = outer_quantification.variables; + variables.append(&mut inner_quantification.variables); + variables.sort(); + variables.dedup(); + + inner_formula.quantify(outer_quantification.quantifier, variables) + } + x => x.rebox(), + } +} + +#[cfg(test)] +mod tests { + use { + super::{ + apply_equivalence_definition, apply_equivalence_definition_inverse, + apply_negation_definition, apply_negation_definition_inverse, + apply_reverse_implication_definition, apply_reverse_implication_definition_inverse, + evaluate_comparisons, join_nested_quantifiers, remove_annihilations, + remove_empty_quantifications, remove_idempotences, remove_identities, + remove_orphaned_variables, simplify_formula, + }, + crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, + }; + + #[test] + fn test_simplify() { + for (src, target) in [ + ("#true and #true and a", "a"), + ("#true and (#true and a)", "a"), + ("forall X a", "a"), + ("X = X and a", "a"), + ("forall X (X = X)", "#true"), + ] { + assert_eq!( + simplify_formula(src.parse().unwrap()), + target.parse().unwrap() + ) + } + } + + #[test] + fn test_evaluate_comparisons() { + for (src, target) in [ + ("X = X", "#true"), + ("X = Y", "X = Y"), + ("X != X", "#false"), + ("X != Y", "X != Y"), + ("X > X", "#false"), + ("X > Y", "X > Y"), + ("X < X", "#false"), + ("X < Y", "X < Y"), + ("X >= X", "#true"), + ("X >= Y", "X >= Y"), + ("X <= X", "#true"), + ("X <= Y", "X <= Y"), + ("X$i + 1 = X$i + 1", "#true"), + ("X$i + 1 + 1 = X$i + 2", "X$i + 1 + 1 = X$i + 2"), + ("X = X = Y", "#true and X = Y"), + ("X != X = Y", "#false and X = Y"), + ("X = Y = Z", "X = Y and Y = Z"), + ] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut evaluate_comparisons), + target.parse().unwrap() + ) + } + } + + #[test] + fn test_apply_negation_definitions() { + assert_eq!( + "not f" + .parse::() + .unwrap() + .apply(&mut apply_negation_definition), + "f -> #false".parse().unwrap() + ) + } + + #[test] + fn test_apply_negation_definitions_inverse() { + assert_eq!( + "f -> #false" + .parse::() + .unwrap() + .apply(&mut apply_negation_definition_inverse), + "not f".parse().unwrap() + ) + } + + #[test] + fn test_apply_reverse_implication_definitions() { + assert_eq!( + "f <- g" + .parse::() + .unwrap() + .apply(&mut apply_reverse_implication_definition), + "g -> f".parse().unwrap() + ) + } + + #[test] + fn test_apply_reverse_implication_definitions_inverse() { + assert_eq!( + "g -> f" + .parse::() + .unwrap() + .apply(&mut apply_reverse_implication_definition_inverse), + "f <- g".parse().unwrap() + ) + } + + #[test] + fn test_apply_equivalence_definitions() { + assert_eq!( + "f <-> g" + .parse::() + .unwrap() + .apply(&mut apply_equivalence_definition), + "(f -> g) and (g -> f)".parse().unwrap() + ) + } + + #[test] + fn test_apply_equivalence_definitions_inverse() { + assert_eq!( + "(f -> g) and (g -> f)" + .parse::() + .unwrap() + .apply(&mut apply_equivalence_definition_inverse), + "f <-> g".parse().unwrap() + ) + } + + #[test] + fn test_remove_identities() { + for (src, target) in [ + ("#true and a", "a"), + ("a and #true", "a"), + ("#false or a", "a"), + ("a or #false", "a"), + ("#true -> a", "a"), + ] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut remove_identities), + target.parse().unwrap() + ) + } + } + + #[test] + fn test_remove_annihilations() { + for (src, target) in [ + ("#true or a", "#true"), + ("a or #true", "#true"), + ("#false and a", "#false"), + ("a and #false", "#false"), + ("a -> #true", "#true"), + ("#false -> a", "#true"), + ("a -> a", "#true"), + ] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut remove_annihilations), + target.parse().unwrap() + ) + } + } + + #[test] + fn test_remove_idempotences() { + for (src, target) in [("a and a", "a"), ("a or a", "a")] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut remove_idempotences), + target.parse().unwrap() + ) + } + } + + #[test] + fn test_remove_orphaned_variables() { + for (src, target) in [ + ("forall X Y Z (X = X)", "forall X (X = X)"), + ("exists X Y (X = Y)", "exists X Y (X = Y)"), + ("exists X Y Z (X = Y)", "exists X Y (X = Y)"), + ] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut remove_orphaned_variables), + target.parse().unwrap() + ) + } + } + + #[test] + fn test_remove_empty_quantifications() { + use crate::syntax_tree::fol::{Atom, AtomicFormula, Quantification, Quantifier}; + + let src = Formula::QuantifiedFormula { + quantification: Quantification { + quantifier: Quantifier::Forall, + variables: vec![], + }, + formula: Box::new(Formula::AtomicFormula(AtomicFormula::Atom(Atom { + predicate_symbol: "a".into(), + terms: vec![], + }))), + }; + + let target = Formula::AtomicFormula(AtomicFormula::Atom(Atom { + predicate_symbol: "a".into(), + terms: vec![], + })); + + assert_eq!(src.apply(&mut remove_empty_quantifications), target); + } + + #[test] + fn test_join_nested_quantifiers() { + for (src, target) in [ + ("exists X (exists Y (X = Y))", "exists X Y (X = Y)"), + ( + "exists X Y ( exists Z ( X < Y and Y < Z ))", + "exists X Y Z ( X < Y and Y < Z )", + ), + ( + "exists X (exists Y (X = Y and q(Y)))", + "exists X Y (X = Y and q(Y))", + ), + ( + "exists X (exists X$i (p(X) -> X$i < 1))", + "exists X X$i (p(X) -> X$i < 1)", + ), + ( + "forall X Y (forall Y Z (p(X,Y) and q(Y,Z)))", + "forall X Y Z (p(X,Y) and q(Y,Z))", + ), + ( + "forall X (forall Y (forall Z (X = Y = Z)))", + "forall X Y Z (X = Y = Z)", + ), + ] { + assert_eq!( + src.parse::() + .unwrap() + .apply(&mut join_nested_quantifiers), + target.parse().unwrap() + ) + } + } +} diff --git a/src/simplifying/fol/mod.rs b/src/simplifying/fol/mod.rs index 284456e7..a1162b6c 100644 --- a/src/simplifying/fol/mod.rs +++ b/src/simplifying/fol/mod.rs @@ -1,2 +1,3 @@ pub mod classic; pub mod ht; +pub mod intuitionistic; diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs index 41404a27..88019b73 100644 --- a/src/syntax_tree/fol.rs +++ b/src/syntax_tree/fol.rs @@ -11,7 +11,7 @@ use { TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, UserGuideEntryParser, UserGuideParser, VariableParser, }, - simplifying::fol::ht::join_nested_quantifiers, + simplifying::fol::intuitionistic::join_nested_quantifiers, syntax_tree::{impl_node, Node}, verifying::problem, }, diff --git a/src/verifying/task/strong_equivalence.rs b/src/verifying/task/strong_equivalence.rs index f3b5c00c..bfcfe2e3 100644 --- a/src/verifying/task/strong_equivalence.rs +++ b/src/verifying/task/strong_equivalence.rs @@ -66,8 +66,8 @@ impl Task for StrongEquivalenceTask { let mut right = tau_star(self.right); if self.simplify { - left = crate::simplifying::fol::ht::simplify(left); - right = crate::simplifying::fol::ht::simplify(right); + left = crate::simplifying::fol::intuitionistic::simplify(left); + right = crate::simplifying::fol::intuitionistic::simplify(right); } left = gamma(left); From ee98918b831bf34a161dee8954ec50c2a524c0b3 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 1 Feb 2025 01:39:14 +0100 Subject: [PATCH 11/12] Add remove_double_negation simplification --- src/simplifying/fol/classic.rs | 44 ++++++++++++++++++++++++++++++++-- 1 file changed, 42 insertions(+), 2 deletions(-) diff --git a/src/simplifying/fol/classic.rs b/src/simplifying/fol/classic.rs index 51bd44c9..49a44b55 100644 --- a/src/simplifying/fol/classic.rs +++ b/src/simplifying/fol/classic.rs @@ -1,6 +1,46 @@ -use crate::syntax_tree::fol::Theory; +use crate::{ + convenience::unbox::{fol::UnboxedFormula, Unbox as _}, + syntax_tree::fol::{Formula, Theory, UnaryConnective}, +}; pub fn simplify(theory: Theory) -> Theory { crate::simplifying::fol::ht::simplify(theory) - // TODO: Add classic simplifications + // TODO: Apply classic simplifications +} + +pub fn remove_double_negation(formula: Formula) -> Formula { + // Remove double negation + // e.g. not not F => F + + match formula.unbox() { + UnboxedFormula::UnaryFormula { + connective: UnaryConnective::Negation, + formula: + Formula::UnaryFormula { + connective: UnaryConnective::Negation, + formula: inner, + }, + } => *inner, + + x => x.rebox(), + } +} + +#[cfg(test)] +mod tests { + use { + super::remove_double_negation, + crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, + }; + + #[test] + fn test_eliminate_double_negation() { + assert_eq!( + "not not a" + .parse::() + .unwrap() + .apply(&mut remove_double_negation), + "a".parse().unwrap() + ) + } } From ceb4d0e3a463c5239c62a4c56b544716459054b0 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 1 Feb 2025 06:27:11 +0100 Subject: [PATCH 12/12] Split Apply in twain to enable portfolios of simplifications --- src/convenience/apply/mod.rs | 17 ----------------- src/convenience/compose/mod.rs | 23 +++++++++++++++++++++++ src/convenience/mod.rs | 1 + src/simplifying/fol/classic.rs | 18 +++++++++++++++--- src/simplifying/fol/ht.rs | 17 ++++++++++++++--- src/simplifying/fol/intuitionistic.rs | 27 +++++++++++++++------------ 6 files changed, 68 insertions(+), 35 deletions(-) create mode 100644 src/convenience/compose/mod.rs diff --git a/src/convenience/apply/mod.rs b/src/convenience/apply/mod.rs index 46496d35..8a4e754d 100644 --- a/src/convenience/apply/mod.rs +++ b/src/convenience/apply/mod.rs @@ -5,23 +5,6 @@ pub trait Apply { fn apply(self, f: &mut impl FnMut(Self) -> Self) -> Self where Self: Sized; - - /// Apply a series of operations `fs` in post-order to each node of a tree - /// - /// This function will traverse the tree only once. Whenever a node is visited, the first operation is applied first. - /// The remaining operations are also applied in this order. - fn apply_all(self, fs: &mut Vec Self>>) -> Self - where - Self: Sized, - { - let mut f = |mut node: Self| { - for fi in fs.iter_mut() { - node = fi(node); - } - node - }; - self.apply(&mut f) - } } impl Apply for Formula { diff --git a/src/convenience/compose/mod.rs b/src/convenience/compose/mod.rs new file mode 100644 index 00000000..4eefa1d9 --- /dev/null +++ b/src/convenience/compose/mod.rs @@ -0,0 +1,23 @@ +pub trait Compose { + fn compose(self) -> impl Fn(X) -> X; +} + +impl Compose for T +where + ::Item: Fn(X) -> X, +{ + /// Composes a series of operations `f0, f1, ..., fn` into single operation `f`. + /// + /// The operations are applied left-to-right, i.e. `f(x) = fn( .. f1( f0(x) ) .. )`. + fn compose(self) -> impl Fn(X) -> X { + // CAUTION: Cloning is absolutely crucial here. + // self is an Iterator that is moved into the closure and therefore + // returned from the function. It is used whenever the closure is + // called. If we do not clone the iterator, it will be empty after + // the first call which changes the intended behavior. Besides, + // cloning an Iterator is cheap since it is merely a view into the + // underlying data structure. The data structure itself is not + // cloned. + move |x| self.clone().fold(x, |x, f| f(x)) + } +} diff --git a/src/convenience/mod.rs b/src/convenience/mod.rs index ea89163d..5d045f50 100644 --- a/src/convenience/mod.rs +++ b/src/convenience/mod.rs @@ -1,3 +1,4 @@ pub mod apply; +pub mod compose; pub mod unbox; pub mod with_warnings; diff --git a/src/simplifying/fol/classic.rs b/src/simplifying/fol/classic.rs index 49a44b55..7deeb02a 100644 --- a/src/simplifying/fol/classic.rs +++ b/src/simplifying/fol/classic.rs @@ -1,13 +1,25 @@ use crate::{ - convenience::unbox::{fol::UnboxedFormula, Unbox as _}, + convenience::{ + apply::Apply as _, + compose::Compose as _, + unbox::{fol::UnboxedFormula, Unbox as _}, + }, + simplifying::fol::{ht::HT, intuitionistic::INTUITIONISTIC}, syntax_tree::fol::{Formula, Theory, UnaryConnective}, }; pub fn simplify(theory: Theory) -> Theory { - crate::simplifying::fol::ht::simplify(theory) - // TODO: Apply classic simplifications + Theory { + formulas: theory.formulas.into_iter().map(simplify_formula).collect(), + } +} + +pub fn simplify_formula(formula: Formula) -> Formula { + formula.apply(&mut INTUITIONISTIC.iter().chain(HT).chain(CLASSIC).compose()) } +pub const CLASSIC: &[fn(Formula) -> Formula] = &[remove_double_negation]; + pub fn remove_double_negation(formula: Formula) -> Formula { // Remove double negation // e.g. not not F => F diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index c1c68ca3..194d74b3 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -1,6 +1,17 @@ -use crate::syntax_tree::fol::Theory; +use crate::{ + convenience::{apply::Apply as _, compose::Compose as _}, + simplifying::fol::intuitionistic::INTUITIONISTIC, + syntax_tree::fol::{Formula, Theory}, +}; pub fn simplify(theory: Theory) -> Theory { - crate::simplifying::fol::intuitionistic::simplify(theory) - // TODO: Add ht simplifications + Theory { + formulas: theory.formulas.into_iter().map(simplify_formula).collect(), + } } + +pub fn simplify_formula(formula: Formula) -> Formula { + formula.apply(&mut INTUITIONISTIC.iter().chain(HT).compose()) +} + +pub const HT: &[fn(Formula) -> Formula] = &[]; diff --git a/src/simplifying/fol/intuitionistic.rs b/src/simplifying/fol/intuitionistic.rs index b62fb8ca..ca8a3a86 100644 --- a/src/simplifying/fol/intuitionistic.rs +++ b/src/simplifying/fol/intuitionistic.rs @@ -1,6 +1,7 @@ use crate::{ convenience::{ apply::Apply as _, + compose::Compose as _, unbox::{fol::UnboxedFormula, Unbox as _}, }, syntax_tree::fol::{ @@ -16,20 +17,22 @@ pub fn simplify(theory: Theory) -> Theory { } pub fn simplify_formula(formula: Formula) -> Formula { - formula.apply_all(&mut vec![ - Box::new(evaluate_comparisons), - Box::new(apply_negation_definition), - Box::new(apply_reverse_implication_definition), - Box::new(apply_equivalence_definition), - Box::new(remove_identities), - Box::new(remove_annihilations), - Box::new(remove_idempotences), - Box::new(remove_orphaned_variables), - Box::new(remove_empty_quantifications), - Box::new(join_nested_quantifiers), - ]) + formula.apply(&mut INTUITIONISTIC.iter().compose()) } +pub const INTUITIONISTIC: &[fn(Formula) -> Formula] = &[ + evaluate_comparisons, + apply_negation_definition, + apply_reverse_implication_definition, + apply_equivalence_definition, + remove_identities, + remove_annihilations, + remove_idempotences, + remove_orphaned_variables, + remove_empty_quantifications, + join_nested_quantifiers, +]; + pub fn evaluate_comparisons(formula: Formula) -> Formula { // Evaluate comparisons between structurally equal terms // e.g. T = T => #true