diff --git a/src/format/formulas.rs b/src/format/formulas.rs index 944ac89..71fd3dc 100644 --- a/src/format/formulas.rs +++ b/src/format/formulas.rs @@ -433,6 +433,71 @@ mod tests Box::new(Formula::true_()) } + fn x() -> std::rc::Rc + { + variable_declaration("X") + } + + fn y() -> std::rc::Rc + { + variable_declaration("Y") + } + + fn z() -> std::rc::Rc + { + variable_declaration("Z") + } + + fn xyz() -> VariableDeclarations + { + vec![x(), y(), z()] + } + + fn x1y1z1() -> VariableDeclarations + { + vec![variable_declaration("X1"), variable_declaration("Y1"), variable_declaration("Z1")] + } + + fn x2y2z2() -> VariableDeclarations + { + vec![variable_declaration("X2"), variable_declaration("Y2"), variable_declaration("Z2")] + } + + fn x3y3z3() -> VariableDeclarations + { + vec![variable_declaration("X3"), variable_declaration("Y3"), variable_declaration("Z3")] + } + + fn p() -> Box + { + predicate("p", vec![]) + } + + fn q() -> Box + { + predicate("q", vec![]) + } + + fn r() -> Box + { + predicate("r", vec![]) + } + + fn pqr() -> Formulas + { + vec![p(), q(), r()] + } + + fn implies_right(antecedent: Box, implication: Box) -> Box + { + implies(ImplicationDirection::LeftToRight, antecedent, implication) + } + + fn implies_left(antecedent: Box, implication: Box) -> Box + { + implies(ImplicationDirection::RightToLeft, antecedent, implication) + } + #[test] fn format_boolean() { @@ -479,7 +544,7 @@ mod tests #[test] fn format_predicate() { - assert_eq!(format(predicate("p", vec![])), "p"); + assert_eq!(format(p()), "p"); assert_eq!(format(predicate("predicate", vec![])), "predicate"); assert_eq!(format(predicate("q", vec![constant("a")])), "q(a)"); assert_eq!(format( @@ -513,75 +578,50 @@ mod tests #[test] fn format_exists() { - assert_eq!(format( - exists(vec![variable_declaration("X")], predicate("p", vec![]))), - "exists X p"); - assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], predicate("p", vec![]))), - "exists X, Y, Z p"); + assert_eq!(format(exists(vec![x()], p())), "exists X p"); + assert_eq!(format(exists(xyz(), p())), "exists X, Y, Z p"); } #[test] fn format_for_all() { - assert_eq!(format( - for_all(vec![variable_declaration("X")], predicate("p", vec![]))), - "forall X p"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], predicate("p", vec![]))), - "forall X, Y, Z p"); + assert_eq!(format(for_all(vec![x()], p())), "forall X p"); + assert_eq!(format(for_all(xyz(), p())), "forall X, Y, Z p"); } #[test] fn format_not() { - assert_eq!(format(not(predicate("p", vec![]))), "not p"); + assert_eq!(format(not(p())), "not p"); } #[test] fn format_and() { - assert_eq!(format(and(vec![predicate("p", vec![])])), "p"); - assert_eq!(format( - and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])])), - "p and q and r"); + assert_eq!(format(and(vec![p()])), "p"); + assert_eq!(format(and(pqr())), "p and q and r"); } #[test] fn format_or() { - assert_eq!(format(or(vec![predicate("p", vec![])])), "p"); - assert_eq!(format( - or(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])])), - "p or q or r"); + assert_eq!(format(or(vec![p()])), "p"); + assert_eq!(format(or(pqr())), "p or q or r"); } #[test] fn format_implies() { - assert_eq!(format( - implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![]))), - "p -> q"); - assert_eq!(format( - implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![]))), - "q <- p"); + assert_eq!(format(implies_right(p(), q())), "p -> q"); + assert_eq!(format(implies_left(p(), q())), "q <- p"); } #[test] fn format_if_and_only_if() { - assert_eq!(format(if_and_only_if(vec![predicate("p", vec![])])), "p"); - assert_eq!(format( - if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![])])), - "p <-> q"); - assert_eq!(format( - if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])), - "p <-> q <-> r"); + 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"); } #[test] @@ -592,26 +632,14 @@ mod tests assert_eq!(format(not(false_())), "not false"); // Boolean + quantified formula - assert_eq!(format(exists(vec![variable_declaration("X")], true_())), "exists X true"); - assert_eq!(format(exists(vec![variable_declaration("X")], false_())), "exists X false"); - assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], true_())), - "exists X, Y, Z true"); - assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], false_())), - "exists X, Y, Z false"); - assert_eq!(format(for_all(vec![variable_declaration("X")], true_())), "forall X true"); - assert_eq!(format(for_all(vec![variable_declaration("X")], false_())), "forall X false"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], true_())), - "forall X, Y, Z true"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], false_())), - "forall X, Y, Z false"); + 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"); // Boolean + and assert_eq!(format(and(vec![true_()])), "true"); @@ -626,18 +654,10 @@ mod tests assert_eq!(format(or(vec![false_(), false_(), false_()])), "false or false or false"); // Boolean + implies - assert_eq!(format( - implies(ImplicationDirection::LeftToRight, true_(), true_())), - "true -> true"); - assert_eq!(format( - implies(ImplicationDirection::RightToLeft, true_(), true_())), - "true <- true"); - assert_eq!(format( - implies(ImplicationDirection::LeftToRight, false_(), false_())), - "false -> false"); - assert_eq!(format( - implies(ImplicationDirection::RightToLeft, false_(), false_())), - "false <- false"); + 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"); // Boolean + if and only if assert_eq!(format(if_and_only_if(vec![true_()])), "true"); @@ -668,40 +688,40 @@ mod tests // Compare + quantified formula assert_eq!(format( - exists(vec![variable_declaration("X")], greater(term_1(), term_2()))), + exists(vec![x()], greater(term_1(), term_2()))), "exists X (a + b) * c > |d - e|"); assert_eq!(format( - exists(vec![variable_declaration("X")], less(term_1(), term_2()))), + exists(vec![x()], less(term_1(), term_2()))), "exists X (a + b) * c < |d - e|"); assert_eq!(format( - exists(vec![variable_declaration("X")], less_or_equal(term_1(), term_2()))), + exists(vec![x()], less_or_equal(term_1(), term_2()))), "exists X (a + b) * c <= |d - e|"); assert_eq!(format( - exists(vec![variable_declaration("X")], greater_or_equal(term_1(), term_2()))), + exists(vec![x()], greater_or_equal(term_1(), term_2()))), "exists X (a + b) * c >= |d - e|"); assert_eq!(format( - exists(vec![variable_declaration("X")], equal(term_1(), term_2()))), + exists(vec![x()], equal(term_1(), term_2()))), "exists X (a + b) * c = |d - e|"); assert_eq!(format( - exists(vec![variable_declaration("X")], not_equal(term_1(), term_2()))), + exists(vec![x()], not_equal(term_1(), term_2()))), "exists X (a + b) * c != |d - e|"); assert_eq!(format( - for_all(vec![variable_declaration("X")], greater(term_1(), term_2()))), + for_all(vec![x()], greater(term_1(), term_2()))), "forall X (a + b) * c > |d - e|"); assert_eq!(format( - for_all(vec![variable_declaration("X")], less(term_1(), term_2()))), + for_all(vec![x()], less(term_1(), term_2()))), "forall X (a + b) * c < |d - e|"); assert_eq!(format( - for_all(vec![variable_declaration("X")], less_or_equal(term_1(), term_2()))), + for_all(vec![x()], less_or_equal(term_1(), term_2()))), "forall X (a + b) * c <= |d - e|"); assert_eq!(format( - for_all(vec![variable_declaration("X")], greater_or_equal(term_1(), term_2()))), + for_all(vec![x()], greater_or_equal(term_1(), term_2()))), "forall X (a + b) * c >= |d - e|"); assert_eq!(format( - for_all(vec![variable_declaration("X")], equal(term_1(), term_2()))), + for_all(vec![x()], equal(term_1(), term_2()))), "forall X (a + b) * c = |d - e|"); assert_eq!(format( - for_all(vec![variable_declaration("X")], not_equal(term_1(), term_2()))), + for_all(vec![x()], not_equal(term_1(), term_2()))), "forall X (a + b) * c != |d - e|"); // Compare + and @@ -758,52 +778,42 @@ mod tests // Compare + implies assert_eq!(format( - implies(ImplicationDirection::LeftToRight, greater(term_1(), term_2()), - greater(term_3(), term_4()))), + 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(ImplicationDirection::LeftToRight, less(term_1(), term_2()), - less(term_3(), term_4()))), + 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(ImplicationDirection::LeftToRight, less_or_equal(term_1(), term_2()), - less_or_equal(term_3(), term_4()))), + 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(ImplicationDirection::LeftToRight, greater_or_equal(term_1(), term_2()), + 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(ImplicationDirection::LeftToRight, equal(term_1(), term_2()), - equal(term_3(), term_4()))), + 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(ImplicationDirection::LeftToRight, not_equal(term_1(), term_2()), - not_equal(term_3(), term_4()))), + 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(ImplicationDirection::RightToLeft, greater(term_1(), term_2()), - greater(term_3(), term_4()))), + 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(ImplicationDirection::RightToLeft, less(term_1(), term_2()), - less(term_3(), term_4()))), + 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(ImplicationDirection::RightToLeft, less_or_equal(term_1(), term_2()), - less_or_equal(term_3(), term_4()))), + 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(ImplicationDirection::RightToLeft, greater_or_equal(term_1(), term_2()), + 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(ImplicationDirection::RightToLeft, equal(term_1(), term_2()), - equal(term_3(), term_4()))), + 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(ImplicationDirection::RightToLeft, not_equal(term_1(), term_2()), - not_equal(term_3(), term_4()))), + 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 @@ -837,279 +847,115 @@ mod tests fn format_combination_not_and_lower() { // Not + not - assert_eq!(format(not(not(predicate("p", vec![])))), "not not p"); + assert_eq!(format(not(not(p()))), "not not p"); // Not + quantified formulas - assert_eq!(format( - not(exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], predicate("p", vec![])))), - "not exists X, Y, Z p"); - assert_eq!(format( - not(exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], and(vec![predicate("p", vec![])])))), - "not exists X, Y, Z p"); - assert_eq!(format( - not(exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], or(vec![predicate("p", vec![])])))), - "not exists X, Y, Z p"); - assert_eq!(format( - not(exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], if_and_only_if(vec![predicate("p", vec![])])))), - "not exists X, Y, Z p"); - assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], not(predicate("p", vec![])))), - "exists X, Y, Z not p"); - assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], and(vec![not(predicate("p", vec![]))]))), - "exists X, Y, Z not p"); - assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], or(vec![not(predicate("p", vec![]))]))), - "exists X, Y, Z not p"); - assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], if_and_only_if(vec![not(predicate("p", vec![]))]))), - "exists X, Y, Z not p"); - assert_eq!(format( - not(for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], predicate("p", vec![])))), - "not forall X, Y, Z p"); - assert_eq!(format( - not(for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], and(vec![predicate("p", vec![])])))), - "not forall X, Y, Z p"); - assert_eq!(format( - not(for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], or(vec![predicate("p", vec![])])))), - "not forall X, Y, Z p"); - assert_eq!(format( - not(for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], if_and_only_if(vec![predicate("p", vec![])])))), - "not forall X, Y, Z p"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], not(predicate("p", vec![])))), - "forall X, Y, Z not p"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], and(vec![not(predicate("p", vec![]))]))), - "forall X, Y, Z not p"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], or(vec![not(predicate("p", vec![]))]))), - "forall X, Y, Z not p"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], if_and_only_if(vec![not(predicate("p", vec![]))]))), - "forall X, Y, Z not p"); + assert_eq!(format(not(exists(xyz(), p()))), "not exists X, Y, Z p"); + assert_eq!(format(not(exists(xyz(), and(vec![p()])))), "not exists X, Y, Z p"); + assert_eq!(format(not(exists(xyz(), or(vec![p()])))), "not exists X, Y, Z p"); + assert_eq!(format(not(exists(xyz(), if_and_only_if(vec![p()])))), "not exists X, Y, Z p"); + assert_eq!(format(exists(xyz(), not(p()))), "exists X, Y, Z not p"); + assert_eq!(format(exists(xyz(), and(vec![not(p())]))), "exists X, Y, Z not p"); + assert_eq!(format(exists(xyz(), or(vec![not(p())]))), "exists X, Y, Z not p"); + assert_eq!(format(exists(xyz(), if_and_only_if(vec![not(p())]))), "exists X, Y, Z not p"); + assert_eq!(format(not(for_all(xyz(), p()))), "not forall X, Y, Z p"); + assert_eq!(format(not(for_all(xyz(), and(vec![p()])))), "not forall X, Y, Z p"); + assert_eq!(format(not(for_all(xyz(), or(vec![p()])))), "not forall X, Y, Z p"); + assert_eq!(format(not(for_all(xyz(), if_and_only_if(vec![p()])))), "not forall X, Y, Z p"); + assert_eq!(format(for_all(xyz(), not(p()))), "forall X, Y, Z not p"); + assert_eq!(format(for_all(xyz(), and(vec![not(p())]))), "forall X, Y, Z not p"); + assert_eq!(format(for_all(xyz(), or(vec![not(p())]))), "forall X, Y, Z not p"); + assert_eq!(format(for_all(xyz(), if_and_only_if(vec![not(p())]))), "forall X, Y, Z not p"); // Not + and + assert_eq!(format(not(and(pqr()))), "not (p and q and r)"); + assert_eq!(format(not(and(vec![and(pqr())]))), "not (p and q and r)"); + assert_eq!(format(not(or(vec![and(pqr())]))), "not (p and q and r)"); + assert_eq!(format(not(if_and_only_if(vec![and(pqr())]))), "not (p and q and r)"); + assert_eq!(format(and(vec![not(p())])), "not p"); + assert_eq!(format(and(vec![not(and(vec![p()]))])), "not p"); + assert_eq!(format(and(vec![not(or(vec![p()]))])), "not p"); + assert_eq!(format(and(vec![not(if_and_only_if(vec![p()]))])), "not p"); + assert_eq!(format(and(vec![not(p()), not(q()), not(r())])), "not p and not q and not r"); assert_eq!(format( - not(and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))), - "not (p and q and r)"); - assert_eq!(format( - not(and(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "not (p and q and r)"); - assert_eq!(format( - not(or(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "not (p and q and r)"); - assert_eq!(format( - not(if_and_only_if(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "not (p and q and r)"); - assert_eq!(format( - and(vec![not(predicate("p", vec![]))])), - "not p"); - assert_eq!(format( - and(vec![not(and(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - and(vec![not(or(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - and(vec![not(if_and_only_if(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - and(vec![not(predicate("p", vec![])), not(predicate("q", vec![])), - not(predicate("r", vec![]))])), + and(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])), "not p and not q and not r"); assert_eq!(format( - and(vec![and(vec![not(predicate("p", vec![]))]), - and(vec![not(predicate("q", vec![]))]), and(vec![not(predicate("r", vec![]))])])), + and(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])), "not p and not q and not r"); assert_eq!(format( - and(vec![or(vec![not(predicate("p", vec![]))]), - or(vec![not(predicate("q", vec![]))]), or(vec![not(predicate("r", vec![]))])])), - "not p and not q and not r"); - assert_eq!(format( - and(vec![if_and_only_if(vec![not(predicate("p", vec![]))]), - if_and_only_if(vec![not(predicate("q", vec![]))]), - if_and_only_if(vec![not(predicate("r", vec![]))])])), + and(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]), + if_and_only_if(vec![not(r())])])), "not p and not q and not r"); // Not + or + assert_eq!(format(not(or(pqr()))), "not (p or q or r)"); + assert_eq!(format(not(and(vec![or(pqr())]))), "not (p or q or r)"); + assert_eq!(format(not(or(vec![or(pqr())]))), "not (p or q or r)"); + assert_eq!(format(not(if_and_only_if(vec![or(pqr())]))), "not (p or q or r)"); + assert_eq!(format(or(vec![not(p())])), "not p"); + assert_eq!(format(or(vec![not(and(vec![p()]))])), "not p"); + assert_eq!(format(or(vec![not(or(vec![p()]))])), "not p"); + assert_eq!(format(or(vec![not(if_and_only_if(vec![p()]))])), "not p"); + assert_eq!(format(or(vec![not(p()), not(q()), not(r())])), "not p or not q or not r"); assert_eq!(format( - not(or(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))), - "not (p or q or r)"); - assert_eq!(format( - not(and(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "not (p or q or r)"); - assert_eq!(format( - not(or(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "not (p or q or r)"); - assert_eq!(format( - not(if_and_only_if(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "not (p or q or r)"); - assert_eq!(format( - or(vec![not(predicate("p", vec![]))])), - "not p"); - assert_eq!(format( - or(vec![not(and(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - or(vec![not(or(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - or(vec![not(if_and_only_if(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - or(vec![not(predicate("p", vec![])), not(predicate("q", vec![])), - not(predicate("r", vec![]))])), + or(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])), "not p or not q or not r"); assert_eq!(format( - or(vec![and(vec![not(predicate("p", vec![]))]), - and(vec![not(predicate("q", vec![]))]), and(vec![not(predicate("r", vec![]))])])), + or(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])), "not p or not q or not r"); assert_eq!(format( - or(vec![or(vec![not(predicate("p", vec![]))]), - or(vec![not(predicate("q", vec![]))]), or(vec![not(predicate("r", vec![]))])])), - "not p or not q or not r"); - assert_eq!(format( - or(vec![if_and_only_if(vec![not(predicate("p", vec![]))]), - if_and_only_if(vec![not(predicate("q", vec![]))]), - if_and_only_if(vec![not(predicate("r", vec![]))])])), + or(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]), + if_and_only_if(vec![not(r())])])), "not p or not q or not r"); // Not + implies + assert_eq!(format(not(implies_right(p(), q()))), "not (p -> q)"); + assert_eq!(format(not(and(vec![implies_right(p(), q())]))), "not (p -> q)"); + assert_eq!(format(not(or(vec![implies_right(p(), q())]))), "not (p -> q)"); + assert_eq!(format(not(if_and_only_if(vec![implies_right(p(), q())]))), "not (p -> q)"); + assert_eq!(format(not(implies_left(p(), q()))), "not (q <- p)"); + assert_eq!(format(not(and(vec![implies_left(p(), q())]))), "not (q <- p)"); + assert_eq!(format(not(or(vec![implies_left(p(), q())]))), "not (q <- p)"); + assert_eq!(format(not(if_and_only_if(vec![implies_left(p(), q())]))), "not (q <- p)"); + assert_eq!(format(implies_right(not(p()), not(q()))), "not p -> not q"); assert_eq!(format( - not(implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![])))), - "not (p -> q)"); - assert_eq!(format( - not(and(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![]))]))), - "not (p -> q)"); - assert_eq!(format( - not(or(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![]))]))), - "not (p -> q)"); - assert_eq!(format( - not(if_and_only_if(vec![implies(ImplicationDirection::LeftToRight, - predicate("p", vec![]), predicate("q", vec![]))]))), - "not (p -> q)"); - assert_eq!(format( - not(implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![])))), - "not (q <- p)"); - assert_eq!(format( - not(and(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![]))]))), - "not (q <- p)"); - assert_eq!(format( - not(or(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![]))]))), - "not (q <- p)"); - assert_eq!(format( - not(if_and_only_if(vec![implies(ImplicationDirection::RightToLeft, - predicate("p", vec![]), predicate("q", vec![]))]))), - "not (q <- p)"); - assert_eq!(format( - implies(ImplicationDirection::LeftToRight, not(predicate("p", vec![])), - not(predicate("q", vec![])))), + implies_right(and(vec![not(p())]), and(vec![not(q())]))), "not p -> not q"); + assert_eq!(format(implies_right(or(vec![not(p())]), or(vec![not(q())]))), "not p -> not q"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, and(vec![not(predicate("p", vec![]))]), - and(vec![not(predicate("q", vec![]))]))), + implies_right(if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]))), "not p -> not q"); + assert_eq!(format(implies_left(not(p()), not(q()))), "not q <- not p"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, or(vec![not(predicate("p", vec![]))]), - or(vec![not(predicate("q", vec![]))]))), - "not p -> not q"); - assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - if_and_only_if(vec![not(predicate("p", vec![]))]), - if_and_only_if(vec![not(predicate("q", vec![]))]))), - "not p -> not q"); - assert_eq!(format( - implies(ImplicationDirection::RightToLeft, not(predicate("p", vec![])), - not(predicate("q", vec![])))), + implies_left(and(vec![not(p())]), and(vec![not(q())]))), "not q <- not p"); + assert_eq!(format(implies_left(or(vec![not(p())]), or(vec![not(q())]))), "not q <- not p"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, and(vec![not(predicate("p", vec![]))]), - and(vec![not(predicate("q", vec![]))]))), - "not q <- not p"); - assert_eq!(format( - implies(ImplicationDirection::RightToLeft, or(vec![not(predicate("p", vec![]))]), - or(vec![not(predicate("q", vec![]))]))), - "not q <- not p"); - assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - if_and_only_if(vec![not(predicate("p", vec![]))]), - if_and_only_if(vec![not(predicate("q", vec![]))]))), + implies_left(if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]))), "not q <- not p"); // Not + if and only if + assert_eq!(format(not(if_and_only_if(pqr()))), "not (p <-> q <-> r)"); + assert_eq!(format(not(and(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)"); + assert_eq!(format(not(or(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)"); + assert_eq!(format(not(if_and_only_if(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)"); + assert_eq!(format(if_and_only_if(vec![not(p())])), "not p"); + assert_eq!(format(if_and_only_if(vec![not(and(vec![p()]))])),"not p"); + assert_eq!(format(if_and_only_if(vec![not(or(vec![p()]))])), "not p"); + assert_eq!(format(if_and_only_if(vec![not(if_and_only_if(vec![p()]))])), "not p"); assert_eq!(format( - not(if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])]))), - "not (p <-> q <-> r)"); - assert_eq!(format( - not(and(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "not (p <-> q <-> r)"); - assert_eq!(format( - not(or(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "not (p <-> q <-> r)"); - assert_eq!(format( - not(if_and_only_if(vec![if_and_only_if(vec![predicate("p", vec![]), - predicate("q", vec![]), predicate("r", vec![])])]))), - "not (p <-> q <-> r)"); - assert_eq!(format( - if_and_only_if(vec![not(predicate("p", vec![]))])), - "not p"); - assert_eq!(format( - if_and_only_if(vec![not(and(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - if_and_only_if(vec![not(or(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - if_and_only_if(vec![not(if_and_only_if(vec![predicate("p", vec![])]))])), - "not p"); - assert_eq!(format( - if_and_only_if(vec![not(predicate("p", vec![])), not(predicate("q", vec![])), - not(predicate("r", vec![]))])), + if_and_only_if(vec![not(p()), not(q()), not(r())])), "not p <-> not q <-> not r"); assert_eq!(format( - if_and_only_if(vec![and(vec![not(predicate("p", vec![]))]), - and(vec![not(predicate("q", vec![]))]), and(vec![not(predicate("r", vec![]))])])), + if_and_only_if(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])), "not p <-> not q <-> not r"); assert_eq!(format( - if_and_only_if(vec![or(vec![not(predicate("p", vec![]))]), - or(vec![not(predicate("q", vec![]))]), or(vec![not(predicate("r", vec![]))])])), + if_and_only_if(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])), "not p <-> not q <-> not r"); assert_eq!(format( - if_and_only_if(vec![if_and_only_if(vec![not(predicate("p", vec![]))]), - if_and_only_if(vec![not(predicate("q", vec![]))]), - if_and_only_if(vec![not(predicate("r", vec![]))])])), + if_and_only_if(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]), + if_and_only_if(vec![not(r())])])), "not p <-> not q <-> not r"); } @@ -1118,675 +964,332 @@ mod tests { // Quantified formula + quantified formula assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - exists(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![])))), - "exists X, Y, Z exists A, B, C p"); + exists(x1y1z1(), exists(x2y2z2(), p()))), + "exists X1, Y1, Z1 exists X2, Y2, Z2 p"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![exists(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![]))]))), - "exists X, Y, Z exists A, B, C p"); + exists(x1y1z1(), and(vec![exists(x2y2z2(), p())]))), + "exists X1, Y1, Z1 exists X2, Y2, Z2 p"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![exists(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![]))]))), - "exists X, Y, Z exists A, B, C p"); + exists(x1y1z1(), or(vec![exists(x2y2z2(), p())]))), + "exists X1, Y1, Z1 exists X2, Y2, Z2 p"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![exists(vec![variable_declaration("A"), - variable_declaration("B"), variable_declaration("C")], - predicate("p", vec![]))]))), - "exists X, Y, Z exists A, B, C p"); + exists(x1y1z1(), if_and_only_if(vec![exists(x2y2z2(), p())]))), + "exists X1, Y1, Z1 exists X2, Y2, Z2 p"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - for_all(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![])))), - "exists X, Y, Z forall A, B, C p"); + exists(x1y1z1(), for_all(x2y2z2(), p()))), + "exists X1, Y1, Z1 forall X2, Y2, Z2 p"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![]))]))), - "exists X, Y, Z forall A, B, C p"); + exists(x1y1z1(), and(vec![for_all(x2y2z2(), p())]))), + "exists X1, Y1, Z1 forall X2, Y2, Z2 p"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![]))]))), - "exists X, Y, Z forall A, B, C p"); + exists(x1y1z1(), or(vec![for_all(x2y2z2(), p())]))), + "exists X1, Y1, Z1 forall X2, Y2, Z2 p"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![for_all(vec![variable_declaration("A"), - variable_declaration("B"), variable_declaration("C")], - predicate("p", vec![]))]))), - "exists X, Y, Z forall A, B, C p"); + exists(x1y1z1(), if_and_only_if(vec![for_all(x2y2z2(), p())]))), + "exists X1, Y1, Z1 forall X2, Y2, Z2 p"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - exists(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![])))), - "forall X, Y, Z exists A, B, C p"); + for_all(x1y1z1(), exists(x2y2z2(), p()))), + "forall X1, Y1, Z1 exists X2, Y2, Z2 p"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![exists(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![]))]))), - "forall X, Y, Z exists A, B, C p"); + for_all(x1y1z1(), and(vec![exists(x2y2z2(), p())]))), + "forall X1, Y1, Z1 exists X2, Y2, Z2 p"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![exists(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![]))]))), - "forall X, Y, Z exists A, B, C p"); + for_all(x1y1z1(), or(vec![exists(x2y2z2(), p())]))), + "forall X1, Y1, Z1 exists X2, Y2, Z2 p"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![exists(vec![variable_declaration("A"), - variable_declaration("B"), variable_declaration("C")], predicate("p", vec![]))]))), - "forall X, Y, Z exists A, B, C p"); + for_all(x1y1z1(), if_and_only_if(vec![exists(x2y2z2(), p())]))), + "forall X1, Y1, Z1 exists X2, Y2, Z2 p"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - for_all(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![])))), - "forall X, Y, Z forall A, B, C p"); + for_all(x1y1z1(), for_all(x2y2z2(), p()))), + "forall X1, Y1, Z1 forall X2, Y2, Z2 p"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![]))]))), - "forall X, Y, Z forall A, B, C p"); + for_all(x1y1z1(), + and(vec![for_all(x2y2z2(), p())]))), + "forall X1, Y1, Z1 forall X2, Y2, Z2 p"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B"), - variable_declaration("C")], predicate("p", vec![]))]))), - "forall X, Y, Z forall A, B, C p"); + for_all(x1y1z1(), + or(vec![for_all(x2y2z2(), p())]))), + "forall X1, Y1, Z1 forall X2, Y2, Z2 p"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![for_all(vec![variable_declaration("A"), - variable_declaration("B"), variable_declaration("C")], - predicate("p", vec![]))]))), - "forall X, Y, Z forall A, B, C p"); + for_all(x1y1z1(), if_and_only_if(vec![for_all(x2y2z2(), p())]))), + "forall X1, Y1, Z1 forall X2, Y2, Z2 p"); // Quantified formula + and + assert_eq!(format(exists(xyz(), and(pqr()))), "exists X, Y, Z (p and q and r)"); + assert_eq!(format(exists(xyz(), and(pqr()))), "exists X, Y, Z (p and q and r)"); + assert_eq!(format(exists(xyz(), or(vec![and(pqr())]))), "exists X, Y, Z (p and q and r)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))), + exists(xyz(), if_and_only_if(vec![and(pqr())]))), "exists X, Y, Z (p and q and r)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "exists X, Y, Z (p and q and r)"); + and(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()), exists(x3y3z3(), r())])), + "exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "exists X, Y, Z (p and q and r)"); + and(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]), + and(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "exists X, Y, Z (p and q and r)"); + and(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]), + or(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r"); assert_eq!(format( - and(vec![ - exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])), - exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])), - "exists X, Y p and exists A, B q and exists C, D r"); + and(vec![if_and_only_if(vec![exists(x1y1z1(), p())]), + if_and_only_if(vec![exists(x2y2z2(), q())]), + if_and_only_if(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r"); + assert_eq!(format(for_all(xyz(), and(pqr()))), "forall X, Y, Z (p and q and r)"); + assert_eq!(format(for_all(xyz(), and(vec![and(pqr())]))), "forall X, Y, Z (p and q and r)"); + assert_eq!(format(for_all(xyz(), or(vec![and(pqr())]))), "forall X, Y, Z (p and q and r)"); assert_eq!(format( - and(vec![ - and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - and(vec![exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "exists X, Y p and exists A, B q and exists C, D r"); - assert_eq!(format( - and(vec![ - or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - or(vec![exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "exists X, Y p and exists A, B q and exists C, D r"); - assert_eq!(format( - and(vec![ - if_and_only_if(vec![exists(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![exists(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]), - if_and_only_if(vec![exists(vec![variable_declaration("C"), - variable_declaration("D")], predicate("r", vec![]))])])), - "exists X, Y p and exists A, B q and exists C, D r"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))), + for_all(xyz(), if_and_only_if(vec![and(pqr())]))), "forall X, Y, Z (p and q and r)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "forall X, Y, Z (p and q and r)"); + and(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()), for_all(x3y3z3(), r())])), + "forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "forall X, Y, Z (p and q and r)"); + and(vec![and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]), + and(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "forall X, Y, Z (p and q and r)"); + and(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]), + or(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r"); assert_eq!(format( - and(vec![ - for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])), - for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])), - "forall X, Y p and forall A, B q and forall C, D r"); - assert_eq!(format( - and(vec![ - and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - and(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "forall X, Y p and forall A, B q and forall C, D r"); - assert_eq!(format( - and(vec![ - or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - or(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "forall X, Y p and forall A, B q and forall C, D r"); - assert_eq!(format( - and(vec![ - if_and_only_if(vec![for_all(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![for_all(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]), - if_and_only_if(vec![for_all(vec![variable_declaration("C"), - variable_declaration("D")], predicate("r", vec![]))])])), - "forall X, Y p and forall A, B q and forall C, D r"); + and(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]), + if_and_only_if(vec![for_all(x2y2z2(), q())]), + if_and_only_if(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r"); // Quantified formula + or + assert_eq!(format(exists(xyz(), or(pqr()))), "exists X, Y, Z (p or q or r)"); + assert_eq!(format(exists(xyz(), and(vec![or(pqr())]))), "exists X, Y, Z (p or q or r)"); + assert_eq!(format(exists(xyz(), or(vec![or(pqr())]))), "exists X, Y, Z (p or q or r)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))), + exists(xyz(), if_and_only_if(vec![or(pqr())]))), "exists X, Y, Z (p or q or r)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "exists X, Y, Z (p or q or r)"); + or(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()), exists(x3y3z3(), r())])), + "exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "exists X, Y, Z (p or q or r)"); + or(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]), + and(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "exists X, Y, Z (p or q or r)"); + or(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]), + or(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r"); assert_eq!(format( - or(vec![ - exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])), - exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])), - "exists X, Y p or exists A, B q or exists C, D r"); - assert_eq!(format( - or(vec![ - and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - and(vec![exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "exists X, Y p or exists A, B q or exists C, D r"); - assert_eq!(format( - or(vec![ - or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - or(vec![exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "exists X, Y p or exists A, B q or exists C, D r"); - assert_eq!(format( - or(vec![ - if_and_only_if(vec![exists(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![exists(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]), - if_and_only_if(vec![exists(vec![variable_declaration("C"), - variable_declaration("D")], predicate("r", vec![]))])])), - "exists X, Y p or exists A, B q or exists C, D r"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))), + or(vec![if_and_only_if(vec![exists(x1y1z1(), p())]), + if_and_only_if(vec![exists(x2y2z2(), q())]), + if_and_only_if(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r"); + assert_eq!(format(for_all(xyz(), or(pqr()))), "forall X, Y, Z (p or q or r)"); + assert_eq!(format(for_all(xyz(), and(vec![or(pqr())]))), "forall X, Y, Z (p or q or r)"); + assert_eq!(format(for_all(xyz(), or(vec![or(pqr())]))), "forall X, Y, Z (p or q or r)"); + assert_eq!(format(for_all(xyz(), + if_and_only_if(vec![or(pqr())]))), "forall X, Y, Z (p or q or r)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "forall X, Y, Z (p or q or r)"); + or(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()), for_all(x3y3z3(), r())])), + "forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "forall X, Y, Z (p or q or r)"); + or(vec![and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]), + and(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![or(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), - "forall X, Y, Z (p or q or r)"); + or(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]), + or(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r"); assert_eq!(format( - or(vec![ - for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])), - for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])), - "forall X, Y p or forall A, B q or forall C, D r"); - assert_eq!(format( - or(vec![ - and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - and(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "forall X, Y p or forall A, B q or forall C, D r"); - assert_eq!(format( - or(vec![ - or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - or(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "forall X, Y p or forall A, B q or forall C, D r"); - assert_eq!(format( - or(vec![ - if_and_only_if(vec![for_all(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![for_all(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]), - if_and_only_if(vec![for_all(vec![variable_declaration("C"), - variable_declaration("D")], predicate("r", vec![]))])])), - "forall X, Y p or forall A, B q or forall C, D r"); + or(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]), + if_and_only_if(vec![for_all(x2y2z2(), q())]), + if_and_only_if(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r"); // Quantified formula + implies + assert_eq!(format(exists(xyz(), implies_right(p(), q()))), "exists X, Y, Z (p -> q)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![])))), + exists(xyz(), and(vec![implies_right(p(), q())]))), "exists X, Y, Z (p -> q)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![]))]))), + exists(xyz(), or(vec![implies_right(p(), q())]))), "exists X, Y, Z (p -> q)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![]))]))), + exists(xyz(), if_and_only_if(vec![implies_right(p(), q())]))), "exists X, Y, Z (p -> q)"); + assert_eq!(format(exists(xyz(), implies_left(p(), q()))), "exists X, Y, Z (q <- p)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![implies(ImplicationDirection::LeftToRight, - predicate("p", vec![]), predicate("q", vec![]))]))), - "exists X, Y, Z (p -> q)"); - assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![])))), + exists(xyz(), and(vec![implies_left(p(), q())]))), "exists X, Y, Z (q <- p)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![]))]))), + exists(xyz(), or(vec![implies_left(p(), q())]))), "exists X, Y, Z (q <- p)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![]))]))), + exists(xyz(), if_and_only_if(vec![implies_left(p(), q())]))), "exists X, Y, Z (q <- p)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![implies(ImplicationDirection::RightToLeft, - predicate("p", vec![]), predicate("q", vec![]))]))), - "exists X, Y, Z (q <- p)"); + implies_right(exists(x1y1z1(), p()), exists(x2y2z2(), q()))), + "exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])))), - "exists X, Y p -> exists A, B q"); + implies_right(and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]))), + "exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]))), - "exists X, Y p -> exists A, B q"); + implies_right(or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]))), + "exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]))), - "exists X, Y p -> exists A, B q"); + implies_right(if_and_only_if(vec![exists(x1y1z1(), p())]), + if_and_only_if(vec![exists(x2y2z2(), q())]))), + "exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - if_and_only_if(vec![exists(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![exists(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]))), - "exists X, Y p -> exists A, B q"); + implies_left(exists(x1y1z1(), p()), exists(x2y2z2(), q()))), + "exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])))), - "exists A, B q <- exists X, Y p"); + implies_left(and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]))), + "exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]))), - "exists A, B q <- exists X, Y p"); + implies_left(or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]))), + "exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]))), - "exists A, B q <- exists X, Y p"); + implies_left(if_and_only_if(vec![exists(x1y1z1(), p())]), + if_and_only_if(vec![exists(x2y2z2(), q())]))), + "exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p"); + assert_eq!(format(for_all(xyz(), implies_right(p(), q()))), "forall X, Y, Z (p -> q)"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - if_and_only_if(vec![exists(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![exists(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]))), - "exists A, B q <- exists X, Y p"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![])))), + for_all(xyz(), and(vec![implies_right(p(), q())]))), "forall X, Y, Z (p -> q)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![]))]))), + for_all(xyz(), or(vec![implies_right(p(), q())]))), "forall X, Y, Z (p -> q)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![implies(ImplicationDirection::LeftToRight, predicate("p", vec![]), - predicate("q", vec![]))]))), + for_all(xyz(), if_and_only_if(vec![implies_right(p(), q())]))), "forall X, Y, Z (p -> q)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![implies(ImplicationDirection::LeftToRight, - predicate("p", vec![]), predicate("q", vec![]))]))), - "forall X, Y, Z (p -> q)"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![])))), + for_all(xyz(), implies_left(p(), q()))), "forall X, Y, Z (q <- p)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![]))]))), + for_all(xyz(), and(vec![implies_left(p(), q())]))), "forall X, Y, Z (q <- p)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![implies(ImplicationDirection::RightToLeft, predicate("p", vec![]), - predicate("q", vec![]))]))), + for_all(xyz(), or(vec![implies_left(p(), q())]))), "forall X, Y, Z (q <- p)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![implies(ImplicationDirection::RightToLeft, - predicate("p", vec![]), predicate("q", vec![]))]))), + for_all(xyz(), if_and_only_if(vec![implies_left(p(), q())]))), "forall X, Y, Z (q <- p)"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])))), - "forall X, Y p -> forall A, B q"); + implies_right(for_all(x1y1z1(), p()), for_all(x2y2z2(), q()))), + "forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]))), - "forall X, Y p -> forall A, B q"); + implies_right(and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]))), + "forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]))), - "forall X, Y p -> forall A, B q"); + implies_right(or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]))), + "forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q"); assert_eq!(format( - implies(ImplicationDirection::LeftToRight, - if_and_only_if(vec![for_all(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![for_all(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]))), - "forall X, Y p -> forall A, B q"); + implies_right(if_and_only_if(vec![for_all(x1y1z1(), p())]), + if_and_only_if(vec![for_all(x2y2z2(), q())]))), + "forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])))), - "forall A, B q <- forall X, Y p"); + implies_left(for_all(x1y1z1(), p()), for_all(x2y2z2(), q()))), + "forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]))), - "forall A, B q <- forall X, Y p"); + implies_left(and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]))), + "forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]))), - "forall A, B q <- forall X, Y p"); + implies_left(or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]))), + "forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p"); assert_eq!(format( - implies(ImplicationDirection::RightToLeft, - if_and_only_if(vec![for_all(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![for_all(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]))), - "forall A, B q <- forall X, Y p"); + implies_left(if_and_only_if(vec![for_all(x1y1z1(), p())]), + if_and_only_if(vec![for_all(x2y2z2(), q())]))), + "forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p"); // Quantified formula + if and only if + assert_eq!(format(exists(xyz(), if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])]))), + exists(xyz(), and(vec![if_and_only_if(pqr())]))), "exists X, Y, Z (p <-> q <-> r)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), + exists(xyz(), or(vec![if_and_only_if(pqr())]))), "exists X, Y, Z (p <-> q <-> r)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), + exists(xyz(), if_and_only_if(vec![if_and_only_if(pqr())]))), "exists X, Y, Z (p <-> q <-> r)"); assert_eq!(format( - exists(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![if_and_only_if(vec![predicate("p", vec![]), - predicate("q", vec![]), predicate("r", vec![])])]))), - "exists X, Y, Z (p <-> q <-> r)"); + if_and_only_if(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()), + exists(x3y3z3(), r())])), + "exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r"); assert_eq!(format( - if_and_only_if(vec![ - exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])), - exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])), - "exists X, Y p <-> exists A, B q <-> exists C, D r"); + if_and_only_if(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]), + and(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r"); assert_eq!(format( - if_and_only_if(vec![ - and(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - and(vec![exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "exists X, Y p <-> exists A, B q <-> exists C, D r"); + if_and_only_if(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]), + or(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r"); assert_eq!(format( - if_and_only_if(vec![ - or(vec![exists(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![exists(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - or(vec![exists(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "exists X, Y p <-> exists A, B q <-> exists C, D r"); + if_and_only_if(vec![if_and_only_if(vec![exists(x1y1z1(), p())]), + if_and_only_if(vec![exists(x2y2z2(), q())]), + if_and_only_if(vec![exists(x3y3z3(), r())])])), + "exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r"); assert_eq!(format( - if_and_only_if(vec![ - if_and_only_if(vec![exists(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![exists(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]), - if_and_only_if(vec![exists(vec![variable_declaration("C"), - variable_declaration("D")], predicate("r", vec![]))])])), - "exists X, Y p <-> exists A, B q <-> exists C, D r"); - assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])]))), + for_all(xyz(), if_and_only_if(pqr()))), "forall X, Y, Z (p <-> q <-> r)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - and(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), + for_all(xyz(), and(vec![if_and_only_if(pqr())]))), "forall X, Y, Z (p <-> q <-> r)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - or(vec![if_and_only_if(vec![predicate("p", vec![]), predicate("q", vec![]), - predicate("r", vec![])])]))), + for_all(xyz(), or(vec![if_and_only_if(pqr())]))), "forall X, Y, Z (p <-> q <-> r)"); assert_eq!(format( - for_all(vec![variable_declaration("X"), variable_declaration("Y"), - variable_declaration("Z")], - if_and_only_if(vec![if_and_only_if(vec![predicate("p", vec![]), - predicate("q", vec![]), predicate("r", vec![])])]))), + for_all(xyz(), if_and_only_if(vec![if_and_only_if(pqr())]))), "forall X, Y, Z (p <-> q <-> r)"); assert_eq!(format( - if_and_only_if(vec![ - for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![])), - for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![])), - for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])), - "forall X, Y p <-> forall A, B q <-> forall C, D r"); + if_and_only_if(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()), + for_all(x3y3z3(), r())])), + "forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r"); assert_eq!(format( - if_and_only_if(vec![ - and(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - and(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - and(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "forall X, Y p <-> forall A, B q <-> forall C, D r"); + if_and_only_if(vec![and(vec![for_all(x1y1z1(), p())]), + and(vec![for_all(x2y2z2(), q())]), and(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r"); assert_eq!(format( - if_and_only_if(vec![ - or(vec![for_all(vec![variable_declaration("X"), variable_declaration("Y")], - predicate("p", vec![]))]), - or(vec![for_all(vec![variable_declaration("A"), variable_declaration("B")], - predicate("q", vec![]))]), - or(vec![for_all(vec![variable_declaration("C"), variable_declaration("D")], - predicate("r", vec![]))])])), - "forall X, Y p <-> forall A, B q <-> forall C, D r"); + if_and_only_if(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]), + or(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r"); assert_eq!(format( - if_and_only_if(vec![ - if_and_only_if(vec![for_all(vec![variable_declaration("X"), - variable_declaration("Y")], predicate("p", vec![]))]), - if_and_only_if(vec![for_all(vec![variable_declaration("A"), - variable_declaration("B")], predicate("q", vec![]))]), - if_and_only_if(vec![for_all(vec![variable_declaration("C"), - variable_declaration("D")], predicate("r", vec![]))])])), - "forall X, Y p <-> forall A, B q <-> forall C, D r"); + if_and_only_if(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]), + if_and_only_if(vec![for_all(x2y2z2(), q())]), + if_and_only_if(vec![for_all(x3y3z3(), r())])])), + "forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r"); + } + + #[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"); + */ } }