patrick
/
anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Finish implementing definitions

This commit is contained in:
Patrick Lühne 2020-02-02 02:32:32 +01:00
parent 86c8391278
commit 99345bc0ac
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
3 changed files with 273 additions and 139 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

273
src/translate/common.rs
View File

@ -27,12 +27,8 @@ impl FindOrCreateFunctionDeclaration for foliage::FunctionDeclarations
Some(value) => std::rc::Rc::clone(value),
None =>
{
let declaration = foliage::FunctionDeclaration
{
name: name.to_owned(),
arity,
};
let declaration = std::rc::Rc::new(declaration);
let declaration = std::rc::Rc::new(foliage::FunctionDeclaration::new(
name.to_string(), arity));
self.insert(std::rc::Rc::clone(&declaration));
@ -55,12 +51,8 @@ impl FindOrCreatePredicateDeclaration for foliage::PredicateDeclarations
Some(value) => std::rc::Rc::clone(value),
None =>
{
let declaration = foliage::PredicateDeclaration
{
name: name.to_owned(),
arity,
};
let declaration = std::rc::Rc::new(declaration);
let declaration = std::rc::Rc::new(foliage::PredicateDeclaration::new(
name.to_string(), arity));
self.insert(std::rc::Rc::clone(&declaration));
@ -80,14 +72,10 @@ impl FindOrCreateVariableDeclaration for foliage::VariableDeclarationStack
// TODO: check correctness
if name == "_"
{
let variable_declaration = foliage::VariableDeclaration
{
name: "_".to_owned(),
};
let variable_declaration = std::rc::Rc::new(variable_declaration);
let variable_declaration = std::rc::Rc::new(foliage::VariableDeclaration::new(
"_".to_owned()));
self.free_variable_declarations.insert(
std::rc::Rc::clone(&variable_declaration));
self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration));
return variable_declaration;
}
@ -106,17 +94,17 @@ pub(crate) fn translate_binary_operator(binary_operator: clingo::ast::BinaryOper
| clingo::ast::BinaryOperator::Xor
=> return Err(crate::Error::new_unsupported_language_feature("binary logical operators")),
clingo::ast::BinaryOperator::Plus
=> Ok(foliage::BinaryOperator::Addition),
=> Ok(foliage::BinaryOperator::Add),
clingo::ast::BinaryOperator::Minus
=> Ok(foliage::BinaryOperator::Subtraction),
=> Ok(foliage::BinaryOperator::Subtract),
clingo::ast::BinaryOperator::Multiplication
=> Ok(foliage::BinaryOperator::Multiplication),
=> Ok(foliage::BinaryOperator::Multiply),
clingo::ast::BinaryOperator::Division
=> Ok(foliage::BinaryOperator::Division),
=> Ok(foliage::BinaryOperator::Divide),
clingo::ast::BinaryOperator::Modulo
=> Ok(foliage::BinaryOperator::Modulo),
clingo::ast::BinaryOperator::Power
=> Ok(foliage::BinaryOperator::Exponentiation),
=> Ok(foliage::BinaryOperator::Exponentiate),
}
}
@ -142,25 +130,17 @@ pub(crate) fn translate_comparison_operator(comparison_operator: clingo::ast::Co
pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-> foliage::Comparison
-> foliage::Formula
{
let variable = foliage::Variable
{
declaration: std::rc::Rc::clone(variable_declaration),
};
let variable = foliage::Term::variable(variable_declaration);
foliage::Comparison
{
operator: foliage::ComparisonOperator::Equal,
left: Box::new(foliage::Term::Variable(variable)),
right: term,
}
foliage::Formula::equal(Box::new(variable), term)
}
pub(crate) fn choose_value_in_term(term: &clingo::ast::Term,
variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>,
function_declarations: &mut foliage::FunctionDeclarations,
variable_declaration_stack: &mut foliage::VariableDeclarationStack)
mut function_declarations: &mut foliage::FunctionDeclarations,
mut variable_declaration_stack: &mut foliage::VariableDeclarationStack)
-> Result<foliage::Formula, crate::Error>
{
match term.term_type()
@ -168,21 +148,19 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term,
clingo::ast::TermType::Symbol(symbol) => match symbol.symbol_type()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
{
clingo::SymbolType::Number => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
Box::new(foliage::Term::Integer(symbol.number()
clingo::SymbolType::Number => Ok(choose_value_in_primitive(
Box::new(foliage::Term::integer(symbol.number()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?)),
variable_declaration))),
clingo::SymbolType::Infimum => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
Box::new(foliage::Term::SpecialInteger(foliage::SpecialInteger::Infimum)),
variable_declaration))),
clingo::SymbolType::Supremum => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
Box::new(foliage::Term::SpecialInteger(foliage::SpecialInteger::Supremum)),
variable_declaration))),
clingo::SymbolType::String => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
Box::new(foliage::Term::String(symbol.string()
variable_declaration)),
clingo::SymbolType::Infimum => Ok(choose_value_in_primitive(
Box::new(foliage::Term::infimum()), variable_declaration)),
clingo::SymbolType::Supremum => Ok(choose_value_in_primitive(
Box::new(foliage::Term::supremum()), variable_declaration)),
clingo::SymbolType::String => Ok(choose_value_in_primitive(
Box::new(foliage::Term::string(symbol.string()
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
.to_string())),
variable_declaration))),
variable_declaration)),
clingo::SymbolType::Function =>
{
let arguments = symbol.arguments()
@ -199,28 +177,195 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term,
.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
let constant_declaration = function_declarations.find_or_create(constant_name, 0);
let function = foliage::Term::function(&constant_declaration, vec![]);
let function = foliage::Term::Function(foliage::Function
{
declaration: constant_declaration,
arguments: vec![],
});
Ok(foliage::Formula::Comparison(choose_value_in_primitive(Box::new(function), variable_declaration)))
Ok(choose_value_in_primitive(Box::new(function), variable_declaration))
}
},
clingo::ast::TermType::Variable(variable_name) =>
{
let other_variable_declaration = variable_declaration_stack.find_or_create(variable_name);
let other_variable = foliage::Term::variable(&other_variable_declaration);
let other_variable = foliage::Term::Variable(foliage::Variable
{
declaration: other_variable_declaration,
});
Ok(foliage::Formula::Comparison(choose_value_in_primitive(Box::new(other_variable),
variable_declaration)))
Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration))
},
_ => Err(crate::Error::new_not_yet_implemented("todo")),
clingo::ast::TermType::BinaryOperation(binary_operation) =>
{
let operator = crate::translate::common::translate_binary_operator(
binary_operation.binary_operator())?;
match operator
{
foliage::BinaryOperator::Add
| foliage::BinaryOperator::Subtract
| foliage::BinaryOperator::Multiply
=>
{
let parameters = (0..2).map(|_| std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string())))
.collect::<foliage::VariableDeclarations>();
let parameter_1 = &parameters[0];
let parameter_2 = &parameters[1];
let translated_binary_operation = foliage::Term::binary_operation(operator,
Box::new(foliage::Term::variable(&parameter_1)),
Box::new(foliage::Term::variable(&parameter_2)));
let equals = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(translated_binary_operation));
let choose_value_from_left_argument = choose_value_in_term(
binary_operation.left(), &parameter_1, &mut function_declarations,
&mut variable_declaration_stack)?;
let choose_value_from_right_argument = choose_value_in_term(
binary_operation.right(), &parameter_2, &mut function_declarations,
&mut variable_declaration_stack)?;
let and = foliage::Formula::And(vec![Box::new(equals),
Box::new(choose_value_from_left_argument),
Box::new(choose_value_from_right_argument)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
foliage::BinaryOperator::Divide
| foliage::BinaryOperator::Modulo
=>
{
let parameters = (0..4).map(|_| std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string())))
.collect::<foliage::VariableDeclarations>();
let parameter_i = &parameters[0];
let parameter_j = &parameters[1];
let parameter_q = &parameters[2];
let parameter_r = &parameters[3];
let j_times_q = foliage::Term::multiply(
Box::new(foliage::Term::variable(parameter_j)),
Box::new(foliage::Term::variable(parameter_q)));
let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q),
Box::new(foliage::Term::variable(parameter_r)));
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));
let choose_i_in_t1 = choose_value_in_term(binary_operation.left(), parameter_i,
&mut function_declarations, &mut variable_declaration_stack)?;
let choose_i_in_t2 = choose_value_in_term(binary_operation.left(), parameter_j,
&mut function_declarations, &mut variable_declaration_stack)?;
let j_not_equal_to_0 = foliage::Formula::not_equal(
Box::new(foliage::Term::variable(parameter_j)),
Box::new(foliage::Term::integer(0)));
let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal(
Box::new(foliage::Term::variable(parameter_r)),
Box::new(foliage::Term::integer(0)));
let r_less_than_q = foliage::Formula::less(
Box::new(foliage::Term::variable(parameter_r)),
Box::new(foliage::Term::variable(parameter_q)));
let z_equal_to_q = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_q)));
let z_equal_to_r = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_r)));
let last_argument = match operator
{
foliage::BinaryOperator::Divide => z_equal_to_q,
foliage::BinaryOperator::Modulo => z_equal_to_r,
_ => return Err(crate::Error::new_logic("unreachable code")),
};
let and = foliage::Formula::and(vec![Box::new(i_equals_j_times_q_plus_r),
Box::new(choose_i_in_t1), Box::new(choose_i_in_t2),
Box::new(j_not_equal_to_0), Box::new(r_greater_or_equal_to_0),
Box::new(r_less_than_q), Box::new(last_argument)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
_ => Err(crate::Error::new_not_yet_implemented("todo")),
}
},
clingo::ast::TermType::UnaryOperation(unary_operation) =>
{
match unary_operation.unary_operator()
{
clingo::ast::UnaryOperator::Absolute =>
return Err(crate::Error::new_unsupported_language_feature("absolute value")),
clingo::ast::UnaryOperator::Minus =>
{
let parameter_z_prime = std::rc::Rc::new(foliage::VariableDeclaration::new(
"<anonymous>".to_string()));
let negative_z_prime = foliage::Term::negative(Box::new(
foliage::Term::variable(&parameter_z_prime)));
let equals = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(negative_z_prime));
let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(),
&parameter_z_prime, &mut function_declarations,
&mut variable_declaration_stack)?;
let and = foliage::Formula::and(vec![Box::new(equals),
Box::new(choose_z_prime_in_t_prime)]);
let parameters = vec![parameter_z_prime];
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
_ => Err(crate::Error::new_not_yet_implemented("todo")),
}
},
clingo::ast::TermType::Interval(interval) =>
{
let parameters = (0..3).map(|_| std::rc::Rc::new(
foliage::VariableDeclaration::new("<anonymous>".to_string())))
.collect::<foliage::VariableDeclarations>();
let parameter_i = &parameters[0];
let parameter_j = &parameters[1];
let parameter_k = &parameters[2];
let choose_i_in_t_1 = choose_value_in_term(interval.left(), parameter_i,
&mut function_declarations, &mut variable_declaration_stack)?;
let choose_j_in_t_2 = choose_value_in_term(interval.right(), parameter_j,
&mut function_declarations, &mut variable_declaration_stack)?;
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(parameter_k)));
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(parameter_j)));
let z_equals_k = foliage::Formula::equal(
Box::new(foliage::Term::variable(variable_declaration)),
Box::new(foliage::Term::variable(parameter_k)));
let and = foliage::Formula::and(vec![Box::new(choose_i_in_t_1),
Box::new(choose_j_in_t_2), Box::new(i_less_than_or_equal_to_k),
Box::new(k_less_than_or_equal_to_j), Box::new(z_equals_k)]);
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
clingo::ast::TermType::Function(_) =>
Err(crate::Error::new_unsupported_language_feature("symbolic functions")),
clingo::ast::TermType::Pool(_) =>
Err(crate::Error::new_unsupported_language_feature("pools")),
clingo::ast::TermType::ExternalFunction(_) =>
Err(crate::Error::new_unsupported_language_feature("external functions")),
}
}

