Compare commits

...

No commits in common. "prepare-0.1.0" and "master" have entirely different histories.

3 changed files with 103 additions and 48 deletions

View File

@ -1,4 +1,4 @@
# foliage [![GitHub release](https://img.shields.io/github/release/potassco/foliage.svg?maxAge=3600)](https://github.com/potassco/foliage/releases) [![crates.io](https://img.shields.io/crates/v/foliage.svg?maxAge=3600)](https://crates.io/crates/foliage)
# foliage [![crates.io](https://img.shields.io/crates/v/foliage.svg?maxAge=3600)](https://crates.io/crates/foliage)
> First-order logic with integer arithmetics in Rust

View File

@ -379,7 +379,8 @@ impl Term
Self::boolean(false)
}
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
-> Self
{
Self::Function(Function::new(declaration, arguments))
}
@ -551,7 +552,8 @@ impl Formula
Self::Or(arguments)
}
pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
-> Self
{
Self::Predicate(Predicate::new(declaration, arguments))
}

View File

@ -16,18 +16,25 @@ impl Precedence for crate::Term
| Self::String(_)
| Self::Variable(_)
=> 0,
Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
Self::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
=> 1,
Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
=> 2,
Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
| Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
| Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
=> 3,
Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
| Self::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
=> 4,
Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
Self::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
=> 5,
}
}
@ -60,6 +67,26 @@ impl Precedence for crate::Formula
}
}
impl std::fmt::Debug for crate::SpecialInteger
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
crate::SpecialInteger::Infimum => write!(format, "#inf"),
crate::SpecialInteger::Supremum => write!(format, "#sup"),
}
}
}
impl std::fmt::Display for crate::SpecialInteger
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", &self)
}
}
impl std::fmt::Debug for crate::FunctionDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
@ -114,8 +141,7 @@ struct TermDisplay<'term>
term: &'term crate::Term,
}
fn display_term<'term>(term: &'term crate::Term, parent_precedence: Option<i32>)
-> TermDisplay<'term>
fn display_term(term: &crate::Term, parent_precedence: Option<i32>) -> TermDisplay
{
TermDisplay
{
@ -145,8 +171,7 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
{
crate::Term::Boolean(true) => write!(format, "true"),
crate::Term::Boolean(false) => write!(format, "false"),
crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) => write!(format, "#inf"),
crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) => write!(format, "#sup"),
crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
crate::Term::Integer(value) => write!(format, "{}", value),
crate::Term::String(value) => write!(format, "\"{}\"", value),
crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
@ -155,12 +180,12 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
write!(format, "{}", function.declaration.name)?;
assert!(function.declaration.arity == function.arguments.len(),
"function has a different number of arguments than declared (expected {}, got {})",
"number of function arguments differs from declaration (expected {}, got {})",
function.declaration.arity, function.arguments.len());
if function.arguments.len() > 0
if !function.arguments.is_empty()
{
write!(format, "{}(", function.declaration.name)?;
write!(format, "(")?;
let mut separator = "";
@ -176,21 +201,35 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
Ok(())
},
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
=> write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
=> write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
=> write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
=> write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)),
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
=> write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)),
crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
=> write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)),
crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
=> write!(format, "{:?} + {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
=> write!(format, "{:?} - {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
=> write!(format, "{:?} * {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
=> write!(format, "{:?} / {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
=> write!(format, "{:?} % {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::BinaryOperation(
crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
=> write!(format, "{:?} ** {:?}", display_term(left, precedence),
display_term(right, precedence)),
crate::Term::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
=> write!(format, "-{:?}", display_term(argument, precedence)),
crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
crate::Term::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
=> write!(format, "|{:?}|", display_term(argument, precedence)),
}?;
@ -217,8 +256,7 @@ struct FormulaDisplay<'formula>
formula: &'formula crate::Formula,
}
fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: Option<i32>)
-> FormulaDisplay<'formula>
fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
{
FormulaDisplay
{
@ -280,7 +318,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
},
crate::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
crate::Formula::Not(argument) => write!(format, "not {:?}",
display_formula(argument, precedence))?,
crate::Formula::And(arguments) =>
{
let mut separator = "";
@ -308,21 +347,35 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
}
},
crate::Formula::Implies(crate::Implies{antecedent, implication})
=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?,
=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
display_formula(implication, precedence))?,
crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
=> write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
=> write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
=> write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
=> write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
=> write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
=> write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
display_formula(right, precedence))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
=> write!(format, "{:?} < {:?}", display_term(left, None),
display_term(right, None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
=> write!(format, "{:?} <= {:?}", display_term(left, None),
display_term(right, None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
=> write!(format, "{:?} > {:?}", display_term(left, None),
display_term(right, None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
=> write!(format, "{:?} >= {:?}", display_term(left, None),
display_term(right, None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
=> write!(format, "{:?} = {:?}", display_term(left, None),
display_term(right, None))?,
crate::Formula::Compare(
crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
=> write!(format, "{:?} != {:?}", display_term(left, None),
display_term(right, None))?,
crate::Formula::Boolean(true) => write!(format, "#true")?,
crate::Formula::Boolean(false) => write!(format, "#false")?,
crate::Formula::Predicate(predicate) =>