patrick/foliage-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Finish testing biconditionals

Browse Source
This commit is contained in:
Patrick Lühne 2020-04-08 12:03:05 +02:00
parent 3bd52845be
commit 51cbdb313f
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 161 additions and 87 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

248
src/format/formulas.rs
View File

@ -107,17 +107,7 @@ impl<'formula> FormulaDisplay<'formula>
}, },
_ => false, _ => false,
}, },
Formula::IfAndOnlyIf(_) => match *parent_formula Formula::IfAndOnlyIf(_) => true,
{
Formula::Not(_)
| Formula::Exists(_)
| Formula::ForAll(_)
| Formula::And(_)
| Formula::Or(_)
| Formula::Implies(_)
=> true,
_ => false,
},
} }
} }
} }
@ -870,43 +860,41 @@ mod tests
} }
#[test] #[test]
fn format_combination_not_and_lower() fn format_combinations_not()
{ {
// Not + not // Not + not
assert!(not(not(p())), "not not p"); assert!(not(not(p())), "not not p");
// Not + quantified formulas // Quantified formulas + not
assert_all!(i, not(exists(xyz(), i(p()))), "not exists X, Y, Z p"); assert_all!(i, exists(xyz(), i(not(p()))), "exists X, Y, Z not p");
assert_all!(i, not(for_all(xyz(), i(p()))), "not forall X, Y, Z p");
assert_all!(i, for_all(xyz(), i(not(p()))), "forall X, Y, Z not p"); assert_all!(i, for_all(xyz(), i(not(p()))), "forall X, Y, Z not p");
// Not + and // And + not
assert_all!(i, and(vec![not(i(p()))]), "not p"); assert_all!(i, and(vec![i(not(p()))]), "not p");
assert_all!(i, not(i(and(pqr()))), "not (p and q and r)");
assert_all!(i, and(vec![i(not(p())), i(not(q())), i(not(r()))]), assert_all!(i, and(vec![i(not(p())), i(not(q())), i(not(r()))]),
"not p and not q and not r"); "not p and not q and not r");
// Not + or // Or + not
assert_all!(i, or(vec![i(not(p()))]), "not p"); assert_all!(i, or(vec![i(not(p()))]), "not p");
assert_all!(i, not(i(or(pqr()))), "not (p or q or r)");
assert_all!(i, or(vec![i(not(p())), i(not(q())), i(not(r()))]), "not p or not q or not r"); assert_all!(i, or(vec![i(not(p())), i(not(q())), i(not(r()))]), "not p or not q or not r");
// Not + implies // Implies + not
assert_all!(i, not(i(implies_right(p(), q()))), "not (p -> q)");
assert_all!(i, not(i(implies_left(p(), q()))), "not (q <- p)");
assert_all!(i, implies_right(i(not(p())), i(not(q()))), "not p -> not q"); assert_all!(i, implies_right(i(not(p())), i(not(q()))), "not p -> not q");
assert_all!(i, implies_left(i(not(p())), i(not(q()))), "not q <- not p"); assert_all!(i, implies_left(i(not(p())), i(not(q()))), "not q <- not p");
// Not + if and only if // If and only if + not
assert_all!(i, if_and_only_if(vec![i(not(p()))]), "not p"); assert_all!(i, if_and_only_if(vec![i(not(p()))]), "not p");
assert_all!(i, not(i(if_and_only_if(pqr()))), "not (p <-> q <-> r)");
assert_all!(i, if_and_only_if(vec![i(not(p())), i(not(q())), i(not(r()))]), assert_all!(i, if_and_only_if(vec![i(not(p())), i(not(q())), i(not(r()))]),
"not p <-> not q <-> not r"); "not p <-> not q <-> not r");
} }
#[test] #[test]
fn format_combination_quantified_formula_and_lower() fn format_combinations_quantified_formula()
{ {
// Not + quantified formula
assert_all!(i, not(exists(xyz(), i(p()))), "not exists X, Y, Z p");
assert_all!(i, not(for_all(xyz(), i(p()))), "not forall X, Y, Z p");
// Quantified formula + quantified formula // Quantified formula + quantified formula
assert_all!(i, exists(x1y1z1(), i(exists(x2y2z2(), p()))), assert_all!(i, exists(x1y1z1(), i(exists(x2y2z2(), p()))),
"exists X1, Y1, Z1 exists X2, Y2, Z2 p"); "exists X1, Y1, Z1 exists X2, Y2, Z2 p");
@ -917,91 +905,87 @@ mod tests
assert_all!(i, for_all(x1y1z1(), i(for_all(x2y2z2(), p()))), assert_all!(i, for_all(x1y1z1(), i(for_all(x2y2z2(), p()))),
"forall X1, Y1, Z1 forall X2, Y2, Z2 p"); "forall X1, Y1, Z1 forall X2, Y2, Z2 p");
// Quantified formula + and // And + quantified formula
assert_all!(i, exists(xyz(), i(and(pqr()))), "exists X, Y, Z (p and q and r)"); assert_all!(i, and(vec![i(exists(xyz(), p()))]), "exists X, Y, Z p");
assert_all!(i, and(vec![i(for_all(xyz(), p()))]), "forall X, Y, Z p");
assert_all!(i, and(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())), assert_all!(i, and(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())),
i(exists(x3y3z3(), r()))]), i(exists(x3y3z3(), r()))]),
"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r"); "exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
assert_all!(i, for_all(xyz(), i(and(pqr()))), "forall X, Y, Z (p and q and r)");
assert_all!(i, and(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())), assert_all!(i, and(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())),
i(for_all(x3y3z3(), r()))]), i(for_all(x3y3z3(), r()))]),
"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r"); "forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
// Quantified formula + or // Or + quantified formula
assert_all!(i, exists(xyz(), i(or(pqr()))), "exists X, Y, Z (p or q or r)"); assert_all!(i, or(vec![i(exists(xyz(), p()))]), "exists X, Y, Z p");
assert_all!(i, or(vec![i(for_all(xyz(), p()))]), "forall X, Y, Z p");
assert_all!(i, or(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())), assert_all!(i, or(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())),
i(exists(x3y3z3(), r()))]), i(exists(x3y3z3(), r()))]),
"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r"); "exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
assert_all!(i, for_all(xyz(), i(or(pqr()))), "forall X, Y, Z (p or q or r)");
assert_all!(i, or(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())), assert_all!(i, or(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())),
i(for_all(x3y3z3(), r()))]), i(for_all(x3y3z3(), r()))]),
"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r"); "forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
// Quantified formula + implies // Implies + quantified formula
assert_all!(i, exists(xyz(), i(implies_right(p(), q()))), "exists X, Y, Z (p -> q)");
assert_all!(i, exists(xyz(), i(implies_left(p(), q()))), "exists X, Y, Z (q <- p)");
assert_all!(i, implies_right(i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q()))), assert_all!(i, implies_right(i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q()))),
"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q"); "exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
assert_all!(i, implies_left(i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q()))), assert_all!(i, implies_left(i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q()))),
"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p"); "exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
assert_all!(i, for_all(xyz(), i(implies_right(p(), q()))), "forall X, Y, Z (p -> q)");
assert_all!(i, for_all(xyz(), i(implies_left(p(), q()))), "forall X, Y, Z (q <- p)");
assert_all!(i, implies_right(i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q()))), assert_all!(i, implies_right(i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q()))),
"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q"); "forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
assert_all!(i, implies_left(i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q()))), assert_all!(i, implies_left(i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q()))),
"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p"); "forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
// Quantified formula + if and only if // If and only if + quantified formula
assert_all!(i, exists(xyz(), i(if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)"); assert_all!(i, if_and_only_if(vec![i(exists(x1y1z1(), p()))]), "exists X1, Y1, Z1 p");
assert_all!(i, if_and_only_if(vec![i(for_all(x1y1z1(), p()))]), "forall X1, Y1, Z1 p");
assert_all!(i, if_and_only_if(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())), assert_all!(i, if_and_only_if(vec![i(exists(x1y1z1(), p())), i(exists(x2y2z2(), q())),
i(exists(x3y3z3(), r()))]), i(exists(x3y3z3(), r()))]),
"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r"); "exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
assert_all!(i, for_all(xyz(), i(if_and_only_if(pqr()))), "forall X, Y, Z (p <-> q <-> r)");
assert_all!(i, if_and_only_if(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())), assert_all!(i, if_and_only_if(vec![i(for_all(x1y1z1(), p())), i(for_all(x2y2z2(), q())),
i(for_all(x3y3z3(), r()))]), i(for_all(x3y3z3(), r()))]),
"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r"); "forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
} }
#[test] #[test]
fn format_combination_and_and_lower() fn format_combinations_and()
{ {
// Not + and
assert_all!(i, not(i(and(vec![p()]))), "not p");
assert_all!(i, not(i(and(pqr()))), "not (p and q and r)");
// Quantified formula + and
assert_all!(i, exists(xyz(), i(and(vec![p()]))), "exists X, Y, Z p");
assert_all!(i, for_all(xyz(), i(and(vec![p()]))), "forall X, Y, Z p");
assert_all!(i, exists(xyz(), i(and(pqr()))), "exists X, Y, Z (p and q and r)");
assert_all!(i, for_all(xyz(), i(and(pqr()))), "forall X, Y, Z (p and q and r)");
// And + and // And + and
assert_all!(i, and(vec![i(and(vec![p()]))]), "p");
assert_all!(i, and(vec![i(and(pqr()))]), "p and q and r");
assert_all!(i, and(vec![i(and(vec![p()])), i(and(vec![q()])), i(and(vec![r()]))]), assert_all!(i, and(vec![i(and(vec![p()])), i(and(vec![q()])), i(and(vec![r()]))]),
"p and q and r"); "p and q and r");
assert_all!(i, and(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]), assert_all!(i, and(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]),
"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3"); "p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
// And + or // Or + and
assert_all!(i, and(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]), assert_all!(i, or(vec![i(and(vec![p()]))]), "p");
"p and q and r"); assert_all!(i, or(vec![i(and(pqr()))]), "p and q and r");
assert_all!(i, and(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]),
"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
assert_all!(i, or(vec![i(and(vec![p()])), i(and(vec![q()])), i(and(vec![r()]))]), assert_all!(i, or(vec![i(and(vec![p()])), i(and(vec![q()])), i(and(vec![r()]))]),
"p or q or r"); "p or q or r");
assert_all!(i, or(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]), assert_all!(i, or(vec![i(and(p1q1r1())), i(and(p2q2r2())), i(and(p3q3r3()))]),
"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3"); "p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
// And + implies // Implies + and
assert_all!(i, and(vec![i(implies_right(p1(), q1())), i(implies_right(p2(), q2())), assert_all!(i, implies_right(i(and(vec![p()])), i(and(vec![q()]))), "p -> q");
i(implies_right(p3(), q3()))]), assert_all!(i, implies_left(i(and(vec![p()])), i(and(vec![q()]))), "q <- p");
"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
assert_all!(i, and(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())),
i(implies_left(p3(), q3()))]),
"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
assert_all!(i, implies_right(i(and(p1q1r1())), i(and(p2q2r2()))), assert_all!(i, implies_right(i(and(p1q1r1())), i(and(p2q2r2()))),
"p1 and q1 and r1 -> p2 and q2 and r2"); "p1 and q1 and r1 -> p2 and q2 and r2");
assert_all!(i, implies_left(i(and(p1q1r1())), i(and(p2q2r2()))), assert_all!(i, implies_left(i(and(p1q1r1())), i(and(p2q2r2()))),
"p2 and q2 and r2 <- p1 and q1 and r1"); "p2 and q2 and r2 <- p1 and q1 and r1");
// And + if and only if // If and only if + and
assert_all!(i, and(vec![i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()])), assert_all!(i, if_and_only_if(vec![i(and(vec![p()]))]), "p");
i(if_and_only_if(vec![r()]))]), assert_all!(i, if_and_only_if(vec![i(and(pqr()))]), "p and q and r");
"p and q and r");
assert_all!(i, and(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())),
i(if_and_only_if(p3q3r3()))]),
"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
assert_all!(i, if_and_only_if(vec![i(and(vec![p()])), i(and(vec![q()])), assert_all!(i, if_and_only_if(vec![i(and(vec![p()])), i(and(vec![q()])),
i(and(vec![r()]))]), i(and(vec![r()]))]),
"p <-> q <-> r"); "p <-> q <-> r");
@ -1010,37 +994,45 @@ mod tests
} }
#[test] #[test]
fn format_combination_or_and_lower() fn format_combinations_or()
{ {
// Not + or
assert_all!(i, not(i(or(vec![p()]))), "not p");
assert_all!(i, not(i(or(pqr()))), "not (p or q or r)");
// Quantified formula + or
assert_all!(i, exists(xyz(), i(or(vec![p()]))), "exists X, Y, Z p");
assert_all!(i, for_all(xyz(), i(or(vec![p()]))), "forall X, Y, Z p");
assert_all!(i, exists(xyz(), i(or(pqr()))), "exists X, Y, Z (p or q or r)");
assert_all!(i, for_all(xyz(), i(or(pqr()))), "forall X, Y, Z (p or q or r)");
// And + or
assert_all!(i, and(vec![i(or(vec![p()]))]), "p");
assert_all!(i, and(vec![i(or(pqr()))]), "p or q or r");
assert_all!(i, and(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]),
"p and q and r");
assert_all!(i, and(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]),
"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
// Or + or // Or + or
assert_all!(i, or(vec![i(or(vec![p()]))]), "p");
assert_all!(i, or(vec![i(or(pqr()))]), "p or q or r");
assert_all!(i, or(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]), assert_all!(i, or(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]),
"p or q or r"); "p or q or r");
assert_all!(i, or(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]), assert_all!(i, or(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]),
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3"); "p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
// Or + implies // Implies + or
assert_all!(i, or(vec![i(implies_right(p1(), q1())), i(implies_right(p2(), q2())), assert_all!(i, implies_right(i(or(vec![p()])), i(or(vec![q()]))), "p -> q");
i(implies_right(p3(), q3()))]), assert_all!(i, implies_left(i(or(vec![p()])), i(or(vec![q()]))), "q <- p");
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
assert_all!(i, or(vec![i(and(vec![implies_right(p1(), q1())])),
i(and(vec![implies_right(p2(), q2())])), i(and(vec![implies_right(p3(), q3())]))]),
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
assert_all!(i, or(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())),
i(implies_left(p3(), q3()))]),
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
assert_all!(i, implies_right(i(or(p1q1r1())), i(or(p2q2r2()))), assert_all!(i, implies_right(i(or(p1q1r1())), i(or(p2q2r2()))),
"p1 or q1 or r1 -> p2 or q2 or r2"); "p1 or q1 or r1 -> p2 or q2 or r2");
assert_all!(i, implies_left(i(or(p1q1r1())), i(or(p2q2r2()))), assert_all!(i, implies_left(i(or(p1q1r1())), i(or(p2q2r2()))),
"p2 or q2 or r2 <- p1 or q1 or r1"); "p2 or q2 or r2 <- p1 or q1 or r1");
// Or + if and only if // If and only if + or
assert_all!(i, or(vec![i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()])), assert_all!(i, if_and_only_if(vec![i(or(vec![p()]))]), "p");
i(if_and_only_if(vec![r()]))]), assert_all!(i, if_and_only_if(vec![i(or(pqr()))]), "p or q or r");
"p or q or r");
assert_all!(i, or(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())),
i(if_and_only_if(p3q3r3()))]),
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
assert_all!(i, if_and_only_if(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]), assert_all!(i, if_and_only_if(vec![i(or(vec![p()])), i(or(vec![q()])), i(or(vec![r()]))]),
"p <-> q <-> r"); "p <-> q <-> r");
assert_all!(i, if_and_only_if(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]), assert_all!(i, if_and_only_if(vec![i(or(p1q1r1())), i(or(p2q2r2())), i(or(p3q3r3()))]),
@ -1048,8 +1040,38 @@ mod tests
} }
#[test] #[test]
fn format_combination_implies_and_lower() fn format_combinations_implies()
{ {
// Not + implies
assert_all!(i, not(i(implies_right(p(), q()))), "not (p -> q)");
assert_all!(i, not(i(implies_left(p(), q()))), "not (q <- p)");
// Quantified formula + implies
assert_all!(i, exists(xyz(), i(implies_right(p(), q()))), "exists X, Y, Z (p -> q)");
assert_all!(i, exists(xyz(), i(implies_left(p(), q()))), "exists X, Y, Z (q <- p)");
assert_all!(i, for_all(xyz(), i(implies_right(p(), q()))), "forall X, Y, Z (p -> q)");
assert_all!(i, for_all(xyz(), i(implies_left(p(), q()))), "forall X, Y, Z (q <- p)");
// And + implies
assert_all!(i, and(vec![i(implies_right(p(), q()))]), "p -> q");
assert_all!(i, and(vec![i(implies_left(p(), q()))]), "q <- p");
assert_all!(i, and(vec![i(implies_right(p1(), q1())), i(implies_right(p2(), q2())),
i(implies_right(p3(), q3()))]),
"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
assert_all!(i, and(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())),
i(implies_left(p3(), q3()))]),
"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
// Or + implies
assert_all!(i, or(vec![i(implies_right(p(), q()))]), "p -> q");
assert_all!(i, or(vec![i(implies_left(p(), q()))]), "q <- p");
assert_all!(i, or(vec![i(implies_right(p1(), q1())), i(implies_right(p2(), q2())),
i(implies_right(p3(), q3()))]),
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
assert_all!(i, or(vec![i(implies_left(p1(), q1())), i(implies_left(p2(), q2())),
i(implies_left(p3(), q3()))]),
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
// Implies + implies // Implies + implies
assert_all!(i, implies_right(i(implies_right(p1(), q1())), i(implies_right(p2(), q2()))), assert_all!(i, implies_right(i(implies_right(p1(), q1())), i(implies_right(p2(), q2()))),
"(p1 -> q1) -> p2 -> q2"); "(p1 -> q1) -> p2 -> q2");
@ -1060,11 +1082,9 @@ mod tests
assert_all!(i, implies_left(i(implies_left(p1(), q1())), i(implies_left(p2(), q2()))), assert_all!(i, implies_left(i(implies_left(p1(), q1())), i(implies_left(p2(), q2()))),
"q2 <- p2 <- (q1 <- p1)"); "q2 <- p2 <- (q1 <- p1)");
// Implies + if and only if // If and only if + implies
assert_all!(i, implies_right(i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2()))), assert_all!(i, if_and_only_if(vec![i(implies_right(p(), q()))]), "p -> q");
"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)"); assert_all!(i, if_and_only_if(vec![i(implies_left(p(), q()))]), "q <- p");
assert_all!(i, implies_left(i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2()))),
"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
assert_all!(i, if_and_only_if(vec![i(implies_right(p1(), q1())), assert_all!(i, if_and_only_if(vec![i(implies_right(p1(), q1())),
i(implies_right(p2(), q2())), i(implies_right(p3(), q3()))]), i(implies_right(p2(), q2())), i(implies_right(p3(), q3()))]),
"p1 -> q1 <-> p2 -> q2 <-> p3 -> q3"); "p1 -> q1 <-> p2 -> q2 <-> p3 -> q3");
@ -1072,4 +1092,58 @@ mod tests
i(implies_left(p3(), q3()))]), i(implies_left(p3(), q3()))]),
"q1 <- p1 <-> q2 <- p2 <-> q3 <- p3"); "q1 <- p1 <-> q2 <- p2 <-> q3 <- p3");
} }
#[test]
fn format_combinations_if_and_only_if()
{
// Not + if and only if
assert_all!(i, not(i(if_and_only_if(vec![p()]))), "not p");
assert_all!(i, not(i(if_and_only_if(pqr()))), "not (p <-> q <-> r)");
// Quantified formula + if and only if
assert_all!(i, exists(xyz(), i(if_and_only_if(vec![p()]))), "exists X, Y, Z p");
assert_all!(i, for_all(xyz(), i(if_and_only_if(vec![p()]))), "forall X, Y, Z p");
assert_all!(i, exists(xyz(), i(if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)");
assert_all!(i, for_all(xyz(), i(if_and_only_if(pqr()))), "forall X, Y, Z (p <-> q <-> r)");
// And + if and only if
assert_all!(i, and(vec![i(if_and_only_if(vec![p()]))]), "p");
assert_all!(i, and(vec![i(if_and_only_if(pqr()))]), "p <-> q <-> r");
assert_all!(i, and(vec![i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()])),
i(if_and_only_if(vec![r()]))]),
"p and q and r");
assert_all!(i, and(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())),
i(if_and_only_if(p3q3r3()))]),
"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
// Or + if and only if
assert_all!(i, or(vec![i(if_and_only_if(vec![p()]))]), "p");
assert_all!(i, or(vec![i(if_and_only_if(pqr()))]), "p <-> q <-> r");
assert_all!(i, or(vec![i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()])),
i(if_and_only_if(vec![r()]))]),
"p or q or r");
assert_all!(i, or(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())),
i(if_and_only_if(p3q3r3()))]),
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
// Implies + if and only if
assert_all!(i, implies_right(i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()]))),
"p -> q");
assert_all!(i, implies_left(i(if_and_only_if(vec![p()])), i(if_and_only_if(vec![q()]))),
"q <- p");
assert_all!(i, implies_right(i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2()))),
"(p1 <-> q1 <-> r1) -> (p2 <-> q2 <-> r2)");
assert_all!(i, implies_left(i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2()))),
"(p2 <-> q2 <-> r2) <- (p1 <-> q1 <-> r1)");
// If and only if + if and only if
assert_all!(i, if_and_only_if(vec![i(if_and_only_if(vec![p()]))]), "p");
assert_all!(i, if_and_only_if(vec![i(if_and_only_if(pqr()))]), "p <-> q <-> r");
assert_all!(i, if_and_only_if(vec![i(if_and_only_if(vec![p()])),
i(if_and_only_if(vec![q()])), i(if_and_only_if(vec![r()]))]),
"p <-> q <-> r");
assert_all!(i, if_and_only_if(vec![i(if_and_only_if(p1q1r1())), i(if_and_only_if(p2q2r2())),
i(if_and_only_if(p3q3r3()))]),
"(p1 <-> q1 <-> r1) <-> (p2 <-> q2 <-> r2) <-> (p3 <-> q3 <-> r3)");
}
} }