307 lines
8.3 KiB
Rust
307 lines
8.3 KiB
Rust
fn term_precedence(term: &crate::Term) -> u64
|
|
{
|
|
match term
|
|
{
|
|
crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0,
|
|
crate::Term::Negative(_) => 1,
|
|
crate::Term::Multiply(_, _) => 2,
|
|
crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3,
|
|
}
|
|
}
|
|
|
|
fn formula_precedence(formula: &crate::Formula) -> u64
|
|
{
|
|
match formula
|
|
{
|
|
crate::Formula::Predicate(_) | crate::Formula::Boolean(_) | crate::Formula::Less(_, _) | crate::Formula::LessOrEqual(_, _) | crate::Formula::Greater(_, _) | crate::Formula::GreaterOrEqual(_, _) | crate::Formula::Equal(_, _) | crate::Formula::NotEqual(_, _) => 0,
|
|
crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1,
|
|
crate::Formula::Not(_) => 2,
|
|
crate::Formula::And(_) => 3,
|
|
crate::Formula::Or(_) => 4,
|
|
crate::Formula::Implies(_, _) => 5,
|
|
crate::Formula::Biconditional(_, _) => 6,
|
|
}
|
|
}
|
|
|
|
impl std::fmt::Debug for crate::VariableDeclaration
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match &self.domain
|
|
{
|
|
crate::Domain::Program => write!(format, "X")?,
|
|
crate::Domain::Integer => write!(format, "N")?,
|
|
};
|
|
|
|
write!(format, "{}", &self.name)
|
|
}
|
|
}
|
|
|
|
impl std::fmt::Display for crate::VariableDeclaration
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match &self.domain
|
|
{
|
|
crate::Domain::Program => write!(format, "X")?,
|
|
crate::Domain::Integer => write!(format, "N")?,
|
|
};
|
|
|
|
write!(format, "{}", &self.name)
|
|
}
|
|
}
|
|
|
|
impl std::fmt::Debug for crate::Term
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match *self
|
|
{
|
|
crate::Term::Infimum => write!(format, "#inf"),
|
|
crate::Term::Supremum => write!(format, "#sup"),
|
|
crate::Term::Integer(value) => write!(format, "{}", value),
|
|
crate::Term::Symbolic(ref value) => write!(format, "{}", value),
|
|
crate::Term::String(ref value) => write!(format, "\"{}\"", value),
|
|
crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
|
|
crate::Term::Add(ref left, ref right) => write!(format, "({:?} + {:?})", left, right),
|
|
crate::Term::Subtract(ref left, ref right) => write!(format, "({:?} - {:?})", left, right),
|
|
crate::Term::Multiply(ref left, ref right) => write!(format, "({:?} * {:?})", left, right),
|
|
crate::Term::Negative(ref argument) => write!(format, "-({:?})", argument),
|
|
}
|
|
}
|
|
}
|
|
|
|
impl std::fmt::Display for crate::Term
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match *self
|
|
{
|
|
crate::Term::Infimum => write!(format, "#inf"),
|
|
crate::Term::Supremum => write!(format, "#sup"),
|
|
crate::Term::Integer(value) => write!(format, "{}", value),
|
|
crate::Term::Symbolic(ref value) => write!(format, "{}", value),
|
|
crate::Term::String(ref value) => write!(format, "\"{}\"", value),
|
|
crate::Term::Variable(ref declaration) => write!(format, "{}", declaration),
|
|
crate::Term::Add(ref left, ref right) => write!(format, "({} + {})", left, right),
|
|
crate::Term::Subtract(ref left, ref right) => write!(format, "({} - {})", left, right),
|
|
crate::Term::Multiply(ref left, ref right) => write!(format, "({} * {})", left, right),
|
|
crate::Term::Negative(ref argument) => write!(format, "-({})", argument),
|
|
}
|
|
}
|
|
}
|
|
|
|
impl std::fmt::Debug for crate::Formula
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match *self
|
|
{
|
|
crate::Formula::Exists(ref exists) =>
|
|
{
|
|
write!(format, "exists")?;
|
|
|
|
let mut separator = " ";
|
|
|
|
for parameter in &exists.parameters
|
|
{
|
|
write!(format, "{}{:?}", separator, parameter)?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, " ({:?})", exists.argument)
|
|
},
|
|
crate::Formula::ForAll(ref for_all) =>
|
|
{
|
|
write!(format, "forall")?;
|
|
|
|
let mut separator = " ";
|
|
|
|
for parameter in &for_all.parameters
|
|
{
|
|
write!(format, "{}{:?}", separator, parameter)?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, " ({:?})", for_all.argument)
|
|
},
|
|
crate::Formula::Not(ref argument) => write!(format, "not {:?}", argument),
|
|
crate::Formula::And(ref arguments) =>
|
|
{
|
|
write!(format, "(")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for argument in arguments
|
|
{
|
|
write!(format, "{}{:?}", separator, argument)?;
|
|
|
|
separator = " and "
|
|
}
|
|
|
|
write!(format, ")")
|
|
},
|
|
crate::Formula::Or(ref arguments) =>
|
|
{
|
|
write!(format, "(")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for argument in arguments
|
|
{
|
|
write!(format, "{}{:?}", separator, argument)?;
|
|
|
|
separator = " or "
|
|
}
|
|
|
|
write!(format, ")")
|
|
},
|
|
crate::Formula::Implies(ref left, ref right) => write!(format, "({:?} -> {:?})", left, right),
|
|
crate::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <-> {:?})", left, right),
|
|
crate::Formula::Less(ref left, ref right) => write!(format, "({:?} < {:?})", left, right),
|
|
crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "({:?} <= {:?})", left, right),
|
|
crate::Formula::Greater(ref left, ref right) => write!(format, "({:?} > {:?})", left, right),
|
|
crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({:?} >= {:?})", left, right),
|
|
crate::Formula::Equal(ref left, ref right) => write!(format, "({:?} = {:?})", left, right),
|
|
crate::Formula::NotEqual(ref left, ref right) => write!(format, "({:?} != {:?})", left, right),
|
|
crate::Formula::Boolean(value) =>
|
|
match value
|
|
{
|
|
true => write!(format, "#true"),
|
|
false => write!(format, "#false"),
|
|
},
|
|
crate::Formula::Predicate(ref predicate) =>
|
|
{
|
|
write!(format, "{}", predicate.declaration.name)?;
|
|
|
|
if !predicate.arguments.is_empty()
|
|
{
|
|
write!(format, "(")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for argument in &predicate.arguments
|
|
{
|
|
write!(format, "{}{:?}", separator, argument)?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, ")")?;
|
|
}
|
|
|
|
Ok(())
|
|
},
|
|
}
|
|
}
|
|
}
|
|
|
|
impl std::fmt::Display for crate::Formula
|
|
{
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
{
|
|
match *self
|
|
{
|
|
crate::Formula::Exists(ref exists) =>
|
|
{
|
|
write!(format, "exists")?;
|
|
|
|
let mut separator = " ";
|
|
|
|
for parameter in &exists.parameters
|
|
{
|
|
write!(format, "{}{}", separator, parameter)?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, " ({})", exists.argument)
|
|
},
|
|
crate::Formula::ForAll(ref for_all) =>
|
|
{
|
|
write!(format, "forall")?;
|
|
|
|
let mut separator = " ";
|
|
|
|
for parameter in &for_all.parameters
|
|
{
|
|
write!(format, "{}{}", separator, parameter)?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, " ({})", for_all.argument)
|
|
},
|
|
crate::Formula::Not(ref argument) => write!(format, "not {}", argument),
|
|
crate::Formula::And(ref arguments) =>
|
|
{
|
|
write!(format, "(")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for argument in arguments
|
|
{
|
|
write!(format, "{}{}", separator, argument)?;
|
|
|
|
separator = " and "
|
|
}
|
|
|
|
write!(format, ")")
|
|
},
|
|
crate::Formula::Or(ref arguments) =>
|
|
{
|
|
write!(format, "(")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for argument in arguments
|
|
{
|
|
write!(format, "{}{}", separator, argument)?;
|
|
|
|
separator = " or "
|
|
}
|
|
|
|
write!(format, ")")
|
|
},
|
|
crate::Formula::Implies(ref left, ref right) => write!(format, "({} -> {})", left, right),
|
|
crate::Formula::Biconditional(ref left, ref right) => write!(format, "({} <-> {})", left, right),
|
|
crate::Formula::Less(ref left, ref right) => write!(format, "({} < {})", left, right),
|
|
crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "({} <= {})", left, right),
|
|
crate::Formula::Greater(ref left, ref right) => write!(format, "({} > {})", left, right),
|
|
crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({} >= {})", left, right),
|
|
crate::Formula::Equal(ref left, ref right) => write!(format, "({} = {})", left, right),
|
|
crate::Formula::NotEqual(ref left, ref right) => write!(format, "({} != {})", left, right),
|
|
crate::Formula::Boolean(value) =>
|
|
match value
|
|
{
|
|
true => write!(format, "#true"),
|
|
false => write!(format, "#false"),
|
|
},
|
|
crate::Formula::Predicate(ref predicate) =>
|
|
{
|
|
write!(format, "{}", predicate.declaration.name)?;
|
|
|
|
if !predicate.arguments.is_empty()
|
|
{
|
|
write!(format, "(")?;
|
|
|
|
let mut separator = "";
|
|
|
|
for argument in &predicate.arguments
|
|
{
|
|
write!(format, "{}{}", separator, argument)?;
|
|
|
|
separator = ", "
|
|
}
|
|
|
|
write!(format, ")")?;
|
|
}
|
|
|
|
Ok(())
|
|
},
|
|
}
|
|
}
|
|
}
|