2020-03-30 04:27:58 +02:00
|
|
|
|
use super::*;
|
|
|
|
|
|
|
|
|
|
impl super::Precedence for crate::Formula
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
fn precedence_level(&self) -> i32
|
2020-03-30 04:27:58 +02:00
|
|
|
|
{
|
|
|
|
|
match &self
|
|
|
|
|
{
|
|
|
|
|
Self::Predicate(_)
|
|
|
|
|
| Self::Boolean(_)
|
|
|
|
|
| Self::Compare(_)
|
|
|
|
|
=> 0,
|
|
|
|
|
Self::Exists(_)
|
|
|
|
|
| Self::ForAll(_)
|
|
|
|
|
=> 1,
|
|
|
|
|
Self::Not(_)
|
|
|
|
|
=> 2,
|
|
|
|
|
Self::And(_)
|
|
|
|
|
=> 3,
|
|
|
|
|
Self::Or(_)
|
|
|
|
|
=> 4,
|
|
|
|
|
Self::Implies(_)
|
|
|
|
|
=> 5,
|
|
|
|
|
Self::IfAndOnlyIf(_)
|
|
|
|
|
=> 6,
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
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>
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
parentheses: Parentheses,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
formula: &'formula crate::Formula,
|
|
|
|
|
}
|
|
|
|
|
|
2020-03-30 08:04:09 +02:00
|
|
|
|
fn display_formula(formula: &crate::Formula, parentheses: Parentheses) -> FormulaDisplay
|
2020-03-30 04:27:58 +02:00
|
|
|
|
{
|
|
|
|
|
FormulaDisplay
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
parentheses,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
formula,
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|
|
|
|
{
|
|
|
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
let precedence_level = self.formula.precedence_level();
|
|
|
|
|
let requires_parentheses = match self.parentheses
|
2020-03-30 04:27:58 +02:00
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
Parentheses::None => false,
|
|
|
|
|
Parentheses::PrecedenceBased(parent_precedence_level)
|
|
|
|
|
=> precedence_level > parent_precedence_level,
|
|
|
|
|
Parentheses::Required => true,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
};
|
2020-03-30 08:04:09 +02:00
|
|
|
|
let parentheses = Parentheses::PrecedenceBased(precedence_level);
|
2020-03-30 04:27:58 +02:00
|
|
|
|
|
|
|
|
|
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 = ", "
|
|
|
|
|
}
|
|
|
|
|
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, " {:?}", display_formula(&exists.argument, parentheses))?;
|
2020-03-30 04:27:58 +02:00
|
|
|
|
},
|
|
|
|
|
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 = ", "
|
|
|
|
|
}
|
|
|
|
|
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, " {:?}", display_formula(&for_all.argument, parentheses))?;
|
2020-03-30 04:27:58 +02:00
|
|
|
|
},
|
|
|
|
|
crate::Formula::Not(argument) => write!(format, "not {:?}",
|
2020-03-30 08:04:09 +02:00
|
|
|
|
display_formula(argument, parentheses))?,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
crate::Formula::And(arguments) =>
|
|
|
|
|
{
|
|
|
|
|
let mut separator = "";
|
|
|
|
|
|
|
|
|
|
assert!(!arguments.is_empty());
|
|
|
|
|
|
|
|
|
|
for argument in arguments
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?;
|
2020-03-30 04:27:58 +02:00
|
|
|
|
|
|
|
|
|
separator = " and "
|
|
|
|
|
}
|
|
|
|
|
},
|
|
|
|
|
crate::Formula::Or(arguments) =>
|
|
|
|
|
{
|
|
|
|
|
let mut separator = "";
|
|
|
|
|
|
|
|
|
|
assert!(!arguments.is_empty());
|
|
|
|
|
|
|
|
|
|
for argument in arguments
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?;
|
2020-03-30 04:27:58 +02:00
|
|
|
|
|
|
|
|
|
separator = " or "
|
|
|
|
|
}
|
|
|
|
|
},
|
|
|
|
|
crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
let antecedent_parentheses = match **antecedent
|
2020-03-30 07:29:11 +02:00
|
|
|
|
{
|
|
|
|
|
// Implication is right-associative and thus requires parentheses when nested on
|
|
|
|
|
// the antecedent side
|
2020-03-30 08:04:09 +02:00
|
|
|
|
crate::Formula::Implies(_) => Parentheses::Required,
|
|
|
|
|
_ => parentheses,
|
2020-03-30 07:29:11 +02:00
|
|
|
|
};
|
|
|
|
|
|
2020-03-30 08:04:09 +02:00
|
|
|
|
let implication_parentheses = match **antecedent
|
2020-03-30 07:29:11 +02:00
|
|
|
|
{
|
|
|
|
|
// Implication is right-associative and thus doesn’t require parentheses when
|
|
|
|
|
// nested on the implication side with the same implication direction
|
|
|
|
|
crate::Formula::Implies(crate::Implies{direction: nested_direction, ..})
|
2020-03-30 08:04:09 +02:00
|
|
|
|
if nested_direction == *direction => Parentheses::None,
|
2020-03-30 07:29:11 +02:00
|
|
|
|
// If the nested implication is in the other direction, parentheses are needed
|
2020-03-30 08:04:09 +02:00
|
|
|
|
crate::Formula::Implies(_) => Parentheses::Required,
|
|
|
|
|
_ => parentheses,
|
2020-03-30 07:29:11 +02:00
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, "{:?}", display_formula(antecedent, antecedent_parentheses))
|
2020-03-30 07:29:11 +02:00
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, "{:?}", display_formula(implication, implication_parentheses))
|
2020-03-30 07:29:11 +02:00
|
|
|
|
};
|
|
|
|
|
|
2020-03-30 04:27:58 +02:00
|
|
|
|
match direction
|
|
|
|
|
{
|
|
|
|
|
crate::ImplicationDirection::LeftToRight =>
|
2020-03-30 07:29:11 +02:00
|
|
|
|
{
|
|
|
|
|
format_antecedent(format)?;
|
|
|
|
|
write!(format, " -> ")?;
|
|
|
|
|
format_implication(format)?;
|
|
|
|
|
},
|
2020-03-30 04:27:58 +02:00
|
|
|
|
crate::ImplicationDirection::RightToLeft =>
|
2020-03-30 07:29:11 +02:00
|
|
|
|
{
|
|
|
|
|
format_implication(format)?;
|
|
|
|
|
write!(format, " <- ")?;
|
|
|
|
|
format_antecedent(format)?;
|
|
|
|
|
},
|
|
|
|
|
}
|
2020-03-30 04:27:58 +02:00
|
|
|
|
},
|
|
|
|
|
crate::Formula::IfAndOnlyIf(arguments) =>
|
|
|
|
|
{
|
|
|
|
|
let mut separator = "";
|
|
|
|
|
|
|
|
|
|
for argument in arguments
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, "{}{:?}", separator, display_formula(argument, parentheses))?;
|
2020-03-30 04:27:58 +02:00
|
|
|
|
|
|
|
|
|
separator = " <-> ";
|
|
|
|
|
}
|
|
|
|
|
},
|
|
|
|
|
crate::Formula::Compare(
|
|
|
|
|
crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
|
2020-03-30 08:04:09 +02:00
|
|
|
|
=> write!(format, "{:?} < {:?}", display_term(left, Parentheses::None),
|
|
|
|
|
display_term(right, Parentheses::None))?,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
crate::Formula::Compare(
|
|
|
|
|
crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
|
2020-03-30 08:04:09 +02:00
|
|
|
|
=> write!(format, "{:?} <= {:?}", display_term(left, Parentheses::None),
|
|
|
|
|
display_term(right, Parentheses::None))?,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
crate::Formula::Compare(
|
|
|
|
|
crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
|
2020-03-30 08:04:09 +02:00
|
|
|
|
=> write!(format, "{:?} > {:?}", display_term(left, Parentheses::None),
|
|
|
|
|
display_term(right, Parentheses::None))?,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
crate::Formula::Compare(
|
|
|
|
|
crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
|
2020-03-30 08:04:09 +02:00
|
|
|
|
=> write!(format, "{:?} >= {:?}", display_term(left, Parentheses::None),
|
|
|
|
|
display_term(right, Parentheses::None))?,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
crate::Formula::Compare(
|
|
|
|
|
crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
|
2020-03-30 08:04:09 +02:00
|
|
|
|
=> write!(format, "{:?} = {:?}", display_term(left, Parentheses::None),
|
|
|
|
|
display_term(right, Parentheses::None))?,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
crate::Formula::Compare(
|
|
|
|
|
crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
|
2020-03-30 08:04:09 +02:00
|
|
|
|
=> write!(format, "{:?} != {:?}", display_term(left, Parentheses::None),
|
|
|
|
|
display_term(right, Parentheses::None))?,
|
2020-03-30 04:27:58 +02:00
|
|
|
|
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
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, "{}{:?}", separator,
|
|
|
|
|
display_term(argument, Parentheses::None))?;
|
2020-03-30 04:27:58 +02:00
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, "{:?}", display_formula(&self, Parentheses::None))
|
2020-03-30 04:27:58 +02:00
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
impl std::fmt::Display for crate::Formula
|
|
|
|
|
{
|
|
|
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
|
|
|
{
|
2020-03-30 08:04:09 +02:00
|
|
|
|
write!(format, "{}", display_formula(&self, Parentheses::None))
|
2020-03-30 04:27:58 +02:00
|
|
|
|
}
|
|
|
|
|
}
|
2020-03-30 05:10:59 +02:00
|
|
|
|
|
|
|
|
|
#[cfg(test)]
|
|
|
|
|
mod tests
|
|
|
|
|
{
|
|
|
|
|
use crate::*;
|
2020-04-01 10:53:11 +02:00
|
|
|
|
use crate::format::terms::tests::*;
|
2020-03-30 05:10:59 +02:00
|
|
|
|
|
2020-04-01 10:53:11 +02:00
|
|
|
|
fn format(formula: Box<ast::Formula>) -> String
|
2020-03-30 05:10:59 +02:00
|
|
|
|
{
|
|
|
|
|
format!("{}", formula)
|
|
|
|
|
}
|
|
|
|
|
|
2020-04-01 10:53:11 +02:00
|
|
|
|
fn equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
|
|
|
|
|
{
|
|
|
|
|
Box::new(Formula::equal(left, right))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn false_() -> Box<Formula>
|
|
|
|
|
{
|
|
|
|
|
Box::new(Formula::false_())
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
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 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_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
|
|
|
|
|
{
|
|
|
|
|
Box::new(Formula::not_equal(left, right))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
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");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[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
|
|
|
|
|
}
|
|
|
|
|
|
2020-03-30 05:10:59 +02:00
|
|
|
|
#[test]
|
2020-04-01 10:53:11 +02:00
|
|
|
|
fn format_predicate_declaration()
|
2020-03-30 05:10:59 +02:00
|
|
|
|
{
|
2020-04-01 10:53:11 +02:00
|
|
|
|
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");
|
2020-03-30 05:10:59 +02:00
|
|
|
|
}
|
|
|
|
|
}
|