44
src/translate/verify_properties.rs
View File

@ -33,10 +33,7 @@ pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error>
let declare_predicate_parameters = |predicate_declaration: &foliage::PredicateDeclaration|
{
std::rc::Rc::new((0..predicate_declaration.arity)
.map(|_| std::rc::Rc::new(foliage::VariableDeclaration
{
name: "<anonymous>".to_string(),
}))
.map(|_| std::rc::Rc::new(foliage::VariableDeclaration::new("<anonymous>".to_string())))
.collect())
};
@ -54,24 +51,47 @@ pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error>
});
}
let definitions = definitions.get(&head_atom.predicate_declaration).unwrap();
let definitions = definitions.get_mut(&head_atom.predicate_declaration).unwrap();
variable_declaration_stack.push(std::rc::Rc::clone(&definitions.head_atom_parameters));
let translated_body = translate_body(rule.body(), &mut function_declarations,
&mut predicate_declarations, &mut variable_declaration_stack);
let mut definition_arguments = translate_body(rule.body(), &mut function_declarations,
&mut predicate_declarations, &mut variable_declaration_stack)?;
assert_eq!(definitions.head_atom_parameters.len(), head_atom.arguments.len());
let mut head_atom_arguments_iterator = head_atom.arguments.iter();
for head_atom_parameter in definitions.head_atom_parameters.iter()
{
let head_atom_argument = head_atom_arguments_iterator.next().unwrap();
let translated_head_term = crate::translate::common::choose_value_in_term(
head_atom_argument, head_atom_parameter, &mut function_declarations,
&mut variable_declaration_stack)?;
definition_arguments.push(Box::new(translated_head_term));
}
variable_declaration_stack.pop();
let definition = foliage::Formula::And(definition_arguments);
let definition = ScopedFormula
{
free_variable_declarations: variable_declaration_stack.free_variable_declarations,
formula: definition,
};
log::trace!("translated formula: {:?}", definition.formula);
definitions.definitions.push(definition);
},
HeadType::ChoiceWithSingleAtom(_) =>
log::debug!("translating choice rule with single atom"),
HeadType::IntegrityConstraint =>
log::debug!("translating integrity constraint"),
HeadType::Trivial =>
{
log::debug!("skipping trivial rule");
return Ok(());
},
HeadType::Trivial => log::debug!("skipping trivial rule"),
}
Ok(())

