From 6145c2cf1a8a861cda110d0d4c67d36a42802d6f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 31 Jan 2020 17:19:44 +0100 Subject: [PATCH] Translate body of rules for verifying properties --- Cargo.toml | 2 + src/error.rs | 97 +++++++++++++ src/lib.rs | 5 +- src/main.rs | 6 +- src/translate.rs | 1 + src/translate/common.rs | 93 ++++++++++++ src/translate/verify_properties.rs | 220 ++++++++++++++++++++++++++++- 7 files changed, 414 insertions(+), 10 deletions(-) create mode 100644 src/error.rs create mode 100644 src/translate/common.rs diff --git a/Cargo.toml b/Cargo.toml index c4c1d26..a091148 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,6 +6,8 @@ edition = "2018" [dependencies] clingo = "0.6" +log = "0.4" +pretty_env_logger = "0.3" [dependencies.foliage] git = "ssh://gitea@git.luehne.de/patrick/foliage-rs.git" diff --git a/src/error.rs b/src/error.rs new file mode 100644 index 0000000..6afbc6f --- /dev/null +++ b/src/error.rs @@ -0,0 +1,97 @@ +pub type Source = Box; + +pub enum Kind +{ + Logic(&'static str), + UnsupportedLanguageFeature(&'static str), + NotYetImplemented(&'static str), + DecodeIdentifier, +} + +pub struct Error +{ + pub kind: Kind, + pub source: Option, +} + +impl Error +{ + pub(crate) fn new(kind: Kind) -> Self + { + Self + { + kind, + source: None, + } + } + + pub(crate) fn with>(mut self, source: S) -> Self + { + self.source = Some(source.into()); + self + } + + pub(crate) fn new_logic(description: &'static str) -> Self + { + Self::new(Kind::Logic(description)) + } + + pub(crate) fn new_unsupported_language_feature(description: &'static str) -> Self + { + Self::new(Kind::UnsupportedLanguageFeature(description)) + } + + pub(crate) fn new_not_yet_implemented(description: &'static str) -> Self + { + Self::new(Kind::NotYetImplemented(description)) + } + + pub(crate) fn new_decode_identifier>(source: S) -> Self + { + Self::new(Kind::DecodeIdentifier).with(source) + } +} + +impl std::fmt::Debug for Error +{ + fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + match &self.kind + { + Kind::Logic(ref description) => write!(formatter, + "logic error, please report to bug tracker ({})", description), + Kind::UnsupportedLanguageFeature(ref description) => write!(formatter, + "language feature not yet supported ({})", description), + Kind::NotYetImplemented(ref description) => write!(formatter, + "not yet implemented ({})", description), + Kind::DecodeIdentifier => write!(formatter, "could not decode identifier"), + }?; + + if let Some(source) = &self.source + { + write!(formatter, "\nerror source: {}", source)?; + } + + Ok(()) + } +} + +impl std::fmt::Display for Error +{ + fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(formatter, "{:?}", self) + } +} + +impl std::error::Error for Error +{ + fn source(&self) -> Option<&(dyn std::error::Error + 'static)> + { + match &self.source + { + Some(source) => Some(source.as_ref()), + None => None, + } + } +} diff --git a/src/lib.rs b/src/lib.rs index 242a0ca..c746c8d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,5 +1,4 @@ +pub mod error; pub mod translate; -pub struct Context -{ -} +pub use error::Error; diff --git a/src/main.rs b/src/main.rs index ced6256..242d15a 100644 --- a/src/main.rs +++ b/src/main.rs @@ -13,7 +13,7 @@ impl clingo::StatementHandler for StatementHandler<'_> { anthem::translate::verify_properties::read(rule, self.context) }, - _ => println!("got other kind of statement"), + _ => log::debug!("read statement (other kind)"), } true @@ -26,12 +26,14 @@ impl clingo::Logger for Logger { fn log(&mut self, code: clingo::Warning, message: &str) { - println!("clingo warning ({:?}): {}", code, message); + log::warn!("clingo warning ({:?}): {}", code, message); } } fn main() -> Result<(), Box> { + pretty_env_logger::init(); + let program = std::fs::read_to_string("test.lp")?; let mut context = anthem::translate::verify_properties::Context::new(); let mut statement_handler = StatementHandler diff --git a/src/translate.rs b/src/translate.rs index 84b1437..854878b 100644 --- a/src/translate.rs +++ b/src/translate.rs @@ -1 +1,2 @@ +mod common; pub mod verify_properties; diff --git a/src/translate/common.rs b/src/translate/common.rs new file mode 100644 index 0000000..c63a7f8 --- /dev/null +++ b/src/translate/common.rs @@ -0,0 +1,93 @@ +pub fn translate_comparison_operator(comparison_operator: clingo::ast::ComparisonOperator) + -> foliage::ComparisonOperator +{ + match comparison_operator + { + clingo::ast::ComparisonOperator::GreaterThan + => foliage::ComparisonOperator::Greater, + clingo::ast::ComparisonOperator::LessThan + => foliage::ComparisonOperator::Less, + clingo::ast::ComparisonOperator::LessEqual + => foliage::ComparisonOperator::LessOrEqual, + clingo::ast::ComparisonOperator::GreaterEqual + => foliage::ComparisonOperator::GreaterOrEqual, + clingo::ast::ComparisonOperator::NotEqual + => foliage::ComparisonOperator::NotEqual, + clingo::ast::ComparisonOperator::Equal + => foliage::ComparisonOperator::Equal, + } +} + +pub fn choose_value_in_primitive(term: Box, + variable_declaration: &std::rc::Rc) + -> foliage::Comparison +{ + let variable = foliage::Variable + { + declaration: std::rc::Rc::clone(variable_declaration), + }; + + foliage::Comparison + { + operator: foliage::ComparisonOperator::Equal, + left: Box::new(foliage::Term::Variable(variable)), + right: term, + } +} + +pub fn choose_value_in_term(term: &clingo::ast::Term, + variable_declaration: &std::rc::Rc, + mut find_or_create_function_declaration: F) + -> Result +where + F: FnMut(&str, usize) -> std::rc::Rc +{ + match term.term_type() + { + 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() + .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() + .map_err(|error| crate::Error::new_logic("clingo error").with(error))? + .to_string())), + variable_declaration))), + clingo::SymbolType::Function => + { + let arguments = symbol.arguments() + .map_err(|error| crate::Error::new_logic("clingo error").with(error))?; + + // Functions with arguments are represented as clingo::ast::Function by the parser. + // At this point, we only have to handle (0-ary) constants + if !arguments.is_empty() + { + return Err(crate::Error::new_logic("unexpected arguments, expected (0-ary) constant symbol")); + } + + 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 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(foliage::Formula::Boolean(false)) + } +} diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 9e37df2..032016e 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -7,6 +7,9 @@ pub struct ScopedFormula pub struct Context { scoped_formulas: Vec, + function_declarations: foliage::FunctionDeclarations, + predicate_declarations: foliage::PredicateDeclarations, + variable_declaration_stack: foliage::VariableDeclarationStack, } impl Context @@ -16,16 +19,223 @@ impl Context 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 ... +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 fn read(rule: &clingo::ast::Rule, context: &mut Context) { - let mut variable_declaration_stack: foliage::VariableDeclarationStack; - - println!("{:?}", rule.head()); - println!("{:?}", rule.body()); + println!("{:?}", translate_body(rule.body(), context)); }