Test remaining formula types

src/format/formulas.rs

@@ -304,16 +304,31 @@ mod tests
 		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))
@@ -324,6 +339,17 @@ mod tests
 		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))
@@ -334,11 +360,21 @@ mod tests
 		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))
@@ -405,4 +441,78 @@ mod tests
 		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");
+	}
 }