Upgrade to foliage 0.2 development version
This commit is contained in:
parent
f83695b5dc
commit
becd8d4c19
@ -5,7 +5,7 @@ authors = ["Patrick Lühne <patrick@luehne.de>"]
|
|||||||
edition = "2018"
|
edition = "2018"
|
||||||
|
|
||||||
[dependencies]
|
[dependencies]
|
||||||
foliage = "0.1"
|
foliage = {git = "https://github.com/pluehne/foliage", branch = "master"}
|
||||||
log = "0.4"
|
log = "0.4"
|
||||||
pretty_env_logger = "0.4"
|
pretty_env_logger = "0.4"
|
||||||
structopt = "0.3"
|
structopt = "0.3"
|
||||||
|
@ -5,6 +5,7 @@ use structopt::StructOpt as _;
|
|||||||
enum Command
|
enum Command
|
||||||
{
|
{
|
||||||
#[structopt(about = "Verifies a logic program against a specification")]
|
#[structopt(about = "Verifies a logic program against a specification")]
|
||||||
|
#[structopt(aliases = &["verify-specification", "verify-spec", "vspec"])]
|
||||||
VerifyProgram
|
VerifyProgram
|
||||||
{
|
{
|
||||||
/// ASP input program (one or multiple files)
|
/// ASP input program (one or multiple files)
|
||||||
|
@ -1,403 +1,18 @@
|
|||||||
trait Precedence
|
pub(crate) fn display_variable_declaration<C>(context: &C, formatter: &mut std::fmt::Formatter,
|
||||||
|
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
|
||||||
|
-> std::fmt::Result
|
||||||
|
where C:
|
||||||
|
crate::traits::VariableDeclarationDomain + crate::traits::VariableDeclarationID
|
||||||
{
|
{
|
||||||
fn precedence(&self) -> i32;
|
let id = context.variable_declaration_id(variable_declaration);
|
||||||
}
|
let domain = context.variable_declaration_domain(variable_declaration)
|
||||||
|
.expect("unspecified variable domain");
|
||||||
|
|
||||||
impl Precedence for foliage::Term
|
let prefix = match domain
|
||||||
{
|
|
||||||
fn precedence(&self) -> i32
|
|
||||||
{
|
{
|
||||||
match &self
|
crate::Domain::Integer => "N",
|
||||||
{
|
crate::Domain::Program => "X",
|
||||||
Self::Boolean(_)
|
};
|
||||||
| Self::Function(_)
|
|
||||||
| Self::SpecialInteger(_)
|
write!(formatter, "{}{}", prefix, id + 1)
|
||||||
| Self::Integer(_)
|
|
||||||
| Self::String(_)
|
|
||||||
| Self::Variable(_)
|
|
||||||
=> 0,
|
|
||||||
Self::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::Negative, ..})
|
|
||||||
=> 1,
|
|
||||||
Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Exponentiate, ..})
|
|
||||||
=> 2,
|
|
||||||
Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Multiply, ..})
|
|
||||||
| Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Divide, ..})
|
|
||||||
| Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Modulo, ..})
|
|
||||||
=> 3,
|
|
||||||
Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Add, ..})
|
|
||||||
| Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Subtract, ..})
|
|
||||||
=> 4,
|
|
||||||
Self::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::AbsoluteValue, ..})
|
|
||||||
=> 5,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Precedence for foliage::Formula
|
|
||||||
{
|
|
||||||
fn precedence(&self) -> i32
|
|
||||||
{
|
|
||||||
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,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) struct VariableDeclarationDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
variable_declaration: &'a std::rc::Rc<foliage::VariableDeclaration>,
|
|
||||||
context: &'b C,
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) fn display_variable_declaration<'a, 'b, C>(
|
|
||||||
variable_declaration: &'a std::rc::Rc<foliage::VariableDeclaration>, context: &'b C)
|
|
||||||
-> VariableDeclarationDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
VariableDeclarationDisplay
|
|
||||||
{
|
|
||||||
variable_declaration,
|
|
||||||
context,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a, 'b, C> std::fmt::Debug for VariableDeclarationDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
||||||
{
|
|
||||||
let id = self.context.variable_declaration_id(self.variable_declaration);
|
|
||||||
let domain = self.context.variable_declaration_domain(self.variable_declaration)
|
|
||||||
.expect("unspecified variable domain");
|
|
||||||
|
|
||||||
let prefix = match domain
|
|
||||||
{
|
|
||||||
crate::Domain::Integer => "N",
|
|
||||||
crate::Domain::Program => "X",
|
|
||||||
};
|
|
||||||
|
|
||||||
write!(format, "{}{}", prefix, id + 1)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a, 'b, C> std::fmt::Display for VariableDeclarationDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
||||||
{
|
|
||||||
write!(format, "{:?}", &self)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) struct TermDisplay<'a, 'b, C>
|
|
||||||
{
|
|
||||||
parent_precedence: Option<i32>,
|
|
||||||
term: &'a foliage::Term,
|
|
||||||
context: &'b C,
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) fn display_term<'a, 'b, C>(term: &'a foliage::Term, parent_precedence: Option<i32>,
|
|
||||||
context: &'b C)
|
|
||||||
-> TermDisplay<'a, 'b, C>
|
|
||||||
{
|
|
||||||
TermDisplay
|
|
||||||
{
|
|
||||||
parent_precedence,
|
|
||||||
term,
|
|
||||||
context,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a, 'b, C> std::fmt::Debug for TermDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
||||||
{
|
|
||||||
let display_variable_declaration = |variable_declaration|
|
|
||||||
display_variable_declaration(variable_declaration, self.context);
|
|
||||||
let display_term = |term, precedence| display_term(term, precedence, self.context);
|
|
||||||
|
|
||||||
let precedence = self.term.precedence();
|
|
||||||
let requires_parentheses = match self.parent_precedence
|
|
||||||
{
|
|
||||||
Some(parent_precedence) => precedence > parent_precedence,
|
|
||||||
None => false,
|
|
||||||
};
|
|
||||||
let precedence = Some(precedence);
|
|
||||||
|
|
||||||
if requires_parentheses
|
|
||||||
{
|
|
||||||
write!(format, "(")?;
|
|
||||||
}
|
|
||||||
|
|
||||||
match &self.term
|
|
||||||
{
|
|
||||||
foliage::Term::Boolean(true) => write!(format, "true"),
|
|
||||||
foliage::Term::Boolean(false) => write!(format, "false"),
|
|
||||||
foliage::Term::SpecialInteger(foliage::SpecialInteger::Infimum) => write!(format, "#inf"),
|
|
||||||
foliage::Term::SpecialInteger(foliage::SpecialInteger::Supremum) => write!(format, "#sup"),
|
|
||||||
foliage::Term::Integer(value) => write!(format, "{}", value),
|
|
||||||
foliage::Term::String(value) => write!(format, "\"{}\"", value),
|
|
||||||
foliage::Term::Variable(variable) => write!(format, "{:?}",
|
|
||||||
display_variable_declaration(&variable.declaration)),
|
|
||||||
foliage::Term::Function(function) =>
|
|
||||||
{
|
|
||||||
write!(format, "{}", function.declaration.name)?;
|
|
||||||
|
|
||||||
assert!(function.declaration.arity == function.arguments.len(),
|
|
||||||
"function has a different number of arguments than declared (expected {}, got {})",
|
|
||||||
function.declaration.arity, function.arguments.len());
|
|
||||||
|
|
||||||
if function.arguments.len() > 0
|
|
||||||
{
|
|
||||||
write!(format, "{}(", function.declaration.name)?;
|
|
||||||
|
|
||||||
let mut separator = "";
|
|
||||||
|
|
||||||
for argument in &function.arguments
|
|
||||||
{
|
|
||||||
write!(format, "{}{:?}", separator, display_term(&argument, None))?;
|
|
||||||
|
|
||||||
separator = ", ";
|
|
||||||
}
|
|
||||||
|
|
||||||
write!(format, ")")?;
|
|
||||||
}
|
|
||||||
|
|
||||||
Ok(())
|
|
||||||
},
|
|
||||||
foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Add, left, right})
|
|
||||||
=> write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
|
|
||||||
foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Subtract, left, right})
|
|
||||||
=> write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
|
|
||||||
foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Multiply, left, right})
|
|
||||||
=> write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
|
|
||||||
foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Divide, left, right})
|
|
||||||
=> write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)),
|
|
||||||
foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Modulo, left, right})
|
|
||||||
=> write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)),
|
|
||||||
foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Exponentiate, left, right})
|
|
||||||
=> write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)),
|
|
||||||
foliage::Term::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::Negative, argument})
|
|
||||||
=> write!(format, "-{:?}", display_term(argument, precedence)),
|
|
||||||
foliage::Term::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::AbsoluteValue, argument})
|
|
||||||
=> write!(format, "|{:?}|", display_term(argument, precedence)),
|
|
||||||
}?;
|
|
||||||
|
|
||||||
if requires_parentheses
|
|
||||||
{
|
|
||||||
write!(format, ")")?;
|
|
||||||
}
|
|
||||||
|
|
||||||
Ok(())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a, 'b, C> std::fmt::Display for TermDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
||||||
{
|
|
||||||
write!(format, "{:?}", self)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) struct FormulaDisplay<'a, 'b, C>
|
|
||||||
{
|
|
||||||
parent_precedence: Option<i32>,
|
|
||||||
formula: &'a foliage::Formula,
|
|
||||||
context: &'b C,
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) fn display_formula<'a, 'b, C>(formula: &'a foliage::Formula,
|
|
||||||
parent_precedence: Option<i32>, context: &'b C)
|
|
||||||
-> FormulaDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
FormulaDisplay
|
|
||||||
{
|
|
||||||
parent_precedence,
|
|
||||||
formula,
|
|
||||||
context,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
||||||
{
|
|
||||||
let display_variable_declaration = |variable_declaration|
|
|
||||||
display_variable_declaration(variable_declaration, self.context);
|
|
||||||
let display_term = |term, precedence| display_term(term, precedence, self.context);
|
|
||||||
let display_formula = |formula, precedence| display_formula(formula, precedence, self.context);
|
|
||||||
|
|
||||||
let precedence = self.formula.precedence();
|
|
||||||
let requires_parentheses = match self.parent_precedence
|
|
||||||
{
|
|
||||||
Some(parent_precedence) => precedence > parent_precedence,
|
|
||||||
None => false,
|
|
||||||
};
|
|
||||||
let precedence = Some(precedence);
|
|
||||||
|
|
||||||
if requires_parentheses
|
|
||||||
{
|
|
||||||
write!(format, "(")?;
|
|
||||||
}
|
|
||||||
|
|
||||||
match &self.formula
|
|
||||||
{
|
|
||||||
foliage::Formula::Exists(exists) =>
|
|
||||||
{
|
|
||||||
assert!(!exists.parameters.is_empty());
|
|
||||||
|
|
||||||
write!(format, "exists")?;
|
|
||||||
|
|
||||||
let mut separator = " ";
|
|
||||||
|
|
||||||
for parameter in exists.parameters.iter()
|
|
||||||
{
|
|
||||||
write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?;
|
|
||||||
|
|
||||||
separator = ", "
|
|
||||||
}
|
|
||||||
|
|
||||||
write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
|
|
||||||
},
|
|
||||||
foliage::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, display_variable_declaration(parameter))?;
|
|
||||||
|
|
||||||
separator = ", "
|
|
||||||
}
|
|
||||||
|
|
||||||
write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
|
|
||||||
},
|
|
||||||
foliage::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
|
|
||||||
foliage::Formula::And(arguments) =>
|
|
||||||
{
|
|
||||||
let mut separator = "";
|
|
||||||
|
|
||||||
assert!(!arguments.is_empty());
|
|
||||||
|
|
||||||
for argument in arguments
|
|
||||||
{
|
|
||||||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
|
||||||
|
|
||||||
separator = " and "
|
|
||||||
}
|
|
||||||
},
|
|
||||||
foliage::Formula::Or(arguments) =>
|
|
||||||
{
|
|
||||||
let mut separator = "";
|
|
||||||
|
|
||||||
assert!(!arguments.is_empty());
|
|
||||||
|
|
||||||
for argument in arguments
|
|
||||||
{
|
|
||||||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
|
||||||
|
|
||||||
separator = " or "
|
|
||||||
}
|
|
||||||
},
|
|
||||||
foliage::Formula::Implies(foliage::Implies{antecedent, implication})
|
|
||||||
=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?,
|
|
||||||
foliage::Formula::IfAndOnlyIf(foliage::IfAndOnlyIf{left, right})
|
|
||||||
=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
|
|
||||||
foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right})
|
|
||||||
=> write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
|
|
||||||
foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::LessOrEqual, left, right})
|
|
||||||
=> write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
|
|
||||||
foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Greater, left, right})
|
|
||||||
=> write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
|
|
||||||
foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::GreaterOrEqual, left, right})
|
|
||||||
=> write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
|
|
||||||
foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Equal, left, right})
|
|
||||||
=> write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
|
|
||||||
foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::NotEqual, left, right})
|
|
||||||
=> write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
|
|
||||||
foliage::Formula::Boolean(true) => write!(format, "#true")?,
|
|
||||||
foliage::Formula::Boolean(false) => write!(format, "#false")?,
|
|
||||||
foliage::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, None))?;
|
|
||||||
|
|
||||||
separator = ", "
|
|
||||||
}
|
|
||||||
|
|
||||||
write!(format, ")")?;
|
|
||||||
}
|
|
||||||
},
|
|
||||||
}
|
|
||||||
|
|
||||||
if requires_parentheses
|
|
||||||
{
|
|
||||||
write!(format, ")")?;
|
|
||||||
}
|
|
||||||
|
|
||||||
Ok(())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C>
|
|
||||||
where
|
|
||||||
C: crate::traits::VariableDeclarationDomain
|
|
||||||
+ crate::traits::VariableDeclarationID
|
|
||||||
{
|
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
|
||||||
{
|
|
||||||
write!(format, "{:?}", self)
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
@ -456,12 +456,43 @@ where
|
|||||||
|
|
||||||
write!(format, ")")?;
|
write!(format, ")")?;
|
||||||
},
|
},
|
||||||
foliage::Formula::Implies(foliage::Implies{antecedent, implication})
|
foliage::Formula::Implies(foliage::Implies{antecedent, implication, ..})
|
||||||
=> write!(format, "({:?} => {:?})", display_formula(antecedent),
|
=> write!(format, "({:?} => {:?})", display_formula(antecedent),
|
||||||
display_formula(implication))?,
|
display_formula(implication))?,
|
||||||
foliage::Formula::IfAndOnlyIf(foliage::IfAndOnlyIf{left, right})
|
foliage::Formula::IfAndOnlyIf(arguments) => match arguments.len()
|
||||||
=> write!(format, "({:?} <=> {:?})", display_formula(left),
|
{
|
||||||
display_formula(right))?,
|
0 => write!(format, "$true")?,
|
||||||
|
_ =>
|
||||||
|
{
|
||||||
|
let mut separator = "";
|
||||||
|
let parentheses_required = arguments.len() > 2;
|
||||||
|
|
||||||
|
let mut argument_iterator = arguments.iter().peekable();
|
||||||
|
|
||||||
|
while let Some(argument) = argument_iterator.next()
|
||||||
|
{
|
||||||
|
if let Some(next_argument) = argument_iterator.peek()
|
||||||
|
{
|
||||||
|
write!(format, "{}", separator)?;
|
||||||
|
|
||||||
|
if parentheses_required
|
||||||
|
{
|
||||||
|
write!(format, "(")?;
|
||||||
|
}
|
||||||
|
|
||||||
|
write!(format, "{:?} <=> {:?}", display_formula(argument),
|
||||||
|
display_formula(next_argument))?;
|
||||||
|
|
||||||
|
if parentheses_required
|
||||||
|
{
|
||||||
|
write!(format, ")")?;
|
||||||
|
}
|
||||||
|
|
||||||
|
separator = " & ";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
},
|
||||||
|
},
|
||||||
foliage::Formula::Compare(
|
foliage::Formula::Compare(
|
||||||
foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right})
|
foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right})
|
||||||
=> display_compare(left, right, crate::OperatorNotation::Prefix, "$less",
|
=> display_compare(left, right, crate::OperatorNotation::Prefix, "$less",
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
|
pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
|
||||||
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
|
variable_declaration: std::rc::Rc<foliage::VariableDeclaration>)
|
||||||
-> foliage::Formula
|
-> foliage::Formula
|
||||||
{
|
{
|
||||||
let variable = foliage::Term::variable(variable_declaration);
|
let variable = foliage::Term::variable(variable_declaration);
|
||||||
@ -8,7 +8,7 @@ pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
|
|||||||
}
|
}
|
||||||
|
|
||||||
pub(crate) fn choose_value_in_term<C>(term: &clingo::ast::Term,
|
pub(crate) fn choose_value_in_term<C>(term: &clingo::ast::Term,
|
||||||
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>, context: &C)
|
variable_declaration: std::rc::Rc<foliage::VariableDeclaration>, context: &C)
|
||||||
-> Result<foliage::Formula, crate::Error>
|
-> Result<foliage::Formula, crate::Error>
|
||||||
where
|
where
|
||||||
C: crate::traits::GetOrCreateFunctionDeclaration
|
C: crate::traits::GetOrCreateFunctionDeclaration
|
||||||
@ -42,14 +42,16 @@ where
|
|||||||
// At this point, we only have to handle (0-ary) constants
|
// At this point, we only have to handle (0-ary) constants
|
||||||
if !arguments.is_empty()
|
if !arguments.is_empty()
|
||||||
{
|
{
|
||||||
return Err(crate::Error::new_logic("unexpected arguments, expected (0-ary) constant symbol"));
|
return Err(crate::Error::new_logic(
|
||||||
|
"unexpected arguments, expected (0-ary) constant symbol"));
|
||||||
}
|
}
|
||||||
|
|
||||||
let constant_name = symbol.name()
|
let constant_name = symbol.name()
|
||||||
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
|
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
|
||||||
|
|
||||||
let constant_declaration = context.get_or_create_function_declaration(constant_name, 0);
|
let constant_declaration =
|
||||||
let function = foliage::Term::function(&constant_declaration, vec![]);
|
context.get_or_create_function_declaration(constant_name, 0);
|
||||||
|
let function = foliage::Term::function(constant_declaration, vec![]);
|
||||||
|
|
||||||
Ok(choose_value_in_primitive(Box::new(function), variable_declaration))
|
Ok(choose_value_in_primitive(Box::new(function), variable_declaration))
|
||||||
}
|
}
|
||||||
@ -60,7 +62,7 @@ where
|
|||||||
variable_name);
|
variable_name);
|
||||||
context.assign_variable_declaration_domain(&other_variable_declaration,
|
context.assign_variable_declaration_domain(&other_variable_declaration,
|
||||||
crate::Domain::Program);
|
crate::Domain::Program);
|
||||||
let other_variable = foliage::Term::variable(&other_variable_declaration);
|
let other_variable = foliage::Term::variable(other_variable_declaration);
|
||||||
|
|
||||||
Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration))
|
Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration))
|
||||||
},
|
},
|
||||||
@ -90,22 +92,21 @@ where
|
|||||||
let parameter_2 = ¶meters[1];
|
let parameter_2 = ¶meters[1];
|
||||||
|
|
||||||
let translated_binary_operation = foliage::Term::binary_operation(operator,
|
let translated_binary_operation = foliage::Term::binary_operation(operator,
|
||||||
Box::new(foliage::Term::variable(¶meter_1)),
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(¶meter_1))),
|
||||||
Box::new(foliage::Term::variable(¶meter_2)));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(¶meter_2))));
|
||||||
|
|
||||||
let equals = foliage::Formula::equal(
|
let equals = foliage::Formula::equal(
|
||||||
Box::new(foliage::Term::variable(variable_declaration)),
|
Box::new(foliage::Term::variable(variable_declaration)),
|
||||||
Box::new(translated_binary_operation));
|
Box::new(translated_binary_operation));
|
||||||
|
|
||||||
let choose_value_from_left_argument = choose_value_in_term(
|
let choose_value_from_left_argument = choose_value_in_term(
|
||||||
binary_operation.left(), ¶meter_1, context)?;
|
binary_operation.left(), std::rc::Rc::clone(¶meter_1), context)?;
|
||||||
|
|
||||||
let choose_value_from_right_argument = choose_value_in_term(
|
let choose_value_from_right_argument = choose_value_in_term(
|
||||||
binary_operation.right(), ¶meter_2, context)?;
|
binary_operation.right(), std::rc::Rc::clone(¶meter_2), context)?;
|
||||||
|
|
||||||
let and = foliage::Formula::And(vec![Box::new(equals),
|
let and = foliage::Formula::And(vec![equals, choose_value_from_left_argument,
|
||||||
Box::new(choose_value_from_left_argument),
|
choose_value_from_right_argument]);
|
||||||
Box::new(choose_value_from_right_argument)]);
|
|
||||||
|
|
||||||
Ok(foliage::Formula::exists(parameters, Box::new(and)))
|
Ok(foliage::Formula::exists(parameters, Box::new(and)))
|
||||||
},
|
},
|
||||||
@ -130,40 +131,42 @@ where
|
|||||||
let parameter_r = ¶meters[3];
|
let parameter_r = ¶meters[3];
|
||||||
|
|
||||||
let j_times_q = foliage::Term::multiply(
|
let j_times_q = foliage::Term::multiply(
|
||||||
Box::new(foliage::Term::variable(parameter_j)),
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))),
|
||||||
Box::new(foliage::Term::variable(parameter_q)));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q))));
|
||||||
|
|
||||||
let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q),
|
let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q),
|
||||||
Box::new(foliage::Term::variable(parameter_r)));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))));
|
||||||
|
|
||||||
let i_equals_j_times_q_plus_r = foliage::Formula::equal(
|
let i_equals_j_times_q_plus_r = foliage::Formula::equal(
|
||||||
Box::new(foliage::Term::variable(parameter_j)), Box::new(j_times_q_plus_r));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))),
|
||||||
|
Box::new(j_times_q_plus_r));
|
||||||
|
|
||||||
let choose_i_in_t1 = choose_value_in_term(binary_operation.left(), parameter_i,
|
let choose_i_in_t1 = choose_value_in_term(binary_operation.left(),
|
||||||
context)?;
|
std::rc::Rc::clone(parameter_i), context)?;
|
||||||
|
|
||||||
let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j,
|
let choose_i_in_t2 = choose_value_in_term(binary_operation.left(),
|
||||||
context)?;
|
std::rc::Rc::clone(parameter_j), context)?;
|
||||||
|
|
||||||
let j_not_equal_to_0 = foliage::Formula::not_equal(
|
let j_not_equal_to_0 = foliage::Formula::not_equal(
|
||||||
Box::new(foliage::Term::variable(parameter_j)),
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))),
|
||||||
Box::new(foliage::Term::integer(0)));
|
Box::new(foliage::Term::integer(0)));
|
||||||
|
|
||||||
let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal(
|
let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal(
|
||||||
Box::new(foliage::Term::variable(parameter_r)),
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))),
|
||||||
Box::new(foliage::Term::integer(0)));
|
Box::new(foliage::Term::integer(0)));
|
||||||
|
|
||||||
let r_less_than_q = foliage::Formula::less(
|
let r_less_than_q = foliage::Formula::less(
|
||||||
Box::new(foliage::Term::variable(parameter_r)),
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))),
|
||||||
Box::new(foliage::Term::variable(parameter_q)));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q))));
|
||||||
|
|
||||||
let z_equal_to_q = foliage::Formula::equal(
|
let z_equal_to_q = foliage::Formula::equal(
|
||||||
Box::new(foliage::Term::variable(variable_declaration)),
|
Box::new(
|
||||||
Box::new(foliage::Term::variable(parameter_q)));
|
foliage::Term::variable(std::rc::Rc::clone(&variable_declaration))),
|
||||||
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q))));
|
||||||
|
|
||||||
let z_equal_to_r = foliage::Formula::equal(
|
let z_equal_to_r = foliage::Formula::equal(
|
||||||
Box::new(foliage::Term::variable(variable_declaration)),
|
Box::new(foliage::Term::variable(variable_declaration)),
|
||||||
Box::new(foliage::Term::variable(parameter_r)));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))));
|
||||||
|
|
||||||
let last_argument = match operator
|
let last_argument = match operator
|
||||||
{
|
{
|
||||||
@ -172,10 +175,9 @@ where
|
|||||||
_ => return Err(crate::Error::new_logic("unreachable code")),
|
_ => return Err(crate::Error::new_logic("unreachable code")),
|
||||||
};
|
};
|
||||||
|
|
||||||
let and = foliage::Formula::and(vec![Box::new(i_equals_j_times_q_plus_r),
|
let and = foliage::Formula::and(vec![i_equals_j_times_q_plus_r, choose_i_in_t1,
|
||||||
Box::new(choose_i_in_t1), Box::new(choose_i_in_t2),
|
choose_i_in_t2, j_not_equal_to_0, r_greater_or_equal_to_0, r_less_than_q,
|
||||||
Box::new(j_not_equal_to_0), Box::new(r_greater_or_equal_to_0),
|
last_argument]);
|
||||||
Box::new(r_less_than_q), Box::new(last_argument)]);
|
|
||||||
|
|
||||||
Ok(foliage::Formula::exists(parameters, Box::new(and)))
|
Ok(foliage::Formula::exists(parameters, Box::new(and)))
|
||||||
},
|
},
|
||||||
@ -197,16 +199,15 @@ where
|
|||||||
crate::Domain::Integer);
|
crate::Domain::Integer);
|
||||||
|
|
||||||
let negative_z_prime = foliage::Term::negative(Box::new(
|
let negative_z_prime = foliage::Term::negative(Box::new(
|
||||||
foliage::Term::variable(¶meter_z_prime)));
|
foliage::Term::variable(std::rc::Rc::clone(¶meter_z_prime))));
|
||||||
let equals = foliage::Formula::equal(
|
let equals = foliage::Formula::equal(
|
||||||
Box::new(foliage::Term::variable(variable_declaration)),
|
Box::new(foliage::Term::variable(variable_declaration)),
|
||||||
Box::new(negative_z_prime));
|
Box::new(negative_z_prime));
|
||||||
|
|
||||||
let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(),
|
let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(),
|
||||||
¶meter_z_prime, context)?;
|
std::rc::Rc::clone(¶meter_z_prime), context)?;
|
||||||
|
|
||||||
let and = foliage::Formula::and(vec![Box::new(equals),
|
let and = foliage::Formula::and(vec![equals, choose_z_prime_in_t_prime]);
|
||||||
Box::new(choose_z_prime_in_t_prime)]);
|
|
||||||
|
|
||||||
let parameters = std::rc::Rc::new(vec![parameter_z_prime]);
|
let parameters = std::rc::Rc::new(vec![parameter_z_prime]);
|
||||||
|
|
||||||
@ -232,25 +233,26 @@ where
|
|||||||
let parameter_j = ¶meters[1];
|
let parameter_j = ¶meters[1];
|
||||||
let parameter_k = ¶meters[2];
|
let parameter_k = ¶meters[2];
|
||||||
|
|
||||||
let choose_i_in_t_1 = choose_value_in_term(interval.left(), parameter_i, context)?;
|
let choose_i_in_t_1 = choose_value_in_term(interval.left(),
|
||||||
|
std::rc::Rc::clone(parameter_i), context)?;
|
||||||
|
|
||||||
let choose_j_in_t_2 = choose_value_in_term(interval.right(), parameter_j, context)?;
|
let choose_j_in_t_2 = choose_value_in_term(interval.right(),
|
||||||
|
std::rc::Rc::clone(parameter_j), context)?;
|
||||||
|
|
||||||
let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal(
|
let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal(
|
||||||
Box::new(foliage::Term::variable(parameter_i)),
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_i))),
|
||||||
Box::new(foliage::Term::variable(parameter_k)));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k))));
|
||||||
|
|
||||||
let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal(
|
let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal(
|
||||||
Box::new(foliage::Term::variable(parameter_k)),
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k))),
|
||||||
Box::new(foliage::Term::variable(parameter_j)));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))));
|
||||||
|
|
||||||
let z_equals_k = foliage::Formula::equal(
|
let z_equals_k = foliage::Formula::equal(
|
||||||
Box::new(foliage::Term::variable(variable_declaration)),
|
Box::new(foliage::Term::variable(variable_declaration)),
|
||||||
Box::new(foliage::Term::variable(parameter_k)));
|
Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k))));
|
||||||
|
|
||||||
let and = foliage::Formula::and(vec![Box::new(choose_i_in_t_1),
|
let and = foliage::Formula::and(vec![choose_i_in_t_1, choose_j_in_t_2,
|
||||||
Box::new(choose_j_in_t_2), Box::new(i_less_than_or_equal_to_k),
|
i_less_than_or_equal_to_k, k_less_than_or_equal_to_j, z_equals_k]);
|
||||||
Box::new(k_less_than_or_equal_to_j), Box::new(z_equals_k)]);
|
|
||||||
|
|
||||||
Ok(foliage::Formula::exists(parameters, Box::new(and)))
|
Ok(foliage::Formula::exists(parameters, Box::new(and)))
|
||||||
},
|
},
|
||||||
|
@ -105,7 +105,7 @@ where
|
|||||||
for definition in definitions.definitions.iter()
|
for definition in definitions.definitions.iter()
|
||||||
{
|
{
|
||||||
log::debug!("definition({}/{}): {}.", predicate_declaration.name, predicate_declaration.arity,
|
log::debug!("definition({}/{}): {}.", predicate_declaration.name, predicate_declaration.arity,
|
||||||
crate::output::human_readable::display_formula(&definition.formula, None, &context));
|
foliage::format::display_formula(&definition.formula, &context));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -122,14 +122,14 @@ where
|
|||||||
let or = foliage::Formula::or(or_arguments);
|
let or = foliage::Formula::or(or_arguments);
|
||||||
|
|
||||||
let head_arguments = definitions.head_atom_parameters.iter()
|
let head_arguments = definitions.head_atom_parameters.iter()
|
||||||
.map(|x| Box::new(foliage::Term::variable(x)))
|
.map(|x| foliage::Term::variable(std::rc::Rc::clone(x)))
|
||||||
.collect::<Vec<_>>();
|
.collect::<Vec<_>>();
|
||||||
|
|
||||||
let head_predicate = foliage::Formula::predicate(&predicate_declaration,
|
let head_predicate = foliage::Formula::predicate(
|
||||||
head_arguments);
|
std::rc::Rc::clone(predicate_declaration), head_arguments);
|
||||||
|
|
||||||
let completed_definition = foliage::Formula::if_and_only_if(
|
let completed_definition =
|
||||||
Box::new(head_predicate), Box::new(or));
|
foliage::Formula::if_and_only_if(vec![head_predicate, or]);
|
||||||
|
|
||||||
let scoped_formula = crate::ScopedFormula
|
let scoped_formula = crate::ScopedFormula
|
||||||
{
|
{
|
||||||
@ -154,11 +154,11 @@ where
|
|||||||
.collect::<Vec<_>>());
|
.collect::<Vec<_>>());
|
||||||
|
|
||||||
let head_arguments = head_atom_parameters.iter()
|
let head_arguments = head_atom_parameters.iter()
|
||||||
.map(|x| Box::new(foliage::Term::variable(x)))
|
.map(|x| foliage::Term::variable(std::rc::Rc::clone(x)))
|
||||||
.collect();
|
.collect();
|
||||||
|
|
||||||
let head_predicate = foliage::Formula::predicate(&predicate_declaration,
|
let head_predicate = foliage::Formula::predicate(
|
||||||
head_arguments);
|
std::rc::Rc::clone(predicate_declaration), head_arguments);
|
||||||
|
|
||||||
let not = foliage::Formula::not(Box::new(head_predicate));
|
let not = foliage::Formula::not(Box::new(head_predicate));
|
||||||
|
|
||||||
@ -197,7 +197,7 @@ where
|
|||||||
match output_format
|
match output_format
|
||||||
{
|
{
|
||||||
crate::output::Format::HumanReadable => print!("{}",
|
crate::output::Format::HumanReadable => print!("{}",
|
||||||
crate::output::human_readable::display_formula(formula, None, &context)),
|
foliage::format::display_formula(formula, &context)),
|
||||||
crate::output::Format::TPTP => print!("{}",
|
crate::output::Format::TPTP => print!("{}",
|
||||||
crate::output::tptp::display_formula(formula, &context)),
|
crate::output::tptp::display_formula(formula, &context)),
|
||||||
}
|
}
|
||||||
@ -380,13 +380,13 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
|
|||||||
if let HeadType::ChoiceWithSingleAtom(_) = head_type
|
if let HeadType::ChoiceWithSingleAtom(_) = head_type
|
||||||
{
|
{
|
||||||
let head_arguments = definitions.head_atom_parameters.iter()
|
let head_arguments = definitions.head_atom_parameters.iter()
|
||||||
.map(|x| Box::new(foliage::Term::variable(x)))
|
.map(|x| foliage::Term::variable(std::rc::Rc::clone(x)))
|
||||||
.collect::<Vec<_>>();
|
.collect::<Vec<_>>();
|
||||||
|
|
||||||
let head_predicate = foliage::Formula::predicate(&head_atom.predicate_declaration,
|
let head_predicate = foliage::Formula::predicate(
|
||||||
head_arguments);
|
std::rc::Rc::clone(&head_atom.predicate_declaration), head_arguments);
|
||||||
|
|
||||||
definition_arguments.push(Box::new(head_predicate));
|
definition_arguments.push(head_predicate);
|
||||||
}
|
}
|
||||||
|
|
||||||
let mut head_atom_arguments_iterator = head_atom.arguments.iter();
|
let mut head_atom_arguments_iterator = head_atom.arguments.iter();
|
||||||
@ -396,9 +396,9 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
|
|||||||
let head_atom_argument = head_atom_arguments_iterator.next().unwrap();
|
let head_atom_argument = head_atom_arguments_iterator.next().unwrap();
|
||||||
|
|
||||||
let translated_head_term = crate::translate::common::choose_value_in_term(
|
let translated_head_term = crate::translate::common::choose_value_in_term(
|
||||||
head_atom_argument, head_atom_parameter, context)?;
|
head_atom_argument, std::rc::Rc::clone(head_atom_parameter), context)?;
|
||||||
|
|
||||||
definition_arguments.push(Box::new(translated_head_term));
|
definition_arguments.push(translated_head_term);
|
||||||
}
|
}
|
||||||
|
|
||||||
context.variable_declaration_stack.borrow_mut().pop()?;
|
context.variable_declaration_stack.borrow_mut().pop()?;
|
||||||
@ -410,18 +410,18 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
|
|||||||
let definition = match definition_arguments.len()
|
let definition = match definition_arguments.len()
|
||||||
{
|
{
|
||||||
1 => definition_arguments.pop().unwrap(),
|
1 => definition_arguments.pop().unwrap(),
|
||||||
0 => Box::new(foliage::Formula::true_()),
|
0 => foliage::Formula::true_(),
|
||||||
_ => Box::new(foliage::Formula::and(definition_arguments)),
|
_ => foliage::Formula::and(definition_arguments),
|
||||||
};
|
};
|
||||||
|
|
||||||
let definition = crate::ScopedFormula
|
let definition = crate::ScopedFormula
|
||||||
{
|
{
|
||||||
free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
|
free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
|
||||||
formula: definition,
|
formula: Box::new(definition),
|
||||||
};
|
};
|
||||||
|
|
||||||
log::debug!("translated rule with single atom in head: {}",
|
log::debug!("translated rule with single atom in head: {}",
|
||||||
crate::output::human_readable::display_formula(&definition.formula, None, context));
|
foliage::format::display_formula(&definition.formula, context));
|
||||||
|
|
||||||
definitions.definitions.push(definition);
|
definitions.definitions.push(definition);
|
||||||
},
|
},
|
||||||
@ -435,7 +435,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
|
|||||||
|
|
||||||
let formula = match arguments.len()
|
let formula = match arguments.len()
|
||||||
{
|
{
|
||||||
1 => foliage::Formula::not(arguments.pop().unwrap()),
|
1 => foliage::Formula::not(Box::new(arguments.pop().unwrap())),
|
||||||
0 => foliage::Formula::false_(),
|
0 => foliage::Formula::false_(),
|
||||||
_ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))),
|
_ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))),
|
||||||
};
|
};
|
||||||
@ -449,8 +449,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
|
|||||||
let integrity_constraint = crate::universal_closure(scoped_formula);
|
let integrity_constraint = crate::universal_closure(scoped_formula);
|
||||||
|
|
||||||
log::debug!("translated integrity constraint: {}",
|
log::debug!("translated integrity constraint: {}",
|
||||||
crate::output::human_readable::display_formula(&integrity_constraint, None,
|
foliage::format::display_formula(&integrity_constraint, context));
|
||||||
context));
|
|
||||||
|
|
||||||
context.integrity_constraints.borrow_mut().push(integrity_constraint);
|
context.integrity_constraints.borrow_mut().push(integrity_constraint);
|
||||||
},
|
},
|
||||||
|
@ -208,3 +208,14 @@ impl crate::traits::VariableDeclarationID for Context
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl foliage::format::Format for Context
|
||||||
|
{
|
||||||
|
fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter,
|
||||||
|
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
|
||||||
|
-> std::fmt::Result
|
||||||
|
{
|
||||||
|
crate::output::human_readable::display_variable_declaration(self, formatter,
|
||||||
|
variable_declaration)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
@ -30,10 +30,10 @@ where
|
|||||||
let parameters = std::rc::Rc::new(parameters);
|
let parameters = std::rc::Rc::new(parameters);
|
||||||
|
|
||||||
let predicate_arguments = parameters.iter().map(
|
let predicate_arguments = parameters.iter().map(
|
||||||
|parameter| Box::new(foliage::Term::variable(parameter)))
|
|parameter| foliage::Term::variable(std::rc::Rc::clone(parameter)))
|
||||||
.collect::<Vec<_>>();
|
.collect::<Vec<_>>();
|
||||||
|
|
||||||
let predicate = foliage::Formula::predicate(&predicate_declaration, predicate_arguments);
|
let predicate = foliage::Formula::predicate(predicate_declaration, predicate_arguments);
|
||||||
|
|
||||||
let predicate_literal = match sign
|
let predicate_literal = match sign
|
||||||
{
|
{
|
||||||
@ -53,12 +53,11 @@ where
|
|||||||
|
|
||||||
let mut parameters_iterator = parameters.iter();
|
let mut parameters_iterator = parameters.iter();
|
||||||
let mut arguments = function.arguments().iter().map(
|
let mut arguments = function.arguments().iter().map(
|
||||||
|x| crate::translate::common::choose_value_in_term(x, ¶meters_iterator.next().unwrap(),
|
|x| crate::translate::common::choose_value_in_term(x,
|
||||||
context)
|
std::rc::Rc::clone(¶meters_iterator.next().unwrap()), context))
|
||||||
.map(|x| Box::new(x)))
|
|
||||||
.collect::<Result<Vec<_>, _>>()?;
|
.collect::<Result<Vec<_>, _>>()?;
|
||||||
|
|
||||||
arguments.push(Box::new(predicate_literal));
|
arguments.push(predicate_literal);
|
||||||
|
|
||||||
let and = foliage::Formula::and(arguments);
|
let and = foliage::Formula::and(arguments);
|
||||||
|
|
||||||
@ -120,12 +119,12 @@ where
|
|||||||
let parameter_z2 = ¶meters_iterator.next().unwrap();
|
let parameter_z2 = ¶meters_iterator.next().unwrap();
|
||||||
|
|
||||||
let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(),
|
let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(),
|
||||||
parameter_z1, context)?;
|
std::rc::Rc::clone(parameter_z1), context)?;
|
||||||
let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(),
|
let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(),
|
||||||
parameter_z2, context)?;
|
std::rc::Rc::clone(parameter_z2), context)?;
|
||||||
|
|
||||||
let variable_1 = foliage::Term::variable(parameter_z1);
|
let variable_1 = foliage::Term::variable(std::rc::Rc::clone(parameter_z1));
|
||||||
let variable_2 = foliage::Term::variable(parameter_z2);
|
let variable_2 = foliage::Term::variable(std::rc::Rc::clone(parameter_z2));
|
||||||
|
|
||||||
let operator = crate::translate::common::translate_comparison_operator(
|
let operator = crate::translate::common::translate_comparison_operator(
|
||||||
comparison.comparison_type());
|
comparison.comparison_type());
|
||||||
@ -133,8 +132,8 @@ where
|
|||||||
let compare_z1_and_z2 = foliage::Formula::compare(operator, Box::new(variable_1),
|
let compare_z1_and_z2 = foliage::Formula::compare(operator, Box::new(variable_1),
|
||||||
Box::new(variable_2));
|
Box::new(variable_2));
|
||||||
|
|
||||||
let and = foliage::Formula::and(vec![Box::new(choose_z1_in_t1),
|
let and =
|
||||||
Box::new(choose_z2_in_t2), Box::new(compare_z1_and_z2)]);
|
foliage::Formula::and(vec![choose_z1_in_t1, choose_z2_in_t2, compare_z1_and_z2]);
|
||||||
|
|
||||||
Ok(foliage::Formula::exists(parameters, Box::new(and)))
|
Ok(foliage::Formula::exists(parameters, Box::new(and)))
|
||||||
},
|
},
|
||||||
@ -153,7 +152,6 @@ where
|
|||||||
+ crate::traits::AssignVariableDeclarationDomain
|
+ crate::traits::AssignVariableDeclarationDomain
|
||||||
{
|
{
|
||||||
body_literals.iter()
|
body_literals.iter()
|
||||||
.map(|body_literal| translate_body_literal(body_literal, context)
|
.map(|body_literal| translate_body_literal(body_literal, context))
|
||||||
.map(|value| Box::new(value)))
|
|
||||||
.collect::<Result<foliage::Formulas, crate::Error>>()
|
.collect::<Result<foliage::Formulas, crate::Error>>()
|
||||||
}
|
}
|
||||||
|
16
src/utils.rs
16
src/utils.rs
@ -44,23 +44,23 @@ pub(crate) struct ScopedFormula
|
|||||||
pub formula: Box<foliage::Formula>,
|
pub formula: Box<foliage::Formula>,
|
||||||
}
|
}
|
||||||
|
|
||||||
pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> Box<foliage::Formula>
|
pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
|
||||||
{
|
{
|
||||||
match scoped_formula.free_variable_declarations.is_empty()
|
match scoped_formula.free_variable_declarations.is_empty()
|
||||||
{
|
{
|
||||||
true => scoped_formula.formula,
|
true => *scoped_formula.formula,
|
||||||
false => Box::new(foliage::Formula::exists(scoped_formula.free_variable_declarations,
|
false => foliage::Formula::exists(scoped_formula.free_variable_declarations,
|
||||||
scoped_formula.formula)),
|
scoped_formula.formula),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> Box<foliage::Formula>
|
pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
|
||||||
{
|
{
|
||||||
match scoped_formula.free_variable_declarations.is_empty()
|
match scoped_formula.free_variable_declarations.is_empty()
|
||||||
{
|
{
|
||||||
true => scoped_formula.formula,
|
true => *scoped_formula.formula,
|
||||||
false => Box::new(foliage::Formula::for_all(scoped_formula.free_variable_declarations,
|
false => foliage::Formula::for_all(scoped_formula.free_variable_declarations,
|
||||||
scoped_formula.formula)),
|
scoped_formula.formula),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user