Test disjunction
This commit is contained in:
parent
e4700fc638
commit
33f751781e
GPG Key ID:
05F3611E97A70ABF
|
|
@ -64,6 +64,7 @@ fn requires_parentheses<'formula>(formula: &'formula crate::Formula,
|
|||
| Formula::Exists(_)
|
||||
| Formula::ForAll(_)
|
||||
| Formula::And(_)
|
||||
| Formula::Or(_)
|
||||
| Formula::Implies(_)
|
||||
=> true,
|
||||
_ => false,
|
||||
|
|
@ -1511,4 +1512,165 @@ mod tests
|
|||
if_and_only_if(vec![and(p2q2r2())]), if_and_only_if(vec![and(p3q3r3())])])),
|
||||
"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn format_combination_or_and_lower()
|
||||
{
|
||||
// Or + or
|
||||
assert_eq!(format(
|
||||
or(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])),
|
||||
"p or q or r");
|
||||
assert_eq!(format(
|
||||
or(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]), and(vec![or(vec![r()])])])),
|
||||
"p or q or r");
|
||||
assert_eq!(format(
|
||||
or(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]),
|
||||
or(vec![or(vec![r()])])])),
|
||||
"p or q or r");
|
||||
assert_eq!(format(
|
||||
or(vec![if_and_only_if(vec![or(vec![p()])]), if_and_only_if(vec![or(vec![q()])]),
|
||||
if_and_only_if(vec![or(vec![r()])])])),
|
||||
"p or q or r");
|
||||
assert_eq!(format(
|
||||
or(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])),
|
||||
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
|
||||
assert_eq!(format(
|
||||
or(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]), and(vec![or(p3q3r3())])])),
|
||||
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
|
||||
assert_eq!(format(
|
||||
or(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]), or(vec![or(p3q3r3())])])),
|
||||
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
|
||||
assert_eq!(format(
|
||||
or(vec![if_and_only_if(vec![or(p1q1r1())]), if_and_only_if(vec![or(p2q2r2())]),
|
||||
if_and_only_if(vec![or(p3q3r3())])])),
|
||||
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
|
||||
|
||||
// Or + implies
|
||||
assert_eq!(format(
|
||||
or(vec![implies_right(p1(), q1()), implies_right(p2(), q2()),
|
||||
implies_right(p3(), q3())])),
|
||||
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
|
||||
assert_eq!(format(
|
||||
or(vec![and(vec![implies_right(p1(), q1())]), and(vec![implies_right(p2(), q2())]),
|
||||
and(vec![implies_right(p3(), q3())])])),
|
||||
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
|
||||
assert_eq!(format(
|
||||
or(vec![or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]),
|
||||
or(vec![implies_right(p3(), q3())])])),
|
||||
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
|
||||
assert_eq!(format(
|
||||
or(vec![if_and_only_if(vec![implies_right(p1(), q1())]),
|
||||
if_and_only_if(vec![implies_right(p2(), q2())]),
|
||||
if_and_only_if(vec![implies_right(p3(), q3())])])),
|
||||
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
|
||||
assert_eq!(format(
|
||||
or(vec![implies_left(p1(), q1()), implies_left(p2(), q2()),
|
||||
implies_left(p3(), q3())])),
|
||||
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
|
||||
assert_eq!(format(
|
||||
or(vec![and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]),
|
||||
and(vec![implies_left(p3(), q3())])])),
|
||||
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
|
||||
assert_eq!(format(
|
||||
or(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]),
|
||||
or(vec![implies_left(p3(), q3())])])),
|
||||
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
|
||||
assert_eq!(format(
|
||||
or(vec![if_and_only_if(vec![implies_left(p1(), q1())]),
|
||||
if_and_only_if(vec![implies_left(p2(), q2())]),
|
||||
if_and_only_if(vec![implies_left(p3(), q3())])])),
|
||||
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
|
||||
assert_eq!(format(
|
||||
implies_right(or(p1q1r1()), or(p2q2r2()))),
|
||||
"p1 or q1 or r1 -> p2 or q2 or r2");
|
||||
assert_eq!(format(
|
||||
implies_right(and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]))),
|
||||
"p1 or q1 or r1 -> p2 or q2 or r2");
|
||||
assert_eq!(format(
|
||||
implies_right(or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]))),
|
||||
"p1 or q1 or r1 -> p2 or q2 or r2");
|
||||
assert_eq!(format(
|
||||
implies_right(if_and_only_if(vec![or(p1q1r1())]),
|
||||
if_and_only_if(vec![or(p2q2r2())]))),
|
||||
"p1 or q1 or r1 -> p2 or q2 or r2");
|
||||
assert_eq!(format(
|
||||
implies_left(or(p1q1r1()), or(p2q2r2()))),
|
||||
"p2 or q2 or r2 <- p1 or q1 or r1");
|
||||
assert_eq!(format(
|
||||
implies_left(and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]))),
|
||||
"p2 or q2 or r2 <- p1 or q1 or r1");
|
||||
assert_eq!(format(
|
||||
implies_left(or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]))),
|
||||
"p2 or q2 or r2 <- p1 or q1 or r1");
|
||||
assert_eq!(format(
|
||||
implies_left(if_and_only_if(vec![or(p1q1r1())]), if_and_only_if(vec![or(p2q2r2())]))),
|
||||
"p2 or q2 or r2 <- p1 or q1 or r1");
|
||||
|
||||
// Or + if and only if
|
||||
assert_eq!(format(
|
||||
or(vec![if_and_only_if(vec![p()]), if_and_only_if(vec![q()]),
|
||||
if_and_only_if(vec![r()])])),
|
||||
"p or q or r");
|
||||
assert_eq!(format(
|
||||
or(vec![and(vec![if_and_only_if(vec![p()])]), and(vec![if_and_only_if(vec![q()])]),
|
||||
and(vec![if_and_only_if(vec![r()])])])),
|
||||
"p or q or r");
|
||||
assert_eq!(format(
|
||||
or(vec![or(vec![if_and_only_if(vec![p()])]), or(vec![if_and_only_if(vec![q()])]),
|
||||
or(vec![if_and_only_if(vec![r()])])])),
|
||||
"p or q or r");
|
||||
assert_eq!(format(
|
||||
or(vec![if_and_only_if(vec![if_and_only_if(vec![p()])]),
|
||||
if_and_only_if(vec![if_and_only_if(vec![q()])]),
|
||||
if_and_only_if(vec![if_and_only_if(vec![r()])])])),
|
||||
"p or q or r");
|
||||
assert_eq!(format(
|
||||
or(vec![if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()),
|
||||
if_and_only_if(p3q3r3())])),
|
||||
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
|
||||
assert_eq!(format(
|
||||
or(vec![and(vec![if_and_only_if(p1q1r1())]), and(vec![if_and_only_if(p2q2r2())]),
|
||||
and(vec![if_and_only_if(p3q3r3())])])),
|
||||
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
|
||||
assert_eq!(format(
|
||||
or(vec![or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]),
|
||||
or(vec![if_and_only_if(p3q3r3())])])),
|
||||
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
|
||||
assert_eq!(format(
|
||||
or(vec![if_and_only_if(vec![if_and_only_if(p1q1r1())]),
|
||||
if_and_only_if(vec![if_and_only_if(p2q2r2())]),
|
||||
if_and_only_if(vec![if_and_only_if(p3q3r3())])])),
|
||||
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
|
||||
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])),
|
||||
"p <-> q <-> r");
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]),
|
||||
and(vec![or(vec![r()])])])),
|
||||
"p <-> q <-> r");
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]),
|
||||
or(vec![or(vec![r()])])])),
|
||||
"p <-> q <-> r");
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![if_and_only_if(vec![or(vec![p()])]),
|
||||
if_and_only_if(vec![or(vec![q()])]), if_and_only_if(vec![or(vec![r()])])])),
|
||||
"p <-> q <-> r");
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])),
|
||||
"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]),
|
||||
and(vec![or(p3q3r3())])])),
|
||||
"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]),
|
||||
or(vec![or(p3q3r3())])])),
|
||||
"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
|
||||
assert_eq!(format(
|
||||
if_and_only_if(vec![if_and_only_if(vec![or(p1q1r1())]),
|
||||
if_and_only_if(vec![or(p2q2r2())]), if_and_only_if(vec![or(p3q3r3())])])),
|
||||
"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue