Support empty n-aries

This commit is contained in:
Patrick Lühne 2020-04-08 12:09:27 +02:00
parent 51cbdb313f
commit 9a8013f1cb
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 57 additions and 45 deletions

View File

@ -486,8 +486,6 @@ impl Formula
{
pub fn and(arguments: Formulas) -> Self
{
assert!(!arguments.is_empty());
Self::And(arguments)
}
@ -537,8 +535,6 @@ impl Formula
pub fn if_and_only_if(arguments: Formulas) -> Self
{
assert!(!arguments.is_empty());
Self::IfAndOnlyIf(arguments)
}
@ -570,8 +566,6 @@ impl Formula
pub fn or(arguments: Formulas) -> Self
{
assert!(!arguments.is_empty());
Self::Or(arguments)
}

View File

@ -177,42 +177,52 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
display_formula(argument, Some(self.formula), ChildPosition::Any))?,
crate::Formula::And(arguments) =>
{
let mut separator = "";
assert!(!arguments.is_empty());
let (parent_formula, position) = match arguments.len()
if arguments.is_empty()
{
0 | 1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
for argument in arguments
write!(format, "true")?;
}
else
{
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
let (parent_formula, position) = match arguments.len()
{
1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
separator = " and "
let mut separator = "";
for argument in arguments
{
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " and "
}
}
},
crate::Formula::Or(arguments) =>
{
let mut separator = "";
assert!(!arguments.is_empty());
let (parent_formula, position) = match arguments.len()
if arguments.is_empty()
{
0 | 1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
for argument in arguments
write!(format, "false")?;
}
else
{
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
let (parent_formula, position) = match arguments.len()
{
1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
separator = " or "
let mut separator = "";
for argument in arguments
{
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " or "
}
}
},
crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
@ -248,22 +258,27 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
},
crate::Formula::IfAndOnlyIf(arguments) =>
{
let mut separator = "";
assert!(!arguments.is_empty());
let (parent_formula, position) = match arguments.len()
if arguments.is_empty()
{
0 | 1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
for argument in arguments
write!(format, "true")?;
}
else
{
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
let (parent_formula, position) = match arguments.len()
{
1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
separator = " <-> "
let mut separator = "";
for argument in arguments
{
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " <-> "
}
}
},
crate::Formula::Compare(
@ -666,6 +681,7 @@ mod tests
#[test]
fn format_and()
{
assert!(and(vec![]), "true");
assert!(and(vec![p()]), "p");
assert!(and(pqr()), "p and q and r");
}
@ -673,6 +689,7 @@ mod tests
#[test]
fn format_or()
{
assert!(or(vec![]), "false");
assert!(or(vec![p()]), "p");
assert!(or(pqr()), "p or q or r");
}
@ -687,6 +704,7 @@ mod tests
#[test]
fn format_if_and_only_if()
{
assert!(if_and_only_if(vec![]), "true");
assert!(if_and_only_if(vec![p()]), "p");
assert!(if_and_only_if(vec![p(), q()]), "p <-> q");
assert!(if_and_only_if(pqr()), "p <-> q <-> r");