use super::*;

impl super::Precedence for crate::Formula
{
	fn precedence_level(&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
	{
		match &self
		{
			Self::LeftToRight => write!(format, "left to right"),
			Self::RightToLeft => write!(format, "right to left"),
		}
	}
}

impl std::fmt::Debug for crate::PredicateDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{}/{}", &self.name, self.arity)
	}
}

impl std::fmt::Display for crate::PredicateDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", &self)
	}
}

struct FormulaDisplay<'formula>
{
	parentheses: Parentheses,
	formula: &'formula crate::Formula,
}

fn display_formula(formula: &crate::Formula, parentheses: Parentheses) -> FormulaDisplay
{
	FormulaDisplay
	{
		parentheses,
		formula,
	}
}

impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		let precedence_level = self.formula.precedence_level();
		let requires_parentheses = match self.parentheses
		{
			Parentheses::None => false,
			Parentheses::PrecedenceBased(parent_precedence_level)
				=> precedence_level > parent_precedence_level,
			Parentheses::Required => true,
		};
		let parentheses = Parentheses::PrecedenceBased(precedence_level);

		if requires_parentheses
		{
			write!(format, "(")?;
		}

		match &self.formula
		{
			crate::Formula::Exists(exists) =>
			{
				assert!(!exists.parameters.is_empty());

				write!(format, "exists")?;

				let mut separator = " ";

				for parameter in exists.parameters.iter()
				{
					write!(format, "{}{:?}", separator, parameter)?;

					separator = ", "
				}

				write!(format, " {:?}", display_formula(&exists.argument, parentheses))?;
			},
			crate::Formula::ForAll(for_all) =>
			{
				assert!(!for_all.parameters.is_empty());

				write!(format, "forall")?;

				let mut separator = " ";

				for parameter in for_all.parameters.iter()
				{
					write!(format, "{}{:?}", separator, parameter)?;

					separator = ", "
				}

				write!(format, " {:?}", display_formula(&for_all.argument, parentheses))?;
			},
			crate::Formula::Not(argument) => write!(format, "not {:?}",
				display_formula(argument, parentheses))?,
			crate::Formula::And(arguments) =>
			{
				let mut separator = "";

				assert!(!arguments.is_empty());

				for argument in arguments
				{
					write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?;

					separator = " and "
				}
			},
			crate::Formula::Or(arguments) =>
			{
				let mut separator = "";

				assert!(!arguments.is_empty());

				for argument in arguments
				{
					write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?;

					separator = " or "
				}
			},
			crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
			{
				let antecedent_parentheses = match **antecedent
				{
					// Implication is right-associative and thus requires parentheses when nested on
					// the antecedent side
					crate::Formula::Implies(_) => Parentheses::Required,
					_ => parentheses,
				};

				let implication_parentheses = match **antecedent
				{
					// Implication is right-associative and thus doesn’t require parentheses when
					// nested on the implication side with the same implication direction
					crate::Formula::Implies(crate::Implies{direction: nested_direction, ..})
						if nested_direction == *direction => Parentheses::None,
					// If the nested implication is in the other direction, parentheses are needed
					crate::Formula::Implies(_) => Parentheses::Required,
					_ => parentheses,
				};

				let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
				{
					write!(format, "{:?}", display_formula(antecedent, antecedent_parentheses))
				};

				let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
				{
					write!(format, "{:?}", display_formula(implication, implication_parentheses))
				};

				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::IfAndOnlyIf(arguments) =>
			{
				let mut separator = "";

				for argument in arguments
				{
					write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?;

					separator = " <-> ";
				}
			},
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
				=> write!(format, "{:?} < {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
				=> write!(format, "{:?} <= {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
				=> write!(format, "{:?} > {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
				=> write!(format, "{:?} >= {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
				=> write!(format, "{:?} = {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
				=> write!(format, "{:?} != {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Boolean(true) => write!(format, "true")?,
			crate::Formula::Boolean(false) => write!(format, "false")?,
			crate::Formula::Predicate(predicate) =>
			{
				write!(format, "{}", predicate.declaration.name)?;

				if !predicate.arguments.is_empty()
				{
					write!(format, "(")?;

					let mut separator = "";

					for argument in &predicate.arguments
					{
						write!(format, "{}{:?}", separator,
							display_term(argument, Parentheses::None))?;

						separator = ", "
					}

					write!(format, ")")?;
				}
			},
		}

		if requires_parentheses
		{
			write!(format, ")")?;
		}

		Ok(())
	}
}

impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", self)
	}
}

impl std::fmt::Debug for crate::Formula
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", display_formula(&self, Parentheses::None))
	}
}

impl std::fmt::Display for crate::Formula
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{}", display_formula(&self, Parentheses::None))
	}
}

