patrick
/
foliage-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
foliage-rs/src/format/formulas.rs

913 lines
29 KiB
Rust
Raw Blame History

use super::*;
impl super::Precedence for crate::Formula
{
fn precedence_level(&self) -> i32
{
match &self
{
Self::Predicate(_)
| Self::Boolean(_)
| Self::Compare(_)
=> 0,
/*Self::And(formulas)
| Self::Or(formulas) if formulas.len() == 1
=> 0,*/
Self::Not(_)
| Self::Exists(_)
| Self::ForAll(_)
=> 1,
Self::And(_)
=> 2,
Self::Or(_)
=> 3,
Self::Implies(_)
=> 4,
Self::IfAndOnlyIf(_)
=> 5,
}
}
}
fn requires_parentheses<'formula>(formula: &'formula crate::Formula,
parent_formula: &'formula crate::Formula)
-> bool
{
use crate::Formula;
match formula
{
Formula::Predicate(_)
| Formula::Boolean(_)
| Formula::Compare(_)
| Formula::Not(_)
| Formula::Exists(_)
| Formula::ForAll(_)
=> false,
Formula::And(formulas)
| Formula::Or(formulas) if formulas.len() <= 1
=> false,
Formula::And(formulas) => match *parent_formula
{
Formula::Not(_)
| Formula::Exists(_)
| Formula::ForAll(_)
=> true,
_ => false,
},
Formula::Or(formulas) => match *parent_formula
{
Formula::Not(_)
| Formula::Exists(_)
| Formula::ForAll(_)
| Formula::And(_)
=> true,
_ => false,
},
Formula::Implies(crate::Implies{direction, ..}) => match &*parent_formula
{
Formula::Not(_)
| Formula::Exists(_)
| Formula::ForAll(_)
| Formula::And(_)
| Formula::Or(_)
=> true,
Formula::Implies(
crate::Implies{direction: parent_direction, antecedent: parent_antecedent, ..}) =>
if direction == parent_direction
{
// Implications with the same direction nested on the antecedent side require
// parentheses because implication is considered right-associative
std::ptr::eq(formula, &**parent_antecedent)
}
else
{
true
},
_ => false,
},
Formula::IfAndOnlyIf(formulas) => match *parent_formula
{
Formula::Not(_)
| Formula::Exists(_)
| Formula::ForAll(_)
| Formula::And(_)
| Formula::Implies(_)
=> true,
_ => false,
},
_ => true,
}
}
impl std::fmt::Debug for crate::ImplicationDirection
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::LeftToRight => write!(format, "left to right"),
Self::RightToLeft => write!(format, "right to left"),
}
}
}
impl std::fmt::Debug for crate::PredicateDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}/{}", &self.name, self.arity)
}
}
impl std::fmt::Display for crate::PredicateDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", &self)
}
}
struct FormulaDisplay<'formula>
{
formula: &'formula crate::Formula,
parent_formula: Option<&'formula crate::Formula>,
}
fn display_formula<'formula>(formula: &'formula crate::Formula,
parent_formula: Option<&'formula crate::Formula>)
-> FormulaDisplay<'formula>
{
FormulaDisplay
{
formula,
parent_formula,
}
}
impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
let precedence_level = self.formula.precedence_level();
let requires_parentheses = match self.parent_formula
{
Some(ref parent_formula) => requires_parentheses(self.formula, parent_formula),
None => false,
};
if requires_parentheses
{
write!(format, "(")?;
}
match &self.formula
{
crate::Formula::Exists(exists) =>
{
assert!(!exists.parameters.is_empty());
write!(format, "exists")?;
let mut separator = " ";
for parameter in exists.parameters.iter()
{
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?;
},
crate::Formula::ForAll(for_all) =>
{
assert!(!for_all.parameters.is_empty());
write!(format, "forall")?;
let mut separator = " ";
for parameter in for_all.parameters.iter()
{
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?;
},
crate::Formula::Not(argument) => write!(format, "not {:?}",
display_formula(argument, Some(self.formula)))?,
crate::Formula::And(arguments) =>
{
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
{
write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
separator = " and "
}
},
crate::Formula::Or(arguments) =>
{
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
{
write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
separator = " or "
}
},
crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
{
let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
{
write!(format, "{:?}", display_formula(antecedent, Some(self.formula)))
};
let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
{
write!(format, "{:?}", display_formula(implication, Some(self.formula)))
};
match direction
{
crate::ImplicationDirection::LeftToRight =>
{
format_antecedent(format)?;
write!(format, " -> ")?;
format_implication(format)?;
},
crate::ImplicationDirection::RightToLeft =>
{
format_implication(format)?;
write!(format, " <- ")?;
format_antecedent(format)?;
},
}
},
crate::Formula::IfAndOnlyIf(arguments) =>
{
let mut separator = "";
for argument in arguments
{
write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
separator = " <-> ";
}
},
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
=> write!(format, "{:?} < {:?}", display_term(left, Parentheses::None),
display_term(right, Parentheses::None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
=> write!(format, "{:?} <= {:?}", display_term(left, Parentheses::None),
display_term(right, Parentheses::None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
=> write!(format, "{:?} > {:?}", display_term(left, Parentheses::None),
display_term(right, Parentheses::None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
=> write!(format, "{:?} >= {:?}", display_term(left, Parentheses::None),
display_term(right, Parentheses::None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
=> write!(format, "{:?} = {:?}", display_term(left, Parentheses::None),
display_term(right, Parentheses::None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
=> write!(format, "{:?} != {:?}", display_term(left, Parentheses::None),
display_term(right, Parentheses::None))?,
crate::Formula::Boolean(true) => write!(format, "true")?,
crate::Formula::Boolean(false) => write!(format, "false")?,
crate::Formula::Predicate(predicate) =>
{
write!(format, "{}", predicate.declaration.name)?;
if !predicate.arguments.is_empty()
{
write!(format, "(")?;
let mut separator = "";
for argument in &predicate.arguments
{
write!(format, "{}{:?}", separator,
display_term(argument, Parentheses::None))?;
separator = ", "
}
write!(format, ")")?;
}
},
}
if requires_parentheses
{
write!(format, ")")?;
}
Ok(())
}
}
impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", self)
}
}
impl std::fmt::Debug for crate::Formula
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", display_formula(&self, None))
}
}
impl std::fmt::Display for crate::Formula
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}", display_formula(&self, None))
}
}
#[cfg(test)]
mod tests
{
use crate::*;
use crate::format::terms::tests::*;
fn format(formula: Box<ast::Formula>) -> String
{
format!("{}", formula)
}
fn and(arguments: Formulas) -> Box<Formula>
{
Box::new(Formula::and(arguments))
}
fn equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
{
Box::new(Formula::equal(left, right))
}
fn exists(parameters: VariableDeclarations, argument: Box<Formula>) -> Box<Formula>
{
Box::new(Formula::exists(std::rc::Rc::new(parameters), argument))
}
fn false_() -> Box<Formula>
{
Box::new(Formula::false_())
}
fn for_all(parameters: VariableDeclarations, argument: Box<Formula>) -> Box<Formula>
{
Box::new(Formula::for_all(std::rc::Rc::new(parameters), argument))
}
fn greater(left: Box<Term>, right: Box<Term>) -> Box<Formula>
{
Box::new(Formula::greater(left, right))
}
fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
{
Box::new(Formula::greater_or_equal(left, right))
}
fn if_and_only_if(arguments: Formulas) -> Box<Formula>
{
Box::new(Formula::if_and_only_if(arguments))
}
fn implies(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
-> Box<Formula>
{
Box::new(Formula::implies(direction, antecedent, implication))
}
fn less(left: Box<Term>, right: Box<Term>) -> Box<Formula>
{
Box::new(Formula::less(left, right))
}
fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
{
Box::new(Formula::less_or_equal(left, right))
}
fn not(argument: Box<Formula>) -> Box<Formula>
{
Box::new(Formula::not(argument))
}
fn not_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
{
Box::new(Formula::not_equal(left, right))
}
fn or(arguments: Formulas) -> Box<Formula>
{
Box::new(Formula::or(arguments))
}
fn predicate(name: &str, arguments: Vec<Box<Term>>) -> Box<Formula>
{
Box::new(Formula::predicate(predicate_declaration(name, arguments.len()), arguments))
}
fn predicate_declaration(name: &str, arity: usize) -> std::rc::Rc<PredicateDeclaration>
{
std::rc::Rc::new(PredicateDeclaration::new(name.to_string(), arity))
}
fn true_() -> Box<Formula>
{
Box::new(Formula::true_())
}
#[test]
fn format_boolean()
{
assert_eq!(format(true_()), "true");
assert_eq!(format(false_()), "false");
}
#[test]
fn format_compare()
{
assert_eq!(format(greater(constant("a"), constant("b"))), "a > b");
assert_eq!(format(less(constant("a"), constant("b"))), "a < b");
assert_eq!(format(less_or_equal(constant("a"), constant("b"))), "a <= b");
assert_eq!(format(greater_or_equal(constant("a"), constant("b"))), "a >= b");
assert_eq!(format(equal(constant("a"), constant("b"))), "a = b");
assert_eq!(format(not_equal(constant("a"), constant("b"))), "a != b");
assert_eq!(format(
greater(multiply(add(constant("a"), constant("b")), constant("c")),
absolute_value(subtract(constant("d"), constant("e"))))),
"(a + b) * c > |d - e|");
assert_eq!(format(
less(multiply(add(constant("a"), constant("b")), constant("c")),
absolute_value(subtract(constant("d"), constant("e"))))),
"(a + b) * c < |d - e|");
assert_eq!(format(
less_or_equal(multiply(add(constant("a"), constant("b")), constant("c")),
absolute_value(subtract(constant("d"), constant("e"))))),
"(a + b) * c <= |d - e|");
assert_eq!(format(
greater_or_equal(multiply(add(constant("a"), constant("b")), constant("c")),
absolute_value(subtract(constant("d"), constant("e"))))),
"(a + b) * c >= |d - e|");
assert_eq!(format(
equal(multiply(add(constant("a"), constant("b")), constant("c")),
absolute_value(subtract(constant("d"), constant("e"))))),
"(a + b) * c = |d - e|");
assert_eq!(format(
not_equal(multiply(add(constant("a"), constant("b")), constant("c")),
absolute_value(subtract(constant("d"), constant("e"))))),
"(a + b) * c != |d - e|");
}
#[test]
fn format_predicate()
{
assert_eq!(format(predicate("p", vec![])), "p");
assert_eq!(format(predicate("predicate", vec![])), "predicate");
assert_eq!(format(predicate("q", vec![constant("a")])), "q(a)");
assert_eq!(format(
predicate("q", vec![constant("a"), constant("b"), constant("c")])),
"q(a, b, c)");
assert_eq!(format(
predicate("predicate", vec![constant("a"), constant("b"), constant("c")])),
"predicate(a, b, c)");
assert_eq!(format(
predicate("predicate", vec![
exponentiate(absolute_value(multiply(constant("a"), integer(-20))), integer(2)),
string("test"),
function("f", vec![multiply(add(constant("b"), constant("c")),
subtract(constant("b"), constant("c"))), infimum(), variable("X")])])),
"predicate(|a * -20| ** 2, \"test\", f((b + c) * (b - c), #inf, X))");
// TODO: escape predicates that start with capital letters or that conflict with keywords
}
#[test]
fn format_predicate_declaration()
{
assert_eq!(format!("{}", predicate_declaration("p", 0)), "p/0");
assert_eq!(format!("{}", predicate_declaration("predicate", 0)), "predicate/0");
assert_eq!(format!("{}", predicate_declaration("q", 1)), "q/1");
assert_eq!(format!("{}", predicate_declaration("q", 3)), "q/3");
assert_eq!(format!("{}", predicate_declaration("predicate", 3)), "predicate/3");
}
#[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");
}
#[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");
}
#[test]
fn format_not()
{
assert_eq!(format(not(predicate("p", vec![]))), "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");
}
#[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");
}
#[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");
}
#[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");
}
#[test]
fn format_combination_boolean_and_lower()
{
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(not(true_())), "not true");
assert_eq!(format(not(false_())), "not false");
assert_eq!(format(and(vec![true_()])), "true");
assert_eq!(format(and(vec![true_(), true_(), true_()])), "true and true and true");
assert_eq!(format(and(vec![false_()])), "false");
assert_eq!(format(and(vec![false_(), false_(), false_()])), "false and false and false");
assert_eq!(format(or(vec![true_()])), "true");
assert_eq!(format(or(vec![true_(), true_(), true_()])), "true or true or true");
assert_eq!(format(or(vec![false_()])), "false");
assert_eq!(format(or(vec![false_(), false_(), false_()])), "false or false or false");
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(if_and_only_if(vec![true_()])), "true");
assert_eq!(format(
if_and_only_if(vec![true_(), true_(), true_()])),
"true <-> true <-> true");
assert_eq!(format(if_and_only_if(vec![false_()])), "false");
assert_eq!(format(
if_and_only_if(vec![false_(), false_(), false_()])),
"false <-> false <-> false");
}
#[test]
fn format_combination_compare_and_lower()
{
let term_1 = || multiply(add(constant("a"), constant("b")), constant("c"));
let term_2 = || absolute_value(subtract(constant("d"), constant("e")));
let term_3 = || exponentiate(constant("a"), exponentiate(constant("b"), constant("c")));
let term_4 = || negative(function("f", vec![integer(5), add(variable("X"), integer(3))]));
assert_eq!(format(not(greater(term_1(), term_2()))), "not (a + b) * c > |d - e|");
assert_eq!(format(not(less(term_1(), term_2()))), "not (a + b) * c < |d - e|");
assert_eq!(format(not(less_or_equal(term_1(), term_2()))), "not (a + b) * c <= |d - e|");
assert_eq!(format(not(greater_or_equal(term_1(), term_2()))), "not (a + b) * c >= |d - e|");
assert_eq!(format(not(equal(term_1(), term_2()))), "not (a + b) * c = |d - e|");
assert_eq!(format(not(not_equal(term_1(), term_2()))), "not (a + b) * c != |d - e|");
assert_eq!(format(
exists(vec![variable_declaration("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 X (a + b) * c < |d - e|");
assert_eq!(format(
exists(vec![variable_declaration("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 X (a + b) * c >= |d - e|");
assert_eq!(format(
exists(vec![variable_declaration("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 X (a + b) * c != |d - e|");
assert_eq!(format(
for_all(vec![variable_declaration("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()))),
"forall X (a + b) * c < |d - e|");
assert_eq!(format(
for_all(vec![variable_declaration("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()))),
"forall X (a + b) * c >= |d - e|");
assert_eq!(format(
for_all(vec![variable_declaration("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()))),
"forall X (a + b) * c != |d - e|");
assert_eq!(format(
and(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
greater(term_2(), term_4())])),
"(a + b) * c > |d - e| and a ** b ** c > -f(5, X + 3) and |d - e| > -f(5, X + 3)");
assert_eq!(format(
and(vec![less(term_1(), term_2()), less(term_3(), term_4()),
less(term_2(), term_4())])),
"(a + b) * c < |d - e| and a ** b ** c < -f(5, X + 3) and |d - e| < -f(5, X + 3)");
assert_eq!(format(
and(vec![less_or_equal(term_1(), term_2()), less_or_equal(term_3(), term_4()),
less_or_equal(term_2(), term_4())])),
"(a + b) * c <= |d - e| and a ** b ** c <= -f(5, X + 3) and |d - e| <= -f(5, X + 3)");
assert_eq!(format(
and(vec![greater_or_equal(term_1(), term_2()), greater_or_equal(term_3(), term_4()),
greater_or_equal(term_2(), term_4())])),
"(a + b) * c >= |d - e| and a ** b ** c >= -f(5, X + 3) and |d - e| >= -f(5, X + 3)");
assert_eq!(format(
and(vec![equal(term_1(), term_2()), equal(term_3(), term_4()),
equal(term_2(), term_4())])),
"(a + b) * c = |d - e| and a ** b ** c = -f(5, X + 3) and |d - e| = -f(5, X + 3)");
assert_eq!(format(
and(vec![not_equal(term_1(), term_2()), not_equal(term_3(), term_4()),
not_equal(term_2(), term_4())])),
"(a + b) * c != |d - e| and a ** b ** c != -f(5, X + 3) and |d - e| != -f(5, X + 3)");
assert_eq!(format(
or(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
greater(term_2(), term_4())])),
"(a + b) * c > |d - e| or a ** b ** c > -f(5, X + 3) or |d - e| > -f(5, X + 3)");
assert_eq!(format(
or(vec![less(term_1(), term_2()), less(term_3(), term_4()),
less(term_2(), term_4())])),
"(a + b) * c < |d - e| or a ** b ** c < -f(5, X + 3) or |d - e| < -f(5, X + 3)");
assert_eq!(format(
or(vec![less_or_equal(term_1(), term_2()), less_or_equal(term_3(), term_4()),
less_or_equal(term_2(), term_4())])),
"(a + b) * c <= |d - e| or a ** b ** c <= -f(5, X + 3) or |d - e| <= -f(5, X + 3)");
assert_eq!(format(
or(vec![greater_or_equal(term_1(), term_2()), greater_or_equal(term_3(), term_4()),
greater_or_equal(term_2(), term_4())])),
"(a + b) * c >= |d - e| or a ** b ** c >= -f(5, X + 3) or |d - e| >= -f(5, X + 3)");
assert_eq!(format(
or(vec![equal(term_1(), term_2()), equal(term_3(), term_4()),
equal(term_2(), term_4())])),
"(a + b) * c = |d - e| or a ** b ** c = -f(5, X + 3) or |d - e| = -f(5, X + 3)");
assert_eq!(format(
or(vec![not_equal(term_1(), term_2()), not_equal(term_3(), term_4()),
not_equal(term_2(), term_4())])),
"(a + b) * c != |d - e| or a ** b ** c != -f(5, X + 3) or |d - e| != -f(5, X + 3)");
assert_eq!(format(
implies(ImplicationDirection::LeftToRight, 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()))),
"(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()))),
"(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()),
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()))),
"(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()))),
"(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()))),
"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()))),
"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()))),
"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()),
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()))),
"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()))),
"a ** b ** c != -f(5, X + 3) <- (a + b) * c != |d - e|");
assert_eq!(format(
if_and_only_if(vec![greater(term_1(), term_2()), greater(term_3(), term_4()),
greater(term_2(), term_4())])),
"(a + b) * c > |d - e| <-> a ** b ** c > -f(5, X + 3) <-> |d - e| > -f(5, X + 3)");
assert_eq!(format(
if_and_only_if(vec![less(term_1(), term_2()), less(term_3(), term_4()),
less(term_2(), term_4())])),
"(a + b) * c < |d - e| <-> a ** b ** c < -f(5, X + 3) <-> |d - e| < -f(5, X + 3)");
assert_eq!(format(
if_and_only_if(vec![less_or_equal(term_1(), term_2()),
less_or_equal(term_3(), term_4()), less_or_equal(term_2(), term_4())])),
"(a + b) * c <= |d - e| <-> a ** b ** c <= -f(5, X + 3) <-> |d - e| <= -f(5, X + 3)");
assert_eq!(format(
if_and_only_if(vec![greater_or_equal(term_1(), term_2()),
greater_or_equal(term_3(), term_4()), greater_or_equal(term_2(), term_4())])),
"(a + b) * c >= |d - e| <-> a ** b ** c >= -f(5, X + 3) <-> |d - e| >= -f(5, X + 3)");
assert_eq!(format(
if_and_only_if(vec![equal(term_1(), term_2()), equal(term_3(), term_4()),
equal(term_2(), term_4())])),
"(a + b) * c = |d - e| <-> a ** b ** c = -f(5, X + 3) <-> |d - e| = -f(5, X + 3)");
assert_eq!(format(
if_and_only_if(vec![not_equal(term_1(), term_2()), not_equal(term_3(), term_4()),
not_equal(term_2(), term_4())])),
"(a + b) * c != |d - e| <-> a ** b ** c != -f(5, X + 3) <-> |d - e| != -f(5, X + 3)");
}
#[test]
fn format_combination_not_and_lower()
{
assert_eq!(format(not(not(predicate("p", vec![])))), "not not p");
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(
exists(vec![variable_declaration("X"), variable_declaration("Y"),
variable_declaration("Z")], 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(
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(
not(and(vec![predicate("p", vec![])]))),
"not p");
assert_eq!(format(
not(and(vec![predicate("p", vec![]), predicate("q", vec![]), predicate("r", vec![])]))),
"not (p and q and r)");
assert_eq!(format(
or(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
"p or q or r");
assert_eq!(format(
and(vec![predicate("p", vec![]), or(vec![or(vec![predicate("q", vec![]), predicate("r", vec![])])])])),
"p and (q or r)");
}
#[test]
fn format_combination_quantifiers_and_lower()
{
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");
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");
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");
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");
}
}
Reference in New Issue View Git Blame Copy Permalink