From 442d9f6ac00cec9e3690569211411057556c8f59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 31 Jan 2020 17:24:13 +0100 Subject: [PATCH] Split translation code into smaller modules --- src/translate/verify_properties.rs | 239 +----------------- src/translate/verify_properties/context.rs | 77 ++++++ .../verify_properties/translate_body.rs | 158 ++++++++++++ 3 files changed, 239 insertions(+), 235 deletions(-) create mode 100644 src/translate/verify_properties/context.rs create mode 100644 src/translate/verify_properties/translate_body.rs diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 032016e..ce560e8 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -1,239 +1,8 @@ -pub struct ScopedFormula -{ - free_variable_declarations: foliage::VariableDeclarations, - formula: foliage::Formula, -} +mod context; +mod translate_body; -pub struct Context -{ - scoped_formulas: Vec, - function_declarations: foliage::FunctionDeclarations, - predicate_declarations: foliage::PredicateDeclarations, - variable_declaration_stack: foliage::VariableDeclarationStack, -} - -impl Context -{ - pub fn new() -> Self - { - Self - { - scoped_formulas: vec![], - function_declarations: foliage::FunctionDeclarations::new(), - predicate_declarations: foliage::PredicateDeclarations::new(), - variable_declaration_stack: foliage::VariableDeclarationStack::new(), - } - } - - pub fn find_or_create_predicate_declaration(&mut self, name: &str, arity: usize) - -> std::rc::Rc - { - match self.predicate_declarations.iter() - .find(|x| x.name == name && x.arity == arity) - { - Some(value) => std::rc::Rc::clone(value), - None => - { - let declaration = foliage::PredicateDeclaration - { - name: name.to_owned(), - arity, - }; - let declaration = std::rc::Rc::new(declaration); - - self.predicate_declarations.insert(std::rc::Rc::clone(&declaration)); - - log::debug!("new predicate declaration: {}/{}", name, arity); - - declaration - }, - } - } - - pub fn find_or_create_function_declaration(&mut self, name: &str, arity: usize) - -> std::rc::Rc - { - match self.function_declarations.iter() - .find(|x| x.name == name && x.arity == arity) - { - Some(value) => std::rc::Rc::clone(value), - None => - { - let declaration = foliage::FunctionDeclaration - { - name: name.to_owned(), - arity, - }; - let declaration = std::rc::Rc::new(declaration); - - self.function_declarations.insert(std::rc::Rc::clone(&declaration)); - - log::debug!("new function declaration: {}/{}", name, arity); - - declaration - }, - } - } -} - -pub fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, - context: &mut Context) - -> Result -{ - let function = match body_term.term_type() - { - clingo::ast::TermType::Function(value) => value, - _ => return Err(crate::Error::new_unsupported_language_feature("only functions supported as body terms")), - }; - - let function_name = function.name().map_err(|error| crate::Error::new_decode_identifier(error))?; - - let predicate_declaration = context.find_or_create_predicate_declaration(function_name, - function.arguments().len()); - - let parameters = function.arguments().iter().map(|_| std::rc::Rc::new( - foliage::VariableDeclaration - { - name: "".to_string(), - })) - .collect::>(); - - let predicate_arguments = parameters.iter().map( - |parameter| Box::new(foliage::Term::Variable(foliage::Variable{declaration: std::rc::Rc::clone(parameter)}))) - .collect::>(); - - let predicate = foliage::Predicate - { - declaration: predicate_declaration, - arguments: predicate_arguments, - }; - - let predicate_literal = match sign - { - clingo::ast::Sign::None - | clingo::ast::Sign::DoubleNegation - => foliage::Formula::Predicate(predicate), - clingo::ast::Sign::Negation - => foliage::Formula::Not(Box::new(foliage::Formula::Predicate(predicate))), - }; - - if function.arguments().is_empty() - { - return Ok(predicate_literal); - } - - let mut i = 0; - - let mut arguments = function.arguments().iter().map(|x| - { - let result = super::common::choose_value_in_term(x, ¶meters[i], - |name, arity| context.find_or_create_function_declaration(name, arity)) - .map(|x| Box::new(x)); - i += 1; - result - }) - .collect::, _>>()?; - - arguments.push(Box::new(predicate_literal)); - - let and = foliage::Formula::And(arguments); - - Ok(foliage::Formula::Exists(foliage::Exists - { - parameters, - argument: Box::new(and), - })) -} - -pub fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, context: &mut Context) - -> Result -{ - match body_literal.sign() - { - clingo::ast::Sign::None => (), - _ => return Err(crate::Error::new_unsupported_language_feature( - "signed body literals")), - } - - let literal = match body_literal.body_literal_type() - { - clingo::ast::BodyLiteralType::Literal(literal) => literal, - _ => return Err(crate::Error::new_unsupported_language_feature( - "only plain body literals supported")), - }; - - match literal.literal_type() - { - clingo::ast::LiteralType::Boolean(value) => - { - match literal.sign() - { - clingo::ast::Sign::None => (), - _ => return Err(crate::Error::new_logic("unexpected negated Boolean value")), - } - - Ok(foliage::Formula::Boolean(value)) - }, - clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(), context), - clingo::ast::LiteralType::Comparison(comparison) => - { - let new_variable_declaration = || std::rc::Rc::new(foliage::VariableDeclaration - { - name: "".to_string() - }); - - let parameters = vec![new_variable_declaration(), new_variable_declaration()]; - - let parameter_z1 = ¶meters[0]; - let parameter_z2 = ¶meters[1]; - - let choose_z1_in_t1 = super::common::choose_value_in_term(comparison.left(), ¶meter_z1, - |name, arity| context.find_or_create_function_declaration(name, arity))?; - let choose_z2_in_t2 = super::common::choose_value_in_term(comparison.right(), ¶meter_z2, - |name, arity| context.find_or_create_function_declaration(name, arity))?; - - let variable_1 = foliage::Variable - { - declaration: std::rc::Rc::clone(¶meter_z1), - }; - - let variable_2 = foliage::Variable - { - declaration: std::rc::Rc::clone(¶meter_z2), - }; - - let comparison_operator - = super::common::translate_comparison_operator(comparison.comparison_type()); - - 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), - })) - }, - _ => Err(crate::Error::new_unsupported_language_feature( - "body literals other than Booleans, terms, or comparisons")), - } -} - -pub fn translate_body(body_literals: &[clingo::ast::BodyLiteral], context: &mut Context) - -> Result -{ - body_literals.iter() - .map(|body_literal| translate_body_literal(body_literal, context) - .map(|value| Box::new(value))) - .collect::>() -} +pub use context::Context; +use translate_body::translate_body; pub fn read(rule: &clingo::ast::Rule, context: &mut Context) { diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs new file mode 100644 index 0000000..294eb49 --- /dev/null +++ b/src/translate/verify_properties/context.rs @@ -0,0 +1,77 @@ +pub struct ScopedFormula +{ + free_variable_declarations: foliage::VariableDeclarations, + formula: foliage::Formula, +} + +pub struct Context +{ + scoped_formulas: Vec, + function_declarations: foliage::FunctionDeclarations, + predicate_declarations: foliage::PredicateDeclarations, + variable_declaration_stack: foliage::VariableDeclarationStack, +} + +impl Context +{ + pub fn new() -> Self + { + Self + { + scoped_formulas: vec![], + function_declarations: foliage::FunctionDeclarations::new(), + predicate_declarations: foliage::PredicateDeclarations::new(), + variable_declaration_stack: foliage::VariableDeclarationStack::new(), + } + } + + pub fn find_or_create_predicate_declaration(&mut self, name: &str, arity: usize) + -> std::rc::Rc + { + match self.predicate_declarations.iter() + .find(|x| x.name == name && x.arity == arity) + { + Some(value) => std::rc::Rc::clone(value), + None => + { + let declaration = foliage::PredicateDeclaration + { + name: name.to_owned(), + arity, + }; + let declaration = std::rc::Rc::new(declaration); + + self.predicate_declarations.insert(std::rc::Rc::clone(&declaration)); + + log::debug!("new predicate declaration: {}/{}", name, arity); + + declaration + }, + } + } + + pub fn find_or_create_function_declaration(&mut self, name: &str, arity: usize) + -> std::rc::Rc + { + match self.function_declarations.iter() + .find(|x| x.name == name && x.arity == arity) + { + Some(value) => std::rc::Rc::clone(value), + None => + { + let declaration = foliage::FunctionDeclaration + { + name: name.to_owned(), + arity, + }; + let declaration = std::rc::Rc::new(declaration); + + self.function_declarations.insert(std::rc::Rc::clone(&declaration)); + + log::debug!("new function declaration: {}/{}", name, arity); + + declaration + }, + } + } +} diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs new file mode 100644 index 0000000..c64a1bb --- /dev/null +++ b/src/translate/verify_properties/translate_body.rs @@ -0,0 +1,158 @@ +pub fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign, + context: &mut super::Context) + -> Result +{ + let function = match body_term.term_type() + { + clingo::ast::TermType::Function(value) => value, + _ => return Err(crate::Error::new_unsupported_language_feature("only functions supported as body terms")), + }; + + let function_name = function.name().map_err(|error| crate::Error::new_decode_identifier(error))?; + + let predicate_declaration = context.find_or_create_predicate_declaration(function_name, + function.arguments().len()); + + let parameters = function.arguments().iter().map(|_| std::rc::Rc::new( + foliage::VariableDeclaration + { + name: "".to_string(), + })) + .collect::>(); + + let predicate_arguments = parameters.iter().map( + |parameter| Box::new(foliage::Term::Variable(foliage::Variable{declaration: std::rc::Rc::clone(parameter)}))) + .collect::>(); + + let predicate = foliage::Predicate + { + declaration: predicate_declaration, + arguments: predicate_arguments, + }; + + let predicate_literal = match sign + { + clingo::ast::Sign::None + | clingo::ast::Sign::DoubleNegation + => foliage::Formula::Predicate(predicate), + clingo::ast::Sign::Negation + => foliage::Formula::Not(Box::new(foliage::Formula::Predicate(predicate))), + }; + + if function.arguments().is_empty() + { + return Ok(predicate_literal); + } + + let mut i = 0; + + let mut arguments = function.arguments().iter().map(|x| + { + let result = crate::translate::common::choose_value_in_term(x, ¶meters[i], + |name, arity| context.find_or_create_function_declaration(name, arity)) + .map(|x| Box::new(x)); + i += 1; + result + }) + .collect::, _>>()?; + + arguments.push(Box::new(predicate_literal)); + + let and = foliage::Formula::And(arguments); + + Ok(foliage::Formula::Exists(foliage::Exists + { + parameters, + argument: Box::new(and), + })) +} + +pub fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, context: &mut super::Context) + -> Result +{ + match body_literal.sign() + { + clingo::ast::Sign::None => (), + _ => return Err(crate::Error::new_unsupported_language_feature( + "signed body literals")), + } + + let literal = match body_literal.body_literal_type() + { + clingo::ast::BodyLiteralType::Literal(literal) => literal, + _ => return Err(crate::Error::new_unsupported_language_feature( + "only plain body literals supported")), + }; + + match literal.literal_type() + { + clingo::ast::LiteralType::Boolean(value) => + { + match literal.sign() + { + clingo::ast::Sign::None => (), + _ => return Err(crate::Error::new_logic("unexpected negated Boolean value")), + } + + Ok(foliage::Formula::Boolean(value)) + }, + clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(), context), + clingo::ast::LiteralType::Comparison(comparison) => + { + let new_variable_declaration = || std::rc::Rc::new(foliage::VariableDeclaration + { + name: "".to_string() + }); + + let parameters = vec![new_variable_declaration(), new_variable_declaration()]; + + let parameter_z1 = ¶meters[0]; + let parameter_z2 = ¶meters[1]; + + let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), ¶meter_z1, + |name, arity| context.find_or_create_function_declaration(name, arity))?; + let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), ¶meter_z2, + |name, arity| context.find_or_create_function_declaration(name, arity))?; + + let variable_1 = foliage::Variable + { + declaration: std::rc::Rc::clone(¶meter_z1), + }; + + let variable_2 = foliage::Variable + { + declaration: std::rc::Rc::clone(¶meter_z2), + }; + + let comparison_operator + = crate::translate::common::translate_comparison_operator(comparison.comparison_type()); + + 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), + })) + }, + _ => Err(crate::Error::new_unsupported_language_feature( + "body literals other than Booleans, terms, or comparisons")), + } +} + +pub fn translate_body(body_literals: &[clingo::ast::BodyLiteral], context: &mut super::Context) + -> Result +{ + body_literals.iter() + .map(|body_literal| translate_body_literal(body_literal, context) + .map(|value| Box::new(value))) + .collect::>() +}