1762 lines
65 KiB
Rust
1762 lines
65 KiB
Rust
use super::*;
|
|
|
|
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)
|
|
}
|
|
}
|
|
|
|
#[derive(Clone, Copy, Eq, PartialEq)]
|
|
enum ChildPosition
|
|
{
|
|
Any,
|
|
ImpliesAntecedent,
|
|
}
|
|
|
|
struct FormulaDisplay<'formula>
|
|
{
|
|
formula: &'formula crate::Formula,
|
|
parent_formula: Option<&'formula crate::Formula>,
|
|
position: ChildPosition,
|
|
}
|
|
|
|
impl<'formula> FormulaDisplay<'formula>
|
|
{
|
|
fn requires_parentheses(&self) -> bool
|
|
{
|
|
use crate::Formula;
|
|
|
|
let parent_formula = match self.parent_formula
|
|
{
|
|
Some(parent_formula) => parent_formula,
|
|
None => return false,
|
|
};
|
|
|
|
match self.formula
|
|
{
|
|
Formula::Predicate(_)
|
|
| Formula::Boolean(_)
|
|
| Formula::Compare(_)
|
|
| Formula::Not(_)
|
|
| Formula::Exists(_)
|
|
| Formula::ForAll(_)
|
|
=> false,
|
|
Formula::And(formulas)
|
|
| Formula::Or(formulas)
|
|
| Formula::IfAndOnlyIf(formulas) if formulas.len() <= 1
|
|
=> false,
|
|
Formula::And(_) => match *parent_formula
|
|
{
|
|
Formula::Not(_)
|
|
| Formula::Exists(_)
|
|
| Formula::ForAll(_)
|
|
=> true,
|
|
_ => false,
|
|
},
|
|
Formula::Or(_) => 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, ..}) =>
|
|
if direction == parent_direction
|
|
{
|
|
// Implications with the same direction nested on the antecedent side
|
|
// require parentheses because implication is considered right-associative
|
|
self.position == ChildPosition::ImpliesAntecedent
|
|
}
|
|
else
|
|
{
|
|
// Nested implications with opposite direction always require parentheses
|
|
// because the order of formulas like p <- q -> r would be ambiguous
|
|
true
|
|
},
|
|
_ => false,
|
|
},
|
|
Formula::IfAndOnlyIf(_) => match *parent_formula
|
|
{
|
|
Formula::Not(_)
|
|
| Formula::Exists(_)
|
|
| Formula::ForAll(_)
|
|
| Formula::And(_)
|
|
| Formula::Or(_)
|
|
| Formula::Implies(_)
|
|
=> true,
|
|
_ => false,
|
|
},
|
|
}
|
|
}
|
|
}
|
|
|
|
fn display_formula<'formula>(formula: &'formula crate::Formula,
|
|
parent_formula: Option<&'formula crate::Formula>, position: ChildPosition)
|
|
-> FormulaDisplay<'formula>
|
|
{
|
|
FormulaDisplay
|
|
{
|
|
formula,
|
|
parent_formula,
|
|
position,
|
|
}
|
|
}
|
|
|
|
impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
let requires_parentheses = self.requires_parentheses();
|
|
|
|
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), ChildPosition::Any))?;
|
|
},
|
|
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), ChildPosition::Any))?;
|
|
},
|
|
crate::Formula::Not(argument) => write!(format, "not {:?}",
|
|
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()
|
|
{
|
|
0 | 1 => (self.parent_formula, self.position),
|
|
_ => (Some(self.formula), ChildPosition::Any),
|
|
};
|
|
|
|
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()
|
|
{
|
|
0 | 1 => (self.parent_formula, self.position),
|
|
_ => (Some(self.formula), ChildPosition::Any),
|
|
};
|
|
|
|
for argument in arguments
|
|
{
|
|
write!(format, "{}{:?}", separator,
|
|
display_formula(argument, parent_formula, position))?;
|
|
|
|
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),
|
|
ChildPosition::ImpliesAntecedent))
|
|
};
|
|
|
|
let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
|
|
{
|
|
write!(format, "{:?}",
|
|
display_formula(implication, Some(self.formula), ChildPosition::Any))
|
|
};
|
|
|
|
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 = "";
|
|
|
|
assert!(!arguments.is_empty());
|
|
|
|
let (parent_formula, position) = match arguments.len()
|
|
{
|
|
0 | 1 => (self.parent_formula, self.position),
|
|
_ => (Some(self.formula), ChildPosition::Any),
|
|
};
|
|
|
|
for argument in arguments
|
|
{
|
|
write!(format, "{}{:?}", separator,
|
|
display_formula(argument, parent_formula, position))?;
|
|
|
|
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, ChildPosition::Any))
|
|
}
|
|
}
|
|
|
|
impl std::fmt::Display for crate::Formula
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
write!(format, "{}", display_formula(&self, None, ChildPosition::Any))
|
|
}
|
|
}
|
|
|
|
#[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_())
|
|
}
|
|
|
|
fn x() -> std::rc::Rc<VariableDeclaration>
|
|
{
|
|
variable_declaration("X")
|
|
}
|
|
|
|
fn y() -> std::rc::Rc<VariableDeclaration>
|
|
{
|
|
variable_declaration("Y")
|
|
}
|
|
|
|
fn z() -> std::rc::Rc<VariableDeclaration>
|
|
{
|
|
variable_declaration("Z")
|
|
}
|
|
|
|
fn xyz() -> VariableDeclarations
|
|
{
|
|
vec![x(), y(), z()]
|
|
}
|
|
|
|
fn x1y1z1() -> VariableDeclarations
|
|
{
|
|
vec![variable_declaration("X1"), variable_declaration("Y1"), variable_declaration("Z1")]
|
|
}
|
|
|
|
fn x2y2z2() -> VariableDeclarations
|
|
{
|
|
vec![variable_declaration("X2"), variable_declaration("Y2"), variable_declaration("Z2")]
|
|
}
|
|
|
|
fn x3y3z3() -> VariableDeclarations
|
|
{
|
|
vec![variable_declaration("X3"), variable_declaration("Y3"), variable_declaration("Z3")]
|
|
}
|
|
|
|
fn p() -> Box<Formula>
|
|
{
|
|
predicate("p", vec![])
|
|
}
|
|
|
|
fn q() -> Box<Formula>
|
|
{
|
|
predicate("q", vec![])
|
|
}
|
|
|
|
fn p1() -> Box<Formula>
|
|
{
|
|
predicate("p1", vec![])
|
|
}
|
|
|
|
fn q1() -> Box<Formula>
|
|
{
|
|
predicate("q1", vec![])
|
|
}
|
|
|
|
fn p2() -> Box<Formula>
|
|
{
|
|
predicate("p2", vec![])
|
|
}
|
|
|
|
fn q2() -> Box<Formula>
|
|
{
|
|
predicate("q2", vec![])
|
|
}
|
|
|
|
fn p3() -> Box<Formula>
|
|
{
|
|
predicate("p3", vec![])
|
|
}
|
|
|
|
fn q3() -> Box<Formula>
|
|
{
|
|
predicate("q3", vec![])
|
|
}
|
|
|
|
fn r() -> Box<Formula>
|
|
{
|
|
predicate("r", vec![])
|
|
}
|
|
|
|
fn pqr() -> Formulas
|
|
{
|
|
vec![p(), q(), r()]
|
|
}
|
|
|
|
fn p1q1r1() -> Formulas
|
|
{
|
|
vec![p1(), q1(), predicate("r1", vec![])]
|
|
}
|
|
|
|
fn p2q2r2() -> Formulas
|
|
{
|
|
vec![p2(), q2(), predicate("r2", vec![])]
|
|
}
|
|
|
|
fn p3q3r3() -> Formulas
|
|
{
|
|
vec![p3(), q3(), predicate("r3", vec![])]
|
|
}
|
|
|
|
fn implies_right(antecedent: Box<Formula>, implication: Box<Formula>) -> Box<Formula>
|
|
{
|
|
implies(ImplicationDirection::LeftToRight, antecedent, implication)
|
|
}
|
|
|
|
fn implies_left(antecedent: Box<Formula>, implication: Box<Formula>) -> Box<Formula>
|
|
{
|
|
implies(ImplicationDirection::RightToLeft, antecedent, implication)
|
|
}
|
|
|
|
#[test]
|
|
fn format_boolean()
|
|
{
|
|
assert_eq!(format(true_()), "true");
|
|
assert_eq!(format(false_()), "false");
|
|
}
|
|
|
|
#[test]
|
|
fn format_compare()
|
|
{
|
|
assert_eq!(format(greater(a(), b())), "a > b");
|
|
assert_eq!(format(less(a(), b())), "a < b");
|
|
assert_eq!(format(less_or_equal(a(), b())), "a <= b");
|
|
assert_eq!(format(greater_or_equal(a(), b())), "a >= b");
|
|
assert_eq!(format(equal(a(), b())), "a = b");
|
|
assert_eq!(format(not_equal(a(), b())), "a != b");
|
|
|
|
assert_eq!(format(
|
|
greater(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
|
"(a + b) * c > |d - e|");
|
|
assert_eq!(format(
|
|
less(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
|
"(a + b) * c < |d - e|");
|
|
assert_eq!(format(
|
|
less_or_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
|
"(a + b) * c <= |d - e|");
|
|
assert_eq!(format(
|
|
greater_or_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
|
"(a + b) * c >= |d - e|");
|
|
assert_eq!(format(
|
|
equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
|
"(a + b) * c = |d - e|");
|
|
assert_eq!(format(
|
|
not_equal(multiply(add(a(), b()), c()), absolute_value(subtract(d(), e())))),
|
|
"(a + b) * c != |d - e|");
|
|
}
|
|
|
|
#[test]
|
|
fn format_predicate()
|
|
{
|
|
assert_eq!(format(p()), "p");
|
|
assert_eq!(format(predicate("predicate", vec![])), "predicate");
|
|
assert_eq!(format(predicate("q", vec![a()])), "q(a)");
|
|
assert_eq!(format(predicate("q", abc())), "q(a, b, c)");
|
|
assert_eq!(format(predicate("predicate", abc())), "predicate(a, b, c)");
|
|
|
|
assert_eq!(format(
|
|
predicate("predicate", vec![
|
|
exponentiate(absolute_value(multiply(a(), integer(-20))), integer(2)),
|
|
string("test"),
|
|
function("f", vec![multiply(add(b(), c()),
|
|
subtract(b(), 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![x()], p())), "exists X p");
|
|
assert_eq!(format(exists(xyz(), p())), "exists X, Y, Z p");
|
|
}
|
|
|
|
#[test]
|
|
fn format_for_all()
|
|
{
|
|
assert_eq!(format(for_all(vec![x()], p())), "forall X p");
|
|
assert_eq!(format(for_all(xyz(), p())), "forall X, Y, Z p");
|
|
}
|
|
|
|
#[test]
|
|
fn format_not()
|
|
{
|
|
assert_eq!(format(not(p())), "not p");
|
|
}
|
|
|
|
#[test]
|
|
fn format_and()
|
|
{
|
|
assert_eq!(format(and(vec![p()])), "p");
|
|
assert_eq!(format(and(pqr())), "p and q and r");
|
|
}
|
|
|
|
#[test]
|
|
fn format_or()
|
|
{
|
|
assert_eq!(format(or(vec![p()])), "p");
|
|
assert_eq!(format(or(pqr())), "p or q or r");
|
|
}
|
|
|
|
#[test]
|
|
fn format_implies()
|
|
{
|
|
assert_eq!(format(implies_right(p(), q())), "p -> q");
|
|
assert_eq!(format(implies_left(p(), q())), "q <- p");
|
|
}
|
|
|
|
#[test]
|
|
fn format_if_and_only_if()
|
|
{
|
|
assert_eq!(format(if_and_only_if(vec![p()])), "p");
|
|
assert_eq!(format(if_and_only_if(vec![p(), q()])), "p <-> q");
|
|
assert_eq!(format(if_and_only_if(pqr())), "p <-> q <-> r");
|
|
}
|
|
|
|
#[test]
|
|
fn format_combination_boolean_and_lower()
|
|
{
|
|
// Boolean + not
|
|
assert_eq!(format(not(true_())), "not true");
|
|
assert_eq!(format(not(false_())), "not false");
|
|
|
|
// Boolean + quantified formula
|
|
assert_eq!(format(exists(vec![x()], true_())), "exists X true");
|
|
assert_eq!(format(exists(vec![x()], false_())), "exists X false");
|
|
assert_eq!(format(exists(xyz(), true_())), "exists X, Y, Z true");
|
|
assert_eq!(format(exists(xyz(), false_())), "exists X, Y, Z false");
|
|
assert_eq!(format(for_all(vec![x()], true_())), "forall X true");
|
|
assert_eq!(format(for_all(vec![x()], false_())), "forall X false");
|
|
assert_eq!(format(for_all(xyz(), true_())), "forall X, Y, Z true");
|
|
assert_eq!(format(for_all(xyz(), false_())), "forall X, Y, Z false");
|
|
|
|
// Boolean + and
|
|
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");
|
|
|
|
// Boolean + or
|
|
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");
|
|
|
|
// Boolean + implies
|
|
assert_eq!(format(implies_right(true_(), true_())), "true -> true");
|
|
assert_eq!(format(implies_left(true_(), true_())), "true <- true");
|
|
assert_eq!(format(implies_right(false_(), false_())), "false -> false");
|
|
assert_eq!(format(implies_left(false_(), false_())), "false <- false");
|
|
|
|
// Boolean + if and only if
|
|
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(a(), b()), c());
|
|
let term_2 = || absolute_value(subtract(d(), e()));
|
|
let term_3 = || exponentiate(a(), exponentiate(b(), c()));
|
|
let term_4 = || negative(function("f", vec![integer(5), add(variable("X"), integer(3))]));
|
|
|
|
// Compare + not
|
|
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|");
|
|
|
|
// Compare + quantified formula
|
|
assert_eq!(format(
|
|
exists(vec![x()], greater(term_1(), term_2()))),
|
|
"exists X (a + b) * c > |d - e|");
|
|
assert_eq!(format(
|
|
exists(vec![x()], less(term_1(), term_2()))),
|
|
"exists X (a + b) * c < |d - e|");
|
|
assert_eq!(format(
|
|
exists(vec![x()], less_or_equal(term_1(), term_2()))),
|
|
"exists X (a + b) * c <= |d - e|");
|
|
assert_eq!(format(
|
|
exists(vec![x()], greater_or_equal(term_1(), term_2()))),
|
|
"exists X (a + b) * c >= |d - e|");
|
|
assert_eq!(format(
|
|
exists(vec![x()], equal(term_1(), term_2()))),
|
|
"exists X (a + b) * c = |d - e|");
|
|
assert_eq!(format(
|
|
exists(vec![x()], not_equal(term_1(), term_2()))),
|
|
"exists X (a + b) * c != |d - e|");
|
|
assert_eq!(format(
|
|
for_all(vec![x()], greater(term_1(), term_2()))),
|
|
"forall X (a + b) * c > |d - e|");
|
|
assert_eq!(format(
|
|
for_all(vec![x()], less(term_1(), term_2()))),
|
|
"forall X (a + b) * c < |d - e|");
|
|
assert_eq!(format(
|
|
for_all(vec![x()], less_or_equal(term_1(), term_2()))),
|
|
"forall X (a + b) * c <= |d - e|");
|
|
assert_eq!(format(
|
|
for_all(vec![x()], greater_or_equal(term_1(), term_2()))),
|
|
"forall X (a + b) * c >= |d - e|");
|
|
assert_eq!(format(
|
|
for_all(vec![x()], equal(term_1(), term_2()))),
|
|
"forall X (a + b) * c = |d - e|");
|
|
assert_eq!(format(
|
|
for_all(vec![x()], not_equal(term_1(), term_2()))),
|
|
"forall X (a + b) * c != |d - e|");
|
|
|
|
// Compare + and
|
|
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)");
|
|
|
|
// Compare + or
|
|
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)");
|
|
|
|
// Compare + implies
|
|
assert_eq!(format(
|
|
implies_right(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_right(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_right(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_right(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_right(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_right(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_left(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_left(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_left(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_left(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_left(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_left(not_equal(term_1(), term_2()), not_equal(term_3(), term_4()))),
|
|
"a ** b ** c != -f(5, X + 3) <- (a + b) * c != |d - e|");
|
|
|
|
// Compare + if and only if
|
|
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()
|
|
{
|
|
// Not + not
|
|
assert_eq!(format(not(not(p()))), "not not p");
|
|
|
|
// Not + quantified formulas
|
|
assert_eq!(format(not(exists(xyz(), p()))), "not exists X, Y, Z p");
|
|
assert_eq!(format(not(exists(xyz(), and(vec![p()])))), "not exists X, Y, Z p");
|
|
assert_eq!(format(not(exists(xyz(), or(vec![p()])))), "not exists X, Y, Z p");
|
|
assert_eq!(format(not(exists(xyz(), if_and_only_if(vec![p()])))), "not exists X, Y, Z p");
|
|
assert_eq!(format(exists(xyz(), not(p()))), "exists X, Y, Z not p");
|
|
assert_eq!(format(exists(xyz(), and(vec![not(p())]))), "exists X, Y, Z not p");
|
|
assert_eq!(format(exists(xyz(), or(vec![not(p())]))), "exists X, Y, Z not p");
|
|
assert_eq!(format(exists(xyz(), if_and_only_if(vec![not(p())]))), "exists X, Y, Z not p");
|
|
assert_eq!(format(not(for_all(xyz(), p()))), "not forall X, Y, Z p");
|
|
assert_eq!(format(not(for_all(xyz(), and(vec![p()])))), "not forall X, Y, Z p");
|
|
assert_eq!(format(not(for_all(xyz(), or(vec![p()])))), "not forall X, Y, Z p");
|
|
assert_eq!(format(not(for_all(xyz(), if_and_only_if(vec![p()])))), "not forall X, Y, Z p");
|
|
assert_eq!(format(for_all(xyz(), not(p()))), "forall X, Y, Z not p");
|
|
assert_eq!(format(for_all(xyz(), and(vec![not(p())]))), "forall X, Y, Z not p");
|
|
assert_eq!(format(for_all(xyz(), or(vec![not(p())]))), "forall X, Y, Z not p");
|
|
assert_eq!(format(for_all(xyz(), if_and_only_if(vec![not(p())]))), "forall X, Y, Z not p");
|
|
|
|
// Not + and
|
|
assert_eq!(format(not(and(pqr()))), "not (p and q and r)");
|
|
assert_eq!(format(not(and(vec![and(pqr())]))), "not (p and q and r)");
|
|
assert_eq!(format(not(or(vec![and(pqr())]))), "not (p and q and r)");
|
|
assert_eq!(format(not(if_and_only_if(vec![and(pqr())]))), "not (p and q and r)");
|
|
assert_eq!(format(and(vec![not(p())])), "not p");
|
|
assert_eq!(format(and(vec![not(and(vec![p()]))])), "not p");
|
|
assert_eq!(format(and(vec![not(or(vec![p()]))])), "not p");
|
|
assert_eq!(format(and(vec![not(if_and_only_if(vec![p()]))])), "not p");
|
|
assert_eq!(format(and(vec![not(p()), not(q()), not(r())])), "not p and not q and not r");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])),
|
|
"not p and not q and not r");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])),
|
|
"not p and not q and not r");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]),
|
|
if_and_only_if(vec![not(r())])])),
|
|
"not p and not q and not r");
|
|
|
|
// Not + or
|
|
assert_eq!(format(not(or(pqr()))), "not (p or q or r)");
|
|
assert_eq!(format(not(and(vec![or(pqr())]))), "not (p or q or r)");
|
|
assert_eq!(format(not(or(vec![or(pqr())]))), "not (p or q or r)");
|
|
assert_eq!(format(not(if_and_only_if(vec![or(pqr())]))), "not (p or q or r)");
|
|
assert_eq!(format(or(vec![not(p())])), "not p");
|
|
assert_eq!(format(or(vec![not(and(vec![p()]))])), "not p");
|
|
assert_eq!(format(or(vec![not(or(vec![p()]))])), "not p");
|
|
assert_eq!(format(or(vec![not(if_and_only_if(vec![p()]))])), "not p");
|
|
assert_eq!(format(or(vec![not(p()), not(q()), not(r())])), "not p or not q or not r");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])),
|
|
"not p or not q or not r");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])),
|
|
"not p or not q or not r");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]),
|
|
if_and_only_if(vec![not(r())])])),
|
|
"not p or not q or not r");
|
|
|
|
// Not + implies
|
|
assert_eq!(format(not(implies_right(p(), q()))), "not (p -> q)");
|
|
assert_eq!(format(not(and(vec![implies_right(p(), q())]))), "not (p -> q)");
|
|
assert_eq!(format(not(or(vec![implies_right(p(), q())]))), "not (p -> q)");
|
|
assert_eq!(format(not(if_and_only_if(vec![implies_right(p(), q())]))), "not (p -> q)");
|
|
assert_eq!(format(not(implies_left(p(), q()))), "not (q <- p)");
|
|
assert_eq!(format(not(and(vec![implies_left(p(), q())]))), "not (q <- p)");
|
|
assert_eq!(format(not(or(vec![implies_left(p(), q())]))), "not (q <- p)");
|
|
assert_eq!(format(not(if_and_only_if(vec![implies_left(p(), q())]))), "not (q <- p)");
|
|
assert_eq!(format(implies_right(not(p()), not(q()))), "not p -> not q");
|
|
assert_eq!(format(
|
|
implies_right(and(vec![not(p())]), and(vec![not(q())]))),
|
|
"not p -> not q");
|
|
assert_eq!(format(implies_right(or(vec![not(p())]), or(vec![not(q())]))), "not p -> not q");
|
|
assert_eq!(format(
|
|
implies_right(if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]))),
|
|
"not p -> not q");
|
|
assert_eq!(format(implies_left(not(p()), not(q()))), "not q <- not p");
|
|
assert_eq!(format(
|
|
implies_left(and(vec![not(p())]), and(vec![not(q())]))),
|
|
"not q <- not p");
|
|
assert_eq!(format(implies_left(or(vec![not(p())]), or(vec![not(q())]))), "not q <- not p");
|
|
assert_eq!(format(
|
|
implies_left(if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]))),
|
|
"not q <- not p");
|
|
|
|
// Not + if and only if
|
|
assert_eq!(format(not(if_and_only_if(pqr()))), "not (p <-> q <-> r)");
|
|
assert_eq!(format(not(and(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)");
|
|
assert_eq!(format(not(or(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)");
|
|
assert_eq!(format(not(if_and_only_if(vec![if_and_only_if(pqr())]))), "not (p <-> q <-> r)");
|
|
assert_eq!(format(if_and_only_if(vec![not(p())])), "not p");
|
|
assert_eq!(format(if_and_only_if(vec![not(and(vec![p()]))])),"not p");
|
|
assert_eq!(format(if_and_only_if(vec![not(or(vec![p()]))])), "not p");
|
|
assert_eq!(format(if_and_only_if(vec![not(if_and_only_if(vec![p()]))])), "not p");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![not(p()), not(q()), not(r())])),
|
|
"not p <-> not q <-> not r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(vec![not(p())]), and(vec![not(q())]), and(vec![not(r())])])),
|
|
"not p <-> not q <-> not r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(vec![not(p())]), or(vec![not(q())]), or(vec![not(r())])])),
|
|
"not p <-> not q <-> not r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![if_and_only_if(vec![not(p())]), if_and_only_if(vec![not(q())]),
|
|
if_and_only_if(vec![not(r())])])),
|
|
"not p <-> not q <-> not r");
|
|
}
|
|
|
|
#[test]
|
|
fn format_combination_quantified_formula_and_lower()
|
|
{
|
|
// Quantified formula + quantified formula
|
|
assert_eq!(format(
|
|
exists(x1y1z1(), exists(x2y2z2(), p()))),
|
|
"exists X1, Y1, Z1 exists X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
exists(x1y1z1(), and(vec![exists(x2y2z2(), p())]))),
|
|
"exists X1, Y1, Z1 exists X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
exists(x1y1z1(), or(vec![exists(x2y2z2(), p())]))),
|
|
"exists X1, Y1, Z1 exists X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
exists(x1y1z1(), if_and_only_if(vec![exists(x2y2z2(), p())]))),
|
|
"exists X1, Y1, Z1 exists X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
exists(x1y1z1(), for_all(x2y2z2(), p()))),
|
|
"exists X1, Y1, Z1 forall X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
exists(x1y1z1(), and(vec![for_all(x2y2z2(), p())]))),
|
|
"exists X1, Y1, Z1 forall X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
exists(x1y1z1(), or(vec![for_all(x2y2z2(), p())]))),
|
|
"exists X1, Y1, Z1 forall X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
exists(x1y1z1(), if_and_only_if(vec![for_all(x2y2z2(), p())]))),
|
|
"exists X1, Y1, Z1 forall X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
for_all(x1y1z1(), exists(x2y2z2(), p()))),
|
|
"forall X1, Y1, Z1 exists X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
for_all(x1y1z1(), and(vec![exists(x2y2z2(), p())]))),
|
|
"forall X1, Y1, Z1 exists X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
for_all(x1y1z1(), or(vec![exists(x2y2z2(), p())]))),
|
|
"forall X1, Y1, Z1 exists X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
for_all(x1y1z1(), if_and_only_if(vec![exists(x2y2z2(), p())]))),
|
|
"forall X1, Y1, Z1 exists X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
for_all(x1y1z1(), for_all(x2y2z2(), p()))),
|
|
"forall X1, Y1, Z1 forall X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
for_all(x1y1z1(),
|
|
and(vec![for_all(x2y2z2(), p())]))),
|
|
"forall X1, Y1, Z1 forall X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
for_all(x1y1z1(),
|
|
or(vec![for_all(x2y2z2(), p())]))),
|
|
"forall X1, Y1, Z1 forall X2, Y2, Z2 p");
|
|
assert_eq!(format(
|
|
for_all(x1y1z1(), if_and_only_if(vec![for_all(x2y2z2(), p())]))),
|
|
"forall X1, Y1, Z1 forall X2, Y2, Z2 p");
|
|
|
|
// Quantified formula + and
|
|
assert_eq!(format(exists(xyz(), and(pqr()))), "exists X, Y, Z (p and q and r)");
|
|
assert_eq!(format(exists(xyz(), and(pqr()))), "exists X, Y, Z (p and q and r)");
|
|
assert_eq!(format(exists(xyz(), or(vec![and(pqr())]))), "exists X, Y, Z (p and q and r)");
|
|
assert_eq!(format(
|
|
exists(xyz(), if_and_only_if(vec![and(pqr())]))),
|
|
"exists X, Y, Z (p and q and r)");
|
|
assert_eq!(format(
|
|
and(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()), exists(x3y3z3(), r())])),
|
|
"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]),
|
|
and(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]),
|
|
or(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![exists(x1y1z1(), p())]),
|
|
if_and_only_if(vec![exists(x2y2z2(), q())]),
|
|
if_and_only_if(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p and exists X2, Y2, Z2 q and exists X3, Y3, Z3 r");
|
|
assert_eq!(format(for_all(xyz(), and(pqr()))), "forall X, Y, Z (p and q and r)");
|
|
assert_eq!(format(for_all(xyz(), and(vec![and(pqr())]))), "forall X, Y, Z (p and q and r)");
|
|
assert_eq!(format(for_all(xyz(), or(vec![and(pqr())]))), "forall X, Y, Z (p and q and r)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), if_and_only_if(vec![and(pqr())]))),
|
|
"forall X, Y, Z (p and q and r)");
|
|
assert_eq!(format(
|
|
and(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()), for_all(x3y3z3(), r())])),
|
|
"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]),
|
|
and(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]),
|
|
or(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]),
|
|
if_and_only_if(vec![for_all(x2y2z2(), q())]),
|
|
if_and_only_if(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p and forall X2, Y2, Z2 q and forall X3, Y3, Z3 r");
|
|
|
|
// Quantified formula + or
|
|
assert_eq!(format(exists(xyz(), or(pqr()))), "exists X, Y, Z (p or q or r)");
|
|
assert_eq!(format(exists(xyz(), and(vec![or(pqr())]))), "exists X, Y, Z (p or q or r)");
|
|
assert_eq!(format(exists(xyz(), or(vec![or(pqr())]))), "exists X, Y, Z (p or q or r)");
|
|
assert_eq!(format(
|
|
exists(xyz(), if_and_only_if(vec![or(pqr())]))),
|
|
"exists X, Y, Z (p or q or r)");
|
|
assert_eq!(format(
|
|
or(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()), exists(x3y3z3(), r())])),
|
|
"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]),
|
|
and(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]),
|
|
or(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![exists(x1y1z1(), p())]),
|
|
if_and_only_if(vec![exists(x2y2z2(), q())]),
|
|
if_and_only_if(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p or exists X2, Y2, Z2 q or exists X3, Y3, Z3 r");
|
|
assert_eq!(format(for_all(xyz(), or(pqr()))), "forall X, Y, Z (p or q or r)");
|
|
assert_eq!(format(for_all(xyz(), and(vec![or(pqr())]))), "forall X, Y, Z (p or q or r)");
|
|
assert_eq!(format(for_all(xyz(), or(vec![or(pqr())]))), "forall X, Y, Z (p or q or r)");
|
|
assert_eq!(format(for_all(xyz(),
|
|
if_and_only_if(vec![or(pqr())]))),
|
|
"forall X, Y, Z (p or q or r)");
|
|
assert_eq!(format(
|
|
or(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()), for_all(x3y3z3(), r())])),
|
|
"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]),
|
|
and(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]),
|
|
or(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]),
|
|
if_and_only_if(vec![for_all(x2y2z2(), q())]),
|
|
if_and_only_if(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p or forall X2, Y2, Z2 q or forall X3, Y3, Z3 r");
|
|
|
|
// Quantified formula + implies
|
|
assert_eq!(format(exists(xyz(), implies_right(p(), q()))), "exists X, Y, Z (p -> q)");
|
|
assert_eq!(format(
|
|
exists(xyz(), and(vec![implies_right(p(), q())]))),
|
|
"exists X, Y, Z (p -> q)");
|
|
assert_eq!(format(
|
|
exists(xyz(), or(vec![implies_right(p(), q())]))),
|
|
"exists X, Y, Z (p -> q)");
|
|
assert_eq!(format(
|
|
exists(xyz(), if_and_only_if(vec![implies_right(p(), q())]))),
|
|
"exists X, Y, Z (p -> q)");
|
|
assert_eq!(format(exists(xyz(), implies_left(p(), q()))), "exists X, Y, Z (q <- p)");
|
|
assert_eq!(format(
|
|
exists(xyz(), and(vec![implies_left(p(), q())]))),
|
|
"exists X, Y, Z (q <- p)");
|
|
assert_eq!(format(
|
|
exists(xyz(), or(vec![implies_left(p(), q())]))),
|
|
"exists X, Y, Z (q <- p)");
|
|
assert_eq!(format(
|
|
exists(xyz(), if_and_only_if(vec![implies_left(p(), q())]))),
|
|
"exists X, Y, Z (q <- p)");
|
|
assert_eq!(format(
|
|
implies_right(exists(x1y1z1(), p()), exists(x2y2z2(), q()))),
|
|
"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
|
|
assert_eq!(format(
|
|
implies_right(and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]))),
|
|
"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
|
|
assert_eq!(format(
|
|
implies_right(or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]))),
|
|
"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
|
|
assert_eq!(format(
|
|
implies_right(if_and_only_if(vec![exists(x1y1z1(), p())]),
|
|
if_and_only_if(vec![exists(x2y2z2(), q())]))),
|
|
"exists X1, Y1, Z1 p -> exists X2, Y2, Z2 q");
|
|
assert_eq!(format(
|
|
implies_left(exists(x1y1z1(), p()), exists(x2y2z2(), q()))),
|
|
"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
|
|
assert_eq!(format(
|
|
implies_left(and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]))),
|
|
"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
|
|
assert_eq!(format(
|
|
implies_left(or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]))),
|
|
"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
|
|
assert_eq!(format(
|
|
implies_left(if_and_only_if(vec![exists(x1y1z1(), p())]),
|
|
if_and_only_if(vec![exists(x2y2z2(), q())]))),
|
|
"exists X2, Y2, Z2 q <- exists X1, Y1, Z1 p");
|
|
assert_eq!(format(for_all(xyz(), implies_right(p(), q()))), "forall X, Y, Z (p -> q)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), and(vec![implies_right(p(), q())]))),
|
|
"forall X, Y, Z (p -> q)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), or(vec![implies_right(p(), q())]))),
|
|
"forall X, Y, Z (p -> q)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), if_and_only_if(vec![implies_right(p(), q())]))),
|
|
"forall X, Y, Z (p -> q)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), implies_left(p(), q()))),
|
|
"forall X, Y, Z (q <- p)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), and(vec![implies_left(p(), q())]))),
|
|
"forall X, Y, Z (q <- p)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), or(vec![implies_left(p(), q())]))),
|
|
"forall X, Y, Z (q <- p)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), if_and_only_if(vec![implies_left(p(), q())]))),
|
|
"forall X, Y, Z (q <- p)");
|
|
assert_eq!(format(
|
|
implies_right(for_all(x1y1z1(), p()), for_all(x2y2z2(), q()))),
|
|
"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
|
|
assert_eq!(format(
|
|
implies_right(and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]))),
|
|
"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
|
|
assert_eq!(format(
|
|
implies_right(or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]))),
|
|
"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
|
|
assert_eq!(format(
|
|
implies_right(if_and_only_if(vec![for_all(x1y1z1(), p())]),
|
|
if_and_only_if(vec![for_all(x2y2z2(), q())]))),
|
|
"forall X1, Y1, Z1 p -> forall X2, Y2, Z2 q");
|
|
assert_eq!(format(
|
|
implies_left(for_all(x1y1z1(), p()), for_all(x2y2z2(), q()))),
|
|
"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
|
|
assert_eq!(format(
|
|
implies_left(and(vec![for_all(x1y1z1(), p())]), and(vec![for_all(x2y2z2(), q())]))),
|
|
"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
|
|
assert_eq!(format(
|
|
implies_left(or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]))),
|
|
"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
|
|
assert_eq!(format(
|
|
implies_left(if_and_only_if(vec![for_all(x1y1z1(), p())]),
|
|
if_and_only_if(vec![for_all(x2y2z2(), q())]))),
|
|
"forall X2, Y2, Z2 q <- forall X1, Y1, Z1 p");
|
|
|
|
// Quantified formula + if and only if
|
|
assert_eq!(format(exists(xyz(), if_and_only_if(pqr()))), "exists X, Y, Z (p <-> q <-> r)");
|
|
assert_eq!(format(
|
|
exists(xyz(), and(vec![if_and_only_if(pqr())]))),
|
|
"exists X, Y, Z (p <-> q <-> r)");
|
|
assert_eq!(format(
|
|
exists(xyz(), or(vec![if_and_only_if(pqr())]))),
|
|
"exists X, Y, Z (p <-> q <-> r)");
|
|
assert_eq!(format(
|
|
exists(xyz(), if_and_only_if(vec![if_and_only_if(pqr())]))),
|
|
"exists X, Y, Z (p <-> q <-> r)");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![exists(x1y1z1(), p()), exists(x2y2z2(), q()),
|
|
exists(x3y3z3(), r())])),
|
|
"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(vec![exists(x1y1z1(), p())]), and(vec![exists(x2y2z2(), q())]),
|
|
and(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(vec![exists(x1y1z1(), p())]), or(vec![exists(x2y2z2(), q())]),
|
|
or(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![if_and_only_if(vec![exists(x1y1z1(), p())]),
|
|
if_and_only_if(vec![exists(x2y2z2(), q())]),
|
|
if_and_only_if(vec![exists(x3y3z3(), r())])])),
|
|
"exists X1, Y1, Z1 p <-> exists X2, Y2, Z2 q <-> exists X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
for_all(xyz(), if_and_only_if(pqr()))),
|
|
"forall X, Y, Z (p <-> q <-> r)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), and(vec![if_and_only_if(pqr())]))),
|
|
"forall X, Y, Z (p <-> q <-> r)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), or(vec![if_and_only_if(pqr())]))),
|
|
"forall X, Y, Z (p <-> q <-> r)");
|
|
assert_eq!(format(
|
|
for_all(xyz(), if_and_only_if(vec![if_and_only_if(pqr())]))),
|
|
"forall X, Y, Z (p <-> q <-> r)");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![for_all(x1y1z1(), p()), for_all(x2y2z2(), q()),
|
|
for_all(x3y3z3(), r())])),
|
|
"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(vec![for_all(x1y1z1(), p())]),
|
|
and(vec![for_all(x2y2z2(), q())]), and(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(vec![for_all(x1y1z1(), p())]), or(vec![for_all(x2y2z2(), q())]),
|
|
or(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![if_and_only_if(vec![for_all(x1y1z1(), p())]),
|
|
if_and_only_if(vec![for_all(x2y2z2(), q())]),
|
|
if_and_only_if(vec![for_all(x3y3z3(), r())])])),
|
|
"forall X1, Y1, Z1 p <-> forall X2, Y2, Z2 q <-> forall X3, Y3, Z3 r");
|
|
}
|
|
|
|
#[test]
|
|
fn format_combination_and_and_lower()
|
|
{
|
|
// And + and
|
|
assert_eq!(format(
|
|
and(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]),
|
|
and(vec![and(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]),
|
|
or(vec![and(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![and(vec![p()])]), if_and_only_if(vec![and(vec![q()])]),
|
|
if_and_only_if(vec![and(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])),
|
|
"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]),
|
|
and(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]), or(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]),
|
|
if_and_only_if(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 and p2 and q2 and r2 and p3 and q3 and r3");
|
|
|
|
// And + or
|
|
assert_eq!(format(and(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])), "p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]),
|
|
and(vec![or(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]), or(vec![or(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![or(vec![p()])]), if_and_only_if(vec![or(vec![q()])]),
|
|
if_and_only_if(vec![or(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])),
|
|
"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]), and(vec![or(p3q3r3())])])),
|
|
"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]), or(vec![or(p3q3r3())])])),
|
|
"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![or(p1q1r1())]), if_and_only_if(vec![or(p2q2r2())]),
|
|
if_and_only_if(vec![or(p3q3r3())])])),
|
|
"(p1 or q1 or r1) and (p2 or q2 or r2) and (p3 or q3 or r3)");
|
|
|
|
assert_eq!(format(or(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])), "p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]),
|
|
and(vec![and(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]), or(vec![and(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![and(vec![p()])]), if_and_only_if(vec![and(vec![q()])]),
|
|
if_and_only_if(vec![and(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])),
|
|
"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]), and(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]), or(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]),
|
|
if_and_only_if(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 or p2 and q2 and r2 or p3 and q3 and r3");
|
|
|
|
// And + implies
|
|
assert_eq!(format(
|
|
and(vec![implies_right(p1(), q1()), implies_right(p2(), q2()),
|
|
implies_right(p3(), q3())])),
|
|
"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![implies_right(p1(), q1())]), and(vec![implies_right(p2(), q2())]),
|
|
and(vec![implies_right(p3(), q3())])])),
|
|
"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]),
|
|
or(vec![implies_right(p3(), q3())])])),
|
|
"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![implies_right(p1(), q1())]),
|
|
if_and_only_if(vec![implies_right(p2(), q2())]),
|
|
if_and_only_if(vec![implies_right(p3(), q3())])])),
|
|
"(p1 -> q1) and (p2 -> q2) and (p3 -> q3)");
|
|
assert_eq!(format(
|
|
and(vec![implies_left(p1(), q1()), implies_left(p2(), q2()),
|
|
implies_left(p3(), q3())])),
|
|
"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]),
|
|
and(vec![implies_left(p3(), q3())])])),
|
|
"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]),
|
|
or(vec![implies_left(p3(), q3())])])),
|
|
"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![implies_left(p1(), q1())]),
|
|
if_and_only_if(vec![implies_left(p2(), q2())]),
|
|
if_and_only_if(vec![implies_left(p3(), q3())])])),
|
|
"(q1 <- p1) and (q2 <- p2) and (q3 <- p3)");
|
|
assert_eq!(format(
|
|
implies_right(and(p1q1r1()), and(p2q2r2()))),
|
|
"p1 and q1 and r1 -> p2 and q2 and r2");
|
|
assert_eq!(format(
|
|
implies_right(and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]))),
|
|
"p1 and q1 and r1 -> p2 and q2 and r2");
|
|
assert_eq!(format(
|
|
implies_right(or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]))),
|
|
"p1 and q1 and r1 -> p2 and q2 and r2");
|
|
assert_eq!(format(
|
|
implies_right(if_and_only_if(vec![and(p1q1r1())]),
|
|
if_and_only_if(vec![and(p2q2r2())]))),
|
|
"p1 and q1 and r1 -> p2 and q2 and r2");
|
|
assert_eq!(format(
|
|
implies_left(and(p1q1r1()), and(p2q2r2()))),
|
|
"p2 and q2 and r2 <- p1 and q1 and r1");
|
|
assert_eq!(format(
|
|
implies_left(and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]))),
|
|
"p2 and q2 and r2 <- p1 and q1 and r1");
|
|
assert_eq!(format(
|
|
implies_left(or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]))),
|
|
"p2 and q2 and r2 <- p1 and q1 and r1");
|
|
assert_eq!(format(
|
|
implies_left(if_and_only_if(vec![and(p1q1r1())]), if_and_only_if(vec![and(p2q2r2())]))),
|
|
"p2 and q2 and r2 <- p1 and q1 and r1");
|
|
|
|
// And + if and only if
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![p()]), if_and_only_if(vec![q()]),
|
|
if_and_only_if(vec![r()])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![if_and_only_if(vec![p()])]), and(vec![if_and_only_if(vec![q()])]),
|
|
and(vec![if_and_only_if(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![if_and_only_if(vec![p()])]), or(vec![if_and_only_if(vec![q()])]),
|
|
or(vec![if_and_only_if(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![if_and_only_if(vec![p()])]),
|
|
if_and_only_if(vec![if_and_only_if(vec![q()])]),
|
|
if_and_only_if(vec![if_and_only_if(vec![r()])])])),
|
|
"p and q and r");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()),
|
|
if_and_only_if(p3q3r3())])),
|
|
"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
|
|
assert_eq!(format(
|
|
and(vec![and(vec![if_and_only_if(p1q1r1())]), and(vec![if_and_only_if(p2q2r2())]),
|
|
and(vec![if_and_only_if(p3q3r3())])])),
|
|
"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
|
|
assert_eq!(format(
|
|
and(vec![or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]),
|
|
or(vec![if_and_only_if(p3q3r3())])])),
|
|
"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
|
|
assert_eq!(format(
|
|
and(vec![if_and_only_if(vec![if_and_only_if(p1q1r1())]),
|
|
if_and_only_if(vec![if_and_only_if(p2q2r2())]),
|
|
if_and_only_if(vec![if_and_only_if(p3q3r3())])])),
|
|
"(p1 <-> q1 <-> r1) and (p2 <-> q2 <-> r2) and (p3 <-> q3 <-> r3)");
|
|
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(vec![p()]), and(vec![q()]), and(vec![r()])])),
|
|
"p <-> q <-> r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(vec![and(vec![p()])]), and(vec![and(vec![q()])]),
|
|
and(vec![and(vec![r()])])])),
|
|
"p <-> q <-> r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(vec![and(vec![p()])]), or(vec![and(vec![q()])]),
|
|
or(vec![and(vec![r()])])])),
|
|
"p <-> q <-> r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![if_and_only_if(vec![and(vec![p()])]),
|
|
if_and_only_if(vec![and(vec![q()])]), if_and_only_if(vec![and(vec![r()])])])),
|
|
"p <-> q <-> r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(p1q1r1()), and(p2q2r2()), and(p3q3r3())])),
|
|
"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(vec![and(p1q1r1())]), and(vec![and(p2q2r2())]),
|
|
and(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(vec![and(p1q1r1())]), or(vec![and(p2q2r2())]),
|
|
or(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![if_and_only_if(vec![and(p1q1r1())]),
|
|
if_and_only_if(vec![and(p2q2r2())]), if_and_only_if(vec![and(p3q3r3())])])),
|
|
"p1 and q1 and r1 <-> p2 and q2 and r2 <-> p3 and q3 and r3");
|
|
}
|
|
|
|
#[test]
|
|
fn format_combination_or_and_lower()
|
|
{
|
|
// Or + or
|
|
assert_eq!(format(
|
|
or(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]), and(vec![or(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]),
|
|
or(vec![or(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![or(vec![p()])]), if_and_only_if(vec![or(vec![q()])]),
|
|
if_and_only_if(vec![or(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])),
|
|
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]), and(vec![or(p3q3r3())])])),
|
|
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]), or(vec![or(p3q3r3())])])),
|
|
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![or(p1q1r1())]), if_and_only_if(vec![or(p2q2r2())]),
|
|
if_and_only_if(vec![or(p3q3r3())])])),
|
|
"p1 or q1 or r1 or p2 or q2 or r2 or p3 or q3 or r3");
|
|
|
|
// Or + implies
|
|
assert_eq!(format(
|
|
or(vec![implies_right(p1(), q1()), implies_right(p2(), q2()),
|
|
implies_right(p3(), q3())])),
|
|
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![implies_right(p1(), q1())]), and(vec![implies_right(p2(), q2())]),
|
|
and(vec![implies_right(p3(), q3())])])),
|
|
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]),
|
|
or(vec![implies_right(p3(), q3())])])),
|
|
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![implies_right(p1(), q1())]),
|
|
if_and_only_if(vec![implies_right(p2(), q2())]),
|
|
if_and_only_if(vec![implies_right(p3(), q3())])])),
|
|
"(p1 -> q1) or (p2 -> q2) or (p3 -> q3)");
|
|
assert_eq!(format(
|
|
or(vec![implies_left(p1(), q1()), implies_left(p2(), q2()),
|
|
implies_left(p3(), q3())])),
|
|
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]),
|
|
and(vec![implies_left(p3(), q3())])])),
|
|
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]),
|
|
or(vec![implies_left(p3(), q3())])])),
|
|
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![implies_left(p1(), q1())]),
|
|
if_and_only_if(vec![implies_left(p2(), q2())]),
|
|
if_and_only_if(vec![implies_left(p3(), q3())])])),
|
|
"(q1 <- p1) or (q2 <- p2) or (q3 <- p3)");
|
|
assert_eq!(format(
|
|
implies_right(or(p1q1r1()), or(p2q2r2()))),
|
|
"p1 or q1 or r1 -> p2 or q2 or r2");
|
|
assert_eq!(format(
|
|
implies_right(and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]))),
|
|
"p1 or q1 or r1 -> p2 or q2 or r2");
|
|
assert_eq!(format(
|
|
implies_right(or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]))),
|
|
"p1 or q1 or r1 -> p2 or q2 or r2");
|
|
assert_eq!(format(
|
|
implies_right(if_and_only_if(vec![or(p1q1r1())]),
|
|
if_and_only_if(vec![or(p2q2r2())]))),
|
|
"p1 or q1 or r1 -> p2 or q2 or r2");
|
|
assert_eq!(format(
|
|
implies_left(or(p1q1r1()), or(p2q2r2()))),
|
|
"p2 or q2 or r2 <- p1 or q1 or r1");
|
|
assert_eq!(format(
|
|
implies_left(and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]))),
|
|
"p2 or q2 or r2 <- p1 or q1 or r1");
|
|
assert_eq!(format(
|
|
implies_left(or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]))),
|
|
"p2 or q2 or r2 <- p1 or q1 or r1");
|
|
assert_eq!(format(
|
|
implies_left(if_and_only_if(vec![or(p1q1r1())]), if_and_only_if(vec![or(p2q2r2())]))),
|
|
"p2 or q2 or r2 <- p1 or q1 or r1");
|
|
|
|
// Or + if and only if
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![p()]), if_and_only_if(vec![q()]),
|
|
if_and_only_if(vec![r()])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![if_and_only_if(vec![p()])]), and(vec![if_and_only_if(vec![q()])]),
|
|
and(vec![if_and_only_if(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![if_and_only_if(vec![p()])]), or(vec![if_and_only_if(vec![q()])]),
|
|
or(vec![if_and_only_if(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![if_and_only_if(vec![p()])]),
|
|
if_and_only_if(vec![if_and_only_if(vec![q()])]),
|
|
if_and_only_if(vec![if_and_only_if(vec![r()])])])),
|
|
"p or q or r");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(p1q1r1()), if_and_only_if(p2q2r2()),
|
|
if_and_only_if(p3q3r3())])),
|
|
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
|
|
assert_eq!(format(
|
|
or(vec![and(vec![if_and_only_if(p1q1r1())]), and(vec![if_and_only_if(p2q2r2())]),
|
|
and(vec![if_and_only_if(p3q3r3())])])),
|
|
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
|
|
assert_eq!(format(
|
|
or(vec![or(vec![if_and_only_if(p1q1r1())]), or(vec![if_and_only_if(p2q2r2())]),
|
|
or(vec![if_and_only_if(p3q3r3())])])),
|
|
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
|
|
assert_eq!(format(
|
|
or(vec![if_and_only_if(vec![if_and_only_if(p1q1r1())]),
|
|
if_and_only_if(vec![if_and_only_if(p2q2r2())]),
|
|
if_and_only_if(vec![if_and_only_if(p3q3r3())])])),
|
|
"(p1 <-> q1 <-> r1) or (p2 <-> q2 <-> r2) or (p3 <-> q3 <-> r3)");
|
|
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(vec![p()]), or(vec![q()]), or(vec![r()])])),
|
|
"p <-> q <-> r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(vec![or(vec![p()])]), and(vec![or(vec![q()])]),
|
|
and(vec![or(vec![r()])])])),
|
|
"p <-> q <-> r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(vec![or(vec![p()])]), or(vec![or(vec![q()])]),
|
|
or(vec![or(vec![r()])])])),
|
|
"p <-> q <-> r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![if_and_only_if(vec![or(vec![p()])]),
|
|
if_and_only_if(vec![or(vec![q()])]), if_and_only_if(vec![or(vec![r()])])])),
|
|
"p <-> q <-> r");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(p1q1r1()), or(p2q2r2()), or(p3q3r3())])),
|
|
"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![and(vec![or(p1q1r1())]), and(vec![or(p2q2r2())]),
|
|
and(vec![or(p3q3r3())])])),
|
|
"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![or(vec![or(p1q1r1())]), or(vec![or(p2q2r2())]),
|
|
or(vec![or(p3q3r3())])])),
|
|
"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
|
|
assert_eq!(format(
|
|
if_and_only_if(vec![if_and_only_if(vec![or(p1q1r1())]),
|
|
if_and_only_if(vec![or(p2q2r2())]), if_and_only_if(vec![or(p3q3r3())])])),
|
|
"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
|
|
}
|
|
|
|
#[test]
|
|
fn format_combination_implies_and_lower()
|
|
{
|
|
// Implies + implies
|
|
assert_eq!(format(
|
|
implies_right(implies_right(p1(), q1()), implies_right(p2(), q2()))),
|
|
"(p1 -> q1) -> p2 -> q2");
|
|
assert_eq!(format(
|
|
implies_right(and(vec![implies_right(p1(), q1())]),
|
|
and(vec![implies_right(p2(), q2())]))),
|
|
"(p1 -> q1) -> p2 -> q2");
|
|
assert_eq!(format(
|
|
implies_right(or(vec![implies_right(p1(), q1())]),
|
|
or(vec![implies_right(p2(), q2())]))),
|
|
"(p1 -> q1) -> p2 -> q2");
|
|
assert_eq!(format(
|
|
implies_right(if_and_only_if(vec![implies_right(p1(), q1())]),
|
|
if_and_only_if(vec![implies_right(p2(), q2())]))),
|
|
"(p1 -> q1) -> p2 -> q2");
|
|
assert_eq!(format(
|
|
implies_right(implies_left(p1(), q1()), implies_left(p2(), q2()))),
|
|
"(q1 <- p1) -> (q2 <- p2)");
|
|
assert_eq!(format(
|
|
implies_right(and(vec![implies_left(p1(), q1())]),
|
|
and(vec![implies_left(p2(), q2())]))),
|
|
"(q1 <- p1) -> (q2 <- p2)");
|
|
assert_eq!(format(
|
|
implies_right(or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]))),
|
|
"(q1 <- p1) -> (q2 <- p2)");
|
|
assert_eq!(format(
|
|
implies_right(if_and_only_if(vec![implies_left(p1(), q1())]),
|
|
if_and_only_if(vec![implies_left(p2(), q2())]))),
|
|
"(q1 <- p1) -> (q2 <- p2)");
|
|
assert_eq!(format(
|
|
implies_left(implies_right(p1(), q1()), implies_right(p2(), q2()))),
|
|
"(p2 -> q2) <- (p1 -> q1)");
|
|
assert_eq!(format(
|
|
implies_left(and(vec![implies_right(p1(), q1())]),
|
|
and(vec![implies_right(p2(), q2())]))),
|
|
"(p2 -> q2) <- (p1 -> q1)");
|
|
assert_eq!(format(
|
|
implies_left(or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]))),
|
|
"(p2 -> q2) <- (p1 -> q1)");
|
|
assert_eq!(format(
|
|
implies_left(if_and_only_if(vec![implies_right(p1(), q1())]),
|
|
if_and_only_if(vec![implies_right(p2(), q2())]))),
|
|
"(p2 -> q2) <- (p1 -> q1)");
|
|
assert_eq!(format(
|
|
implies_left(implies_left(p1(), q1()), implies_left(p2(), q2()))),
|
|
"q2 <- p2 <- (q1 <- p1)");
|
|
assert_eq!(format(
|
|
implies_left(and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]))),
|
|
"q2 <- p2 <- (q1 <- p1)");
|
|
assert_eq!(format(
|
|
implies_left(or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]))),
|
|
"q2 <- p2 <- (q1 <- p1)");
|
|
assert_eq!(format(
|
|
implies_left(if_and_only_if(vec![implies_left(p1(), q1())]),
|
|
if_and_only_if(vec![implies_left(p2(), q2())]))),
|
|
"q2 <- p2 <- (q1 <- p1)");
|
|
|
|
// TODO: Implies + if and only if
|
|
}
|
|
}
|