95
src/translate/verify_properties/translate_body.rs
View File

@ -18,29 +18,22 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::a
function.arguments().len());
let parameters = function.arguments().iter().map(|_| std::rc::Rc::new(
foliage::VariableDeclaration
{
name: "<anonymous>".to_string(),
}))
.collect::<Vec<_>>();
foliage::VariableDeclaration::new("<anonymous>".to_string())))
.collect::<foliage::VariableDeclarations>();
let predicate_arguments = parameters.iter().map(
|parameter| Box::new(foliage::Term::Variable(foliage::Variable{declaration: std::rc::Rc::clone(parameter)})))
|parameter| Box::new(foliage::Term::variable(parameter)))
.collect::<Vec<_>>();
let predicate = foliage::Predicate
{
declaration: predicate_declaration,
arguments: predicate_arguments,
};
let predicate = foliage::Formula::predicate(&predicate_declaration, predicate_arguments);
let predicate_literal = match sign
{
clingo::ast::Sign::None
| clingo::ast::Sign::DoubleNegation
=> foliage::Formula::Predicate(predicate),
=> predicate,
clingo::ast::Sign::Negation
=> foliage::Formula::Not(Box::new(foliage::Formula::Predicate(predicate))),
=> foliage::Formula::not(Box::new(predicate)),
};
if function.arguments().is_empty()
@ -48,27 +41,20 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::a
return Ok(predicate_literal);
}
let mut i = 0;
assert_eq!(function.arguments().len(), parameters.len());
let mut arguments = function.arguments().iter().map(|x|
{
let result = crate::translate::common::choose_value_in_term(x, &parameters[i],
let mut parameters_iterator = parameters.iter();
let mut arguments = function.arguments().iter().map(
|x| crate::translate::common::choose_value_in_term(x, &parameters_iterator.next().unwrap(),
&mut function_declarations, &mut variable_declaration_stack)
.map(|x| Box::new(x));
i += 1;
result
})
.map(|x| Box::new(x)))
.collect::<Result<Vec<_>, _>>()?;
arguments.push(Box::new(predicate_literal));
let and = foliage::Formula::And(arguments);
let and = foliage::Formula::and(arguments);
Ok(foliage::Formula::Exists(foliage::Exists
{
parameters,
argument: Box::new(and),
}))
Ok(foliage::Formula::exists(parameters, Box::new(and)))
}
pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral,
@ -108,49 +94,32 @@ pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral,
&mut variable_declaration_stack),
clingo::ast::LiteralType::Comparison(comparison) =>
{
let new_variable_declaration = || std::rc::Rc::new(foliage::VariableDeclaration
{
name: "<anonymous>".to_string()
});
let parameters = (0..2).map(|_| std::rc::Rc::new(foliage::VariableDeclaration::new(
"<anonymous>".to_string())))
.collect::<foliage::VariableDeclarations>();
let parameters = vec![new_variable_declaration(), new_variable_declaration()];
let mut parameters_iterator = parameters.iter();
let parameter_z1 = &parameters_iterator.next().unwrap();
let parameter_z2 = &parameters_iterator.next().unwrap();
let parameter_z1 = &parameters[0];
let parameter_z2 = &parameters[1];
let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(),
parameter_z1, &mut function_declarations, &mut variable_declaration_stack)?;
let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(),
parameter_z2, &mut function_declarations, &mut variable_declaration_stack)?;
let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), &parameter_z1,
&mut function_declarations, &mut variable_declaration_stack)?;
let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), &parameter_z2,
&mut function_declarations, &mut variable_declaration_stack)?;
let variable_1 = foliage::Term::variable(parameter_z1);
let variable_2 = foliage::Term::variable(parameter_z2);
let variable_1 = foliage::Variable
{
declaration: std::rc::Rc::clone(&parameter_z1),
};
let operator = crate::translate::common::translate_comparison_operator(
comparison.comparison_type());
let variable_2 = foliage::Variable
{
declaration: std::rc::Rc::clone(&parameter_z2),
};
let compare_z1_and_z2 = foliage::Formula::compare(operator, Box::new(variable_1),
Box::new(variable_2));
let comparison_operator
= crate::translate::common::translate_comparison_operator(comparison.comparison_type());
let and = foliage::Formula::and(vec![Box::new(choose_z1_in_t1),
Box::new(choose_z2_in_t2), Box::new(compare_z1_and_z2)]);
let compare_z1_and_z2 = foliage::Comparison
{
operator: comparison_operator,
left: Box::new(foliage::Term::Variable(variable_1)),
right: Box::new(foliage::Term::Variable(variable_2)),
};
let and = foliage::Formula::And(vec![Box::new(choose_z1_in_t1),
Box::new(choose_z2_in_t2), Box::new(foliage::Formula::Comparison(compare_z1_and_z2))]);
Ok(foliage::Formula::Exists(foliage::Exists
{
parameters,
argument: Box::new(and),
}))
Ok(foliage::Formula::exists(parameters, Box::new(and)))
},
_ => Err(crate::Error::new_unsupported_language_feature(
"body literals other than Booleans, terms, or comparisons")),