Test negation
This commit is contained in:
parent
121c858bff
commit
cc3265fc72
GPG Key ID:
05F3611E97A70ABF
|
|
@ -16,7 +16,8 @@ fn requires_parentheses<'formula>(formula: &'formula crate::Formula,
|
||||||
| Formula::ForAll(_)
|
| Formula::ForAll(_)
|
||||||
=> false,
|
=> false,
|
||||||
Formula::And(formulas)
|
Formula::And(formulas)
|
||||||
| Formula::Or(formulas) if formulas.len() <= 1
|
| Formula::Or(formulas)
|
||||||
|
| Formula::IfAndOnlyIf(formulas) if formulas.len() <= 1
|
||||||
=> false,
|
=> false,
|
||||||
Formula::And(_) => match *parent_formula
|
Formula::And(_) => match *parent_formula
|
||||||
{
|
{
|
||||||
|
|
@ -238,11 +239,19 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
||||||
{
|
{
|
||||||
let mut separator = "";
|
let mut separator = "";
|
||||||
|
|
||||||
|
assert!(!arguments.is_empty());
|
||||||
|
|
||||||
|
let parent_formula = match arguments.len()
|
||||||
|
{
|
||||||
|
0 | 1 => self.parent_formula,
|
||||||
|
_ => Some(self.formula),
|
||||||
|
};
|
||||||
|
|
||||||
for argument in arguments
|
for argument in arguments
|
||||||
{
|
{
|
||||||
write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
|
write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
|
||||||
|
|
||||||
separator = " <-> ";
|
separator = " <-> "
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
crate::Formula::Compare(
|
crate::Formula::Compare(
|
||||||
|
|
@ -815,39 +824,317 @@ mod tests
|
||||||
#[test]
|
#[test]
|
||||||
fn format_combination_not_and_lower()
|
fn format_combination_not_and_lower()
|
||||||
{
|
{
|
||||||
|
// Not + not
|
||||||
assert_eq!(format(not(not(predicate("p", vec![])))), "not not p");
|
assert_eq!(format(not(not(predicate("p", vec![])))), "not not p");
|
||||||
|
|
||||||
|
// Not + quantified formulas
|
||||||
assert_eq!(format(
|
assert_eq!(format(
|
||||||
not(exists(vec![variable_declaration("X"), variable_declaration("Y"),
|
not(exists(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||||
variable_declaration("Z")], predicate("p", vec![])))),
|
variable_declaration("Z")], predicate("p", vec![])))),
|
||||||
"not exists X, Y, Z p");
|
"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(
|
assert_eq!(format(
|
||||||
exists(vec![variable_declaration("X"), variable_declaration("Y"),
|
exists(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||||
variable_declaration("Z")], not(predicate("p", vec![])))),
|
variable_declaration("Z")], not(predicate("p", vec![])))),
|
||||||
"exists X, Y, Z not p");
|
"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(
|
assert_eq!(format(
|
||||||
not(for_all(vec![variable_declaration("X"), variable_declaration("Y"),
|
not(for_all(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||||
variable_declaration("Z")], predicate("p", vec![])))),
|
variable_declaration("Z")], predicate("p", vec![])))),
|
||||||
"not forall X, Y, Z p");
|
"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(
|
assert_eq!(format(
|
||||||
for_all(vec![variable_declaration("X"), variable_declaration("Y"),
|
for_all(vec![variable_declaration("X"), variable_declaration("Y"),
|
||||||
variable_declaration("Z")], not(predicate("p", vec![])))),
|
variable_declaration("Z")], not(predicate("p", vec![])))),
|
||||||
"forall X, Y, Z not p");
|
"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");
|
||||||
|
|
||||||
|
// Not + and
|
||||||
assert_eq!(format(
|
assert_eq!(format(
|
||||||
not(and(vec![predicate("p", vec![])]))),
|
not(and(vec![predicate("p", vec![])]))),
|
||||||
"not p");
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(and(vec![and(vec![predicate("p", vec![])])]))),
|
||||||
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(or(vec![and(vec![predicate("p", vec![])])]))),
|
||||||
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(if_and_only_if(vec![and(vec![predicate("p", vec![])])]))),
|
||||||
|
"not p");
|
||||||
assert_eq!(format(
|
assert_eq!(format(
|
||||||
not(and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
|
not(and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
|
||||||
"not (p and q and r)");
|
"not (p and q and r)");
|
||||||
|
|
||||||
assert_eq!(format(
|
assert_eq!(format(
|
||||||
or(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
|
not(and(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
|
||||||
"p or q or r");
|
predicate("r", vec![])])]))),
|
||||||
|
"not (p and q and r)");
|
||||||
assert_eq!(format(
|
assert_eq!(format(
|
||||||
and(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
|
not(or(vec![and(vec![predicate("p", vec![]), predicate("q", vec![]),
|
||||||
"p and (q or r)");
|
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![]))])),
|
||||||
|
"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![]))])])),
|
||||||
|
"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![]))])])),
|
||||||
|
"not p and not q and not r");
|
||||||
|
|
||||||
|
// Not + or
|
||||||
|
assert_eq!(format(
|
||||||
|
not(or(vec![predicate("p", vec![])]))),
|
||||||
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(and(vec![or(vec![predicate("p", vec![])])]))),
|
||||||
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(or(vec![or(vec![predicate("p", vec![])])]))),
|
||||||
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(if_and_only_if(vec![or(vec![predicate("p", vec![])])]))),
|
||||||
|
"not p");
|
||||||
|
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![]))])),
|
||||||
|
"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![]))])])),
|
||||||
|
"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![]))])])),
|
||||||
|
"not p or not q or not r");
|
||||||
|
|
||||||
|
// Not + implies
|
||||||
|
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![])))),
|
||||||
|
"not p -> not q");
|
||||||
|
assert_eq!(format(
|
||||||
|
implies(ImplicationDirection::LeftToRight, and(vec![not(predicate("p", vec![]))]),
|
||||||
|
and(vec![not(predicate("q", vec![]))]))),
|
||||||
|
"not p -> not q");
|
||||||
|
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![])))),
|
||||||
|
"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![]))]))),
|
||||||
|
"not q <- not p");
|
||||||
|
|
||||||
|
// Not + if and only if
|
||||||
|
assert_eq!(format(
|
||||||
|
not(if_and_only_if(vec![predicate("p", vec![])]))),
|
||||||
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(and(vec![if_and_only_if(vec![predicate("p", vec![])])]))),
|
||||||
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(or(vec![if_and_only_if(vec![predicate("p", vec![])])]))),
|
||||||
|
"not p");
|
||||||
|
assert_eq!(format(
|
||||||
|
not(if_and_only_if(vec![if_and_only_if(vec![predicate("p", vec![])])]))),
|
||||||
|
"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![]))])),
|
||||||
|
"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![]))])])),
|
||||||
|
"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![]))])])),
|
||||||
|
"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![]))])])),
|
||||||
|
"not p <-> not q <-> not r");
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue