From 3bd52845be1be310eb27b291f3a933616672db92 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 8 Apr 2020 11:02:52 +0200 Subject: [PATCH] Reorganize tests --- src/format/formulas.rs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/format/formulas.rs b/src/format/formulas.rs index ba3c9f9..a662062 100644 --- a/src/format/formulas.rs +++ b/src/format/formulas.rs @@ -703,13 +703,13 @@ mod tests } #[test] - fn format_combination_boolean_and_lower() + fn format_combinations_boolean() { - // Boolean + not + // Not + Boolean assert!(not(true_()), "not true"); assert!(not(false_()), "not false"); - // Boolean + quantified formula + // Quantified formula + Boolean 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"); @@ -719,25 +719,25 @@ mod tests assert!(for_all(xyz(), true_()), "forall X, Y, Z true"); assert!(for_all(xyz(), false_()), "forall X, Y, Z false"); - // Boolean + and + // 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"); - // Boolean + or + // 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"); - // Boolean + implies + // 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"); - // Boolean + if and only if + // 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"); @@ -745,14 +745,14 @@ mod tests } #[test] - fn format_combination_compare_and_lower() + 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))])); - // Compare + not + // 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|"); @@ -760,7 +760,7 @@ mod tests 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|"); - // Compare + quantified formula + // Quantified formula + compare 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())), @@ -780,7 +780,7 @@ mod tests assert!(for_all(vec![x()], not_equal(term_1(), term_2())), "forall X (a + b) * c != |d - e|"); - // Compare + and + // 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)"); @@ -800,7 +800,7 @@ mod tests 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)"); - // Compare + or + // 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)"); @@ -820,7 +820,7 @@ mod tests 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)"); - // Compare + implies + // 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())), @@ -848,7 +848,7 @@ mod tests 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|"); - // Compare + if and only if + // 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)");