Rewrite tests for clarity
This commit is contained in:
parent
a8df440fdf
commit
186ed314d3
GPG Key ID:
05F3611E97A70ABF
@ -596,55 +596,48 @@ mod tests
|
||||
#[test]
|
||||
fn format_boolean()
|
||||
{
|
||||
assert_eq!(format(true_()), "true");
|
||||
assert_eq!(format(false_()), "false");
|
||||
assert!(true_(), "true");
|
||||
assert!(false_(), "false");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_compare()
|
||||
{
|
||||
assert_eq!(format(greater(a(), b())), "a > b");
|
||||
assert_eq!(format(less(a(), b())), "a < b");
|
||||
assert_eq!(format(less_or_equal(a(), b())), "a <= b");
|
||||
assert_eq!(format(greater_or_equal(a(), b())), "a >= b");
|
||||
assert_eq!(format(equal(a(), b())), "a = b");
|
||||
assert_eq!(format(not_equal(a(), b())), "a != b");
|
||||
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_eq!(format(
|
||||
greater(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
||||
assert!(greater(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))),
|
||||
"(a + b) * c > |d - e|");
|
||||
assert_eq!(format(
|
||||
less(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
||||
assert!(less(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))),
|
||||
"(a + b) * c < |d - e|");
|
||||
assert_eq!(format(
|
||||
less_or_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
||||
assert!(less_or_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))),
|
||||
"(a + b) * c <= |d - e|");
|
||||
assert_eq!(format(
|
||||
greater_or_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
||||
assert!(greater_or_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))),
|
||||
"(a + b) * c >= |d - e|");
|
||||
assert_eq!(format(
|
||||
equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
||||
assert!(equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e()))),
|
||||
"(a + b) * c = |d - e|");
|
||||
assert_eq!(format(
|
||||
not_equal(multiply(add(a(), b()), c()), absolute_value(subtract(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_eq!(format(p()), "p");
|
||||
assert_eq!(format(predicate("predicate", vec![])), "predicate");
|
||||
assert_eq!(format(predicate("q", vec![a()])), "q(a)");
|
||||
assert_eq!(format(predicate("q", abc())), "q(a, b, c)");
|
||||
assert_eq!(format(predicate("predicate", abc())), "predicate(a, b, c)");
|
||||
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_eq!(format(
|
||||
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")])])),
|
||||
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
|
||||
@ -663,96 +656,92 @@ mod tests
|
||||
#[test]
|
||||
fn format_exists()
|
||||
{
|
||||
assert_eq!(format(exists(vec![x()], p())), "exists X p");
|
||||
assert_eq!(format(exists(xyz(), p())), "exists X, Y, Z p");
|
||||
assert!(exists(vec![x()], p()), "exists X p");
|
||||
assert!(exists(xyz(), p()), "exists X, Y, Z p");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_for_all()
|
||||
{
|
||||
assert_eq!(format(for_all(vec![x()], p())), "forall X p");
|
||||
assert_eq!(format(for_all(xyz(), p())), "forall X, Y, Z 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_eq!(format(not(p())), "not p");
|
||||
assert!(not(p()), "not p");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_and()
|
||||
{
|
||||
assert_eq!(format(and(vec![p()])), "p");
|
||||
assert_eq!(format(and(pqr())), "p and q and r");
|
||||
assert!(and(vec![p()]), "p");
|
||||
assert!(and(pqr()), "p and q and r");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_or()
|
||||
{
|
||||
assert_eq!(format(or(vec![p()])), "p");
|
||||
assert_eq!(format(or(pqr())), "p or q or r");
|
||||
assert!(or(vec![p()]), "p");
|
||||
assert!(or(pqr()), "p or q or r");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_implies()
|
||||
{
|
||||
assert_eq!(format(implies_right(p(), q())), "p -> q");
|
||||
assert_eq!(format(implies_left(p(), q())), "q <- p");
|
||||
assert!(implies_right(p(), q()), "p -> q");
|
||||
assert!(implies_left(p(), q()), "q <- p");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_if_and_only_if()
|
||||
{
|
||||
assert_eq!(format(if_and_only_if(vec![p()])), "p");
|
||||
assert_eq!(format(if_and_only_if(vec![p(), q()])), "p <-> q");
|
||||
assert_eq!(format(if_and_only_if(pqr())), "p <-> q <-> r");
|
||||
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_combination_boolean_and_lower()
|
||||
{
|
||||
// Boolean + not
|
||||
assert_eq!(format(not(true_())), "not true");
|
||||
assert_eq!(format(not(false_())), "not false");
|
||||
assert!(not(true_()), "not true");
|
||||
assert!(not(false_()), "not false");
|
||||
|
||||
// Boolean + quantified formula
|
||||
assert_eq!(format(exists(vec![x()], true_())), "exists X true");
|
||||
assert_eq!(format(exists(vec![x()], false_())), "exists X false");
|
||||
assert_eq!(format(exists(xyz(), true_())), "exists X, Y, Z true");
|
||||
assert_eq!(format(exists(xyz(), false_())), "exists X, Y, Z false");
|
||||
assert_eq!(format(for_all(vec![x()], true_())), "forall X true");
|
||||
assert_eq!(format(for_all(vec![x()], false_())), "forall X false");
|
||||
assert_eq!(format(for_all(xyz(), true_())), "forall X, Y, Z true");
|
||||
assert_eq!(format(for_all(xyz(), false_())), "forall X, Y, Z 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![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");
|
||||
|
||||
// Boolean + and
|
||||
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!(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
|
||||
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!(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
|
||||
assert_eq!(format(implies_right(true_(), true_())), "true -> true");
|
||||
assert_eq!(format(implies_left(true_(), true_())), "true <- true");
|
||||
assert_eq!(format(implies_right(false_(), false_())), "false -> false");
|
||||
assert_eq!(format(implies_left(false_(), false_())), "false <- false");
|
||||
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
|
||||
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");
|
||||
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]
|
||||
@ -764,167 +753,119 @@ mod tests
|
||||
let term_4 = || negative(function("f", vec![integer(5), add(variable("X"), integer(3))]));
|
||||
|
||||
// Compare + not
|
||||
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!(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|");
|
||||
|
||||
// Compare + quantified formula
|
||||
assert_eq!(format(
|
||||
exists(vec![x()], greater(term_1(), term_2()))),
|
||||
"exists X (a + b) * c > |d - e|");
|
||||
assert_eq!(format(
|
||||
exists(vec![x()], less(term_1(), term_2()))),
|
||||
"exists X (a + b) * c < |d - e|");
|
||||
assert_eq!(format(
|
||||
exists(vec![x()], less_or_equal(term_1(), term_2()))),
|
||||
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_eq!(format(
|
||||
exists(vec![x()], greater_or_equal(term_1(), term_2()))),
|
||||
assert!(exists(vec![x()], greater_or_equal(term_1(), term_2())),
|
||||
"exists X (a + b) * c >= |d - e|");
|
||||
assert_eq!(format(
|
||||
exists(vec![x()], equal(term_1(), term_2()))),
|
||||
"exists X (a + b) * c = |d - e|");
|
||||
assert_eq!(format(
|
||||
exists(vec![x()], not_equal(term_1(), term_2()))),
|
||||
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_eq!(format(
|
||||
for_all(vec![x()], greater(term_1(), term_2()))),
|
||||
"forall X (a + b) * c > |d - e|");
|
||||
assert_eq!(format(
|
||||
for_all(vec![x()], less(term_1(), term_2()))),
|
||||
"forall X (a + b) * c < |d - e|");
|
||||
assert_eq!(format(
|
||||
for_all(vec![x()], less_or_equal(term_1(), term_2()))),
|
||||
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_eq!(format(
|
||||
for_all(vec![x()], greater_or_equal(term_1(), term_2()))),
|
||||
assert!(for_all(vec![x()], greater_or_equal(term_1(), term_2())),
|
||||
"forall X (a + b) * c >= |d - e|");
|
||||
assert_eq!(format(
|
||||
for_all(vec![x()], equal(term_1(), term_2()))),
|
||||
"forall X (a + b) * c = |d - e|");
|
||||
assert_eq!(format(
|
||||
for_all(vec![x()], not_equal(term_1(), term_2()))),
|
||||
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|");
|
||||
|
||||
// Compare + and
|
||||
assert_eq!(format(
|
||||
and(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
|
||||
greater(term_2(), term_4())])),
|
||||
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_eq!(format(
|
||||
and(vec![less(term_1(), term_2()), less(term_3(), term_4()),
|
||||
less(term_2(), term_4())])),
|
||||
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_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())])),
|
||||
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_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())])),
|
||||
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_eq!(format(
|
||||
and(vec![equal(term_1(), term_2()), equal(term_3(), term_4()),
|
||||
equal(term_2(), term_4())])),
|
||||
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_eq!(format(
|
||||
and(vec![not_equal(term_1(), term_2()), not_equal(term_3(), term_4()),
|
||||
not_equal(term_2(), term_4())])),
|
||||
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)");
|
||||
|
||||
// Compare + or
|
||||
assert_eq!(format(
|
||||
or(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
|
||||
greater(term_2(), term_4())])),
|
||||
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_eq!(format(
|
||||
or(vec![less(term_1(), term_2()), less(term_3(), term_4()),
|
||||
less(term_2(), term_4())])),
|
||||
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_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())])),
|
||||
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_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())])),
|
||||
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_eq!(format(
|
||||
or(vec![equal(term_1(), term_2()), equal(term_3(), term_4()),
|
||||
equal(term_2(), term_4())])),
|
||||
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_eq!(format(
|
||||
or(vec![not_equal(term_1(), term_2()), not_equal(term_3(), term_4()),
|
||||
not_equal(term_2(), term_4())])),
|
||||
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)");
|
||||
|
||||
// Compare + implies
|
||||
assert_eq!(format(
|
||||
implies_right(greater(term_1(), term_2()), greater(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_right(less(term_1(), term_2()), less(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_right(less_or_equal(term_1(), term_2()), less_or_equal(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_right(greater_or_equal(term_1(), term_2()),
|
||||
greater_or_equal(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_right(equal(term_1(), term_2()), equal(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_right(not_equal(term_1(), term_2()), not_equal(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_left(greater(term_1(), term_2()), greater(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_left(less(term_1(), term_2()), less(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_left(less_or_equal(term_1(), term_2()), less_or_equal(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_left(greater_or_equal(term_1(), term_2()),
|
||||
greater_or_equal(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_left(equal(term_1(), term_2()), equal(term_3(), term_4()))),
|
||||
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_eq!(format(
|
||||
implies_left(not_equal(term_1(), term_2()), not_equal(term_3(), term_4()))),
|
||||
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
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
|
||||
greater(term_2(), term_4())])),
|
||||
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_eq!(format(
|
||||
if_and_only_if(vec![less(term_1(), term_2()), less(term_3(), term_4()),
|
||||
less(term_2(), term_4())])),
|
||||
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_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())])),
|
||||
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_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())])),
|
||||
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_eq!(format(
|
||||
if_and_only_if(vec![equal(term_1(), term_2()), equal(term_3(), term_4()),
|
||||
equal(term_2(), term_4())])),
|
||||
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_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())])),
|
||||
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)");
|
||||
}
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user