From b6c1db88012cc18871fcd79b9746ad8267eae87c Mon Sep 17 00:00:00 2001 From: AurumTheEnd <47597303+aurumtheend@users.noreply.github.com> Date: Fri, 26 Apr 2024 13:21:26 +0200 Subject: [PATCH] feat(bool fn trait): finished implementing BooleanFunction for Expression --- src/expressions/traits/boolean_function.rs | 197 +++++++++++++++++++-- 1 file changed, 181 insertions(+), 16 deletions(-) diff --git a/src/expressions/traits/boolean_function.rs b/src/expressions/traits/boolean_function.rs index bbcc8c1..1f49fdd 100644 --- a/src/expressions/traits/boolean_function.rs +++ b/src/expressions/traits/boolean_function.rs @@ -3,11 +3,14 @@ use crate::expressions::iterators::{ ExpressionSupportIterator, }; use crate::expressions::Expression; -use crate::traits::{BooleanFunction, BooleanValuation, Evaluate, GatherLiterals}; +use crate::expressions::ExpressionNode::{And, Constant, Literal, Not, Or}; +use crate::traits::{ + BooleanFunction, BooleanValuation, Evaluate, GatherLiterals, PowerSet, SemanticEq, +}; use std::collections::{BTreeMap, BTreeSet}; use std::fmt::Debug; -impl BooleanFunction for Expression { +impl BooleanFunction for Expression { type DomainIterator = ExpressionDomainIterator; type RangeIterator = ExpressionImageIterator; type RelationIterator = ExpressionRelationIterator; @@ -44,31 +47,193 @@ impl BooleanFunction for Expression { self.into() } - fn restrict(&self, _valuation: &BooleanValuation) -> Self { - todo!() + fn restrict(&self, valuation: &BooleanValuation) -> Self { + let mapping = BTreeMap::from_iter( + valuation + .iter() + .map(|(key, value)| (key.clone(), Constant(*value).into())), + ); + + self.substitute(&mapping) + } + + fn substitute(&self, mapping: &BTreeMap) -> Self { + self.substitute_rec(mapping) + } + + fn existential_quantification(&self, variables: BTreeSet) -> Self { + self.restrict(&btreeset_to_valuation(variables.clone(), false)) + | self.restrict(&btreeset_to_valuation(variables, true)) } - fn substitute(&self, _mapping: BTreeMap) -> Self { - todo!() + fn universal_quantification(&self, variables: BTreeSet) -> Self { + self.restrict(&btreeset_to_valuation(variables.clone(), false)) + & self.restrict(&btreeset_to_valuation(variables, true)) } - fn existential_quantification(&self, _variables: BTreeSet) -> Self { - todo!() + fn derivative(&self, variables: BTreeSet) -> Self { + self.restrict(&btreeset_to_valuation(variables.clone(), false)) + ^ self.restrict(&btreeset_to_valuation(variables, true)) } - fn universal_quantification(&self, _variables: BTreeSet) -> Self { - todo!() + fn is_equivalent(&self, other: &Self) -> bool { + self.semantic_eq(other) } - fn derivative(&self, _variables: BTreeSet) -> Self { - todo!() + fn is_implied_by(&self, other: &Self) -> bool { + let self_literals = self.gather_literals(); + let other_literals = other.gather_literals(); + let literals_union = BTreeSet::from_iter(self_literals.union(&other_literals).cloned()); + + let all_options = Self::generate_arbitrary_power_set(literals_union); + + all_options + .into_iter() + .all(|valuation| !other.evaluate(&valuation) | self.evaluate(&valuation)) + } +} + +impl Expression { + fn substitute_rec(&self, mapping: &BTreeMap) -> Self { + match self.node() { + Literal(name) => match mapping.get(name) { + None => Literal(name.clone()).into(), + Some(new_value) => new_value.clone(), + }, + Not(e) => Not(e.substitute_rec(mapping)).into(), + And(es) => And(es.iter().map(|e| e.substitute_rec(mapping)).collect()).into(), + Or(es) => Or(es.iter().map(|e| e.substitute_rec(mapping)).collect()).into(), + Constant(const_value) => Constant(*const_value).into(), + } } +} + +fn btreeset_to_valuation( + set: BTreeSet, + bool_value: bool, +) -> BTreeMap { + BTreeMap::from_iter(set.into_iter().map(|element| (element, bool_value))) +} + +#[cfg(test)] +mod tests { + use crate::expressions::{bool, var, Expression}; + use crate::traits::{BooleanFunction, SemanticEq}; + use std::collections::BTreeMap; + + #[test] + fn test_restrict_ok() { + let input = (var("a") | var("b")) & var("c"); + let valuation = BTreeMap::from_iter([("a".to_string(), false), ("c".to_string(), true)]); + + let expected = (bool(false) | var("b")) & bool(true); + let actual = input.restrict(&valuation); + + assert_eq!(expected, actual); + assert!(expected.semantic_eq(&actual)); + + assert_eq!(actual.degree(), 1); + } + + #[test] + fn test_restrict_too_many_variables_ok() { + let input = (var("a") | var("b")) & var("c"); + let valuation = BTreeMap::from_iter([ + ("a".to_string(), false), + ("c".to_string(), true), + ("notinthere".to_string(), true), + ]); + + let expected = (bool(false) | var("b")) & bool(true); + let actual = input.restrict(&valuation); - fn is_equivalent(&self, _other: Self) -> bool { - todo!() + assert_eq!(expected, actual); + assert!(expected.semantic_eq(&actual)); + assert_eq!(actual.degree(), 1); } - fn is_implied_by(&self, _other: Self) -> bool { - todo!() + #[test] + fn test_restrict_no_variables_ok() { + let input = (var("a") | var("b")) & var("c"); + let valuation = BTreeMap::new(); + + let expected = input.clone(); + let actual = input.restrict(&valuation); + + assert_eq!(expected, actual); + assert!(expected.semantic_eq(&actual)); + assert_eq!(actual.degree(), expected.degree()); + } + + #[test] + fn test_substitute_no_variables() { + let input = (var("a") | var("b")) & var("c"); + let valuation = BTreeMap::new(); + + let expected = input.clone(); + let actual = input.substitute(&valuation); + + assert_eq!(expected, actual); + assert!(expected.semantic_eq(&actual)); + assert_eq!(actual.degree(), expected.degree()); + } + + #[test] + fn test_substitute_variables_same_ok() { + let input = (var("a") | var("b")) & var("c") & !var("a"); + let mapping = BTreeMap::from_iter([("a".to_string(), var("a") | !var("b"))]); + + // cannot use `var("a") | !var("b") | var("b")` for defining expected here + // since that collapses Or(Or(a, !b), b), which substitute doesn't do + let expected = Expression::n_ary_or(&[var("a") | !var("b"), var("b")]) + & var("c") + & !(var("a") | !var("b")); + let actual = input.substitute(&mapping); + + assert_eq!(expected, actual); + assert!(expected.semantic_eq(&actual)); + assert_eq!(actual.degree(), expected.degree()); + } + + #[test] + fn test_substitute_variables_added_ok() { + let input = (var("a") | var("b")) & var("c") & !var("a"); + + let new_value = var("ddd") & (bool(false) | var("a")); + let mapping = BTreeMap::from_iter([("a".to_string(), new_value.clone())]); + + // cannot use bitwise operators for defining expected here + // since that collapses Or(Or(a, !b), b), which substitute doesn't do + let expected = + Expression::n_ary_or(&[new_value.clone(), var("b")]) & var("c") & !new_value.clone(); + let actual = input.substitute(&mapping); + + assert_eq!(expected, actual); + assert!(expected.semantic_eq(&actual)); + + assert_eq!(input.degree(), 3); + assert_eq!(actual.degree(), 4); + assert_eq!(actual.degree(), expected.degree()); + } + + #[test] + fn test_substitute_variables_removed_ok() { + let input = (var("a") | var("b")) & var("c") & !var("a"); + + let new_value = bool(false); + let mapping = BTreeMap::from_iter([("a".to_string(), new_value.clone())]); + + // cannot use bitwise operators for defining expected here + // since that collapses Or(Or(a, !b), b), which substitute doesn't do + let expected = + Expression::n_ary_or(&[new_value.clone(), var("b")]) & var("c") & !new_value.clone(); + let actual = input.substitute(&mapping); + + assert_eq!(expected, actual); + assert!(expected.semantic_eq(&actual)); + + assert_eq!(input.degree(), 3); + assert_eq!(actual.degree(), 2); + assert_eq!(actual.degree(), expected.degree()); } }