diff --git a/src/translate/common.rs b/src/translate/common.rs index 5d6aecb..eae009f 100644 --- a/src/translate/common.rs +++ b/src/translate/common.rs @@ -1,61 +1,122 @@ -pub(crate) trait FindOrCreateFunctionDeclaration = FnMut(&str, usize) - -> std::rc::Rc; - -pub(crate) trait FindOrCreatePredicateDeclaration = FnMut(&str, usize) - -> std::rc::Rc; - -pub(crate) trait FindOrCreateVariableDeclaration = FnMut(&str) - -> std::rc::Rc; - -pub(crate) fn find_or_create_predicate_declaration(predicate_declarations: &mut foliage::PredicateDeclarations, - name: &str, arity: usize) - -> std::rc::Rc +pub(crate) trait FindOrCreateFunctionDeclaration { - match predicate_declarations.iter() - .find(|x| x.name == name && x.arity == arity) + fn find_or_create(&mut self, name: &str, arity: usize) + -> std::rc::Rc; +} + +pub(crate) trait FindOrCreatePredicateDeclaration +{ + fn find_or_create(&mut self, name: &str, arity: usize) + -> std::rc::Rc; +} + +pub(crate) trait FindOrCreateVariableDeclaration +{ + fn find_or_create(&mut self, name: &str) + -> std::rc::Rc; +} + +impl FindOrCreateFunctionDeclaration for foliage::FunctionDeclarations +{ + fn find_or_create(&mut self, name: &str, arity: usize) + -> std::rc::Rc { - Some(value) => std::rc::Rc::clone(value), - None => + match self.iter() + .find(|x| x.name == name && x.arity == arity) { - let declaration = foliage::PredicateDeclaration + Some(value) => std::rc::Rc::clone(value), + None => { - name: name.to_owned(), - arity, - }; - let declaration = std::rc::Rc::new(declaration); + let declaration = foliage::FunctionDeclaration + { + name: name.to_owned(), + arity, + }; + let declaration = std::rc::Rc::new(declaration); - predicate_declarations.insert(std::rc::Rc::clone(&declaration)); + self.insert(std::rc::Rc::clone(&declaration)); - log::debug!("new predicate declaration: {}/{}", name, arity); + log::debug!("new function declaration: {}/{}", name, arity); - declaration - }, + declaration + }, + } } } -pub(crate) fn find_or_create_function_declaration(function_declarations: &mut foliage::FunctionDeclarations, - name: &str, arity: usize) - -> std::rc::Rc +impl FindOrCreatePredicateDeclaration for foliage::PredicateDeclarations { - match function_declarations.iter() - .find(|x| x.name == name && x.arity == arity) + fn find_or_create(&mut self, name: &str, arity: usize) + -> std::rc::Rc { - Some(value) => std::rc::Rc::clone(value), - None => + match self.iter() + .find(|x| x.name == name && x.arity == arity) { - let declaration = foliage::FunctionDeclaration + Some(value) => std::rc::Rc::clone(value), + None => { - name: name.to_owned(), - arity, + let declaration = foliage::PredicateDeclaration + { + name: name.to_owned(), + arity, + }; + let declaration = std::rc::Rc::new(declaration); + + self.insert(std::rc::Rc::clone(&declaration)); + + log::debug!("new predicate declaration: {}/{}", name, arity); + + declaration + }, + } + } +} + +impl FindOrCreateVariableDeclaration for foliage::VariableDeclarationStack +{ + fn find_or_create(&mut self, name: &str) + -> std::rc::Rc + { + // TODO: check correctness + if name == "_" + { + let variable_declaration = foliage::VariableDeclaration + { + name: "_".to_owned(), }; - let declaration = std::rc::Rc::new(declaration); + let variable_declaration = std::rc::Rc::new(variable_declaration); - function_declarations.insert(std::rc::Rc::clone(&declaration)); + self.free_variable_declarations.insert( + std::rc::Rc::clone(&variable_declaration)); - log::debug!("new function declaration: {}/{}", name, arity); + return variable_declaration; + } - declaration - }, + self.find_or_create(name) + } +} + +pub(crate) fn translate_binary_operator(binary_operator: clingo::ast::BinaryOperator) + -> Result +{ + match binary_operator + { + clingo::ast::BinaryOperator::And + | clingo::ast::BinaryOperator::Or + | clingo::ast::BinaryOperator::Xor + => return Err(crate::Error::new_unsupported_language_feature("binary logical operators")), + clingo::ast::BinaryOperator::Plus + => Ok(foliage::BinaryOperator::Addition), + clingo::ast::BinaryOperator::Minus + => Ok(foliage::BinaryOperator::Subtraction), + clingo::ast::BinaryOperator::Multiplication + => Ok(foliage::BinaryOperator::Multiplication), + clingo::ast::BinaryOperator::Division + => Ok(foliage::BinaryOperator::Division), + clingo::ast::BinaryOperator::Modulo + => Ok(foliage::BinaryOperator::Modulo), + clingo::ast::BinaryOperator::Power + => Ok(foliage::BinaryOperator::Exponentiation), } } @@ -96,13 +157,11 @@ pub(crate) fn choose_value_in_primitive(term: Box, } } -pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, +pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, variable_declaration: &std::rc::Rc, - mut find_or_create_function_declaration: F1, mut find_or_create_variable_declaration: F2) + function_declarations: &mut foliage::FunctionDeclarations, + variable_declaration_stack: &mut foliage::VariableDeclarationStack) -> Result -where - F1: FindOrCreateFunctionDeclaration, - F2: FindOrCreateVariableDeclaration, { match term.term_type() { @@ -139,7 +198,7 @@ where let constant_name = symbol.name() .map_err(|error| crate::Error::new_logic("clingo error").with(error))?; - let constant_declaration = find_or_create_function_declaration(constant_name, 0); + let constant_declaration = function_declarations.find_or_create(constant_name, 0); let function = foliage::Term::Function(foliage::Function { @@ -150,8 +209,18 @@ where Ok(foliage::Formula::Comparison(choose_value_in_primitive(Box::new(function), variable_declaration))) } }, - clingo::ast::TermType::Variable(variable) => - Err(crate::Error::new_not_yet_implemented("todo")), + clingo::ast::TermType::Variable(variable_name) => + { + let other_variable_declaration = variable_declaration_stack.find_or_create(variable_name); + + 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))) + }, _ => Err(crate::Error::new_not_yet_implemented("todo")), } } diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 6ed2bbd..d9d4979 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -12,31 +12,32 @@ pub struct ScopedFormula pub struct Definitions { - head_atom_parameters: foliage::VariableDeclarations, + head_atom_parameters: std::rc::Rc, definitions: Vec, } pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error> { + use super::common::FindOrCreatePredicateDeclaration; + let mut function_declarations = foliage::FunctionDeclarations::new(); let mut predicate_declarations = foliage::PredicateDeclarations::new(); let mut variable_declaration_stack = foliage::VariableDeclarationStack::new(); let head_type = determine_head_type(rule.head(), - |name, arity| super::common::find_or_create_predicate_declaration( - &mut predicate_declarations, name, arity))?; + |name, arity| predicate_declarations.find_or_create(name, arity))?; let mut definitions = std::collections::BTreeMap::, Definitions>::new(); let declare_predicate_parameters = |predicate_declaration: &foliage::PredicateDeclaration| { - (0..predicate_declaration.arity) + std::rc::Rc::new((0..predicate_declaration.arity) .map(|_| std::rc::Rc::new(foliage::VariableDeclaration { name: "".to_string(), })) - .collect() + .collect()) }; match head_type @@ -54,8 +55,15 @@ pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error> } let definitions = definitions.get(&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); + + variable_declaration_stack.pop(); }, - HeadType::ChoiceWithSingleAtom(test) => + HeadType::ChoiceWithSingleAtom(_) => log::debug!("translating choice rule with single atom"), HeadType::IntegrityConstraint => log::debug!("translating integrity constraint"), diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index 773e112..b5b5218 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -1,12 +1,11 @@ -pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, - mut find_or_create_function_declaration: F1, mut find_or_create_predicate_declaration: F2, - mut find_or_create_variable_declaration: F3) +pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, + mut function_declarations: &mut foliage::FunctionDeclarations, + predicate_declarations: &mut foliage::PredicateDeclarations, + mut variable_declaration_stack: &mut foliage::VariableDeclarationStack) -> Result -where - F1: crate::translate::common::FindOrCreateFunctionDeclaration, - F2: crate::translate::common::FindOrCreatePredicateDeclaration, - F3: crate::translate::common::FindOrCreateVariableDeclaration, { + use crate::translate::common::FindOrCreatePredicateDeclaration; + let function = match body_term.term_type() { clingo::ast::TermType::Function(value) => value, @@ -15,7 +14,7 @@ where let function_name = function.name().map_err(|error| crate::Error::new_decode_identifier(error))?; - let predicate_declaration = find_or_create_predicate_declaration(function_name, + let predicate_declaration = predicate_declarations.find_or_create(function_name, function.arguments().len()); let parameters = function.arguments().iter().map(|_| std::rc::Rc::new( @@ -54,7 +53,7 @@ where let mut arguments = function.arguments().iter().map(|x| { let result = crate::translate::common::choose_value_in_term(x, ¶meters[i], - &mut find_or_create_function_declaration, &mut find_or_create_variable_declaration) + &mut function_declarations, &mut variable_declaration_stack) .map(|x| Box::new(x)); i += 1; result @@ -72,14 +71,11 @@ where })) } -pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, - mut find_or_create_function_declaration: F1, mut find_or_create_predicate_declaration: F2, - mut find_or_create_variable_declaration: F3) +pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, + mut function_declarations: &mut foliage::FunctionDeclarations, + mut predicate_declarations: &mut foliage::PredicateDeclarations, + mut variable_declaration_stack: &mut foliage::VariableDeclarationStack) -> Result -where - F1: crate::translate::common::FindOrCreateFunctionDeclaration, - F2: crate::translate::common::FindOrCreatePredicateDeclaration, - F3: crate::translate::common::FindOrCreateVariableDeclaration, { match body_literal.sign() { @@ -108,8 +104,8 @@ where Ok(foliage::Formula::Boolean(value)) }, clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(), - &mut find_or_create_function_declaration, &mut find_or_create_predicate_declaration, - &mut find_or_create_variable_declaration), + &mut function_declarations, &mut predicate_declarations, + &mut variable_declaration_stack), clingo::ast::LiteralType::Comparison(comparison) => { let new_variable_declaration = || std::rc::Rc::new(foliage::VariableDeclaration @@ -123,9 +119,9 @@ where let parameter_z2 = ¶meters[1]; let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), ¶meter_z1, - &mut find_or_create_function_declaration, &mut find_or_create_variable_declaration)?; + &mut function_declarations, &mut variable_declaration_stack)?; let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), ¶meter_z2, - &mut find_or_create_function_declaration, &mut find_or_create_variable_declaration)?; + &mut function_declarations, &mut variable_declaration_stack)?; let variable_1 = foliage::Variable { @@ -161,19 +157,15 @@ where } } -pub(crate) fn translate_body(body_literals: &[clingo::ast::BodyLiteral], - mut find_or_create_function_declaration: F1, mut find_or_create_predicate_declaration: F2, - mut find_or_create_variable_declaration: F3) +pub(crate) fn translate_body(body_literals: &[clingo::ast::BodyLiteral], + mut function_declaration: &mut foliage::FunctionDeclarations, + mut predicate_declaration: &mut foliage::PredicateDeclarations, + mut variable_declaration_stack: &mut foliage::VariableDeclarationStack) -> Result -where - F1: crate::translate::common::FindOrCreateFunctionDeclaration, - F2: crate::translate::common::FindOrCreatePredicateDeclaration, - F3: crate::translate::common::FindOrCreateVariableDeclaration, { body_literals.iter() - .map(|body_literal| translate_body_literal(body_literal, - &mut find_or_create_function_declaration, &mut find_or_create_predicate_declaration, - &mut find_or_create_variable_declaration) + .map(|body_literal| translate_body_literal(body_literal, &mut function_declaration, + &mut predicate_declaration, &mut variable_declaration_stack) .map(|value| Box::new(value))) .collect::>() }