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

Test conjunction

Browse Source
This commit is contained in:
Patrick Lühne 2020-04-06 17:32:57 +02:00
parent 9e74116a4d
commit e4700fc638
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 254 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

279
src/format/formulas.rs
View File

@ -478,6 +478,36 @@ mod tests
predicate("q", vec![])
}
fn p1() -> Box<Formula>
{
predicate("p1", vec![])
}
fn q1() -> Box<Formula>
{
predicate("q1", vec![])
}
fn p2() -> Box<Formula>
{
predicate("p2", vec![])
}
fn q2() -> Box<Formula>
{
predicate("q2", vec![])
}
fn p3() -> Box<Formula>
{
predicate("p3", vec![])
}
fn q3() -> Box<Formula>
{
predicate("q3", vec![])
}
fn r() -> Box<Formula>
{
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<Formula>, implication: Box<Formula>) -> Box<Formula>
{
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");
}
}