From 6a7f62932ed4594797704b1884d4750e0bc550da Mon Sep 17 00:00:00 2001 From: ZachJHansen Date: Sat, 7 Sep 2024 15:25:35 -0500 Subject: [PATCH 1/8] making simplifications public --- src/simplifying/fol/ht.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 31207bcc..62fdf25b 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -12,7 +12,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(remove_identities), Box::new(remove_annihilations), @@ -21,7 +21,7 @@ fn simplify_formula(formula: Formula) -> Formula { ]) } -fn remove_identities(formula: Formula) -> Formula { +pub fn remove_identities(formula: Formula) -> Formula { // Remove identities // e.g. F op E => F @@ -58,7 +58,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 @@ -95,7 +95,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 @@ -112,7 +112,7 @@ fn remove_idempotences(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 f0fb5c5c8e30dfad1f39b38c6e0e266eba056669 Mon Sep 17 00:00:00 2001 From: ZachJHansen Date: Sat, 7 Sep 2024 15:35:43 -0500 Subject: [PATCH 2/8] adding extend_quantifier_scope --- src/simplifying/fol/ht.rs | 124 +++++++++++++++++++++++++++++++++++++- 1 file changed, 121 insertions(+), 3 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 62fdf25b..98acfe5b 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -3,7 +3,7 @@ use crate::{ apply::Apply as _, unbox::{fol::UnboxedFormula, Unbox as _}, }, - syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Theory}, + syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Quantification, Theory}, }; pub fn simplify(theory: Theory) -> Theory { @@ -18,6 +18,7 @@ pub fn simplify_formula(formula: Formula) -> Formula { Box::new(remove_annihilations), Box::new(remove_idempotences), Box::new(join_nested_quantifiers), + Box::new(extend_quantifier_scope), ]) } @@ -138,12 +139,103 @@ pub fn join_nested_quantifiers(formula: Formula) -> Formula { } } +pub fn extend_quantifier_scope(formula: Formula) -> Formula { + match formula.clone().unbox() { + // Bring a conjunctive or disjunctive term into the scope of a quantifer + // e.g. exists X ( F(X) ) & G => exists X ( F(X) & G ) + // where X does not occur free in G + UnboxedFormula::BinaryFormula { + connective, + lhs: + Formula::QuantifiedFormula { + quantification: + Quantification { + quantifier, + variables, + }, + formula: f, + }, + rhs, + } => match connective { + BinaryConnective::Conjunction | BinaryConnective::Disjunction => { + let mut collision = false; + for var in variables.iter() { + if rhs.free_variables().contains(var) { + collision = true; + break; + } + } + + match collision { + true => formula, + false => Formula::QuantifiedFormula { + quantification: Quantification { + quantifier, + variables, + }, + formula: Formula::BinaryFormula { + connective, + lhs: f, + rhs: rhs.into(), + } + .into(), + }, + } + } + _ => formula, + }, + + UnboxedFormula::BinaryFormula { + connective, + lhs, + rhs: + Formula::QuantifiedFormula { + quantification: + Quantification { + quantifier, + variables, + }, + formula: f, + }, + } => match connective { + BinaryConnective::Conjunction | BinaryConnective::Disjunction => { + let mut collision = false; + for var in variables.iter() { + if lhs.free_variables().contains(var) { + collision = true; + break; + } + } + + match collision { + true => formula, + false => Formula::QuantifiedFormula { + quantification: Quantification { + quantifier, + variables, + }, + formula: Formula::BinaryFormula { + connective, + lhs: lhs.into(), + rhs: f, + } + .into(), + }, + } + } + _ => formula, + }, + + x => x.rebox(), + } +} + #[cfg(test)] mod tests { use { super::{ - join_nested_quantifiers, remove_annihilations, remove_idempotences, remove_identities, - simplify_formula, + extend_quantifier_scope, join_nested_quantifiers, remove_annihilations, + remove_idempotences, remove_identities, simplify_formula, }, crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, }; @@ -240,4 +332,30 @@ mod tests { ) } } + + #[test] + fn test_extend_quantification_scope() { + for (src, target) in [ + ( + "exists X (q(X) and 1 < 3) and p(Z)", + "exists X (q(X) and 1 < 3 and p(Z))", + ), + ( + "exists X (q(X) and 1 < 3) and p(X)", + "exists X (q(X) and 1 < 3) and p(X)", + ), + ( + "forall Z X (q(X) and 1 < Z) or p(Y,Z$)", + "forall Z X (q(X) and 1 < Z or p(Y,Z$))", + ), + ( + "p(Z) and exists X (q(X) and 1 < 3)", + "exists X (p(Z) and (q(X) and 1 < 3))", + ), + ] { + let result = extend_quantifier_scope(src.parse().unwrap()); + let target = target.parse().unwrap(); + assert_eq!(result, target, "{result} != {target}") + } + } } From 52fdc97f6cd9ee7152fc598e86a2c4724f44a8f9 Mon Sep 17 00:00:00 2001 From: ZachJHansen Date: Sat, 7 Sep 2024 15:45:41 -0500 Subject: [PATCH 3/8] adding cleanup simplifications --- src/simplifying/fol/ht.rs | 80 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 79 insertions(+), 1 deletion(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 98acfe5b..c7e36f75 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -19,6 +19,8 @@ pub fn simplify_formula(formula: Formula) -> Formula { Box::new(remove_idempotences), Box::new(join_nested_quantifiers), Box::new(extend_quantifier_scope), + Box::new(simplify_variable_lists), + Box::new(simplify_empty_quantifiers), ]) } @@ -230,12 +232,59 @@ pub fn extend_quantifier_scope(formula: Formula) -> Formula { } } +pub fn simplify_variable_lists(formula: Formula) -> Formula { + match formula.clone().unbox() { + // Removes variables from quantifiers when they do not occur in the quantified formula + // e.g. exists X Y ( q(Y) ) => exists Y ( q(Y) ) + UnboxedFormula::QuantifiedFormula { + quantification: + Quantification { + mut variables, + quantifier, + }, + formula, + } => { + let fvars = formula.variables(); + variables.retain(|x| fvars.contains(x)); + Formula::QuantifiedFormula { + quantification: Quantification { + variables, + quantifier, + }, + formula: formula.into(), + } + } + + x => x.rebox(), + } +} + +pub fn simplify_empty_quantifiers(formula: Formula) -> Formula { + match formula.clone().unbox() { + // Remove quantifiers with no variables + // e.g. exists ( F ) => F + UnboxedFormula::QuantifiedFormula { + quantification: Quantification { variables, .. }, + formula: f, + } => { + if variables.is_empty() { + f + } else { + formula + } + } + + x => x.rebox(), + } +} + #[cfg(test)] mod tests { use { super::{ extend_quantifier_scope, join_nested_quantifiers, remove_annihilations, - remove_idempotences, remove_identities, simplify_formula, + remove_idempotences, remove_identities, simplify_empty_quantifiers, simplify_formula, + simplify_variable_lists, }, crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, }; @@ -358,4 +407,33 @@ mod tests { assert_eq!(result, target, "{result} != {target}") } } + + #[test] + fn test_simplify_variable_lists() { + for (src, target) in [ + ( + "exists X Y ( q or (t and q(Y)))", + "exists Y ( q or (t and q(Y)))", + ), + ( + "exists Y V ( q or forall X (t(Y) and q(X)))", + "exists Y ( q or forall X (t(Y) and q(X)))", + ), + ] { + assert_eq!( + simplify_variable_lists(src.parse().unwrap()), + target.parse().unwrap() + ) + } + } + + #[test] + fn test_simplify_empty_quantifiers() { + for (src, target) in [("exists Y (1 < 2)", "1 < 2"), ("forall Z #true", "#true")] { + assert_eq!( + simplify_empty_quantifiers(simplify_variable_lists(src.parse().unwrap())), + target.parse().unwrap() + ) + } + } } From 6a6632fb5e1751597a4b4cc1fac0efcda3e3b087 Mon Sep 17 00:00:00 2001 From: ZachJHansen Date: Sat, 7 Sep 2024 16:12:58 -0500 Subject: [PATCH 4/8] Adding restrict_quantifier_domain simplification --- src/convenience/mod.rs | 36 +++++++ src/simplifying/fol/ht.rs | 195 +++++++++++++++++++++++++++++++++++-- src/simplifying/fol/mod.rs | 79 +++++++++++++++ src/syntax_tree/fol.rs | 24 +++++ 4 files changed, 328 insertions(+), 6 deletions(-) diff --git a/src/convenience/mod.rs b/src/convenience/mod.rs index ea89163d..15328641 100644 --- a/src/convenience/mod.rs +++ b/src/convenience/mod.rs @@ -1,3 +1,39 @@ pub mod apply; pub mod unbox; pub mod with_warnings; + +use {crate::syntax_tree::fol, indexmap::IndexSet}; + +/// Choose `arity` variable names by incrementing `variant`, disjoint from `variables` +pub fn choose_fresh_variable_names( + variables: &IndexSet, + variant: &str, + arity: usize, +) -> Vec { + let mut taken_vars = Vec::::new(); + for var in variables.iter() { + taken_vars.push(var.name.to_string()); + } + let mut fresh_vars = Vec::::new(); + let arity_bound = match taken_vars.contains(&variant.to_string()) { + true => arity + 1, + false => { + fresh_vars.push(variant.to_string()); + arity + } + }; + for n in 1..arity_bound { + let mut candidate: String = variant.to_owned(); + let number: &str = &n.to_string(); + candidate.push_str(number); + let mut m = n; + while taken_vars.contains(&candidate) || fresh_vars.contains(&candidate) { + variant.clone_into(&mut candidate); + m += 1; + let number = &m.to_string(); + candidate.push_str(number); + } + fresh_vars.push(candidate.to_string()); + } + fresh_vars +} diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index c7e36f75..4dc54fb7 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -1,9 +1,14 @@ -use crate::{ - convenience::{ - apply::Apply as _, - unbox::{fol::UnboxedFormula, Unbox as _}, +use { + super::replacement_helper, + crate::{ + convenience::{ + apply::Apply as _, + unbox::{fol::UnboxedFormula, Unbox as _}, + }, + syntax_tree::fol::{ + AtomicFormula, BinaryConnective, Formula, Quantification, Quantifier, Sort, Theory, + }, }, - syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Quantification, Theory}, }; pub fn simplify(theory: Theory) -> Theory { @@ -278,6 +283,137 @@ pub fn simplify_empty_quantifiers(formula: Formula) -> Formula { } } +pub fn restrict_quantifier_domain(formula: Formula) -> Formula { + let mut simplified_formula = formula.clone(); + match formula.clone().unbox() { + // Replace a general variable in an outer quantification with a fresh integer variable capturing an inner quantification + // e.g. exists Z$g (exists I$i J$i (I$i = Z$g & G) & H) => exists K$i (exists I$i J$i (I$i = K$i & G) & H) + // or forall Z$g (exists I$i J$i (I$i = Z$g & G) -> H) => forall K$i (exists I$i J$i (I$i = K$i & G) -> H) + UnboxedFormula::QuantifiedFormula { + quantification: + Quantification { + quantifier: Quantifier::Exists, + variables: outer_vars, + }, + formula: + Formula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs, + rhs, + }, + } => { + let mut replaced = false; + let mut conjunctive_terms = Formula::conjoin_invert(*lhs); + conjunctive_terms.extend(Formula::conjoin_invert(*rhs)); + for ct in conjunctive_terms.iter() { + if let Formula::QuantifiedFormula { + quantification: + Quantification { + quantifier: Quantifier::Exists, + variables: inner_vars, + }, + formula: inner_formula, + } = ct + { + let inner_ct = Formula::conjoin_invert(*inner_formula.clone()); + for ict in inner_ct.iter() { + if let Formula::AtomicFormula(AtomicFormula::Comparison(comp)) = ict { + if comp.equality_comparison() { + for ovar in outer_vars.iter() { + for ivar in inner_vars.iter() { + if ovar.sort == Sort::General && ivar.sort == Sort::Integer + { + let replacement_result = + replacement_helper(ivar, ovar, comp, &formula); + + if replacement_result.1 { + simplified_formula = replacement_result.0; + replaced = true; + break; + } + } + } + if replaced { + break; + } + } + } + if replaced { + break; + } + } + } + } + if replaced { + break; + } + } + } + + UnboxedFormula::QuantifiedFormula { + quantification: + Quantification { + quantifier: Quantifier::Forall, + variables: outer_vars, + }, + formula: + Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs, + rhs, + }, + } => match lhs.unbox() { + UnboxedFormula::QuantifiedFormula { + quantification: + Quantification { + quantifier: Quantifier::Exists, + variables: inner_vars, + }, + formula: inner_formula, + } => { + let mut replaced = false; + let conjunctive_terms = Formula::conjoin_invert(inner_formula); + for ct in conjunctive_terms.iter() { + if let Formula::AtomicFormula(AtomicFormula::Comparison(comp)) = ct { + if comp.equality_comparison() { + for ovar in outer_vars.iter() { + for ivar in inner_vars.iter() { + if ovar.sort == Sort::General + && ivar.sort == Sort::Integer + && !rhs.free_variables().contains(ovar) + { + let replacement_result = + replacement_helper(ivar, ovar, comp, &formula); + if replacement_result.1 { + simplified_formula = replacement_result.0; + replaced = true; + break; + } + } + if replaced { + break; + } + } + } + if replaced { + break; + } + } + } + if replaced { + break; + } + } + } + + _ => (), + }, + + _ => (), + } + simplified_formula +} + #[cfg(test)] mod tests { use { @@ -286,7 +422,7 @@ mod tests { remove_idempotences, remove_identities, simplify_empty_quantifiers, simplify_formula, simplify_variable_lists, }, - crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, + crate::{convenience::apply::Apply as _, simplifying::fol::ht::restrict_quantifier_domain, syntax_tree::fol::Formula}, }; #[test] @@ -436,4 +572,51 @@ mod tests { ) } } + + #[test] + fn test_restrict_quantifiers() { + for (src, target) in [ + ( + "exists Z Z1 ( exists I$i J$i ( Z = J$i and q(I$i, J$i) ) and Z = Z1 )", + "exists Z1 J1$i ( exists I$i J$i ( J1$i = J$i and q(I$i, J$i) ) and J1$i = Z1 )", + ), + ( + "exists Z Z1 ( exists I$i J$i ( q(I$i, J$i) and Z = J$i) and Z = Z1 )", + "exists Z1 J1$i ( exists I$i J$i ( q(I$i, J$i) and J1$i = J$i) and J1$i = Z1 )", + ), + ( + "exists Z Z1 ( Z = Z1 and exists I$i J$i ( q(I$i, J$i) and Z = J$i) )", + "exists Z1 J1$i ( J1$i = Z1 and exists I$i J$i ( q(I$i, J$i) and J1$i = J$i) )", + ), + ( + "exists Z Z1 ( Z = Z1 and exists I$i J$i ( q(I$i, J$i) and Z = J$i and 3 > 2) and 1 < 5 )", + "exists Z1 J1$i ( J1$i = Z1 and exists I$i J$i ( q(I$i, J$i) and J1$i = J$i and 3 > 2) and 1 < 5 )", + ), + ( + "forall X Y ( exists Z I$i (p(X) and p(Z) and Y = I$i) -> q(X) )", + "forall X I1$i ( exists Z I$i (p(X) and p(Z) and I1$i = I$i) -> q(X) )", + ), + ( + "forall X Y ( exists Z I$i (p(X) and p(Z) and Y = I$i) -> q(Y) )", + "forall X Y ( exists Z I$i (p(X) and p(Z) and Y = I$i) -> q(Y) )", + ), + ( + "forall X Y ( exists I$i J$i (Y = J$i and p(I$i, J$i) and I$i = X) -> q(Z) )", + "forall X J1$i ( exists I$i J$i (J1$i = J$i and p(I$i, J$i) and I$i = X) -> q(Z) )", + ), + ( + "forall X Y ( exists Z I$i (p(X,Z) or Y = I$i) -> q(X) )", + "forall X Y ( exists Z I$i (p(X,Z) or Y = I$i) -> q(X) )", + ), + ( + "forall X Y ( exists Z I$i (p(X,Z) and I$i = X) -> exists A X (q(A,X)) )", + "forall Y I1$i ( exists Z I$i (p(I1$i,Z) and I$i = I1$i) -> exists A X (q(A,X)) )", + ), + ] { + let src = + restrict_quantifier_domain(src.parse().unwrap()); + let target = target.parse().unwrap(); + assert_eq!(src, target, "{src} != {target}") + } + } } diff --git a/src/simplifying/fol/mod.rs b/src/simplifying/fol/mod.rs index 284456e7..832a9b45 100644 --- a/src/simplifying/fol/mod.rs +++ b/src/simplifying/fol/mod.rs @@ -1,2 +1,81 @@ pub mod classic; pub mod ht; + +use crate::syntax_tree::fol::{ + Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Relation, Sort, Variable, +}; + +use crate::convenience::choose_fresh_variable_names; + +// ASSUMES ivar is an integer variable and ovar is a general variable +// This function checks if the comparison `ivar = ovar` or `ovar = ivar` matches the comparison `comp` +// If so, it replaces ovar with a fresh integer variable within `formula` +// Otherwise it returns `formula` +fn replacement_helper( + ivar: &Variable, + ovar: &Variable, + comp: &Comparison, + formula: &Formula, +) -> (Formula, bool) { + let mut simplified_formula = formula.clone(); + let ivar_term = GeneralTerm::IntegerTerm(IntegerTerm::Variable(ivar.name.clone())); + let candidate = Comparison { + term: GeneralTerm::Variable(ovar.name.clone()), + guards: vec![Guard { + relation: Relation::Equal, + term: ivar_term.clone(), + }], + }; + let mut replace = false; + if comp == &candidate { + replace = true; + } else { + let candidate = Comparison { + term: ivar_term.clone(), + guards: vec![Guard { + relation: Relation::Equal, + term: GeneralTerm::Variable(ovar.name.clone()), + }], + }; + if comp == &candidate { + replace = true; + } + } + + if replace { + let varnames = choose_fresh_variable_names( + &formula.variables(), + &ivar.name.chars().next().unwrap().to_string(), + 1, + ); + let fvar = varnames[0].clone(); + let fvar_term = GeneralTerm::IntegerTerm(IntegerTerm::Variable(fvar.clone())); + match formula.clone() { + Formula::QuantifiedFormula { + quantification: + Quantification { + quantifier, + mut variables, + }, + formula: f, + } => { + variables.retain(|x| x != ovar); // Drop ovar from the outer quantification, leaving ovar free within formula + variables.push(Variable { + // Add the new integer variable to replace ovar + name: fvar, + sort: Sort::Integer, + }); + simplified_formula = Formula::QuantifiedFormula { + quantification: Quantification { + quantifier: quantifier.clone(), + variables, + }, + formula: f.substitute(ovar.clone(), fvar_term).into(), // Replace all free occurences of ovar with fvar_term + }; + } + + _ => panic!("You are using the replacement helper function wrong"), + } + } + (simplified_formula, replace) +} diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs index c501ecbd..bc551a02 100644 --- a/src/syntax_tree/fol.rs +++ b/src/syntax_tree/fol.rs @@ -419,6 +419,12 @@ impl Comparison { .collect(), } } + + pub fn equality_comparison(&self) -> bool { + let guards = &self.guards; + let first = &guards[0]; + guards.len() == 1 && first.relation == Relation::Equal + } } #[derive(Clone, Debug, Eq, PartialEq, Hash)] @@ -668,6 +674,24 @@ impl Formula { .unwrap_or_else(|| Formula::AtomicFormula(AtomicFormula::Truth)) } + /// Inverse function to conjoin + pub fn conjoin_invert(formula: Formula) -> Vec { + match formula { + Formula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs, + rhs, + } => { + let mut formulas = Self::conjoin_invert(*lhs); + formulas.append(&mut Self::conjoin_invert(*rhs)); + formulas + } + _ => { + vec![formula] + } + } + } + /// Recursively turn a list of formulas into a tree of disjunctions pub fn disjoin(formulas: impl IntoIterator) -> Formula { /* From b13f0005483852d76dea981712bc3e90c3f66ed6 Mon Sep 17 00:00:00 2001 From: ZachJHansen Date: Sat, 7 Sep 2024 16:19:28 -0500 Subject: [PATCH 5/8] appeasing clippy --- src/simplifying/fol/ht.rs | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 4dc54fb7..4ad2ff8e 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -362,15 +362,16 @@ pub fn restrict_quantifier_domain(formula: Formula) -> Formula { lhs, rhs, }, - } => match lhs.unbox() { - UnboxedFormula::QuantifiedFormula { + } => { + if let UnboxedFormula::QuantifiedFormula { quantification: Quantification { quantifier: Quantifier::Exists, variables: inner_vars, }, formula: inner_formula, - } => { + } = lhs.unbox() + { let mut replaced = false; let conjunctive_terms = Formula::conjoin_invert(inner_formula); for ct in conjunctive_terms.iter() { @@ -405,9 +406,7 @@ pub fn restrict_quantifier_domain(formula: Formula) -> Formula { } } } - - _ => (), - }, + } _ => (), } @@ -422,7 +421,10 @@ mod tests { remove_idempotences, remove_identities, simplify_empty_quantifiers, simplify_formula, simplify_variable_lists, }, - crate::{convenience::apply::Apply as _, simplifying::fol::ht::restrict_quantifier_domain, syntax_tree::fol::Formula}, + crate::{ + convenience::apply::Apply as _, simplifying::fol::ht::restrict_quantifier_domain, + syntax_tree::fol::Formula, + }, }; #[test] From 5568d7e5187281ef9ab9f8b3de511e5d623446ac Mon Sep 17 00:00:00 2001 From: ZachJHansen Date: Sat, 7 Sep 2024 16:21:42 -0500 Subject: [PATCH 6/8] cleaning up --- src/simplifying/fol/ht.rs | 1 + src/translating/tau_star.rs | 39 ++++--------------------------------- 2 files changed, 5 insertions(+), 35 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 4ad2ff8e..a7a41e5e 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -24,6 +24,7 @@ pub fn simplify_formula(formula: Formula) -> Formula { Box::new(remove_idempotences), Box::new(join_nested_quantifiers), Box::new(extend_quantifier_scope), + Box::new(restrict_quantifier_domain), Box::new(simplify_variable_lists), Box::new(simplify_empty_quantifiers), ]) diff --git a/src/translating/tau_star.rs b/src/translating/tau_star.rs index 5510dbf4..62f07b65 100644 --- a/src/translating/tau_star.rs +++ b/src/translating/tau_star.rs @@ -1,5 +1,8 @@ use { - crate::syntax_tree::{asp, fol}, + crate::{ + convenience::choose_fresh_variable_names, + syntax_tree::{asp, fol}, + }, indexmap::IndexSet, lazy_static::lazy_static, regex::Regex, @@ -39,40 +42,6 @@ fn choose_fresh_global_variables(program: &asp::Program) -> Vec { globals } -/// Choose `arity` variable names by incrementing `variant`, disjoint from `variables` -fn choose_fresh_variable_names( - variables: &IndexSet, - variant: &str, - arity: usize, -) -> Vec { - let mut taken_vars = Vec::::new(); - for var in variables.iter() { - taken_vars.push(var.name.to_string()); - } - let mut fresh_vars = Vec::::new(); - let arity_bound = match taken_vars.contains(&variant.to_string()) { - true => arity + 1, - false => { - fresh_vars.push(variant.to_string()); - arity - } - }; - for n in 1..arity_bound { - let mut candidate: String = variant.to_owned(); - let number: &str = &n.to_string(); - candidate.push_str(number); - let mut m = n; - while taken_vars.contains(&candidate) || fresh_vars.contains(&candidate) { - variant.clone_into(&mut candidate); - m += 1; - let number = &m.to_string(); - candidate.push_str(number); - } - fresh_vars.push(candidate.to_string()); - } - fresh_vars -} - // Z = t fn construct_equality_formula(term: asp::Term, z: fol::Variable) -> fol::Formula { let z_var_term = match z.sort { From 67b971cd755863a1db1c628c3cd88c622d4a1964 Mon Sep 17 00:00:00 2001 From: ZachJHansen Date: Sat, 7 Sep 2024 16:32:16 -0500 Subject: [PATCH 7/8] adding eliminate_redundant_quantifiers --- src/simplifying/fol/ht.rs | 119 ++++++++++++++++++++++- src/simplifying/fol/mod.rs | 187 ++++++++++++++++++++++++++++++++++++- src/syntax_tree/fol.rs | 21 +++++ 3 files changed, 319 insertions(+), 8 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index a7a41e5e..0f0acd29 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -1,5 +1,5 @@ use { - super::replacement_helper, + super::{replacement_helper, simplify_conjunction_tree_with_equality}, crate::{ convenience::{ apply::Apply as _, @@ -414,13 +414,100 @@ pub fn restrict_quantifier_domain(formula: Formula) -> Formula { simplified_formula } +pub fn eliminate_redundant_quantifiers(formula: Formula) -> Formula { + match formula.clone().unbox() { + // Remove redundant existentials + // e.g. exists Z$g (Z$g = X$g and F(Z$g)) => F(X$g) + UnboxedFormula::QuantifiedFormula { + quantification: + Quantification { + quantifier: Quantifier::Exists, + mut variables, + }, + formula: f, + } => match f.clone().unbox() { + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + .. + } => { + let simplification_result = + simplify_conjunction_tree_with_equality(f, variables.clone()); + match simplification_result.1 { + Some(sub_pair) => { + variables.retain(|v| v != &sub_pair.0); + Formula::QuantifiedFormula { + quantification: Quantification { + quantifier: Quantifier::Exists, + variables, + }, + formula: simplification_result.0.into(), + } + } + None => formula, + } + } + _ => formula, + }, + + // A universally quantified implication can sometimes be simplified + // e.g. forall X1 .. Xj .. Xn (F1 and .. Fi .. and Fm -> G), where Fi is Xj=t, and Xj doesn’t occur in t, and free variables occurring in t are not bound by quantifiers in F1, F2, .. + // becomes forall X1 .. Xn (F1 and .. and Fm -> G) + UnboxedFormula::QuantifiedFormula { + quantification: + Quantification { + quantifier: Quantifier::Forall, + mut variables, + }, + formula: + Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs, + rhs, + }, + } => match lhs.clone().unbox() { + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + .. + } => { + let mut f = formula; + let lhs_simplify = simplify_conjunction_tree_with_equality(*lhs, variables.clone()); + match lhs_simplify.1 { + Some(sub_pair) => { + if !rhs.clone().unsafe_substitution(&sub_pair.0, &sub_pair.1) { + variables.retain(|v| v != &sub_pair.0); + f = Formula::QuantifiedFormula { + quantification: Quantification { + quantifier: Quantifier::Forall, + variables, + }, + formula: Formula::BinaryFormula { + connective: BinaryConnective::Implication, + lhs: lhs_simplify.0.into(), + rhs: rhs.substitute(sub_pair.0, sub_pair.1).into(), + } + .into(), + }; + } + f + } + None => f, + } + } + + _ => formula, + }, + + _ => formula, + } +} + #[cfg(test)] mod tests { use { super::{ - extend_quantifier_scope, join_nested_quantifiers, remove_annihilations, - remove_idempotences, remove_identities, simplify_empty_quantifiers, simplify_formula, - simplify_variable_lists, + eliminate_redundant_quantifiers, extend_quantifier_scope, join_nested_quantifiers, + remove_annihilations, remove_idempotences, remove_identities, + simplify_empty_quantifiers, simplify_formula, simplify_variable_lists, }, crate::{ convenience::apply::Apply as _, simplifying::fol::ht::restrict_quantifier_domain, @@ -622,4 +709,28 @@ mod tests { assert_eq!(src, target, "{src} != {target}") } } + + #[test] + fn test_eliminate_redundant_quantifiers() { + for (src, target) in [ + ("exists X ( X = Z and not q(X) )", "not q(Z)"), + ( + "exists Y ( Y = X and forall V (p(Y,V) -> q(X)) )", + "forall V (p(X,V) -> q(X))", + ), + ( + "exists Z Z1 ( Z = I and (exists K$i (K$i = I) and Z = Z1) )", + "exists Z1 ( exists K$i (K$i = I) and I = Z1)", + ), + ( + "forall X V (p(X) and X = V -> q(V))", + "forall V (p(V) -> q(V))", + ), + ] { + let src = + simplify_empty_quantifiers(eliminate_redundant_quantifiers(src.parse().unwrap())); + let target = target.parse().unwrap(); + assert_eq!(src, target, "{src} != {target}") + } + } } diff --git a/src/simplifying/fol/mod.rs b/src/simplifying/fol/mod.rs index 832a9b45..dfc75765 100644 --- a/src/simplifying/fol/mod.rs +++ b/src/simplifying/fol/mod.rs @@ -1,12 +1,17 @@ pub mod classic; pub mod ht; -use crate::syntax_tree::fol::{ - Comparison, Formula, GeneralTerm, Guard, IntegerTerm, Quantification, Relation, Sort, Variable, +use crate::{ + convenience::{ + choose_fresh_variable_names, + unbox::{fol::UnboxedFormula, Unbox as _}, + }, + syntax_tree::fol::{ + AtomicFormula, BinaryConnective, Comparison, Formula, GeneralTerm, Guard, IntegerTerm, + Quantification, Relation, Sort, SymbolicTerm, Variable, + }, }; -use crate::convenience::choose_fresh_variable_names; - // ASSUMES ivar is an integer variable and ovar is a general variable // This function checks if the comparison `ivar = ovar` or `ovar = ivar` matches the comparison `comp` // If so, it replaces ovar with a fresh integer variable within `formula` @@ -79,3 +84,177 @@ fn replacement_helper( } (simplified_formula, replace) } + +// ASSUMES formula has the form: +// F(var) & var = term OR +// F(var) & term = var +// If var is a variable of sort S and term is a term of a subsort of S, +// and term doesn't contain variables quantified within F, return `F(term)` +// Otherwise, return the original formula +fn subsort_equality(var: Variable, term: GeneralTerm, formula: Formula) -> (Formula, bool) { + let mut modified = false; + let mut simplified_formula = formula.clone(); + match formula.clone().unbox() { + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + lhs, + .. + } => { + let term_vars = term.variables(); // term must not contain var + match var.sort { + Sort::General => { + if !term_vars.contains(&var) && !lhs.clone().unsafe_substitution(&var, &term) { + modified = true; + simplified_formula = lhs.substitute(var, term); + } + } + Sort::Integer => match term.clone() { + GeneralTerm::IntegerTerm(_) => { + if !term_vars.contains(&var) + && !lhs.clone().unsafe_substitution(&var, &term) + { + modified = true; + simplified_formula = lhs.substitute(var, term); + } + } + _ => { + simplified_formula = formula; + } + }, + Sort::Symbol => match term.clone() { + GeneralTerm::SymbolicTerm(_) => { + if !term_vars.contains(&var) + && !lhs.clone().unsafe_substitution(&var, &term) + { + modified = true; + simplified_formula = lhs.substitute(var, term); + } + } + _ => { + simplified_formula = formula; + } + }, + } + } + + _ => panic!("you're using the subsort equality fn wrong"), + } + (simplified_formula, modified) +} + +// Given a tree of conjunctions, F1, .. Fi, .. Fn, identify an equality formula Fi: X = t or t = X +// If possible, substitute t for X within the tree and drop Fi +// Return the original formula and None if not possible +// Otherwise, return the simplified formula and the (X, t) substitution pair +fn simplify_conjunction_tree_with_equality( + formula: Formula, + enclosing_variables: Vec, +) -> (Formula, Option<(Variable, GeneralTerm)>) { + let mut result = (formula.clone(), None); + let conjunctive_terms = Formula::conjoin_invert(formula.clone()); + for ct in conjunctive_terms.iter() { + // Search for an equality formula + if let Formula::AtomicFormula(AtomicFormula::Comparison(comp)) = ct { + if comp.equality_comparison() { + let term = &comp.term; + let g = comp.guards[0].clone(); + let lhs_is_var = match term.clone() { + GeneralTerm::Variable(v) => Some(Variable { + sort: Sort::General, + name: v, + }), + GeneralTerm::IntegerTerm(IntegerTerm::Variable(v)) => Some(Variable { + sort: Sort::Integer, + name: v, + }), + GeneralTerm::SymbolicTerm(SymbolicTerm::Variable(v)) => Some(Variable { + sort: Sort::Symbol, + name: v, + }), + _ => None, + }; + let rhs_is_var = match g.term.clone() { + GeneralTerm::Variable(v) => Some(Variable { + sort: Sort::General, + name: v, + }), + GeneralTerm::IntegerTerm(IntegerTerm::Variable(v)) => Some(Variable { + sort: Sort::Integer, + name: v, + }), + GeneralTerm::SymbolicTerm(SymbolicTerm::Variable(v)) => Some(Variable { + sort: Sort::Symbol, + name: v, + }), + _ => None, + }; + + let mut safety = true; // Simplify var = term or term = var but not both + // Don't restructure the conjunction tree unless simplification occurs + let mut restructured = vec![]; // Make the equality formula the top rhs leaf of a new conjunction tree + // for i in 0..conjunctive_terms.len() { + // if conjunctive_terms[i] != *ct { + // restructured.push(conjunctive_terms[i].clone()); + // } + // } + for alt_ct in conjunctive_terms.clone() { + if alt_ct != *ct { + restructured.push(alt_ct); + } + } + restructured.push(ct.clone()); + + let simplified = Formula::conjoin(restructured); + + if let Some(v1) = lhs_is_var { + if enclosing_variables.contains(&v1) { + let simplification_result = + subsort_equality(v1.clone(), g.term.clone(), simplified.clone()); + if simplification_result.1 { + result = (simplification_result.0, Some((v1, g.term))); + safety = false; + } + } + } + if let Some(v2) = rhs_is_var { + if enclosing_variables.contains(&v2) && safety { + let simplification_result = + subsort_equality(v2.clone(), term.clone(), simplified); + if simplification_result.1 { + result = (simplification_result.0, Some((v2, term.clone()))); + safety = false; + } + } + } + if !safety { + break; + } + } + } + } + result +} + +#[test] +fn test_simplify_conjunction_tree() { + for (src, target) in [( + ( + "X = Z and not q(X)", + vec![ + Variable { + name: "X".to_string(), + sort: Sort::General, + }, + Variable { + name: "Y".to_string(), + sort: Sort::General, + }, + ], + ), + "not q(Z)", + )] { + let result = simplify_conjunction_tree_with_equality(src.0.parse().unwrap(), src.1).0; + let target = target.parse().unwrap(); + assert_eq!(result, target, "{result} != {target}") + } +} diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs index bc551a02..53d471f4 100644 --- a/src/syntax_tree/fol.rs +++ b/src/syntax_tree/fol.rs @@ -825,6 +825,27 @@ impl Formula { } } + // Replacing var with term within self is unsafe if self contains a subformula + // of the form QxF, where var is free in F and a variable in term occurs in x + pub fn unsafe_substitution(self, var: &Variable, term: &GeneralTerm) -> bool { + match self { + Formula::AtomicFormula(_) => false, + Formula::UnaryFormula { formula, .. } => formula.unsafe_substitution(var, term), + Formula::BinaryFormula { lhs, rhs, .. } => { + lhs.unsafe_substitution(var, term) || rhs.unsafe_substitution(var, term) + } + Formula::QuantifiedFormula { + quantification, + formula, + } => { + let tvars = term.variables(); + let qvars: IndexSet = IndexSet::from_iter(quantification.variables); + let overlap: IndexSet<&Variable> = tvars.intersection(&qvars).collect(); + formula.free_variables().contains(var) && !overlap.is_empty() + } + } + } + pub fn quantify(self, quantifier: Quantifier, variables: Vec) -> Formula { if variables.is_empty() { self From 5ebb388fd53a0904a83687b6eb9fe5cd56e24521 Mon Sep 17 00:00:00 2001 From: ZachJHansen Date: Sat, 7 Sep 2024 16:41:41 -0500 Subject: [PATCH 8/8] add simplify_transitive_equality --- src/convenience/mod.rs | 18 ++++++ src/simplifying/fol/ht.rs | 113 +++++++++++++++++++++++++++++++- src/simplifying/fol/mod.rs | 128 ++++++++++++++++++++++++++++++++++++- 3 files changed, 255 insertions(+), 4 deletions(-) diff --git a/src/convenience/mod.rs b/src/convenience/mod.rs index 15328641..3756831e 100644 --- a/src/convenience/mod.rs +++ b/src/convenience/mod.rs @@ -4,6 +4,24 @@ pub mod with_warnings; use {crate::syntax_tree::fol, indexmap::IndexSet}; +/// True if v1 is subsorteq to v2 and False otherwise +pub fn subsort(v1: &fol::Variable, v2: &fol::Variable) -> bool { + match v1.sort { + fol::Sort::General => match v2.sort { + fol::Sort::General => true, + fol::Sort::Integer | fol::Sort::Symbol => false, + }, + fol::Sort::Integer => match v2.sort { + fol::Sort::General | fol::Sort::Integer => true, + fol::Sort::Symbol => false, + }, + fol::Sort::Symbol => match v2.sort { + fol::Sort::General | fol::Sort::Symbol => true, + fol::Sort::Integer => false, + }, + } +} + /// Choose `arity` variable names by incrementing `variant`, disjoint from `variables` pub fn choose_fresh_variable_names( variables: &IndexSet, diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 0f0acd29..00d493ba 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -1,12 +1,13 @@ use { - super::{replacement_helper, simplify_conjunction_tree_with_equality}, + super::{replacement_helper, simplify_conjunction_tree_with_equality, transitive_equality}, crate::{ convenience::{ apply::Apply as _, unbox::{fol::UnboxedFormula, Unbox as _}, }, syntax_tree::fol::{ - AtomicFormula, BinaryConnective, Formula, Quantification, Quantifier, Sort, Theory, + AtomicFormula, BinaryConnective, Formula, GeneralTerm, IntegerTerm, Quantification, + Quantifier, Sort, SymbolicTerm, Theory, }, }, }; @@ -25,6 +26,11 @@ pub fn simplify_formula(formula: Formula) -> Formula { Box::new(join_nested_quantifiers), Box::new(extend_quantifier_scope), Box::new(restrict_quantifier_domain), + // cleanup + Box::new(simplify_variable_lists), + Box::new(simplify_empty_quantifiers), + Box::new(simplify_transitive_equality), + // cleanup Box::new(simplify_variable_lists), Box::new(simplify_empty_quantifiers), ]) @@ -501,13 +507,102 @@ pub fn eliminate_redundant_quantifiers(formula: Formula) -> Formula { } } +pub fn simplify_transitive_equality(formula: Formula) -> Formula { + match formula.clone().unbox() { + // When X is a subsort of Y (or sort(X) = sort(Y)) and t is a term: + // exists X Y (X = t and Y = t and F) + // => + // exists X (X = t and F(X)) + // Replace Y with X within F + UnboxedFormula::QuantifiedFormula { + quantification: + Quantification { + quantifier: Quantifier::Exists, + mut variables, + }, + formula: f, + } => match f.clone().unbox() { + UnboxedFormula::BinaryFormula { + connective: BinaryConnective::Conjunction, + .. + } => { + let mut simplified = formula.clone(); + let mut simplify = false; + let conjunctive_terms = Formula::conjoin_invert(f.clone()); + let mut ct_copy = conjunctive_terms.clone(); + for (i, ct1) in conjunctive_terms.iter().enumerate() { + // Search for an equality formula + if let Formula::AtomicFormula(AtomicFormula::Comparison(c1)) = ct1 { + if c1.equality_comparison() { + for (j, ct2) in conjunctive_terms.iter().enumerate() { + // Search for a second equality formula + if let Formula::AtomicFormula(AtomicFormula::Comparison(c2)) = ct2 { + if c2.equality_comparison() && i != j { + if let Some((keep_var, drop_var, drop_term)) = + transitive_equality( + c1.clone(), + c2.clone(), + variables.clone(), + ) + { + variables.retain(|x| x != &drop_var); + ct_copy.retain(|t| { + t != &Formula::AtomicFormula( + AtomicFormula::Comparison(drop_term.clone()), + ) + }); + let keep = match keep_var.sort { + Sort::General => { + GeneralTerm::Variable(keep_var.name) + } + Sort::Integer => GeneralTerm::IntegerTerm( + IntegerTerm::Variable(keep_var.name), + ), + Sort::Symbol => GeneralTerm::SymbolicTerm( + SymbolicTerm::Variable(keep_var.name), + ), + }; + let inner = Formula::conjoin(ct_copy.clone()) + .substitute(drop_var, keep); + simplified = Formula::QuantifiedFormula { + quantification: Quantification { + quantifier: Quantifier::Exists, + variables: variables.clone(), + }, + formula: inner.into(), + }; + simplify = true; + } + } + } + if simplify { + break; + } + } + } + } + if simplify { + break; + } + } + simplified + } + + _ => formula, + }, + + x => x.rebox(), + } +} + #[cfg(test)] mod tests { use { super::{ eliminate_redundant_quantifiers, extend_quantifier_scope, join_nested_quantifiers, remove_annihilations, remove_idempotences, remove_identities, - simplify_empty_quantifiers, simplify_formula, simplify_variable_lists, + simplify_empty_quantifiers, simplify_formula, simplify_transitive_equality, + simplify_variable_lists, }, crate::{ convenience::apply::Apply as _, simplifying::fol::ht::restrict_quantifier_domain, @@ -733,4 +828,16 @@ mod tests { assert_eq!(src, target, "{src} != {target}") } } + + #[test] + fn test_simplify_transitive_equality() { + for (src, target) in [( + "exists X Y Z ( X = 5 and Y = 5 and not p(X,Y))", + "exists X Z ( X = 5 and not p(X,X))", + )] { + let src = simplify_transitive_equality(src.parse().unwrap()); + let target = target.parse().unwrap(); + assert_eq!(src, target, "{src} != {target}") + } + } } diff --git a/src/simplifying/fol/mod.rs b/src/simplifying/fol/mod.rs index dfc75765..e73b2e2a 100644 --- a/src/simplifying/fol/mod.rs +++ b/src/simplifying/fol/mod.rs @@ -3,7 +3,7 @@ pub mod ht; use crate::{ convenience::{ - choose_fresh_variable_names, + choose_fresh_variable_names, subsort, unbox::{fol::UnboxedFormula, Unbox as _}, }, syntax_tree::fol::{ @@ -235,6 +235,132 @@ fn simplify_conjunction_tree_with_equality( result } +// Checks if two equality comparisons V1 = t1 (t1 = V1) and V2 = t2 (t2 = V2) +// satisfy that V1 is subsorteq to V2 and t1 = t2 and V1 and V2 occur in variables +// Returns keep_var, drop_var, drop_term +pub fn transitive_equality( + c1: Comparison, + c2: Comparison, + variables: Vec, +) -> Option<(Variable, Variable, Comparison)> { + let lhs1 = c1.term.clone(); + let rhs1 = c1.guards[0].term.clone(); + let lhs2 = c2.term.clone(); + let rhs2 = c2.guards[0].term.clone(); + + let is_var = |term: GeneralTerm| match term { + GeneralTerm::Variable(ref v) => { + let var = Variable { + sort: Sort::General, + name: v.to_string(), + }; + match variables.contains(&var) { + true => Some(var), + false => None, + } + } + GeneralTerm::IntegerTerm(IntegerTerm::Variable(ref v)) => { + let var = Variable { + sort: Sort::Integer, + name: v.to_string(), + }; + match variables.contains(&var) { + true => Some(var), + false => None, + } + } + GeneralTerm::SymbolicTerm(SymbolicTerm::Variable(ref v)) => { + let var = Variable { + sort: Sort::Symbol, + name: v.to_string(), + }; + match variables.contains(&var) { + true => Some(var), + false => None, + } + } + _ => None, + }; + + // Is V1 a variable? + let lhs1_is_var = is_var(lhs1.clone()); + + // Is V2 a variable? + let lhs2_is_var = is_var(lhs2.clone()); + + // Is t1 a variable? + let rhs1_is_var = is_var(rhs1.clone()); + + // Is t2 a variable? + let rhs2_is_var = is_var(rhs2.clone()); + + let mut result = None; + match lhs1_is_var { + Some(v1) => match lhs2_is_var { + // v1 = rhs1 + Some(v2) => { + // v1 = rhs1, v2 = rhs2 + if rhs1 == rhs2 { + if subsort(&v1, &v2) { + result = Some((v1, v2, c2)); + } else if subsort(&v2, &v1) { + result = Some((v2, v1, c1)); + } + } + } + None => match rhs2_is_var { + Some(v2) => { + // v1 = rhs1, lhs2 = v2 + if rhs1 == lhs2 { + if subsort(&v1, &v2) { + result = Some((v1, v2, c2)); + } else if subsort(&v2, &v1) { + result = Some((v2, v1, c1)); + } + } + } + None => result = None, + }, + }, + None => match rhs1_is_var { + Some(v1) => { + // lhs1 = v1 + match lhs2_is_var { + Some(v2) => { + // lhs1 = v1, v2 = rhs2 + if lhs1 == rhs2 { + if subsort(&v1, &v2) { + result = Some((v1, v2, c2)); + } else if subsort(&v2, &v1) { + result = Some((v2, v1, c1)); + } + } + } + None => match rhs2_is_var { + Some(v2) => { + // lhs1 = v1, lhs2 = v2 + if lhs1 == lhs2 { + if subsort(&v1, &v2) { + result = Some((v1, v2, c2)); + } else if subsort(&v2, &v1) { + result = Some((v2, v1, c1)); + } + } + } + None => { + result = None; + } + }, + } + } + None => { + result = None; + } + }, + } + result +} + #[test] fn test_simplify_conjunction_tree() { for (src, target) in [(