From d67e530feccded6ed6462e85a0b4231db3d308ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Mon, 13 Apr 2020 22:26:32 +0200 Subject: [PATCH] Rewrite formula and term formatting The rules for determining required parentheses as opposed to parentheses that can be omitted are more complicated than just showing parentheses whenever a child expression has lower precedence than its parent. This necessitated a rewrite. This new implementation determines whether an expression requires to be parenthesized with individual rules for each type of expression, which may or may not depend on the type of the parent expression and the position of a child within its parent expression. For example, implication is defined to be right-associative, which means that the parentheses in the formula (F -> G) -> H cannot be ommitted. When determining whether the subformula (F -> G) needs to be parenthesized, the new algorithm notices that the subformula is contained as the antecedent of another implication and concludes that parentheses are required. Furthermore, this adds extensive unit tests for both formula and term formatting. The general idea is to test all types of expressions individually and, in addition to that, all combinations of parent and child expression types. Unit testing made it clear that the formatting of empty and 1-ary conjunctions, disjunctions, and biconditionals needs to be well-defined even though these types of formulas may be unconventional. The same applies to existentially and universally quantified formulas where the list of parameters is empty. Now, empty conjunctions and biconditionals are rendered like true Booleans, empty disjunctions like false Booleans, and 1-ary conjunctions, disjunctions, biconditionals, as well as quantified expressions with empty parameter lists as their singleton argument. The latter formulas can be considered neutral intermediates. That is, they should not affect whether their singleton arguments are parenthesized or not. To account for that, all unit tests covering combinations of formulas are tested with any of those five neutral intermediates additionally. --- src/ast.rs | 8 - src/format.rs | 5 - src/format/formulas.rs | 1220 ++++++++++++++++++++++++++++++++++++---- src/format/terms.rs | 1063 ++++++++++++++++++++++++++++++---- 4 files changed, 2045 insertions(+), 251 deletions(-) diff --git a/src/ast.rs b/src/ast.rs index 08a44dc..ca15d17 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -445,8 +445,6 @@ impl Formula { pub fn and(arguments: Formulas) -> Self { - assert!(!arguments.is_empty()); - Self::And(arguments) } @@ -462,8 +460,6 @@ impl Formula pub fn exists(parameters: std::rc::Rc, argument: Box) -> Self { - assert!(!parameters.is_empty()); - Self::Exists(QuantifiedFormula::new(parameters, argument)) } @@ -479,8 +475,6 @@ impl Formula pub fn for_all(parameters: std::rc::Rc, argument: Box) -> Self { - assert!(!parameters.is_empty()); - Self::ForAll(QuantifiedFormula::new(parameters, argument)) } @@ -527,8 +521,6 @@ impl Formula pub fn or(arguments: Formulas) -> Self { - assert!(!arguments.is_empty()); - Self::Or(arguments) } diff --git a/src/format.rs b/src/format.rs index 0b2fb3a..a4495bd 100644 --- a/src/format.rs +++ b/src/format.rs @@ -1,7 +1,2 @@ mod formulas; mod terms; - -trait Precedence -{ - fn precedence(&self) -> i32; -} diff --git a/src/format/formulas.rs b/src/format/formulas.rs index d3c0f8f..98f928d 100644 --- a/src/format/formulas.rs +++ b/src/format/formulas.rs @@ -1,33 +1,5 @@ -use super::Precedence; use super::terms::*; -impl Precedence for crate::Formula -{ - fn precedence(&self) -> i32 - { - match &self - { - Self::Predicate(_) - | Self::Boolean(_) - | Self::Compare(_) - => 0, - Self::Exists(_) - | Self::ForAll(_) - => 1, - Self::Not(_) - => 2, - Self::And(_) - => 3, - Self::Or(_) - => 4, - Self::Implies(_) - => 5, - Self::IfAndOnlyIf(_) - => 6, - } - } -} - impl std::fmt::Debug for crate::ImplicationDirection { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result @@ -56,18 +28,99 @@ impl std::fmt::Display for crate::PredicateDeclaration } } -struct FormulaDisplay<'formula> +#[derive(Clone, Copy, Eq, PartialEq)] +enum FormulaPosition { - parent_precedence: Option, - formula: &'formula crate::Formula, + Any, + ImpliesAntecedent, } -fn display_formula(formula: &crate::Formula, parent_precedence: Option) -> FormulaDisplay +struct FormulaDisplay<'formula> +{ + formula: &'formula crate::Formula, + parent_formula: Option<&'formula crate::Formula>, + position: FormulaPosition, +} + +impl<'formula> FormulaDisplay<'formula> +{ + fn requires_parentheses(&self) -> bool + { + use crate::Formula; + + let parent_formula = match self.parent_formula + { + Some(parent_formula) => parent_formula, + None => return false, + }; + + match self.formula + { + Formula::Predicate(_) + | Formula::Boolean(_) + | Formula::Compare(_) + | Formula::Not(_) + | Formula::Exists(_) + | Formula::ForAll(_) + => false, + Formula::And(formulas) + | Formula::Or(formulas) + | Formula::IfAndOnlyIf(formulas) if formulas.len() <= 1 + => false, + Formula::And(_) => match *parent_formula + { + Formula::Not(_) + | Formula::Exists(_) + | Formula::ForAll(_) + => true, + _ => false, + }, + Formula::Or(_) => match *parent_formula + { + Formula::Not(_) + | Formula::Exists(_) + | Formula::ForAll(_) + | Formula::And(_) + => true, + _ => false, + }, + Formula::Implies(crate::Implies{direction, ..}) => match &*parent_formula + { + Formula::Not(_) + | Formula::Exists(_) + | Formula::ForAll(_) + | Formula::And(_) + | Formula::Or(_) + => true, + Formula::Implies(crate::Implies{direction: parent_direction, ..}) => + if direction == parent_direction + { + // Implications with the same direction nested on the antecedent side + // require parentheses because implication is considered right-associative + self.position == FormulaPosition::ImpliesAntecedent + } + else + { + // Nested implications with opposite direction always require parentheses + // because the order of formulas like p <- q -> r would be ambiguous + true + }, + _ => false, + }, + Formula::IfAndOnlyIf(_) => true, + } + } +} + +fn display_formula<'formula>(formula: &'formula crate::Formula, + parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition) + -> FormulaDisplay<'formula> { FormulaDisplay { - parent_precedence, formula, + parent_formula, + position, } } @@ -75,13 +128,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - let precedence = self.formula.precedence(); - let requires_parentheses = match self.parent_precedence - { - Some(parent_precedence) => precedence > parent_precedence, - None => false, - }; - let precedence = Some(precedence); + let requires_parentheses = self.requires_parentheses(); if requires_parentheses { @@ -92,111 +139,177 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> { crate::Formula::Exists(exists) => { - assert!(!exists.parameters.is_empty()); - - write!(format, "exists")?; - - let mut separator = " "; - - for parameter in exists.parameters.iter() + if exists.parameters.is_empty() { - write!(format, "{}{:?}", separator, parameter)?; - - separator = ", " + write!(format, "{:?}", display_formula(&exists.argument, self.parent_formula, + self.position))?; } + else + { + write!(format, "exists")?; - write!(format, " {:?}", display_formula(&exists.argument, precedence))?; + let mut separator = " "; + + for parameter in exists.parameters.iter() + { + write!(format, "{}{:?}", separator, parameter)?; + + separator = ", " + } + + write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula), + FormulaPosition::Any))?; + } }, crate::Formula::ForAll(for_all) => { - assert!(!for_all.parameters.is_empty()); - - write!(format, "forall")?; - - let mut separator = " "; - - for parameter in for_all.parameters.iter() + if for_all.parameters.is_empty() { - write!(format, "{}{:?}", separator, parameter)?; - - separator = ", " + write!(format, "{:?}", display_formula(&for_all.argument, self.parent_formula, + self.position))?; } + else + { + write!(format, "forall")?; - write!(format, " {:?}", display_formula(&for_all.argument, precedence))?; + let mut separator = " "; + + for parameter in for_all.parameters.iter() + { + write!(format, "{}{:?}", separator, parameter)?; + + separator = ", " + } + + write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula), + FormulaPosition::Any))?; + } }, crate::Formula::Not(argument) => write!(format, "not {:?}", - display_formula(argument, precedence))?, + display_formula(argument, Some(self.formula), FormulaPosition::Any))?, crate::Formula::And(arguments) => { - let mut separator = ""; - - assert!(!arguments.is_empty()); - - for argument in arguments + if arguments.is_empty() { - write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + write!(format, "true")?; + } + else + { + let (parent_formula, position) = match arguments.len() + { + 1 => (self.parent_formula, self.position), + _ => (Some(self.formula), FormulaPosition::Any), + }; - separator = " and " + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, + display_formula(argument, parent_formula, position))?; + + separator = " and " + } } }, crate::Formula::Or(arguments) => { - let mut separator = ""; - - assert!(!arguments.is_empty()); - - for argument in arguments + if arguments.is_empty() { - write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + write!(format, "false")?; + } + else + { + let (parent_formula, position) = match arguments.len() + { + 1 => (self.parent_formula, self.position), + _ => (Some(self.formula), FormulaPosition::Any), + }; - separator = " or " + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, + display_formula(argument, parent_formula, position))?; + + separator = " or " + } + } + }, + crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) => + { + let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _> + { + write!(format, "{:?}", + display_formula(antecedent, Some(self.formula), + FormulaPosition::ImpliesAntecedent)) + }; + + let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _> + { + write!(format, "{:?}", + display_formula(implication, Some(self.formula), FormulaPosition::Any)) + }; + + match direction + { + crate::ImplicationDirection::LeftToRight => + { + format_antecedent(format)?; + write!(format, " -> ")?; + format_implication(format)?; + }, + crate::ImplicationDirection::RightToLeft => + { + format_implication(format)?; + write!(format, " <- ")?; + format_antecedent(format)?; + }, } }, - crate::Formula::Implies(crate::Implies{ - direction: crate::ImplicationDirection::LeftToRight, antecedent, implication}) - => write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), - display_formula(implication, precedence))?, - crate::Formula::Implies(crate::Implies{ - direction: crate::ImplicationDirection::RightToLeft, antecedent, implication}) - => write!(format, "{:?} <- {:?}", display_formula(implication, precedence), - display_formula(antecedent, precedence))?, crate::Formula::IfAndOnlyIf(arguments) => { - let mut separator = ""; - - assert!(!arguments.is_empty()); - - for argument in arguments + if arguments.is_empty() { - write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + write!(format, "true")?; + } + else + { + let (parent_formula, position) = match arguments.len() + { + 1 => (self.parent_formula, self.position), + _ => (Some(self.formula), FormulaPosition::Any), + }; - separator = " <-> " + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, + display_formula(argument, parent_formula, position))?; + + separator = " <-> " + } } }, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::Less, left, right}) - => write!(format, "{:?} < {:?}", display_term(left, None), - display_term(right, None))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right}) - => write!(format, "{:?} <= {:?}", display_term(left, None), - display_term(right, None))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::Greater, left, right}) - => write!(format, "{:?} > {:?}", display_term(left, None), - display_term(right, None))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right}) - => write!(format, "{:?} >= {:?}", display_term(left, None), - display_term(right, None))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::Equal, left, right}) - => write!(format, "{:?} = {:?}", display_term(left, None), - display_term(right, None))?, - crate::Formula::Compare( - crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right}) - => write!(format, "{:?} != {:?}", display_term(left, None), - display_term(right, None))?, + crate::Formula::Compare(compare) => + { + let operator_string = match compare.operator + { + crate::ComparisonOperator::Less => "<", + crate::ComparisonOperator::LessOrEqual => "<=", + crate::ComparisonOperator::Greater => ">", + crate::ComparisonOperator::GreaterOrEqual => ">=", + crate::ComparisonOperator::Equal => "=", + crate::ComparisonOperator::NotEqual => "!=", + }; + + write!(format, "{:?} {} {:?}", + display_term(&compare.left, None, TermPosition::Any), + operator_string, + display_term(&compare.right, None, TermPosition::Any))?; + }, crate::Formula::Boolean(true) => write!(format, "true")?, crate::Formula::Boolean(false) => write!(format, "false")?, crate::Formula::Predicate(predicate) => @@ -211,7 +324,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> for argument in &predicate.arguments { - write!(format, "{}{:?}", separator, display_term(argument, None))?; + write!(format, "{}{:?}", separator, display_term(argument, None, + TermPosition::Any))?; separator = ", " } @@ -242,7 +356,7 @@ impl std::fmt::Debug for crate::Formula { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{:?}", display_formula(&self, None)) + write!(format, "{:?}", display_formula(&self, None, FormulaPosition::Any)) } } @@ -250,6 +364,874 @@ impl std::fmt::Display for crate::Formula { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{}", display_formula(&self, None)) + write!(format, "{}", display_formula(&self, None, FormulaPosition::Any)) + } +} + +#[cfg(test)] +mod tests +{ + use crate::*; + use crate::format::terms::tests::*; + + macro_rules! assert + { + ($formula:expr, $output:expr) => + { + assert_eq!(format($formula), $output); + }; + } + + // Tests all neutral intermediates (such as 1-ary conjunction) + macro_rules! assert_all + { + ($intermediate:ident, $formula:expr, $output:expr) => + { + let $intermediate = |f: Box| f; + assert!($formula, $output); + + let $intermediate = |f: Box| exists(vec![], f); + assert!($formula, $output); + + let $intermediate = |f: Box| for_all(vec![], f); + assert!($formula, $output); + + let $intermediate = |f: Box| and(vec![f]); + assert!($formula, $output); + + let $intermediate = |f: Box| or(vec![f]); + assert!($formula, $output); + + let $intermediate = |f: Box| if_and_only_if(vec![f]); + assert!($formula, $output); + }; + } + + fn format(formula: Box) -> String + { + format!("{}", formula) + } + + fn and(arguments: Vec>) -> Box + { + Box::new(Formula::and(arguments.into_iter().map(|x| *x).collect())) + } + + fn equal(left: Box, right: Box) -> Box + { + Box::new(Formula::equal(left, right)) + } + + fn exists(parameters: VariableDeclarations, argument: Box) -> Box + { + Box::new(Formula::exists(std::rc::Rc::new(parameters), argument)) + } + + fn false_() -> Box + { + Box::new(Formula::false_()) + } + + fn for_all(parameters: VariableDeclarations, argument: Box) -> Box + { + Box::new(Formula::for_all(std::rc::Rc::new(parameters), argument)) + } + + fn greater(left: Box, right: Box) -> Box + { + Box::new(Formula::greater(left, right)) + } + + fn greater_or_equal(left: Box, right: Box) -> Box + { + Box::new(Formula::greater_or_equal(left, right)) + } + + fn if_and_only_if(arguments: Vec>) -> Box + { + Box::new(Formula::if_and_only_if(arguments.into_iter().map(|x| *x).collect())) + } + + fn implies(direction: ImplicationDirection, antecedent: Box, implication: Box) + -> Box + { + Box::new(Formula::implies(direction, antecedent, implication)) + } + + fn less(left: Box, right: Box) -> Box + { + Box::new(Formula::less(left, right)) + } + + fn less_or_equal(left: Box, right: Box) -> Box + { + Box::new(Formula::less_or_equal(left, right)) + } + + fn not(argument: Box) -> Box + { + Box::new(Formula::not(argument)) + } + + fn not_equal(left: Box, right: Box) -> Box + { + Box::new(Formula::not_equal(left, right)) + } + + fn or(arguments: Vec>) -> Box + { + Box::new(Formula::or(arguments.into_iter().map(|x| *x).collect())) + } + + fn predicate(name: &str, arguments: Vec>) -> Box + { + Box::new(Formula::predicate(predicate_declaration(name, arguments.len()), + arguments.into_iter().map(|x| *x).collect())) + } + + fn predicate_declaration(name: &str, arity: usize) -> std::rc::Rc + { + std::rc::Rc::new(PredicateDeclaration::new(name.to_string(), arity)) + } + + fn true_() -> Box + { + Box::new(Formula::true_()) + } + + fn x() -> std::rc::Rc + { + variable_declaration("X") + } + + fn y() -> std::rc::Rc + { + variable_declaration("Y") + } + + fn z() -> std::rc::Rc + { + variable_declaration("Z") + } + + fn xyz() -> VariableDeclarations + { + vec![x(), y(), z()] + } + + fn x1y1z1() -> VariableDeclarations + { + vec![variable_declaration("X1"), variable_declaration("Y1"), variable_declaration("Z1")] + } + + fn x2y2z2() -> VariableDeclarations + { + vec![variable_declaration("X2"), variable_declaration("Y2"), variable_declaration("Z2")] + } + + fn x3y3z3() -> VariableDeclarations + { + vec![variable_declaration("X3"), variable_declaration("Y3"), variable_declaration("Z3")] + } + + fn p() -> Box + { + predicate("p", vec![]) + } + + fn q() -> Box + { + predicate("q", vec![]) + } + + fn p1() -> Box + { + predicate("p1", vec![]) + } + + fn q1() -> Box + { + predicate("q1", vec![]) + } + + fn p2() -> Box + { + predicate("p2", vec![]) + } + + fn q2() -> Box + { + predicate("q2", vec![]) + } + + fn p3() -> Box + { + predicate("p3", vec![]) + } + + fn q3() -> Box + { + predicate("q3", vec![]) + } + + fn r() -> Box + { + predicate("r", vec![]) + } + + fn pqr() -> Vec> + { + vec![p(), q(), r()] + } + + fn p1q1r1() -> Vec> + { + vec![p1(), q1(), predicate("r1", vec![])] + } + + fn p2q2r2() -> Vec> + { + vec![p2(), q2(), predicate("r2", vec![])] + } + + fn p3q3r3() -> Vec> + { + vec![p3(), q3(), predicate("r3", vec![])] + } + + fn implies_right(antecedent: Box, implication: Box) -> Box + { + implies(ImplicationDirection::LeftToRight, antecedent, implication) + } + + fn implies_left(antecedent: Box, implication: Box) -> Box + { + implies(ImplicationDirection::RightToLeft, antecedent, implication) + } + + #[test] + fn format_boolean() + { + assert!(true_(), "true"); + assert!(false_(), "false"); + } + + #[test] + fn format_compare() + { + assert!(greater(a(), b()), "a > b"); + assert!(less(a(), b()), "a < b"); + assert!(less_or_equal(a(), b()), "a <= b"); + assert!(greater_or_equal(a(), b()), "a >= b"); + assert!(equal(a(), b()), "a = b"); + assert!(not_equal(a(), b()), "a != b"); + + assert!(greater(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))), + "(a + b) * c > |d - e|"); + assert!(less(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))), + "(a + b) * c < |d - e|"); + assert!(less_or_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))), + "(a + b) * c <= |d - e|"); + assert!(greater_or_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))), + "(a + b) * c >= |d - e|"); + assert!(equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))), + "(a + b) * c = |d - e|"); + assert!(not_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))), + "(a + b) * c != |d - e|"); + } + + #[test] + fn format_predicate() + { + assert!(p(), "p"); + assert!(predicate("predicate", vec![]), "predicate"); + assert!(predicate("q", vec![a()]), "q(a)"); + assert!(predicate("q", abc()), "q(a, b, c)"); + assert!(predicate("predicate", abc()), "predicate(a, b, c)"); + + assert!(predicate("predicate", vec![ + exponentiate(absolute_value(multiply(a(), integer(-20))), integer(2)), + string("test"), + function("f", vec![multiply(add(b(), c()), subtract(b(), c())), infimum(), + variable("X")])]), + "predicate(|a * -20| ** 2, \"test\", f((b + c) * (b - c), #inf, X))"); + + // TODO: escape predicates that start with capital letters or that conflict with keywords + } + + #[test] + fn format_predicate_declaration() + { + assert_eq!(format!("{}", predicate_declaration("p", 0)), "p/0"); + assert_eq!(format!("{}", predicate_declaration("predicate", 0)), "predicate/0"); + assert_eq!(format!("{}", predicate_declaration("q", 1)), "q/1"); + assert_eq!(format!("{}", predicate_declaration("q", 3)), "q/3"); + assert_eq!(format!("{}", predicate_declaration("predicate", 3)), "predicate/3"); + } + + #[test] + fn format_exists() + { + assert!(exists(vec![], p()), "p"); + assert!(exists(vec![x()], p()), "exists X p"); + assert!(exists(xyz(), p()), "exists X, Y, Z p"); + } + + #[test] + fn format_for_all() + { + assert!(for_all(vec![], p()), "p"); + assert!(for_all(vec![x()], p()), "forall X p"); + assert!(for_all(xyz(), p()), "forall X, Y, Z p"); + } + + #[test] + fn format_not() + { + assert!(not(p()), "not p"); + } + + #[test] + fn format_and() + { + assert!(and(vec![]), "true"); + assert!(and(vec![p()]), "p"); + assert!(and(pqr()), "p and q and r"); + } + + #[test] + fn format_or() + { + assert!(or(vec![]), "false"); + assert!(or(vec![p()]), "p"); + assert!(or(pqr()), "p or q or r"); + } + + #[test] + fn format_implies() + { + assert!(implies_right(p(), q()), "p -> q"); + assert!(implies_left(p(), q()), "q <- p"); + } + + #[test] + fn format_if_and_only_if() + { + assert!(if_and_only_if(vec![]), "true"); + assert!(if_and_only_if(vec![p()]), "p"); + assert!(if_and_only_if(vec![p(), q()]), "p <-> q"); + assert!(if_and_only_if(pqr()), "p <-> q <-> r"); + } + + #[test] + fn format_combinations_boolean() + { + // Not + Boolean + assert!(not(true_()), "not true"); + assert!(not(false_()), "not false"); + + // Quantified formula + Boolean + assert!(exists(vec![], true_()), "true"); + assert!(exists(vec![], false_()), "false"); + assert!(exists(vec![x()], true_()), "exists X true"); + assert!(exists(vec![x()], false_()), "exists X false"); + assert!(exists(xyz(), true_()), "exists X, Y, Z true"); + assert!(exists(xyz(), false_()), "exists X, Y, Z false"); + assert!(for_all(vec![], true_()), "true"); + assert!(for_all(vec![], false_()), "false"); + assert!(for_all(vec![x()], true_()), "forall X true"); + assert!(for_all(vec![x()], false_()), "forall X false"); + assert!(for_all(xyz(), true_()), "forall X, Y, Z true"); + assert!(for_all(xyz(), false_()), "forall X, Y, Z false"); + + // And + Boolean + assert!(and(vec![true_()]), "true"); + assert!(and(vec![true_(), true_(), true_()]), "true and true and true"); + assert!(and(vec![false_()]), "false"); + assert!(and(vec![false_(), false_(), false_()]), "false and false and false"); + + // Or + Boolean + assert!(or(vec![true_()]), "true"); + assert!(or(vec![true_(), true_(), true_()]), "true or true or true"); + assert!(or(vec![false_()]), "false"); + assert!(or(vec![false_(), false_(), false_()]), "false or false or false"); + + // Implies + Boolean + assert!(implies_right(true_(), true_()), "true -> true"); + assert!(implies_left(true_(), true_()), "true <- true"); + assert!(implies_right(false_(), false_()), "false -> false"); + assert!(implies_left(false_(), false_()), "false <- false"); + + // If and only if + Boolean + assert!(if_and_only_if(vec![true_()]), "true"); + assert!(if_and_only_if(vec![true_(), true_(), true_()]), "true <-> true <-> true"); + assert!(if_and_only_if(vec![false_()]), "false"); + assert!(if_and_only_if(vec![false_(), false_(), false_()]), "false <-> false <-> false"); + } + + #[test] + fn format_combinations_compare() + { + let term_1 = || multiply(add(a(), b()), c()); + let term_2 = || absolute_value(subtract(d(), e())); + let term_3 = || exponentiate(a(), exponentiate(b(), c())); + let term_4 = || negative(function("f", vec![integer(5), add(variable("X"), integer(3))])); + + // Not + compare + assert!(not(greater(term_1(), term_2())), "not (a + b) * c > |d - e|"); + assert!(not(less(term_1(), term_2())), "not (a + b) * c < |d - e|"); + assert!(not(less_or_equal(term_1(), term_2())), "not (a + b) * c <= |d - e|"); + assert!(not(greater_or_equal(term_1(), term_2())), "not (a + b) * c >= |d - e|"); + assert!(not(equal(term_1(), term_2())), "not (a + b) * c = |d - e|"); + assert!(not(not_equal(term_1(), term_2())), "not (a + b) * c != |d - e|"); + + // Quantified formula + compare + assert!(exists(vec![], greater(term_1(), term_2())), "(a + b) * c > |d - e|"); + assert!(exists(vec![], less(term_1(), term_2())), "(a + b) * c < |d - e|"); + assert!(exists(vec![], less_or_equal(term_1(), term_2())), "(a + b) * c <= |d - e|"); + assert!(exists(vec![], greater_or_equal(term_1(), term_2())), "(a + b) * c >= |d - e|"); + assert!(exists(vec![], equal(term_1(), term_2())), "(a + b) * c = |d - e|"); + assert!(exists(vec![], not_equal(term_1(), term_2())), "(a + b) * c != |d - e|"); + assert!(for_all(vec![], greater(term_1(), term_2())), "(a + b) * c > |d - e|"); + assert!(for_all(vec![], less(term_1(), term_2())), "(a + b) * c < |d - e|"); + assert!(for_all(vec![], less_or_equal(term_1(), term_2())), "(a + b) * c <= |d - e|"); + assert!(for_all(vec![], greater_or_equal(term_1(), term_2())), "(a + b) * c >= |d - e|"); + assert!(for_all(vec![], equal(term_1(), term_2())), "(a + b) * c = |d - e|"); + assert!(for_all(vec![], not_equal(term_1(), term_2())), "(a + b) * c != |d - e|"); + assert!(exists(vec![x()], greater(term_1(), term_2())), "exists X (a + b) * c > |d - e|"); + assert!(exists(vec![x()], less(term_1(), term_2())), "exists X (a + b) * c < |d - e|"); + assert!(exists(vec![x()], less_or_equal(term_1(), term_2())), + "exists X (a + b) * c <= |d - e|"); + assert!(exists(vec![x()], greater_or_equal(term_1(), term_2())), + "exists X (a + b) * c >= |d - e|"); + assert!(exists(vec![x()], equal(term_1(), term_2())), "exists X (a + b) * c = |d - e|"); + assert!(exists(vec![x()], not_equal(term_1(), term_2())), + "exists X (a + b) * c != |d - e|"); + assert!(for_all(vec![x()], greater(term_1(), term_2())), "forall X (a + b) * c > |d - e|"); + assert!(for_all(vec![x()], less(term_1(), term_2())), "forall X (a + b) * c < |d - e|"); + assert!(for_all(vec![x()], less_or_equal(term_1(), term_2())), + "forall X (a + b) * c <= |d - e|"); + assert!(for_all(vec![x()], greater_or_equal(term_1(), term_2())), + "forall X (a + b) * c >= |d - e|"); + assert!(for_all(vec![x()], equal(term_1(), term_2())), "forall X (a + b) * c = |d - e|"); + assert!(for_all(vec![x()], not_equal(term_1(), term_2())), + "forall X (a + b) * c != |d - e|"); + assert!(exists(xyz(), greater(term_1(), term_2())), "exists X, Y, Z (a + b) * c > |d - e|"); + assert!(exists(xyz(), less(term_1(), term_2())), "exists X, Y, Z (a + b) * c < |d - e|"); + assert!(exists(xyz(), less_or_equal(term_1(), term_2())), + "exists X, Y, Z (a + b) * c <= |d - e|"); + assert!(exists(xyz(), greater_or_equal(term_1(), term_2())), + "exists X, Y, Z (a + b) * c >= |d - e|"); + assert!(exists(xyz(), equal(term_1(), term_2())), "exists X, Y, Z (a + b) * c = |d - e|"); + assert!(exists(xyz(), not_equal(term_1(), term_2())), + "exists X, Y, Z (a + b) * c != |d - e|"); + assert!(for_all(xyz(), greater(term_1(), term_2())), + "forall X, Y, Z (a + b) * c > |d - e|"); + assert!(for_all(xyz(), less(term_1(), term_2())), "forall X, Y, Z (a + b) * c < |d - e|"); + assert!(for_all(xyz(), less_or_equal(term_1(), term_2())), + "forall X, Y, Z (a + b) * c <= |d - e|"); + assert!(for_all(xyz(), greater_or_equal(term_1(), term_2())), + "forall X, Y, Z (a + b) * c >= |d - e|"); + assert!(for_all(xyz(), equal(term_1(), term_2())), "forall X, Y, Z (a + b) * c = |d - e|"); + assert!(for_all(xyz(), not_equal(term_1(), term_2())), + "forall X, Y, Z (a + b) * c != |d - e|"); + + // And + compare + assert!(and(vec![greater(term_1(), term_2()), greater(term_3(), term_4()), + greater(term_2(), term_4())]), + "(a + b) * c > |d - e| and a ** b ** c > -f(5, X + 3) and |d - e| > -f(5, X + 3)"); + assert!(and(vec![less(term_1(), term_2()), less(term_3(), term_4()), + less(term_2(), term_4())]), + "(a + b) * c < |d - e| and a ** b ** c < -f(5, X + 3) and |d - e| < -f(5, X + 3)"); + assert!(and(vec![less_or_equal(term_1(), term_2()), less_or_equal(term_3(), term_4()), + less_or_equal(term_2(), term_4())]), + "(a + b) * c <= |d - e| and a ** b ** c <= -f(5, X + 3) and |d - e| <= -f(5, X + 3)"); + assert!(and(vec![greater_or_equal(term_1(), term_2()), greater_or_equal(term_3(), term_4()), + greater_or_equal(term_2(), term_4())]), + "(a + b) * c >= |d - e| and a ** b ** c >= -f(5, X + 3) and |d - e| >= -f(5, X + 3)"); + assert!(and(vec![equal(term_1(), term_2()), equal(term_3(), term_4()), + equal(term_2(), term_4())]), + "(a + b) * c = |d - e| and a ** b ** c = -f(5, X + 3) and |d - e| = -f(5, X + 3)"); + assert!(and(vec![not_equal(term_1(), term_2()), not_equal(term_3(), term_4()), + not_equal(term_2(), term_4())]), + "(a + b) * c != |d - e| and a ** b ** c != -f(5, X + 3) and |d - e| != -f(5, X + 3)"); + + // Or + compare + assert!(or(vec![greater(term_1(), term_2()), greater(term_3(), term_4()), + greater(term_2(), term_4())]), + "(a + b) * c > |d - e| or a ** b ** c > -f(5, X + 3) or |d - e| > -f(5, X + 3)"); + assert!(or(vec![less(term_1(), term_2()), less(term_3(), term_4()), + less(term_2(), term_4())]), + "(a + b) * c < |d - e| or a ** b ** c < -f(5, X + 3) or |d - e| < -f(5, X + 3)"); + assert!(or(vec![less_or_equal(term_1(), term_2()), less_or_equal(term_3(), term_4()), + less_or_equal(term_2(), term_4())]), + "(a + b) * c <= |d - e| or a ** b ** c <= -f(5, X + 3) or |d - e| <= -f(5, X + 3)"); + assert!(or(vec![greater_or_equal(term_1(), term_2()), greater_or_equal(term_3(), term_4()), + greater_or_equal(term_2(), term_4())]), + "(a + b) * c >= |d - e| or a ** b ** c >= -f(5, X + 3) or |d - e| >= -f(5, X + 3)"); + assert!(or(vec![equal(term_1(), term_2()), equal(term_3(), term_4()), + equal(term_2(), term_4())]), + "(a + b) * c = |d - e| or a ** b ** c = -f(5, X + 3) or |d - e| = -f(5, X + 3)"); + assert!(or(vec![not_equal(term_1(), term_2()), not_equal(term_3(), term_4()), + not_equal(term_2(), term_4())]), + "(a + b) * c != |d - e| or a ** b ** c != -f(5, X + 3) or |d - e| != -f(5, X + 3)"); + + // Implies + compare + assert!(implies_right(greater(term_1(), term_2()), greater(term_3(), term_4())), + "(a + b) * c > |d - e| -> a ** b ** c > -f(5, X + 3)"); + assert!(implies_right(less(term_1(), term_2()), less(term_3(), term_4())), + "(a + b) * c < |d - e| -> a ** b ** c < -f(5, X + 3)"); + assert!(implies_right(less_or_equal(term_1(), term_2()), less_or_equal(term_3(), term_4())), + "(a + b) * c <= |d - e| -> a ** b ** c <= -f(5, X + 3)"); + assert!(implies_right(greater_or_equal(term_1(), term_2()), + greater_or_equal(term_3(), term_4())), + "(a + b) * c >= |d - e| -> a ** b ** c >= -f(5, X + 3)"); + assert!(implies_right(equal(term_1(), term_2()), equal(term_3(), term_4())), + "(a + b) * c = |d - e| -> a ** b ** c = -f(5, X + 3)"); + assert!(implies_right(not_equal(term_1(), term_2()), not_equal(term_3(), term_4())), + "(a + b) * c != |d - e| -> a ** b ** c != -f(5, X + 3)"); + assert!(implies_left(greater(term_1(), term_2()), greater(term_3(), term_4())), + "a ** b ** c > -f(5, X + 3) <- (a + b) * c > |d - e|"); + assert!(implies_left(less(term_1(), term_2()), less(term_3(), term_4())), + "a ** b ** c < -f(5, X + 3) <- (a + b) * c < |d - e|"); + assert!(implies_left(less_or_equal(term_1(), term_2()), less_or_equal(term_3(), term_4())), + "a ** b ** c <= -f(5, X + 3) <- (a + b) * c <= |d - e|"); + assert!(implies_left(greater_or_equal(term_1(), term_2()), + greater_or_equal(term_3(), term_4())), + "a ** b ** c >= -f(5, X + 3) <- (a + b) * c >= |d - e|"); + assert!(implies_left(equal(term_1(), term_2()), equal(term_3(), term_4())), + "a ** b ** c = -f(5, X + 3) <- (a + b) * c = |d - e|"); + assert!(implies_left(not_equal(term_1(), term_2()), not_equal(term_3(), term_4())), + "a ** b ** c != -f(5, X + 3) <- (a + b) * c != |d - e|"); + + // If and only if + compare + assert!(if_and_only_if(vec![greater(term_1(), term_2()), greater(term_3(), term_4()), + greater(term_2(), term_4())]), + "(a + b) * c > |d - e| <-> a ** b ** c > -f(5, X + 3) <-> |d - e| > -f(5, X + 3)"); + assert!(if_and_only_if(vec![less(term_1(), term_2()), less(term_3(), term_4()), + less(term_2(), term_4())]), + "(a + b) * c < |d - e| <-> a ** b ** c < -f(5, X + 3) <-> |d - e| < -f(5, X + 3)"); + assert!(if_and_only_if(vec![less_or_equal(term_1(), term_2()), + less_or_equal(term_3(), term_4()), less_or_equal(term_2(), term_4())]), + "(a + b) * c <= |d - e| <-> a ** b ** c <= -f(5, X + 3) <-> |d - e| <= -f(5, X + 3)"); + assert!(if_and_only_if(vec![greater_or_equal(term_1(), term_2()), + greater_or_equal(term_3(), term_4()), greater_or_equal(term_2(), term_4())]), + "(a + b) * c >= |d - e| <-> a ** b ** c >= -f(5, X + 3) <-> |d - e| >= -f(5, X + 3)"); + assert!(if_and_only_if(vec![equal(term_1(), term_2()), equal(term_3(), term_4()), + equal(term_2(), term_4())]), + "(a + b) * c = |d - e| <-> a ** b ** c = -f(5, X + 3) <-> |d - e| = -f(5, X + 3)"); + assert!(if_and_only_if(vec![not_equal(term_1(), term_2()), not_equal(term_3(), term_4()), + not_equal(term_2(), term_4())]), + "(a + b) * c != |d - e| <-> a ** b ** c != -f(5, X + 3) <-> |d - e| != -f(5, X + 3)"); + } + + #[test] + fn format_combinations_not() + { + // Not + not + assert!(not(not(p())), "not not p"); + + // Quantified formulas + not + assert_all!(i, exists(vec![x()], i(not(p()))), "exists X not p"); + assert_all!(i, for_all(vec![x()], i(not(p()))), "forall X not p"); + assert_all!(i, exists(xyz(), i(not(p()))), "exists X, Y, Z not p"); + assert_all!(i, for_all(xyz(), i(not(p()))), "forall X, Y, Z not p"); + + // And + not + assert_all!(i, and(vec![i(not(p()))]), "not p"); + assert_all!(i, and(vec![i(not(p())), i(not(q())), i(not(r()))]), + "not p and not q and not r"); + + // Or + not + assert_all!(i, or(vec![i(not(p()))]), "not p"); + assert_all!(i, or(vec![i(not(p())), i(not(q())), i(not(r()))]), "not p or not q or not r"); + + // Implies + not + assert_all!(i, implies_right(i(not(p())), i(not(q()))), "not p -> not q"); + assert_all!(i, implies_left(i(not(p())), i(not(q()))), "not q <- not p"); + + // If and only if + not + assert_all!(i, if_and_only_if(vec![i(not(p()))]), "not p"); + assert_all!(i, if_and_only_if(vec![i(not(p())), i(not(q())), i(not(r()))]), + "not p <-> not q <-> not r"); + } + + #[test] + fn format_combinations_quantified_formula() + { + // Not + quantified formula + assert_all!(i, not(exists(xyz(), i(p()))), "not exists X, Y, Z p"); + assert_all!(i, not(for_all(xyz(), i(p()))), "not forall X, Y, Z p"); + + // Quantified formula + quantified formula + assert_all!(i, exists(vec![x()], i(exists(vec![y()], p()))), "exists X exists Y p"); + assert_all!(i, exists(vec![x()], i(for_all(vec![y()], p()))), "exists X forall Y p"); + assert_all!(i, for_all(vec![x()], i(exists(vec![y()], p()))), "forall X exists Y p"); + assert_all!(i, for_all(vec![x()], i(for_all(vec![y()], p()))), "forall X forall Y p"); + assert_all!(i, exists(x1y1z1(), i(exists(x2y2z2(), p()))), + "exists X1, Y1, Z1 exists X2, Y2, Z2 p"); + assert_all!(i, exists(x1y1z1(), i(for_all(x2y2z2(), p()))), + "exists X1, Y1, Z1 forall X2, Y2, Z2 p"); + assert_all!(i, for_all(x1y1z1(), i(exists(x2y2z2(), p()))), + "forall X1, Y1, Z1 exists X2, Y2, Z2 p"); + assert_all!(i, for_all(x1y1z1(), i(for_all(x2y2z2(), p()))), + "forall X1, Y1, Z1 forall X2, Y2, Z2 p"); + + // And + quantified formula + assert_all!(i, and(vec![i(exists(xyz(), p()))]), "exists X, Y, Z p"); + assert_all!(i, and(vec![i(for_all(xyz(), p()))]), "forall X, Y, Z p"); + assert_all!(i, and(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())), + i(exists(x3y3z3(), r()))]), + "exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r"); + assert_all!(i, and(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())), + i(for_all(x3y3z3(), r()))]), + "forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r"); + + // Or + quantified formula + assert_all!(i, or(vec![i(exists(xyz(), p()))]), "exists X, Y, Z p"); + assert_all!(i, or(vec![i(for_all(xyz(), p()))]), "forall X, Y, Z p"); + assert_all!(i, or(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())), + i(exists(x3y3z3(), r()))]), + "exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r"); + assert_all!(i, or(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())), + i(for_all(x3y3z3(), r()))]), + "forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r"); + + // Implies + quantified formula + assert_all!(i, implies_right(i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q()))), + "exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q"); + assert_all!(i, implies_left(i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q()))), + "exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p"); + assert_all!(i, implies_right(i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q()))), + "forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q"); + assert_all!(i, implies_left(i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q()))), + "forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p"); + + // If and only if + quantified formula + assert_all!(i, if_and_only_if(vec![i(exists(x1y1z1(), p()))]), "exists X1, Y1, Z1 p"); + assert_all!(i, if_and_only_if(vec![i(for_all(x1y1z1(), p()))]), "forall X1, Y1, Z1 p"); + assert_all!(i, if_and_only_if(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())), + i(exists(x3y3z3(), r()))]), + "exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r"); + assert_all!(i, if_and_only_if(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())), + i(for_all(x3y3z3(), r()))]), + "forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r"); + } + + #[test] + fn format_combinations_and() + { + // Not + and + assert_all!(i, not(i(and(vec![p()]))), "not p"); + assert_all!(i, not(i(and(pqr()))), "not (p and q and r)"); + + // Quantified formula + and + assert_all!(i, exists(vec![x()], i(and(vec![p()]))), "exists X p"); + assert_all!(i, for_all(vec![x()], i(and(vec![p()]))), "forall X p"); + assert_all!(i, exists(vec![x()], i(and(pqr()))), "exists X (p and q and r)"); + assert_all!(i, for_all(vec![x()], i(and(pqr()))), "forall X (p and q and r)"); + assert_all!(i, exists(xyz(), i(and(vec![p()]))), "exists X, Y, Z p"); + assert_all!(i, for_all(xyz(), i(and(vec![p()]))), "forall X, Y, Z p"); + assert_all!(i, exists(xyz(), i(and(pqr()))), "exists X, Y, Z (p and q and r)"); + assert_all!(i, for_all(xyz(), i(and(pqr()))), "forall X, Y, Z (p and q and r)"); + + // And + and + assert_all!(i, and(vec![i(and(vec![p()]))]), "p"); + assert_all!(i, and(vec![i(and(pqr()))]), "p and q and r"); + assert_all!(i, and(vec![i(and(vec![p()])), i(and(vec![q()])), i(and(vec![r()]))]), + "p and q and r"); + assert_all!(i, and(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]), + "p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3"); + + // Or + and + assert_all!(i, or(vec![i(and(vec![p()]))]), "p"); + assert_all!(i, or(vec![i(and(pqr()))]), "p and q and r"); + assert_all!(i, or(vec![i(and(vec![p()])), i(and(vec![q()])), i(and(vec![r()]))]), + "p or q or r"); + assert_all!(i, or(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]), + "p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3"); + + // Implies + and + assert_all!(i, implies_right(i(and(vec![p()])), i(and(vec![q()]))), "p -> q"); + assert_all!(i, implies_left(i(and(vec![p()])), i(and(vec![q()]))), "q <- p"); + assert_all!(i, implies_right(i(and(p1q1r1())), i(and(p2q2r2()))), + "p1 and q1 and r1 -> p2 and q2 and r2"); + assert_all!(i, implies_left(i(and(p1q1r1())), i(and(p2q2r2()))), + "p2 and q2 and r2 <- p1 and q1 and r1"); + + // If and only if + and + assert_all!(i, if_and_only_if(vec![i(and(vec![p()]))]), "p"); + assert_all!(i, if_and_only_if(vec![i(and(pqr()))]), "p and q and r"); + assert_all!(i, if_and_only_if(vec![i(and(vec![p()])), i(and(vec![q()])), + i(and(vec![r()]))]), + "p <-> q <-> r"); + assert_all!(i, if_and_only_if(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]), + "p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3"); + } + + #[test] + fn format_combinations_or() + { + // Not + or + assert_all!(i, not(i(or(vec![p()]))), "not p"); + assert_all!(i, not(i(or(pqr()))), "not (p or q or r)"); + + // Quantified formula + or + assert_all!(i, exists(vec![x()], i(or(vec![p()]))), "exists X p"); + assert_all!(i, for_all(vec![x()], i(or(vec![p()]))), "forall X p"); + assert_all!(i, exists(vec![x()], i(or(pqr()))), "exists X (p or q or r)"); + assert_all!(i, for_all(vec![x()], i(or(pqr()))), "forall X (p or q or r)"); + assert_all!(i, exists(xyz(), i(or(vec![p()]))), "exists X, Y, Z p"); + assert_all!(i, for_all(xyz(), i(or(vec![p()]))), "forall X, Y, Z p"); + assert_all!(i, exists(xyz(), i(or(pqr()))), "exists X, Y, Z (p or q or r)"); + assert_all!(i, for_all(xyz(), i(or(pqr()))), "forall X, Y, Z (p or q or r)"); + + // And + or + assert_all!(i, and(vec![i(or(vec![p()]))]), "p"); + assert_all!(i, and(vec![i(or(pqr()))]), "p or q or r"); + assert_all!(i, and(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]), + "p and q and r"); + assert_all!(i, and(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]), + "(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)"); + + // Or + or + assert_all!(i, or(vec![i(or(vec![p()]))]), "p"); + assert_all!(i, or(vec![i(or(pqr()))]), "p or q or r"); + assert_all!(i, or(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]), + "p or q or r"); + assert_all!(i, or(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]), + "p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3"); + + // Implies + or + assert_all!(i, implies_right(i(or(vec![p()])), i(or(vec![q()]))), "p -> q"); + assert_all!(i, implies_left(i(or(vec![p()])), i(or(vec![q()]))), "q <- p"); + assert_all!(i, implies_right(i(or(p1q1r1())), i(or(p2q2r2()))), + "p1 or q1 or r1 -> p2 or q2 or r2"); + assert_all!(i, implies_left(i(or(p1q1r1())), i(or(p2q2r2()))), + "p2 or q2 or r2 <- p1 or q1 or r1"); + + // If and only if + or + assert_all!(i, if_and_only_if(vec![i(or(vec![p()]))]), "p"); + assert_all!(i, if_and_only_if(vec![i(or(pqr()))]), "p or q or r"); + assert_all!(i, if_and_only_if(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]), + "p <-> q <-> r"); + assert_all!(i, if_and_only_if(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]), + "p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3"); + } + + #[test] + fn format_combinations_implies() + { + // Not + implies + assert_all!(i, not(i(implies_right(p(), q()))), "not (p -> q)"); + assert_all!(i, not(i(implies_left(p(), q()))), "not (q <- p)"); + + // Quantified formula + implies + assert_all!(i, exists(vec![x()], i(implies_right(p(), q()))), "exists X (p -> q)"); + assert_all!(i, exists(vec![x()], i(implies_left(p(), q()))), "exists X (q <- p)"); + assert_all!(i, for_all(vec![x()], i(implies_right(p(), q()))), "forall X (p -> q)"); + assert_all!(i, for_all(vec![x()], i(implies_left(p(), q()))), "forall X (q <- p)"); + assert_all!(i, exists(xyz(), i(implies_right(p(), q()))), "exists X, Y, Z (p -> q)"); + assert_all!(i, exists(xyz(), i(implies_left(p(), q()))), "exists X, Y, Z (q <- p)"); + assert_all!(i, for_all(xyz(), i(implies_right(p(), q()))), "forall X, Y, Z (p -> q)"); + assert_all!(i, for_all(xyz(), i(implies_left(p(), q()))), "forall X, Y, Z (q <- p)"); + + // And + implies + assert_all!(i, and(vec![i(implies_right(p(), q()))]), "p -> q"); + assert_all!(i, and(vec![i(implies_left(p(), q()))]), "q <- p"); + assert_all!(i, and(vec![i(implies_right(p1(), q1())), i(implies_right(p2(), q2())), + i(implies_right(p3(), q3()))]), + "(p1 -> q1) and (p2 -> q2) and (p3 -> q3)"); + assert_all!(i, and(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())), + i(implies_left(p3(), q3()))]), + "(q1 <- p1) and (q2 <- p2) and (q3 <- p3)"); + + // Or + implies + assert_all!(i, or(vec![i(implies_right(p(), q()))]), "p -> q"); + assert_all!(i, or(vec![i(implies_left(p(), q()))]), "q <- p"); + assert_all!(i, or(vec![i(implies_right(p1(), q1())), i(implies_right(p2(), q2())), + i(implies_right(p3(), q3()))]), + "(p1 -> q1) or (p2 -> q2) or (p3 -> q3)"); + assert_all!(i, or(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())), + i(implies_left(p3(), q3()))]), + "(q1 <- p1) or (q2 <- p2) or (q3 <- p3)"); + + // Implies + implies + assert_all!(i, implies_right(i(implies_right(p1(), q1())), i(implies_right(p2(), q2()))), + "(p1 -> q1) -> p2 -> q2"); + assert_all!(i, implies_right(i(implies_left(p1(), q1())), i(implies_left(p2(), q2()))), + "(q1 <- p1) -> (q2 <- p2)"); + assert_all!(i, implies_left(i(implies_right(p1(), q1())), i(implies_right(p2(), q2()))), + "(p2 -> q2) <- (p1 -> q1)"); + assert_all!(i, implies_left(i(implies_left(p1(), q1())), i(implies_left(p2(), q2()))), + "q2 <- p2 <- (q1 <- p1)"); + + // If and only if + implies + assert_all!(i, if_and_only_if(vec![i(implies_right(p(), q()))]), "p -> q"); + assert_all!(i, if_and_only_if(vec![i(implies_left(p(), q()))]), "q <- p"); + assert_all!(i, if_and_only_if(vec![i(implies_right(p1(), q1())), + i(implies_right(p2(), q2())), i(implies_right(p3(), q3()))]), + "p1 -> q1 <-> p2 -> q2 <-> p3 -> q3"); + assert_all!(i, if_and_only_if(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())), + i(implies_left(p3(), q3()))]), + "q1 <- p1 <-> q2 <- p2 <-> q3 <- p3"); + } + + #[test] + fn format_combinations_if_and_only_if() + { + // Not + if and only if + assert_all!(i, not(i(if_and_only_if(vec![p()]))), "not p"); + assert_all!(i, not(i(if_and_only_if(pqr()))), "not (p <-> q <-> r)"); + + // Quantified formula + if and only if + assert_all!(i, exists(vec![x()], i(if_and_only_if(vec![p()]))), "exists X p"); + assert_all!(i, for_all(vec![x()], i(if_and_only_if(vec![p()]))), "forall X p"); + assert_all!(i, exists(vec![x()], i(if_and_only_if(pqr()))), "exists X (p <-> q <-> r)"); + assert_all!(i, for_all(vec![x()], i(if_and_only_if(pqr()))), "forall X (p <-> q <-> r)"); + assert_all!(i, exists(xyz(), i(if_and_only_if(vec![p()]))), "exists X, Y, Z p"); + assert_all!(i, for_all(xyz(), i(if_and_only_if(vec![p()]))), "forall X, Y, Z p"); + assert_all!(i, exists(xyz(), i(if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)"); + assert_all!(i, for_all(xyz(), i(if_and_only_if(pqr()))), "forall X, Y, Z (p <-> q <-> r)"); + + // And + if and only if + assert_all!(i, and(vec![i(if_and_only_if(vec![p()]))]), "p"); + assert_all!(i, and(vec![i(if_and_only_if(pqr()))]), "p <-> q <-> r"); + assert_all!(i, and(vec![i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()])), + i(if_and_only_if(vec![r()]))]), + "p and q and r"); + assert_all!(i, and(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())), + i(if_and_only_if(p3q3r3()))]), + "(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)"); + + // Or + if and only if + assert_all!(i, or(vec![i(if_and_only_if(vec![p()]))]), "p"); + assert_all!(i, or(vec![i(if_and_only_if(pqr()))]), "p <-> q <-> r"); + assert_all!(i, or(vec![i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()])), + i(if_and_only_if(vec![r()]))]), + "p or q or r"); + assert_all!(i, or(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())), + i(if_and_only_if(p3q3r3()))]), + "(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)"); + + // Implies + if and only if + assert_all!(i, implies_right(i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()]))), + "p -> q"); + assert_all!(i, implies_left(i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()]))), + "q <- p"); + assert_all!(i, implies_right(i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2()))), + "(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)"); + assert_all!(i, implies_left(i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2()))), + "(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)"); + + // If and only if + if and only if + assert_all!(i, if_and_only_if(vec![i(if_and_only_if(vec![p()]))]), "p"); + assert_all!(i, if_and_only_if(vec![i(if_and_only_if(pqr()))]), "p <-> q <-> r"); + assert_all!(i, if_and_only_if(vec![i(if_and_only_if(vec![p()])), + i(if_and_only_if(vec![q()])), i(if_and_only_if(vec![r()]))]), + "p <-> q <-> r"); + assert_all!(i, if_and_only_if(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())), + i(if_and_only_if(p3q3r3()))]), + "(p1 <-> q1 <-> r1) <-> (p2 <-> q2 <-> r2) <-> (p3 <-> q3 <-> r3)"); } } diff --git a/src/format/terms.rs b/src/format/terms.rs index 3222efc..393f482 100644 --- a/src/format/terms.rs +++ b/src/format/terms.rs @@ -1,41 +1,3 @@ -use super::Precedence; - -impl Precedence for crate::Term -{ - fn precedence(&self) -> i32 - { - match &self - { - Self::Boolean(_) - | Self::Function(_) - | Self::SpecialInteger(_) - | Self::Integer(_) - | Self::String(_) - | Self::Variable(_) - | Self::UnaryOperation( - crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..}) - => 0, - Self::UnaryOperation( - crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..}) - => 1, - Self::BinaryOperation( - crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..}) - => 2, - Self::BinaryOperation( - crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..}) - | Self::BinaryOperation( - crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..}) - | Self::BinaryOperation( - crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..}) - => 3, - Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..}) - | Self::BinaryOperation( - crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..}) - => 4, - } - } -} - impl std::fmt::Debug for crate::SpecialInteger { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result @@ -88,18 +50,114 @@ impl std::fmt::Display for crate::VariableDeclaration } } -pub(crate) struct TermDisplay<'term> +#[derive(Clone, Copy, Eq, PartialEq)] +pub(crate) enum TermPosition { - parent_precedence: Option, - term: &'term crate::Term, + Any, + Left, + Right, } -pub(crate) fn display_term(term: &crate::Term, parent_precedence: Option) -> TermDisplay +pub(crate) struct TermDisplay<'term> +{ + term: &'term crate::Term, + parent_term: Option<&'term crate::Term>, + position: TermPosition, +} + +impl<'term> TermDisplay<'term> +{ + fn requires_parentheses(&self) -> bool + { + use crate::Term; + + let parent_term = match self.parent_term + { + Some(parent_term) => parent_term, + None => return false, + }; + + // The absolute value operation never requires parentheses, as it has its own parentheses + if let Term::UnaryOperation( + crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..}) = parent_term + { + return false; + } + + match self.term + { + Term::Boolean(_) + | Term::SpecialInteger(_) + | Term::Integer(_) + | Term::String(_) + | Term::Variable(_) + | Term::Function(_) + | Term::UnaryOperation(_) + => false, + Term::BinaryOperation(binary_operation) => + { + let parent_binary_operation = match parent_term + { + Term::BinaryOperation(parent_binary_operation) => parent_binary_operation, + // Binary operations nested in the negative operation always require parentheses + Term::UnaryOperation( + crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..}) + => return true, + _ => return false, + }; + + match binary_operation.operator + { + crate::BinaryOperator::Exponentiate => + parent_binary_operation.operator == crate::BinaryOperator::Exponentiate + && self.position == TermPosition::Left, + crate::BinaryOperator::Multiply + | crate::BinaryOperator::Divide + => match parent_binary_operation.operator + { + crate::BinaryOperator::Exponentiate => true, + crate::BinaryOperator::Divide + | crate::BinaryOperator::Modulo + => self.position == TermPosition::Right, + _ => false, + }, + crate::BinaryOperator::Modulo => match parent_binary_operation.operator + { + crate::BinaryOperator::Exponentiate => true, + crate::BinaryOperator::Multiply + | crate::BinaryOperator::Divide + | crate::BinaryOperator::Modulo + => self.position == TermPosition::Right, + _ => false, + }, + crate::BinaryOperator::Add + | crate::BinaryOperator::Subtract + => match parent_binary_operation.operator + { + crate::BinaryOperator::Exponentiate + | crate::BinaryOperator::Multiply + | crate::BinaryOperator::Divide + | crate::BinaryOperator::Modulo + => true, + crate::BinaryOperator::Subtract + => self.position == TermPosition::Right, + _ => false, + }, + } + }, + } + } +} + +pub(crate) fn display_term<'term>(term: &'term crate::Term, parent_term: Option<&'term crate::Term>, + position: TermPosition) + -> TermDisplay<'term> { TermDisplay { - parent_precedence, term, + parent_term, + position, } } @@ -107,12 +165,7 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - let precedence = self.term.precedence(); - let requires_parentheses = match self.parent_precedence - { - Some(parent_precedence) => precedence > parent_precedence, - None => false, - }; + let requires_parentheses = self.requires_parentheses(); if requires_parentheses { @@ -121,12 +174,13 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> match &self.term { - crate::Term::Boolean(true) => write!(format, "true"), - crate::Term::Boolean(false) => write!(format, "false"), - crate::Term::SpecialInteger(value) => write!(format, "{:?}", value), - crate::Term::Integer(value) => write!(format, "{}", value), - crate::Term::String(value) => write!(format, "\"{}\"", value), - crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration), + crate::Term::Boolean(true) => write!(format, "true")?, + crate::Term::Boolean(false) => write!(format, "false")?, + crate::Term::SpecialInteger(value) => write!(format, "{:?}", value)?, + crate::Term::Integer(value) => write!(format, "{}", value)?, + crate::Term::String(value) => write!(format, "\"{}\"", + value.replace("\\", "\\\\").replace("\n", "\\n").replace("\t", "\\t"))?, + crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration)?, crate::Term::Function(function) => { write!(format, "{}", function.declaration.name)?; @@ -143,15 +197,14 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> for argument in &function.arguments { - write!(format, "{}{:?}", separator, display_term(&argument, None))?; + write!(format, "{}{:?}", separator, + display_term(&argument, Some(self.term), TermPosition::Any))?; separator = ", "; } write!(format, ")")?; } - - Ok(()) }, crate::Term::BinaryOperation(binary_operation) => { @@ -165,70 +218,20 @@ impl<'term> std::fmt::Debug for TermDisplay<'term> crate::BinaryOperator::Exponentiate => "**", }; - let left_requires_parentheses = binary_operation.left.precedence() == precedence - // Exponentiation is right-associative and thus requires parentheses when - // nested on the left side - && binary_operation.operator == crate::BinaryOperator::Exponentiate; - - // The subtraction, division, and modulo operators require parentheses around the - // right argument even if it has the same precedence - let operator_requires_right_priority = match binary_operation.operator - { - crate::BinaryOperator::Subtract - | crate::BinaryOperator::Divide - | crate::BinaryOperator::Modulo - => true, - _ => false, - }; - - // Additionally, modulo operations nested to the right of another multiplicative - // operation always require parentheses - let right_requires_priority = match *binary_operation.right - { - crate::Term::BinaryOperation( - crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..}) - => true, - _ => false, - }; - - let right_requires_parentheses = binary_operation.right.precedence() == precedence - && (operator_requires_right_priority || right_requires_priority); - - if left_requires_parentheses - { - write!(format, "(")?; - } - - write!(format, "{:?}", display_term(&binary_operation.left, Some(precedence)))?; - - if left_requires_parentheses - { - write!(format, ")")?; - } - - write!(format, " {} ", operator_string)?; - - if right_requires_parentheses - { - write!(format, "(")?; - } - - write!(format, "{:?}", display_term(&binary_operation.right, Some(precedence)))?; - - if right_requires_parentheses - { - write!(format, ")")?; - } - - Ok(()) + write!(format, "{:?} {} {:?}", + display_term(&binary_operation.left, Some(self.term), TermPosition::Left), + operator_string, + display_term(&binary_operation.right, Some(self.term), TermPosition::Right))?; }, crate::Term::UnaryOperation( crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument}) - => write!(format, "-{:?}", display_term(argument, Some(precedence))), + => write!(format, "-{:?}", + display_term(argument, Some(self.term), TermPosition::Any))?, crate::Term::UnaryOperation( crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument}) - => write!(format, "|{:?}|", display_term(argument, None)), - }?; + => write!(format, "|{:?}|", + display_term(argument, Some(self.term), TermPosition::Any))?, + } if requires_parentheses { @@ -251,7 +254,7 @@ impl std::fmt::Debug for crate::Term { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{:?}", display_term(&self, None)) + write!(format, "{:?}", display_term(&self, None, TermPosition::Any)) } } @@ -259,6 +262,828 @@ impl std::fmt::Display for crate::Term { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(format, "{}", display_term(&self, None)) + write!(format, "{}", display_term(&self, None, TermPosition::Any)) + } +} + +#[cfg(test)] +pub(crate) mod tests +{ + use crate::*; + + macro_rules! assert + { + ($term:expr, $output:expr) => + { + assert_eq!(format($term), $output); + }; + } + + fn format(term: Box) -> String + { + format!("{}", term) + } + + pub(crate) fn absolute_value(argument: Box) -> Box + { + Box::new(Term::absolute_value(argument)) + } + + pub(crate) fn add(left: Box, right: Box) -> Box + { + Box::new(Term::add(left, right)) + } + + pub(crate) fn constant(name: &str) -> Box + { + Box::new(Term::function(function_declaration(name, 0), vec![])) + } + + pub(crate) fn divide(left: Box, right: Box) -> Box + { + Box::new(Term::divide(left, right)) + } + + pub(crate) fn exponentiate(left: Box, right: Box) -> Box + { + Box::new(Term::exponentiate(left, right)) + } + + pub(crate) fn false_() -> Box + { + Box::new(Term::false_()) + } + + pub(crate) fn function(name: &str, arguments: Vec>) -> Box + { + Box::new(Term::function(function_declaration(name, arguments.len()), + arguments.into_iter().map(|x| *x).collect())) + } + + pub(crate) fn function_declaration(name: &str, arity: usize) -> std::rc::Rc + { + std::rc::Rc::new(FunctionDeclaration::new(name.to_string(), arity)) + } + + pub(crate) fn infimum() -> Box + { + Box::new(Term::infimum()) + } + + pub(crate) fn integer(value: i32) -> Box + { + Box::new(Term::integer(value)) + } + + pub(crate) fn modulo(left: Box, right: Box) -> Box + { + Box::new(Term::modulo(left, right)) + } + + pub(crate) fn multiply(left: Box, right: Box) -> Box + { + Box::new(Term::multiply(left, right)) + } + + pub(crate) fn negative(argument: Box) -> Box + { + Box::new(Term::negative(argument)) + } + + pub(crate) fn subtract(left: Box, right: Box) -> Box + { + Box::new(Term::subtract(left, right)) + } + + pub(crate) fn supremum() -> Box + { + Box::new(Term::supremum()) + } + + pub(crate) fn string(value: &str) -> Box + { + Box::new(Term::string(value.to_string())) + } + + pub(crate) fn true_() -> Box + { + Box::new(Term::true_()) + } + + pub(crate) fn variable(name: &str) -> Box + { + Box::new(Term::variable(variable_declaration(name))) + } + + pub(crate) fn variable_declaration(name: &str) -> std::rc::Rc + { + std::rc::Rc::new(VariableDeclaration::new(name.to_string())) + } + + pub(crate) fn a() -> Box + { + constant("a") + } + + pub(crate) fn b() -> Box + { + constant("b") + } + + pub(crate) fn c() -> Box + { + constant("c") + } + + pub(crate) fn d() -> Box + { + constant("d") + } + + pub(crate) fn e() -> Box + { + constant("e") + } + + pub(crate) fn abc() -> Vec> + { + vec![a(), b(), c()] + } + + pub(crate) fn a1b1c1() -> Vec> + { + vec![constant("a1"), constant("b1"), constant("c1")] + } + + pub(crate) fn a2b2c2() -> Vec> + { + vec![constant("a2"), constant("b2"), constant("c2")] + } + + pub(crate) fn x() -> Box + { + variable("X") + } + + pub(crate) fn y() -> Box + { + variable("Y") + } + + pub(crate) fn z() -> Box + { + variable("Z") + } + + pub(crate) fn xyz() -> Vec> + { + vec![x(), y(), z()] + } + + #[test] + fn format_binary_operation() + { + assert!(add(a(), constant("b")), "a + b"); + assert!(subtract(a(), constant("b")), "a - b"); + assert!(multiply(a(), constant("b")), "a * b"); + assert!(divide(a(), constant("b")), "a / b"); + assert!(modulo(a(), constant("b")), "a % b"); + assert!(exponentiate(a(), constant("b")), "a ** b"); + } + + #[test] + fn format_boolean() + { + assert!(true_(), "true"); + assert!(false_(), "false"); + } + + #[test] + fn format_special_integer() + { + assert!(infimum(), "#inf"); + assert!(supremum(), "#sup"); + } + + #[test] + fn format_integer() + { + assert!(integer(0), "0"); + assert!(integer(1), "1"); + assert!(integer(10000), "10000"); + assert!(integer(-1), "-1"); + assert!(integer(-10000), "-10000"); + } + + #[test] + fn format_string() + { + assert!(string(""), "\"\""); + assert!(string(" "), "\" \""); + assert!(string(" "), "\" \""); + assert!(string("a"), "\"a\""); + assert!(string("test test"), "\"test test\""); + assert!(string("123 123"), "\"123 123\""); + assert!(string("\ntest\n123\n"), "\"\\ntest\\n123\\n\""); + assert!(string("\ttest\t123\t"), "\"\\ttest\\t123\\t\""); + assert!(string("\\test\\123\\"), "\"\\\\test\\\\123\\\\\""); + assert!(string("๐Ÿ™‚test๐Ÿ™‚123๐Ÿ™‚"), "\"๐Ÿ™‚test๐Ÿ™‚123๐Ÿ™‚\""); + } + + #[test] + fn format_function() + { + assert!(a(), "a"); + assert!(constant("constant"), "constant"); + assert!(function("f", vec![a()]), "f(a)"); + assert!(function("f", abc()), "f(a, b, c)"); + assert!(function("function", abc()), "function(a, b, c)"); + + assert!(function("function", vec![ + exponentiate(absolute_value(multiply(a(), integer(-20))), integer(2)), + string("test"), + function("f", vec![multiply(add(b(), c()), subtract(b(), c())), infimum(), x()])]), + "function(|a * -20| ** 2, \"test\", f((b + c) * (b - c), #inf, X))"); + + // TODO: escape functions that start with capital letters or that conflict with keywords + } + + #[test] + fn format_function_declaration() + { + assert_eq!(format!("{}", function_declaration("a", 0)), "a/0"); + assert_eq!(format!("{}", function_declaration("constant", 0)), "constant/0"); + assert_eq!(format!("{}", function_declaration("f", 1)), "f/1"); + assert_eq!(format!("{}", function_declaration("f", 3)), "f/3"); + assert_eq!(format!("{}", function_declaration("function", 3)), "function/3"); + } + + #[test] + fn format_variable() + { + assert!(variable("X"), "X"); + assert!(variable("Variable"), "Variable"); + } + + #[test] + fn format_combinations_boolean() + { + // Function + Boolean + assert!(function("f", vec![true_()]), "f(true)"); + assert!(function("f", vec![false_()]), "f(false)"); + assert!(function("f", vec![true_(), true_(), true_()]), "f(true, true, true)"); + assert!(function("f", vec![false_(), false_(), false_()]), "f(false, false, false)"); + + // Absolute value + Boolean + assert!(absolute_value(true_()), "|true|"); + assert!(absolute_value(false_()), "|false|"); + + // Negative + Boolean + assert!(negative(true_()), "-true"); + assert!(negative(false_()), "-false"); + + // Exponentiate + Boolean + assert!(exponentiate(true_(), true_()), "true ** true"); + assert!(exponentiate(false_(), false_()), "false ** false"); + + // Multiply + Boolean + assert!(multiply(true_(), true_()), "true * true"); + assert!(multiply(false_(), false_()), "false * false"); + + // Divide + Boolean + assert!(divide(true_(), true_()), "true / true"); + assert!(divide(false_(), false_()), "false / false"); + + // Modulo + Boolean + assert!(modulo(true_(), true_()), "true % true"); + assert!(modulo(false_(), false_()), "false % false"); + + // Add + Boolean + assert!(add(true_(), true_()), "true + true"); + assert!(add(false_(), false_()), "false + false"); + + // Subtract + Boolean + assert!(subtract(true_(), true_()), "true - true"); + assert!(subtract(false_(), false_()), "false - false"); + } + + #[test] + fn format_combinations_special_integer() + { + // Function + special integer + assert!(function("f", vec![infimum()]), "f(#inf)"); + assert!(function("f", vec![supremum()]), "f(#sup)"); + assert!(function("f", vec![infimum(), infimum(), infimum()]), "f(#inf, #inf, #inf)"); + assert!(function("f", vec![supremum(), supremum(), supremum()]), "f(#sup, #sup, #sup)"); + + // Absolute value + special integer + assert!(absolute_value(infimum()), "|#inf|"); + assert!(absolute_value(supremum()), "|#sup|"); + + // Negative + special integer + assert!(negative(infimum()), "-#inf"); + assert!(negative(supremum()), "-#sup"); + + // Exponentiate + special integer + assert!(exponentiate(infimum(), infimum()), "#inf ** #inf"); + assert!(exponentiate(supremum(), supremum()), "#sup ** #sup"); + + // Multiply + special integer + assert!(multiply(infimum(), infimum()), "#inf * #inf"); + assert!(multiply(supremum(), supremum()), "#sup * #sup"); + + // Divide + special integer + assert!(divide(infimum(), infimum()), "#inf / #inf"); + assert!(divide(supremum(), supremum()), "#sup / #sup"); + + // Modulo + special integer + assert!(modulo(infimum(), infimum()), "#inf % #inf"); + assert!(modulo(supremum(), supremum()), "#sup % #sup"); + + // Add + special integer + assert!(add(infimum(), infimum()), "#inf + #inf"); + assert!(add(supremum(), supremum()), "#sup + #sup"); + + // Subtract + special integer + assert!(subtract(infimum(), infimum()), "#inf - #inf"); + assert!(subtract(supremum(), supremum()), "#sup - #sup"); + } + + #[test] + fn format_combinations_integer() + { + // Function + integer + assert!(function("f", vec![integer(0)]), "f(0)"); + assert!(function("f", vec![integer(10000)]), "f(10000)"); + assert!(function("f", vec![integer(-10000)]), "f(-10000)"); + assert!(function("f", vec![integer(0), integer(0), integer(0)]), "f(0, 0, 0)"); + assert!(function("f", vec![integer(10000), integer(10000), integer(10000)]), + "f(10000, 10000, 10000)"); + assert!(function("f", vec![integer(-10000), integer(-10000), integer(-10000)]), + "f(-10000, -10000, -10000)"); + + // Absolute value + integer + assert!(absolute_value(integer(0)), "|0|"); + assert!(absolute_value(integer(10000)), "|10000|"); + assert!(absolute_value(integer(-10000)), "|-10000|"); + + // Negative + integer + assert!(negative(integer(0)), "-0"); + assert!(negative(integer(10000)), "-10000"); + assert!(negative(integer(-10000)), "--10000"); + + // Exponentiate + integer + assert!(exponentiate(integer(0), integer(0)), "0 ** 0"); + assert!(exponentiate(integer(10000), integer(10000)), "10000 ** 10000"); + assert!(exponentiate(integer(-10000), integer(-10000)), "-10000 ** -10000"); + + // Multiply + integer + assert!(multiply(integer(0), integer(0)), "0 * 0"); + assert!(multiply(integer(10000), integer(10000)), "10000 * 10000"); + assert!(multiply(integer(-10000), integer(-10000)), "-10000 * -10000"); + + // Divide + integer + assert!(divide(integer(0), integer(0)), "0 / 0"); + assert!(divide(integer(10000), integer(10000)), "10000 / 10000"); + assert!(divide(integer(-10000), integer(-10000)), "-10000 / -10000"); + + // Modulo + integer + assert!(modulo(integer(0), integer(0)), "0 % 0"); + assert!(modulo(integer(10000), integer(10000)), "10000 % 10000"); + assert!(modulo(integer(-10000), integer(-10000)), "-10000 % -10000"); + + // Add + integer + assert!(add(integer(0), integer(0)), "0 + 0"); + assert!(add(integer(10000), integer(10000)), "10000 + 10000"); + assert!(add(integer(-10000), integer(-10000)), "-10000 + -10000"); + + // Subtract + integer + assert!(subtract(integer(0), integer(0)), "0 - 0"); + assert!(subtract(integer(10000), integer(10000)), "10000 - 10000"); + assert!(subtract(integer(-10000), integer(-10000)), "-10000 - -10000"); + } + + #[test] + fn format_combinations_string() + { + // Function + string + assert!(function("f", vec![string("")]), "f(\"\")"); + assert!(function("f", vec![string("test 123")]), "f(\"test 123\")"); + assert!(function("f", vec![string("\\a\nb๐Ÿ™‚c\t")]), "f(\"\\\\a\\nb๐Ÿ™‚c\\t\")"); + assert!(function("f", vec![string(""), string(""), string("")]), "f(\"\", \"\", \"\")"); + assert!(function("f", vec![string("test 123"), string("test 123"), string("test 123")]), + "f(\"test 123\", \"test 123\", \"test 123\")"); + assert!(function("f", vec![string("\\a\nb๐Ÿ™‚c\t"), string("\\a\nb๐Ÿ™‚c\t"), + string("\\a\nb๐Ÿ™‚c\t")]), + "f(\"\\\\a\\nb๐Ÿ™‚c\\t\", \"\\\\a\\nb๐Ÿ™‚c\\t\", \"\\\\a\\nb๐Ÿ™‚c\\t\")"); + + // Absolute value + string + assert!(absolute_value(string("")), "|\"\"|"); + assert!(absolute_value(string("test 123")), "|\"test 123\"|"); + assert!(absolute_value(string("\\a\nb๐Ÿ™‚c\t")), "|\"\\\\a\\nb๐Ÿ™‚c\\t\"|"); + + // Negative + string + assert!(negative(string("")), "-\"\""); + assert!(negative(string("test 123")), "-\"test 123\""); + assert!(negative(string("\\a\nb๐Ÿ™‚c\t")), "-\"\\\\a\\nb๐Ÿ™‚c\\t\""); + + // Exponentiate + string + assert!(exponentiate(string(""), string("")), "\"\" ** \"\""); + assert!(exponentiate(string("test 123"), string("test 123")), + "\"test 123\" ** \"test 123\""); + assert!(exponentiate(string("\\a\nb๐Ÿ™‚c\t"), string("\\a\nb๐Ÿ™‚c\t")), + "\"\\\\a\\nb๐Ÿ™‚c\\t\" ** \"\\\\a\\nb๐Ÿ™‚c\\t\""); + + // Multiply + string + assert!(multiply(string(""), string("")), "\"\" * \"\""); + assert!(multiply(string("test 123"), string("test 123")), "\"test 123\" * \"test 123\""); + assert!(multiply(string("\\a\nb๐Ÿ™‚c\t"), string("\\a\nb๐Ÿ™‚c\t")), + "\"\\\\a\\nb๐Ÿ™‚c\\t\" * \"\\\\a\\nb๐Ÿ™‚c\\t\""); + + // Divide + string + assert!(divide(string(""), string("")), "\"\" / \"\""); + assert!(divide(string("test 123"), string("test 123")), "\"test 123\" / \"test 123\""); + assert!(divide(string("\\a\nb๐Ÿ™‚c\t"), string("\\a\nb๐Ÿ™‚c\t")), + "\"\\\\a\\nb๐Ÿ™‚c\\t\" / \"\\\\a\\nb๐Ÿ™‚c\\t\""); + + // Modulo + string + assert!(modulo(string(""), string("")), "\"\" % \"\""); + assert!(modulo(string("test 123"), string("test 123")), "\"test 123\" % \"test 123\""); + assert!(modulo(string("\\a\nb๐Ÿ™‚c\t"), string("\\a\nb๐Ÿ™‚c\t")), + "\"\\\\a\\nb๐Ÿ™‚c\\t\" % \"\\\\a\\nb๐Ÿ™‚c\\t\""); + + // Add + string + assert!(add(string(""), string("")), "\"\" + \"\""); + assert!(add(string("test 123"), string("test 123")), "\"test 123\" + \"test 123\""); + assert!(add(string("\\a\nb๐Ÿ™‚c\t"), string("\\a\nb๐Ÿ™‚c\t")), + "\"\\\\a\\nb๐Ÿ™‚c\\t\" + \"\\\\a\\nb๐Ÿ™‚c\\t\""); + + // Subtract + string + assert!(subtract(string(""), string("")), "\"\" - \"\""); + assert!(subtract(string("test 123"), string("test 123")), "\"test 123\" - \"test 123\""); + assert!(subtract(string("\\a\nb๐Ÿ™‚c\t"), string("\\a\nb๐Ÿ™‚c\t")), + "\"\\\\a\\nb๐Ÿ™‚c\\t\" - \"\\\\a\\nb๐Ÿ™‚c\\t\""); + } + + #[test] + fn format_combinations_variable() + { + let variable = || variable("Variable"); + + // Function + variable + assert!(function("f", vec![x()]), "f(X)"); + assert!(function("f", vec![variable()]), "f(Variable)"); + assert!(function("f", xyz()), "f(X, Y, Z)"); + assert!(function("f", vec![variable(), variable(), variable()]), + "f(Variable, Variable, Variable)"); + + // Absolute value + variable + assert!(absolute_value(x()), "|X|"); + assert!(absolute_value(variable()), "|Variable|"); + + // Negative + variable + assert!(negative(x()), "-X"); + assert!(negative(variable()), "-Variable"); + + // Exponentiate + variable + assert!(exponentiate(x(), y()), "X ** Y"); + assert!(exponentiate(variable(), variable()), "Variable ** Variable"); + + // Multiply + variable + assert!(multiply(x(), y()), "X * Y"); + assert!(multiply(variable(), variable()), "Variable * Variable"); + + // Divide + variable + assert!(divide(x(), y()), "X / Y"); + assert!(divide(variable(), variable()), "Variable / Variable"); + + // Modulo + variable + assert!(modulo(x(), y()), "X % Y"); + assert!(modulo(variable(), variable()), "Variable % Variable"); + + // Add + variable + assert!(add(x(), y()), "X + Y"); + assert!(add(variable(), variable()), "Variable + Variable"); + + // Subtract + variable + assert!(subtract(x(), y()), "X - Y"); + assert!(subtract(variable(), variable()), "Variable - Variable"); + } + + #[test] + fn format_combinations_function() + { + let f_a = || function("f", vec![a()]); + let g_b = || function("g", vec![b()]); + let f_abc = || function("f", abc()); + let f_a1b1c1 = || function("f", a1b1c1()); + let g_a2b2c2 = || function("g", a2b2c2()); + + // Function + function + // TODO + + // Absolute value + function + assert!(absolute_value(a()), "|a|"); + assert!(absolute_value(f_a()), "|f(a)|"); + assert!(absolute_value(f_abc()), "|f(a, b, c)|"); + + // Negative + function + assert!(negative(a()), "-a"); + assert!(negative(f_a()), "-f(a)"); + assert!(negative(f_abc()), "-f(a, b, c)"); + + // Exponentiate + function + assert!(exponentiate(a(), b()), "a ** b"); + assert!(exponentiate(f_a(), g_b()), "f(a) ** g(b)"); + assert!(exponentiate(f_a1b1c1(), g_a2b2c2()), "f(a1, b1, c1) ** g(a2, b2, c2)"); + + // Multiply + function + assert!(multiply(a(), b()), "a * b"); + assert!(multiply(f_a(), g_b()), "f(a) * g(b)"); + assert!(multiply(f_a1b1c1(), g_a2b2c2()), "f(a1, b1, c1) * g(a2, b2, c2)"); + + // Divide + function + assert!(divide(a(), b()), "a / b"); + assert!(divide(f_a(), g_b()), "f(a) / g(b)"); + assert!(divide(f_a1b1c1(), g_a2b2c2()), "f(a1, b1, c1) / g(a2, b2, c2)"); + + // Modulo + function + assert!(modulo(a(), b()), "a % b"); + assert!(modulo(f_a(), g_b()), "f(a) % g(b)"); + assert!(modulo(f_a1b1c1(), g_a2b2c2()), "f(a1, b1, c1) % g(a2, b2, c2)"); + + // Add + function + assert!(add(a(), b()), "a + b"); + assert!(add(f_a(), g_b()), "f(a) + g(b)"); + assert!(add(f_a1b1c1(), g_a2b2c2()), "f(a1, b1, c1) + g(a2, b2, c2)"); + + // Subtract + function + assert!(subtract(a(), b()), "a - b"); + assert!(subtract(f_a(), g_b()), "f(a) - g(b)"); + assert!(subtract(f_a1b1c1(), g_a2b2c2()), "f(a1, b1, c1) - g(a2, b2, c2)"); + } + + #[test] + fn format_combinations_absolute_value() + { + // Function + absolute value + assert!(function("f", vec![absolute_value(a())]), "f(|a|)"); + assert!(function("f", vec![absolute_value(a()), absolute_value(b()), absolute_value(c())]), + "f(|a|, |b|, |c|)"); + + // Absolute value + absolute value + assert!(absolute_value(absolute_value(a())), "||a||"); + + // Negative + absolute value + assert!(negative(absolute_value(a())), "-|a|"); + + // Exponentiate + absolute value + assert!(exponentiate(absolute_value(a()), absolute_value(b())), "|a| ** |b|"); + + // Multiply + absolute value + assert!(multiply(absolute_value(a()), absolute_value(b())), "|a| * |b|"); + + // Divide + absolute value + assert!(divide(absolute_value(a()), absolute_value(b())), "|a| / |b|"); + + // Modulo + absolute value + assert!(modulo(absolute_value(a()), absolute_value(b())), "|a| % |b|"); + + // Add + absolute value + assert!(add(absolute_value(a()), absolute_value(b())), "|a| + |b|"); + + // Subtract + absolute value + assert!(subtract(absolute_value(a()), absolute_value(b())), "|a| - |b|"); + } + + #[test] + fn format_combinations_negative() + { + // Function + negative + assert!(function("f", vec![negative(a())]), "f(-a)"); + assert!(function("f", vec![negative(a()), negative(b()), negative(c())]), "f(-a, -b, -c)"); + + // Absolute value + negative + assert!(absolute_value(negative(a())), "|-a|"); + + // Negative + negative + assert!(negative(negative(a())), "--a"); + + // Exponentiate + negative + assert!(exponentiate(negative(a()), negative(b())), "-a ** -b"); + + // Multiply + negative + assert!(multiply(negative(a()), negative(b())), "-a * -b"); + + // Divide + negative + assert!(divide(negative(a()), negative(b())), "-a / -b"); + + // Modulo + negative + assert!(modulo(negative(a()), negative(b())), "-a % -b"); + + // Add + negative + assert!(add(negative(a()), negative(b())), "-a + -b"); + + // Subtract + negative + assert!(subtract(negative(a()), negative(b())), "-a - -b"); + } + + #[test] + fn format_combinations_exponentiate() + { + // Function + exponentiate + assert!(function("f", vec![exponentiate(a(), b())]), "f(a ** b)"); + assert!(function("f", vec![exponentiate(a(), b()), exponentiate(c(), d()), + exponentiate(e(), a())]), + "f(a ** b, c ** d, e ** a)"); + + // Absolute value + exponentiate + assert!(absolute_value(exponentiate(a(), b())), "|a ** b|"); + + // Negative + exponentiate + assert!(negative(exponentiate(a(), b())), "-(a ** b)"); + + // Exponentiate + exponentiate + assert!(exponentiate(exponentiate(a(), b()), exponentiate(c(), d())), "(a ** b) ** c ** d"); + + // Multiply + exponentiate + assert!(multiply(exponentiate(a(), b()), exponentiate(c(), d())), "a ** b * c ** d"); + + // Divide + exponentiate + assert!(divide(exponentiate(a(), b()), exponentiate(c(), d())), "a ** b / c ** d"); + + // Modulo + exponentiate + assert!(modulo(exponentiate(a(), b()), exponentiate(c(), d())), "a ** b % c ** d"); + + // Add + exponentiate + assert!(add(exponentiate(a(), b()), exponentiate(c(), d())), "a ** b + c ** d"); + + // Subtract + exponentiate + assert!(subtract(exponentiate(a(), b()), exponentiate(c(), d())), "a ** b - c ** d"); + } + + #[test] + fn format_combinations_multiply() + { + // Function + multiply + assert!(function("f", vec![multiply(a(), b())]), "f(a * b)"); + assert!(function("f", vec![multiply(a(), b()), multiply(c(), d()), multiply(e(), a())]), + "f(a * b, c * d, e * a)"); + + // Absolute value + multiply + assert!(absolute_value(multiply(a(), b())), "|a * b|"); + + // Negative + multiply + assert!(negative(multiply(a(), b())), "-(a * b)"); + + // Exponentiate + multiply + assert!(exponentiate(multiply(a(), b()), multiply(c(), d())), "(a * b) ** (c * d)"); + + // Multiply + multiply + assert!(multiply(multiply(a(), b()), multiply(c(), d())), "a * b * c * d"); + + // Divide + multiply + assert!(divide(multiply(a(), b()), multiply(c(), d())), "a * b / (c * d)"); + + // Modulo + multiply + assert!(modulo(multiply(a(), b()), multiply(c(), d())), "a * b % (c * d)"); + + // Add + multiply + assert!(add(multiply(a(), b()), multiply(c(), d())), "a * b + c * d"); + + // Subtract + multiply + assert!(subtract(multiply(a(), b()), multiply(c(), d())), "a * b - c * d"); + } + + #[test] + fn format_combinations_divide() + { + // Function + divide + assert!(function("f", vec![divide(a(), b())]), "f(a / b)"); + assert!(function("f", vec![divide(a(), b()), divide(c(), d()), divide(e(), a())]), + "f(a / b, c / d, e / a)"); + + // Absolute value + divide + assert!(absolute_value(divide(a(), b())), "|a / b|"); + + // Negative + divide + assert!(negative(divide(a(), b())), "-(a / b)"); + + // Exponentiate + divide + assert!(exponentiate(divide(a(), b()), divide(c(), d())), "(a / b) ** (c / d)"); + + // Multiply + divide + assert!(multiply(divide(a(), b()), divide(c(), d())), "a / b * c / d"); + + // Divide + divide + assert!(divide(divide(a(), b()), divide(c(), d())), "a / b / (c / d)"); + + // Modulo + divide + assert!(modulo(divide(a(), b()), divide(c(), d())), "a / b % (c / d)"); + + // Add + divide + assert!(add(divide(a(), b()), divide(c(), d())), "a / b + c / d"); + + // Subtract + divide + assert!(subtract(divide(a(), b()), divide(c(), d())), "a / b - c / d"); + } + + #[test] + fn format_combinations_modulo() + { + // Function + modulo + assert!(function("f", vec![modulo(a(), b())]), "f(a % b)"); + assert!(function("f", vec![modulo(a(), b()), modulo(c(), d()), modulo(e(), a())]), + "f(a % b, c % d, e % a)"); + + // Absolute value + modulo + assert!(absolute_value(modulo(a(), b())), "|a % b|"); + + // Negative + modulo + assert!(negative(modulo(a(), b())), "-(a % b)"); + + // Exponentiate + modulo + assert!(exponentiate(modulo(a(), b()), modulo(c(), d())), "(a % b) ** (c % d)"); + + // Multiply + modulo + assert!(multiply(modulo(a(), b()), modulo(c(), d())), "a % b * (c % d)"); + + // Divide + modulo + assert!(divide(modulo(a(), b()), modulo(c(), d())), "a % b / (c % d)"); + + // Modulo + modulo + assert!(modulo(modulo(a(), b()), modulo(c(), d())), "a % b % (c % d)"); + + // Add + modulo + assert!(add(modulo(a(), b()), modulo(c(), d())), "a % b + c % d"); + + // Subtract + modulo + assert!(subtract(modulo(a(), b()), modulo(c(), d())), "a % b - c % d"); + } + + #[test] + fn format_combinations_add() + { + // Function + add + assert!(function("f", vec![add(a(), b())]), "f(a + b)"); + assert!(function("f", vec![add(a(), b()), add(c(), d()), add(e(), a())]), + "f(a + b, c + d, e + a)"); + + // Absolute value + add + assert!(absolute_value(add(a(), b())), "|a + b|"); + + // Negative + add + assert!(negative(add(a(), b())), "-(a + b)"); + + // Exponentiate + add + assert!(exponentiate(add(a(), b()), add(c(), d())), "(a + b) ** (c + d)"); + + // Multiply + add + assert!(multiply(add(a(), b()), add(c(), d())), "(a + b) * (c + d)"); + + // Divide + add + assert!(divide(add(a(), b()), add(c(), d())), "(a + b) / (c + d)"); + + // Modulo + add + assert!(modulo(add(a(), b()), add(c(), d())), "(a + b) % (c + d)"); + + // Add + add + assert!(add(add(a(), b()), add(c(), d())), "a + b + c + d"); + + // Subtract + add + assert!(subtract(add(a(), b()), add(c(), d())), "a + b - (c + d)"); + } + + #[test] + fn format_combinations_subtract() + { + // Function + subtract + assert!(function("f", vec![subtract(a(), b())]), "f(a - b)"); + assert!(function("f", vec![subtract(a(), b()), subtract(c(), d()), subtract(e(), a())]), + "f(a - b, c - d, e - a)"); + + // Absolute value + subtract + assert!(absolute_value(subtract(a(), b())), "|a - b|"); + + // Negative + subtract + assert!(negative(subtract(a(), b())), "-(a - b)"); + + // Exponentiate + subtract + assert!(exponentiate(subtract(a(), b()), subtract(c(), d())), "(a - b) ** (c - d)"); + + // Multiply + subtract + assert!(multiply(subtract(a(), b()), subtract(c(), d())), "(a - b) * (c - d)"); + + // Divide + subtract + assert!(divide(subtract(a(), b()), subtract(c(), d())), "(a - b) / (c - d)"); + + // Modulo + subtract + assert!(modulo(subtract(a(), b()), subtract(c(), d())), "(a - b) % (c - d)"); + + // Add + subtract + assert!(add(subtract(a(), b()), subtract(c(), d())), "a - b + c - d"); + + // Subtract + subtract + assert!(subtract(subtract(a(), b()), subtract(c(), d())), "a - b - (c - d)"); } }