2020-05-11 03:58:30 +02:00
|
|
|
pub(crate) fn existential_closure(open_formula: foliage::OpenFormula) -> foliage::Formula
|
2020-05-11 03:41:33 +02:00
|
|
|
{
|
2020-05-11 03:58:30 +02:00
|
|
|
match open_formula.free_variable_declarations.is_empty()
|
2020-05-11 03:41:33 +02:00
|
|
|
{
|
2020-05-11 03:58:30 +02:00
|
|
|
true => open_formula.formula,
|
|
|
|
false => foliage::Formula::exists(open_formula.free_variable_declarations,
|
|
|
|
Box::new(open_formula.formula)),
|
2020-05-11 03:41:33 +02:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2020-05-11 03:58:30 +02:00
|
|
|
pub(crate) fn universal_closure(open_formula: foliage::OpenFormula) -> foliage::Formula
|
2020-05-11 03:41:33 +02:00
|
|
|
{
|
2020-05-11 03:58:30 +02:00
|
|
|
match open_formula.free_variable_declarations.is_empty()
|
2020-05-11 03:41:33 +02:00
|
|
|
{
|
2020-05-11 03:58:30 +02:00
|
|
|
true => open_formula.formula,
|
|
|
|
false => foliage::Formula::for_all(open_formula.free_variable_declarations,
|
|
|
|
Box::new(open_formula.formula)),
|
2020-05-11 03:41:33 +02:00
|
|
|
}
|
|
|
|
}
|