From e4700fc63843467609315b33976a44f7d19c0aa1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Mon, 6 Apr 2020 17:32:57 +0200 Subject: [PATCH] Test conjunction --- src/format/formulas.rs | 279 +++++++++++++++++++++++++++++++++++++---- 1 file changed, 254 insertions(+), 25 deletions(-) diff --git a/src/format/formulas.rs b/src/format/formulas.rs index 78edb1a..ac2b6f7 100644 --- a/src/format/formulas.rs +++ b/src/format/formulas.rs @@ -478,6 +478,36 @@ mod tests predicate("q", vec![]) } + fn p1() -> Box + { + predicate("p1", vec![]) + } + + fn q1() -> Box + { + predicate("q1", vec![]) + } + + fn p2() -> Box + { + predicate("p2", vec![]) + } + + fn q2() -> Box + { + predicate("q2", vec![]) + } + + fn p3() -> Box + { + predicate("p3", vec![]) + } + + fn q3() -> Box + { + predicate("q3", vec![]) + } + fn r() -> Box { predicate("r", vec![]) @@ -488,6 +518,21 @@ mod tests vec![p(), q(), r()] } + fn p1q1r1() -> Formulas + { + vec![p1(), q1(), predicate("r1", vec![])] + } + + fn p2q2r2() -> Formulas + { + vec![p2(), q2(), predicate("r2", vec![])] + } + + fn p3q3r3() -> Formulas + { + vec![p3(), q3(), predicate("r3", vec![])] + } + fn implies_right(antecedent: Box, implication: Box) -> Box { implies(ImplicationDirection::LeftToRight, antecedent, implication) @@ -1254,32 +1299,216 @@ mod tests #[test] fn format_combination_and_and_lower() { - /* - let and_abc = || and(vec![predicate("a", vec![]), predicate("b", vec![]), - predicate("c", vec![])]); - let and_def = || and(vec![predicate("d", vec![]), predicate("e", vec![]), - predicate("f", vec![])]); - let and_ghi = || and(vec![predicate("g", vec![]), predicate("h", vec![]), - predicate("i", vec![])]); - let or_abc = || and(vec![predicate("a", vec![]), predicate("b", vec![]), - predicate("c", vec![])]); - let or_def = || and(vec![predicate("d", vec![]), predicate("e", vec![]), - predicate("f", vec![])]); - let or_ghi = || and(vec![predicate("g", vec![]), predicate("h", vec![]), - predicate("i", vec![])]); - let if_and_only_if_abc = || if_and_only_if(vec![predicate("a", vec![]), - predicate("b", vec![]), predicate("c", vec![])]); - let if_and_only_if_def = || if_and_only_if(vec![predicate("d", vec![]), - predicate("e", vec![]), predicate("f", vec![])]); - let if_and_only_if_ghi = || if_and_only_if(vec![predicate("g", vec![]), - predicate("h", vec![]), predicate("i", vec![])]); - // And + and assert_eq!(format( - and(vec![and_abc(), and_def(), and_ghi()] - - ))), - "exists X, Y, Z exists A, B, C p"); - */ + and(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])), + "p and q and r"); + assert_eq!(format( + and(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]), + and(vec![and(vec![r()])])])), + "p and q and r"); + assert_eq!(format( + and(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]), + or(vec![and(vec![r()])])])), + "p and q and r"); + assert_eq!(format( + and(vec![if_and_only_if(vec![and(vec![p()])]), if_and_only_if(vec![and(vec![q()])]), + if_and_only_if(vec![and(vec![r()])])])), + "p and q and r"); + assert_eq!(format( + and(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])), + "p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3"); + assert_eq!(format( + and(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]), + and(vec![and(p3q3r3())])])), + "p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3"); + assert_eq!(format( + and(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]), or(vec![and(p3q3r3())])])), + "p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3"); + assert_eq!(format( + and(vec![if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]), + if_and_only_if(vec![and(p3q3r3())])])), + "p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3"); + + // And + or + assert_eq!(format(and(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])), "p and q and r"); + assert_eq!(format( + and(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]), + and(vec![or(vec![r()])])])), + "p and q and r"); + assert_eq!(format( + and(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]), or(vec![or(vec![r()])])])), + "p and q and r"); + assert_eq!(format( + and(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 and q and r"); + assert_eq!(format( + and(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])), + "(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)"); + assert_eq!(format( + and(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]), and(vec![or(p3q3r3())])])), + "(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)"); + assert_eq!(format( + and(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]), or(vec![or(p3q3r3())])])), + "(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)"); + assert_eq!(format( + and(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) and (p2 or q2 or r2) and (p3 or q3 or r3)"); + + assert_eq!(format(or(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])), "p or q or r"); + assert_eq!(format( + or(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]), + and(vec![and(vec![r()])])])), + "p or q or r"); + assert_eq!(format( + or(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]), or(vec![and(vec![r()])])])), + "p or q or r"); + assert_eq!(format( + or(vec![if_and_only_if(vec![and(vec![p()])]), if_and_only_if(vec![and(vec![q()])]), + if_and_only_if(vec![and(vec![r()])])])), + "p or q or r"); + assert_eq!(format( + or(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])), + "p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3"); + assert_eq!(format( + or(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]), and(vec![and(p3q3r3())])])), + "p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3"); + assert_eq!(format( + or(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]), or(vec![and(p3q3r3())])])), + "p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3"); + assert_eq!(format( + or(vec![if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]), + if_and_only_if(vec![and(p3q3r3())])])), + "p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3"); + + // And + implies + assert_eq!(format( + and(vec![implies_right(p1(), q1()), implies_right(p2(), q2()), + implies_right(p3(), q3())])), + "(p1 -> q1) and (p2 -> q2) and (p3 -> q3)"); + assert_eq!(format( + and(vec![and(vec![implies_right(p1(), q1())]), and(vec![implies_right(p2(), q2())]), + and(vec![implies_right(p3(), q3())])])), + "(p1 -> q1) and (p2 -> q2) and (p3 -> q3)"); + assert_eq!(format( + and(vec![or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]), + or(vec![implies_right(p3(), q3())])])), + "(p1 -> q1) and (p2 -> q2) and (p3 -> q3)"); + assert_eq!(format( + and(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) and (p2 -> q2) and (p3 -> q3)"); + assert_eq!(format( + and(vec![implies_left(p1(), q1()), implies_left(p2(), q2()), + implies_left(p3(), q3())])), + "(q1 <- p1) and (q2 <- p2) and (q3 <- p3)"); + assert_eq!(format( + and(vec![and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]), + and(vec![implies_left(p3(), q3())])])), + "(q1 <- p1) and (q2 <- p2) and (q3 <- p3)"); + assert_eq!(format( + and(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]), + or(vec![implies_left(p3(), q3())])])), + "(q1 <- p1) and (q2 <- p2) and (q3 <- p3)"); + assert_eq!(format( + and(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) and (q2 <- p2) and (q3 <- p3)"); + assert_eq!(format( + implies_right(and(p1q1r1()), and(p2q2r2()))), + "p1 and q1 and r1 -> p2 and q2 and r2"); + assert_eq!(format( + implies_right(and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]))), + "p1 and q1 and r1 -> p2 and q2 and r2"); + assert_eq!(format( + implies_right(or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]))), + "p1 and q1 and r1 -> p2 and q2 and r2"); + assert_eq!(format( + implies_right(if_and_only_if(vec![and(p1q1r1())]), + if_and_only_if(vec![and(p2q2r2())]))), + "p1 and q1 and r1 -> p2 and q2 and r2"); + assert_eq!(format( + implies_left(and(p1q1r1()), and(p2q2r2()))), + "p2 and q2 and r2 <- p1 and q1 and r1"); + assert_eq!(format( + implies_left(and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]))), + "p2 and q2 and r2 <- p1 and q1 and r1"); + assert_eq!(format( + implies_left(or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]))), + "p2 and q2 and r2 <- p1 and q1 and r1"); + assert_eq!(format( + implies_left(if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]))), + "p2 and q2 and r2 <- p1 and q1 and r1"); + + // And + if and only if + assert_eq!(format( + and(vec![if_and_only_if(vec![p()]), if_and_only_if(vec![q()]), + if_and_only_if(vec![r()])])), + "p and q and r"); + assert_eq!(format( + and(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 and q and r"); + assert_eq!(format( + and(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 and q and r"); + assert_eq!(format( + and(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 and q and r"); + assert_eq!(format( + and(vec![if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()), + if_and_only_if(p3q3r3())])), + "(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)"); + assert_eq!(format( + and(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) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)"); + assert_eq!(format( + and(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) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)"); + assert_eq!(format( + and(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) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)"); + + assert_eq!(format( + if_and_only_if(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])), + "p <-> q <-> r"); + assert_eq!(format( + if_and_only_if(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]), + and(vec![and(vec![r()])])])), + "p <-> q <-> r"); + assert_eq!(format( + if_and_only_if(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]), + or(vec![and(vec![r()])])])), + "p <-> q <-> r"); + assert_eq!(format( + if_and_only_if(vec![if_and_only_if(vec![and(vec![p()])]), + if_and_only_if(vec![and(vec![q()])]), if_and_only_if(vec![and(vec![r()])])])), + "p <-> q <-> r"); + assert_eq!(format( + if_and_only_if(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])), + "p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3"); + assert_eq!(format( + if_and_only_if(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]), + and(vec![and(p3q3r3())])])), + "p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3"); + assert_eq!(format( + if_and_only_if(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]), + or(vec![and(p3q3r3())])])), + "p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3"); + assert_eq!(format( + if_and_only_if(vec![if_and_only_if(vec![and(p1q1r1())]), + 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"); } }