#[cfg(test)]
mod tests
{
	use crate::*;
	use crate::format::terms::tests::*;

	fn format(formula: Box<ast::Formula>) -> String
	{
		format!("{}", formula)
	}

	fn and(arguments: Formulas) -> Box<Formula>
	{
		Box::new(Formula::and(arguments))
	}

	fn equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
	{
		Box::new(Formula::equal(left, right))
	}

	fn exists(parameters: VariableDeclarations, argument: Box<Formula>) -> Box<Formula>
	{
		Box::new(Formula::exists(std::rc::Rc::new(parameters), argument))
	}

	fn false_() -> Box<Formula>
	{
		Box::new(Formula::false_())
	}

	fn for_all(parameters: VariableDeclarations, argument: Box<Formula>) -> Box<Formula>
	{
		Box::new(Formula::for_all(std::rc::Rc::new(parameters), argument))
	}

	fn greater(left: Box<Term>, right: Box<Term>) -> Box<Formula>
	{
		Box::new(Formula::greater(left, right))
	}

	fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
	{
		Box::new(Formula::greater_or_equal(left, right))
	}

	fn if_and_only_if(arguments: Formulas) -> Box<Formula>
	{
		Box::new(Formula::if_and_only_if(arguments))
	}

	fn implies(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
		-> Box<Formula>
	{
		Box::new(Formula::implies(direction, antecedent, implication))
	}

	fn less(left: Box<Term>, right: Box<Term>) -> Box<Formula>
	{
		Box::new(Formula::less(left, right))
	}

	fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
	{
		Box::new(Formula::less_or_equal(left, right))
	}

	fn not(argument: Box<Formula>) -> Box<Formula>
	{
		Box::new(Formula::not(argument))
	}

	fn not_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
	{
		Box::new(Formula::not_equal(left, right))
	}

	fn or(arguments: Formulas) -> Box<Formula>
	{
		Box::new(Formula::or(arguments))
	}

	fn predicate(name: &str, arguments: Vec<Box<Term>>) -> Box<Formula>
	{
		Box::new(Formula::predicate(predicate_declaration(name, arguments.len()), arguments))
	}

	fn predicate_declaration(name: &str, arity: usize) -> std::rc::Rc<PredicateDeclaration>
	{
		std::rc::Rc::new(PredicateDeclaration::new(name.to_string(), arity))
	}

	fn true_() -> Box<Formula>
	{
		Box::new(Formula::true_())
	}

	#[test]
	fn format_boolean()
	{
		assert_eq!(format(true_()), "true");
		assert_eq!(format(false_()), "false");
	}

	#[test]
	fn format_compare()
	{
		assert_eq!(format(greater(constant("a"), constant("b"))), "a > b");
		assert_eq!(format(less(constant("a"), constant("b"))), "a < b");
		assert_eq!(format(less_or_equal(constant("a"), constant("b"))), "a <= b");
		assert_eq!(format(greater_or_equal(constant("a"), constant("b"))), "a >= b");
		assert_eq!(format(equal(constant("a"), constant("b"))), "a = b");
		assert_eq!(format(not_equal(constant("a"), constant("b"))), "a != b");

		assert_eq!(format(
			greater(multiply(add(constant("a"), constant("b")), constant("c")),
				absolute_value(subtract(constant("d"), constant("e"))))),
			"(a + b) * c > |d - e|");
		assert_eq!(format(
			less(multiply(add(constant("a"), constant("b")), constant("c")),
				absolute_value(subtract(constant("d"), constant("e"))))),
			"(a + b) * c < |d - e|");
		assert_eq!(format(
			less_or_equal(multiply(add(constant("a"), constant("b")), constant("c")),
				absolute_value(subtract(constant("d"), constant("e"))))),
			"(a + b) * c <= |d - e|");
		assert_eq!(format(
			greater_or_equal(multiply(add(constant("a"), constant("b")), constant("c")),
				absolute_value(subtract(constant("d"), constant("e"))))),
			"(a + b) * c >= |d - e|");
		assert_eq!(format(
			equal(multiply(add(constant("a"), constant("b")), constant("c")),
				absolute_value(subtract(constant("d"), constant("e"))))),
			"(a + b) * c = |d - e|");
		assert_eq!(format(
			not_equal(multiply(add(constant("a"), constant("b")), constant("c")),
				absolute_value(subtract(constant("d"), constant("e"))))),
			"(a + b) * c != |d - e|");
	}

	#[test]
	fn format_predicate()
	{
		assert_eq!(format(predicate("p", vec![])), "p");
		assert_eq!(format(predicate("predicate", vec![])), "predicate");
		assert_eq!(format(predicate("q", vec![constant("a")])), "q(a)");
		assert_eq!(format(
			predicate("q", vec![constant("a"), constant("b"), constant("c")])),
			"q(a, b, c)");
		assert_eq!(format(
			predicate("predicate", vec![constant("a"), constant("b"), constant("c")])),
			"predicate(a, b, c)");

		assert_eq!(format(
			predicate("predicate", vec![
				exponentiate(absolute_value(multiply(constant("a"), integer(-20))), integer(2)),
				string("test"),
				function("f", vec![multiply(add(constant("b"), constant("c")),
					subtract(constant("b"), constant("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_eq!(format(
			exists(vec![variable_declaration("X")], predicate("p", vec![]))),
			"exists X p");
		assert_eq!(format(
			exists(vec![variable_declaration("X"), variable_declaration("Y"),
				variable_declaration("Z")], predicate("p", vec![]))),
			"exists X, Y, Z p");
	}

	#[test]
	fn format_for_all()
	{
		assert_eq!(format(
			for_all(vec![variable_declaration("X")], predicate("p", vec![]))),
			"forall X p");
		assert_eq!(format(
			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
				variable_declaration("Z")], predicate("p", vec![]))),
			"forall X, Y, Z p");
	}

	#[test]
	fn format_not()
	{
		assert_eq!(format(not(predicate("p", vec![]))), "not p");
	}

	#[test]
	fn format_and()
	{
		assert_eq!(format(and(vec![predicate("p", vec![])])), "p");
		assert_eq!(format(
			and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])])),
			"p and q and r");
	}

	#[test]
	fn format_or()
	{
		assert_eq!(format(or(vec![predicate("p", vec![])])), "p");
		assert_eq!(format(
			or(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])])),
			"p or q or r");
	}

	#[test]
	fn format_implies()
	{
		assert_eq!(format(
			implies(ImplicationDirection::LeftToRight, predicate("p", vec![]),
				predicate("q", vec![]))),
			"p -> q");
		assert_eq!(format(
			implies(ImplicationDirection::RightToLeft, predicate("p", vec![]),
				predicate("q", vec![]))),
			"q <- p");
	}

	#[test]
	fn format_if_and_only_if()
	{
		assert_eq!(format(if_and_only_if(vec![predicate("p", vec![])])), "p");
		assert_eq!(format(
			if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![])])),
			"p <-> q");
		assert_eq!(format(
			if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]),
				predicate("r", vec![])])),
			"p <-> q <-> r");
	}

	#[test]
	fn format_combination_boolean_and_lower()
	{
		assert_eq!(format(exists(vec![variable_declaration("X")], true_())), "exists X true");
		assert_eq!(format(exists(vec![variable_declaration("X")], false_())), "exists X false");
		assert_eq!(format(
			exists(vec![variable_declaration("X"), variable_declaration("Y"),
				variable_declaration("Z")], true_())),
			"exists X, Y, Z true");
		assert_eq!(format(
			exists(vec![variable_declaration("X"), variable_declaration("Y"),
				variable_declaration("Z")], false_())),
			"exists X, Y, Z false");
		assert_eq!(format(for_all(vec![variable_declaration("X")], true_())), "forall X true");
		assert_eq!(format(for_all(vec![variable_declaration("X")], false_())), "forall X false");
		assert_eq!(format(
			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
				variable_declaration("Z")], true_())),
			"forall X, Y, Z true");
		assert_eq!(format(
			for_all(vec![variable_declaration("X"), variable_declaration("Y"),
				variable_declaration("Z")], false_())),
			"forall X, Y, Z false");

		assert_eq!(format(not(true_())), "not true");
		assert_eq!(format(not(false_())), "not false");

		assert_eq!(format(and(vec![true_()])), "true");
		assert_eq!(format(and(vec![true_(), true_(), true_()])), "true and true and true");
		assert_eq!(format(and(vec![false_()])), "false");
		assert_eq!(format(and(vec![false_(), false_(), false_()])), "false and false and false");

		assert_eq!(format(or(vec![true_()])), "true");
		assert_eq!(format(or(vec![true_(), true_(), true_()])), "true or true or true");
		assert_eq!(format(or(vec![false_()])), "false");
		assert_eq!(format(or(vec![false_(), false_(), false_()])), "false or false or false");

		assert_eq!(format(
			implies(ImplicationDirection::LeftToRight, true_(), true_())),
			"true -> true");
		assert_eq!(format(
			implies(ImplicationDirection::RightToLeft, true_(), true_())),
			"true <- true");
		assert_eq!(format(
			implies(ImplicationDirection::LeftToRight, false_(), false_())),
			"false -> false");
		assert_eq!(format(
			implies(ImplicationDirection::RightToLeft, false_(), false_())),
			"false <- false");

		assert_eq!(format(if_and_only_if(vec![true_()])), "true");
		assert_eq!(format(
			if_and_only_if(vec![true_(), true_(), true_()])),
			"true <-> true <-> true");
		assert_eq!(format(if_and_only_if(vec![false_()])), "false");
		assert_eq!(format(
			if_and_only_if(vec![false_(), false_(), false_()])),
			"false <-> false <-> false");
	}

	#[test]
	fn format_combination_compare_and_lower()
	{
		let term_1 = || multiply(add(constant("a"), constant("b")), constant("c"));
		let term_2 = || absolute_value(subtract(constant("d"), constant("e")));
		let term_3 = || exponentiate(constant("a"), exponentiate(constant("b"), constant("c")));
		let term_4 = || negative(function("f", vec![integer(5), add(variable("X"), integer(3))]));

		assert_eq!(format(
			exists(vec![variable_declaration("X")], greater(term_1(), term_2()))),
			"exists X (a + b) * c > |d - e|");
		assert_eq!(format(
			exists(vec![variable_declaration("X")], less(term_1(), term_2()))),
			"exists X (a + b) * c < |d - e|");
		assert_eq!(format(
			exists(vec![variable_declaration("X")], less_or_equal(term_1(), term_2()))),
			"exists X (a + b) * c <= |d - e|");
		assert_eq!(format(
			exists(vec![variable_declaration("X")], greater_or_equal(term_1(), term_2()))),
			"exists X (a + b) * c >= |d - e|");
		assert_eq!(format(
			exists(vec![variable_declaration("X")], equal(term_1(), term_2()))),
			"exists X (a + b) * c = |d - e|");
		assert_eq!(format(
			exists(vec![variable_declaration("X")], not_equal(term_1(), term_2()))),
			"exists X (a + b) * c != |d - e|");
		assert_eq!(format(
			for_all(vec![variable_declaration("X")], greater(term_1(), term_2()))),
			"forall X (a + b) * c > |d - e|");
		assert_eq!(format(
			for_all(vec![variable_declaration("X")], less(term_1(), term_2()))),
			"forall X (a + b) * c < |d - e|");
		assert_eq!(format(
			for_all(vec![variable_declaration("X")], less_or_equal(term_1(), term_2()))),
			"forall X (a + b) * c <= |d - e|");
		assert_eq!(format(
			for_all(vec![variable_declaration("X")], greater_or_equal(term_1(), term_2()))),
			"forall X (a + b) * c >= |d - e|");
		assert_eq!(format(
			for_all(vec![variable_declaration("X")], equal(term_1(), term_2()))),
			"forall X (a + b) * c = |d - e|");
		assert_eq!(format(
			for_all(vec![variable_declaration("X")], not_equal(term_1(), term_2()))),
			"forall X (a + b) * c != |d - e|");

		assert_eq!(format(not(greater(term_1(), term_2()))), "not (a + b) * c > |d - e|");
		assert_eq!(format(not(less(term_1(), term_2()))), "not (a + b) * c < |d - e|");
		assert_eq!(format(not(less_or_equal(term_1(), term_2()))), "not (a + b) * c <= |d - e|");
		assert_eq!(format(not(greater_or_equal(term_1(), term_2()))), "not (a + b) * c >= |d - e|");
		assert_eq!(format(not(equal(term_1(), term_2()))), "not (a + b) * c = |d - e|");
		assert_eq!(format(not(not_equal(term_1(), term_2()))), "not (a + b) * c != |d - e|");

		assert_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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)");

		assert_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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)");

		assert_eq!(format(
			implies(ImplicationDirection::LeftToRight, greater(term_1(), term_2()),
				greater(term_3(), term_4()))),
			"(a + b) * c > |d - e| -> a ** b ** c > -f(5, X + 3)");
		assert_eq!(format(
			implies(ImplicationDirection::LeftToRight, less(term_1(), term_2()),
				less(term_3(), term_4()))),
			"(a + b) * c < |d - e| -> a ** b ** c < -f(5, X + 3)");
		assert_eq!(format(
			implies(ImplicationDirection::LeftToRight, 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_eq!(format(
			implies(ImplicationDirection::LeftToRight, 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_eq!(format(
			implies(ImplicationDirection::LeftToRight, equal(term_1(), term_2()),
				equal(term_3(), term_4()))),
			"(a + b) * c = |d - e| -> a ** b ** c = -f(5, X + 3)");
		assert_eq!(format(
			implies(ImplicationDirection::LeftToRight, 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_eq!(format(
			implies(ImplicationDirection::RightToLeft, greater(term_1(), term_2()),
				greater(term_3(), term_4()))),
			"a ** b ** c > -f(5, X + 3) <- (a + b) * c > |d - e|");
		assert_eq!(format(
			implies(ImplicationDirection::RightToLeft, less(term_1(), term_2()),
				less(term_3(), term_4()))),
			"a ** b ** c < -f(5, X + 3) <- (a + b) * c < |d - e|");
		assert_eq!(format(
			implies(ImplicationDirection::RightToLeft, 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_eq!(format(
			implies(ImplicationDirection::RightToLeft, 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_eq!(format(
			implies(ImplicationDirection::RightToLeft, equal(term_1(), term_2()),
				equal(term_3(), term_4()))),
			"a ** b ** c = -f(5, X + 3) <- (a + b) * c = |d - e|");
		assert_eq!(format(
			implies(ImplicationDirection::RightToLeft, not_equal(term_1(), term_2()),
				not_equal(term_3(), term_4()))),
			"a ** b ** c != -f(5, X + 3) <- (a + b) * c != |d - e|");

		assert_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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_eq!(format(
			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)");
	}
}