Support quantified expressions with 0 parameters

This commit is contained in:
Patrick Lühne 2020-04-08 12:48:21 +02:00
parent 9a8013f1cb
commit 3b7394a43e
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 101 additions and 28 deletions

View File

@ -501,8 +501,6 @@ impl Formula
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{ {
assert!(!parameters.is_empty());
Self::Exists(Exists::new(parameters, argument)) Self::Exists(Exists::new(parameters, argument))
} }
@ -518,8 +516,6 @@ impl Formula
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{ {
assert!(!parameters.is_empty());
Self::ForAll(ForAll::new(parameters, argument)) Self::ForAll(ForAll::new(parameters, argument))
} }

View File

@ -139,39 +139,51 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{ {
crate::Formula::Exists(exists) => crate::Formula::Exists(exists) =>
{ {
assert!(!exists.parameters.is_empty()); if exists.parameters.is_empty()
write!(format, "exists")?;
let mut separator = " ";
for parameter in exists.parameters.iter()
{ {
write!(format, "{}{:?}", separator, parameter)?; write!(format, "{:?}", display_formula(&exists.argument, self.parent_formula,
self.position))?;
separator = ", "
} }
else
{
write!(format, "exists")?;
write!(format, " {:?}", let mut separator = " ";
display_formula(&exists.argument, Some(self.formula), ChildPosition::Any))?;
for parameter in exists.parameters.iter()
{
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula),
ChildPosition::Any))?;
}
}, },
crate::Formula::ForAll(for_all) => crate::Formula::ForAll(for_all) =>
{ {
assert!(!for_all.parameters.is_empty()); if for_all.parameters.is_empty()
write!(format, "forall")?;
let mut separator = " ";
for parameter in for_all.parameters.iter()
{ {
write!(format, "{}{:?}", separator, parameter)?; write!(format, "{:?}", display_formula(&for_all.argument, self.parent_formula,
self.position))?;
separator = ", "
} }
else
{
write!(format, "forall")?;
write!(format, " {:?}", let mut separator = " ";
display_formula(&for_all.argument, Some(self.formula), ChildPosition::Any))?;
for parameter in for_all.parameters.iter()
{
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula),
ChildPosition::Any))?;
}
}, },
crate::Formula::Not(argument) => write!(format, "not {:?}", crate::Formula::Not(argument) => write!(format, "not {:?}",
display_formula(argument, Some(self.formula), ChildPosition::Any))?, display_formula(argument, Some(self.formula), ChildPosition::Any))?,
@ -386,6 +398,12 @@ mod tests
let $intermediate = |f: Box<Formula>| f; let $intermediate = |f: Box<Formula>| f;
assert!($formula, $output); assert!($formula, $output);
let $intermediate = |f: Box<Formula>| exists(vec![], f);
assert!($formula, $output);
let $intermediate = |f: Box<Formula>| for_all(vec![], f);
assert!($formula, $output);
let $intermediate = |f: Box<Formula>| and(vec![f]); let $intermediate = |f: Box<Formula>| and(vec![f]);
assert!($formula, $output); assert!($formula, $output);
@ -661,6 +679,7 @@ mod tests
#[test] #[test]
fn format_exists() fn format_exists()
{ {
assert!(exists(vec![], p()), "p");
assert!(exists(vec![x()], p()), "exists X p"); assert!(exists(vec![x()], p()), "exists X p");
assert!(exists(xyz(), p()), "exists X, Y, Z p"); assert!(exists(xyz(), p()), "exists X, Y, Z p");
} }
@ -668,6 +687,7 @@ mod tests
#[test] #[test]
fn format_for_all() fn format_for_all()
{ {
assert!(for_all(vec![], p()), "p");
assert!(for_all(vec![x()], p()), "forall X p"); assert!(for_all(vec![x()], p()), "forall X p");
assert!(for_all(xyz(), p()), "forall X, Y, Z p"); assert!(for_all(xyz(), p()), "forall X, Y, Z p");
} }
@ -718,10 +738,14 @@ mod tests
assert!(not(false_()), "not false"); assert!(not(false_()), "not false");
// Quantified formula + Boolean // Quantified formula + Boolean
assert!(exists(vec![], true_()), "true");
assert!(exists(vec![], false_()), "false");
assert!(exists(vec![x()], true_()), "exists X true"); assert!(exists(vec![x()], true_()), "exists X true");
assert!(exists(vec![x()], false_()), "exists X false"); assert!(exists(vec![x()], false_()), "exists X false");
assert!(exists(xyz(), true_()), "exists X, Y, Z true"); assert!(exists(xyz(), true_()), "exists X, Y, Z true");
assert!(exists(xyz(), false_()), "exists X, Y, Z false"); assert!(exists(xyz(), false_()), "exists X, Y, Z false");
assert!(for_all(vec![], true_()), "true");
assert!(for_all(vec![], false_()), "false");
assert!(for_all(vec![x()], true_()), "forall X true"); assert!(for_all(vec![x()], true_()), "forall X true");
assert!(for_all(vec![x()], false_()), "forall X false"); assert!(for_all(vec![x()], false_()), "forall X false");
assert!(for_all(xyz(), true_()), "forall X, Y, Z true"); assert!(for_all(xyz(), true_()), "forall X, Y, Z true");
@ -769,6 +793,18 @@ mod tests
assert!(not(not_equal(term_1(), term_2())), "not (a + b) * c != |d - e|"); assert!(not(not_equal(term_1(), term_2())), "not (a + b) * c != |d - e|");
// Quantified formula + compare // Quantified formula + compare
assert!(exists(vec![], greater(term_1(), term_2())), "(a + b) * c > |d - e|");
assert!(exists(vec![], less(term_1(), term_2())), "(a + b) * c < |d - e|");
assert!(exists(vec![], less_or_equal(term_1(), term_2())), "(a + b) * c <= |d - e|");
assert!(exists(vec![], greater_or_equal(term_1(), term_2())), "(a + b) * c >= |d - e|");
assert!(exists(vec![], equal(term_1(), term_2())), "(a + b) * c = |d - e|");
assert!(exists(vec![], not_equal(term_1(), term_2())), "(a + b) * c != |d - e|");
assert!(for_all(vec![], greater(term_1(), term_2())), "(a + b) * c > |d - e|");
assert!(for_all(vec![], less(term_1(), term_2())), "(a + b) * c < |d - e|");
assert!(for_all(vec![], less_or_equal(term_1(), term_2())), "(a + b) * c <= |d - e|");
assert!(for_all(vec![], greater_or_equal(term_1(), term_2())), "(a + b) * c >= |d - e|");
assert!(for_all(vec![], equal(term_1(), term_2())), "(a + b) * c = |d - e|");
assert!(for_all(vec![], not_equal(term_1(), term_2())), "(a + b) * c != |d - e|");
assert!(exists(vec![x()], greater(term_1(), term_2())), "exists X (a + b) * c > |d - e|"); assert!(exists(vec![x()], greater(term_1(), term_2())), "exists X (a + b) * c > |d - e|");
assert!(exists(vec![x()], less(term_1(), term_2())), "exists X (a + b) * c < |d - e|"); assert!(exists(vec![x()], less(term_1(), term_2())), "exists X (a + b) * c < |d - e|");
assert!(exists(vec![x()], less_or_equal(term_1(), term_2())), assert!(exists(vec![x()], less_or_equal(term_1(), term_2())),
@ -787,6 +823,25 @@ mod tests
assert!(for_all(vec![x()], equal(term_1(), term_2())), "forall X (a + b) * c = |d - e|"); assert!(for_all(vec![x()], equal(term_1(), term_2())), "forall X (a + b) * c = |d - e|");
assert!(for_all(vec![x()], not_equal(term_1(), term_2())), assert!(for_all(vec![x()], not_equal(term_1(), term_2())),
"forall X (a + b) * c != |d - e|"); "forall X (a + b) * c != |d - e|");
assert!(exists(xyz(), greater(term_1(), term_2())), "exists X, Y, Z (a + b) * c > |d - e|");
assert!(exists(xyz(), less(term_1(), term_2())), "exists X, Y, Z (a + b) * c < |d - e|");
assert!(exists(xyz(), less_or_equal(term_1(), term_2())),
"exists X, Y, Z (a + b) * c <= |d - e|");
assert!(exists(xyz(), greater_or_equal(term_1(), term_2())),
"exists X, Y, Z (a + b) * c >= |d - e|");
assert!(exists(xyz(), equal(term_1(), term_2())), "exists X, Y, Z (a + b) * c = |d - e|");
assert!(exists(xyz(), not_equal(term_1(), term_2())),
"exists X, Y, Z (a + b) * c != |d - e|");
assert!(for_all(xyz(), greater(term_1(), term_2())),
"forall X, Y, Z (a + b) * c > |d - e|");
assert!(for_all(xyz(), less(term_1(), term_2())), "forall X, Y, Z (a + b) * c < |d - e|");
assert!(for_all(xyz(), less_or_equal(term_1(), term_2())),
"forall X, Y, Z (a + b) * c <= |d - e|");
assert!(for_all(xyz(), greater_or_equal(term_1(), term_2())),
"forall X, Y, Z (a + b) * c >= |d - e|");
assert!(for_all(xyz(), equal(term_1(), term_2())), "forall X, Y, Z (a + b) * c = |d - e|");
assert!(for_all(xyz(), not_equal(term_1(), term_2())),
"forall X, Y, Z (a + b) * c != |d - e|");
// And + compare // And + compare
assert!(and(vec![greater(term_1(), term_2()), greater(term_3(), term_4()), assert!(and(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
@ -884,6 +939,8 @@ mod tests
assert!(not(not(p())), "not not p"); assert!(not(not(p())), "not not p");
// Quantified formulas + not // Quantified formulas + not
assert_all!(i, exists(vec![x()], i(not(p()))), "exists X not p");
assert_all!(i, for_all(vec![x()], i(not(p()))), "forall X not p");
assert_all!(i, exists(xyz(), i(not(p()))), "exists X, Y, Z not p"); assert_all!(i, exists(xyz(), i(not(p()))), "exists X, Y, Z not p");
assert_all!(i, for_all(xyz(), i(not(p()))), "forall X, Y, Z not p"); assert_all!(i, for_all(xyz(), i(not(p()))), "forall X, Y, Z not p");
@ -914,6 +971,10 @@ mod tests
assert_all!(i, not(for_all(xyz(), i(p()))), "not forall X, Y, Z p"); assert_all!(i, not(for_all(xyz(), i(p()))), "not forall X, Y, Z p");
// Quantified formula + quantified formula // Quantified formula + quantified formula
assert_all!(i, exists(vec![x()], i(exists(vec![y()], p()))), "exists X exists Y p");
assert_all!(i, exists(vec![x()], i(for_all(vec![y()], p()))), "exists X forall Y p");
assert_all!(i, for_all(vec![x()], i(exists(vec![y()], p()))), "forall X exists Y p");
assert_all!(i, for_all(vec![x()], i(for_all(vec![y()], p()))), "forall X forall Y p");
assert_all!(i, exists(x1y1z1(), i(exists(x2y2z2(), p()))), assert_all!(i, exists(x1y1z1(), i(exists(x2y2z2(), p()))),
"exists X1, Y1, Z1 exists X2, Y2, Z2 p"); "exists X1, Y1, Z1 exists X2, Y2, Z2 p");
assert_all!(i, exists(x1y1z1(), i(for_all(x2y2z2(), p()))), assert_all!(i, exists(x1y1z1(), i(for_all(x2y2z2(), p()))),
@ -972,6 +1033,10 @@ mod tests
assert_all!(i, not(i(and(pqr()))), "not (p and q and r)"); assert_all!(i, not(i(and(pqr()))), "not (p and q and r)");
// Quantified formula + and // Quantified formula + and
assert_all!(i, exists(vec![x()], i(and(vec![p()]))), "exists X p");
assert_all!(i, for_all(vec![x()], i(and(vec![p()]))), "forall X p");
assert_all!(i, exists(vec![x()], i(and(pqr()))), "exists X (p and q and r)");
assert_all!(i, for_all(vec![x()], i(and(pqr()))), "forall X (p and q and r)");
assert_all!(i, exists(xyz(), i(and(vec![p()]))), "exists X, Y, Z p"); assert_all!(i, exists(xyz(), i(and(vec![p()]))), "exists X, Y, Z p");
assert_all!(i, for_all(xyz(), i(and(vec![p()]))), "forall X, Y, Z p"); assert_all!(i, for_all(xyz(), i(and(vec![p()]))), "forall X, Y, Z p");
assert_all!(i, exists(xyz(), i(and(pqr()))), "exists X, Y, Z (p and q and r)"); assert_all!(i, exists(xyz(), i(and(pqr()))), "exists X, Y, Z (p and q and r)");
@ -1019,6 +1084,10 @@ mod tests
assert_all!(i, not(i(or(pqr()))), "not (p or q or r)"); assert_all!(i, not(i(or(pqr()))), "not (p or q or r)");
// Quantified formula + or // Quantified formula + or
assert_all!(i, exists(vec![x()], i(or(vec![p()]))), "exists X p");
assert_all!(i, for_all(vec![x()], i(or(vec![p()]))), "forall X p");
assert_all!(i, exists(vec![x()], i(or(pqr()))), "exists X (p or q or r)");
assert_all!(i, for_all(vec![x()], i(or(pqr()))), "forall X (p or q or r)");
assert_all!(i, exists(xyz(), i(or(vec![p()]))), "exists X, Y, Z p"); assert_all!(i, exists(xyz(), i(or(vec![p()]))), "exists X, Y, Z p");
assert_all!(i, for_all(xyz(), i(or(vec![p()]))), "forall X, Y, Z p"); assert_all!(i, for_all(xyz(), i(or(vec![p()]))), "forall X, Y, Z p");
assert_all!(i, exists(xyz(), i(or(pqr()))), "exists X, Y, Z (p or q or r)"); assert_all!(i, exists(xyz(), i(or(pqr()))), "exists X, Y, Z (p or q or r)");
@ -1065,6 +1134,10 @@ mod tests
assert_all!(i, not(i(implies_left(p(), q()))), "not (q <- p)"); assert_all!(i, not(i(implies_left(p(), q()))), "not (q <- p)");
// Quantified formula + implies // Quantified formula + implies
assert_all!(i, exists(vec![x()], i(implies_right(p(), q()))), "exists X (p -> q)");
assert_all!(i, exists(vec![x()], i(implies_left(p(), q()))), "exists X (q <- p)");
assert_all!(i, for_all(vec![x()], i(implies_right(p(), q()))), "forall X (p -> q)");
assert_all!(i, for_all(vec![x()], i(implies_left(p(), q()))), "forall X (q <- p)");
assert_all!(i, exists(xyz(), i(implies_right(p(), q()))), "exists X, Y, Z (p -> q)"); assert_all!(i, exists(xyz(), i(implies_right(p(), q()))), "exists X, Y, Z (p -> q)");
assert_all!(i, exists(xyz(), i(implies_left(p(), q()))), "exists X, Y, Z (q <- p)"); assert_all!(i, exists(xyz(), i(implies_left(p(), q()))), "exists X, Y, Z (q <- p)");
assert_all!(i, for_all(xyz(), i(implies_right(p(), q()))), "forall X, Y, Z (p -> q)"); assert_all!(i, for_all(xyz(), i(implies_right(p(), q()))), "forall X, Y, Z (p -> q)");
@ -1119,6 +1192,10 @@ mod tests
assert_all!(i, not(i(if_and_only_if(pqr()))), "not (p <-> q <-> r)"); assert_all!(i, not(i(if_and_only_if(pqr()))), "not (p <-> q <-> r)");
// Quantified formula + if and only if // Quantified formula + if and only if
assert_all!(i, exists(vec![x()], i(if_and_only_if(vec![p()]))), "exists X p");
assert_all!(i, for_all(vec![x()], i(if_and_only_if(vec![p()]))), "forall X p");
assert_all!(i, exists(vec![x()], i(if_and_only_if(pqr()))), "exists X (p <-> q <-> r)");
assert_all!(i, for_all(vec![x()], i(if_and_only_if(pqr()))), "forall X (p <-> q <-> r)");
assert_all!(i, exists(xyz(), i(if_and_only_if(vec![p()]))), "exists X, Y, Z p"); assert_all!(i, exists(xyz(), i(if_and_only_if(vec![p()]))), "exists X, Y, Z p");
assert_all!(i, for_all(xyz(), i(if_and_only_if(vec![p()]))), "forall X, Y, Z p"); assert_all!(i, for_all(xyz(), i(if_and_only_if(vec![p()]))), "forall X, Y, Z p");
assert_all!(i, exists(xyz(), i(if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)"); assert_all!(i, exists(xyz(), i(if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)");