From aaea04d51b721d0751626d6de4af184fe6249112 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sat, 1 Feb 2020 15:32:41 +0100 Subject: [PATCH] Work in progress --- Cargo.toml | 4 +- src/main.rs | 5 +- src/translate/verify_properties.rs | 24 ++++- .../verify_properties/translate_head.rs | 97 +++++++++++++++++++ 4 files changed, 125 insertions(+), 5 deletions(-) create mode 100644 src/translate/verify_properties/translate_head.rs diff --git a/Cargo.toml b/Cargo.toml index a091148..ceed8ae 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,10 +5,12 @@ authors = ["Patrick Lühne "] edition = "2018" [dependencies] -clingo = "0.6" log = "0.4" pretty_env_logger = "0.3" +[dependencies.clingo] +path = "../clingo-rs" + [dependencies.foliage] git = "ssh://gitea@git.luehne.de/patrick/foliage-rs.git" branch = "refactoring" diff --git a/src/main.rs b/src/main.rs index 242d15a..37b3752 100644 --- a/src/main.rs +++ b/src/main.rs @@ -11,7 +11,10 @@ impl clingo::StatementHandler for StatementHandler<'_> { clingo::ast::StatementType::Rule(ref rule) => { - anthem::translate::verify_properties::read(rule, self.context) + if let Err(error) = anthem::translate::verify_properties::read(rule, self.context) + { + log::error!("could not translate input program: {}", error); + } }, _ => log::debug!("read statement (other kind)"), } diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index ce560e8..8b455b9 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -1,10 +1,28 @@ mod context; mod translate_body; +mod translate_head; pub use context::Context; -use translate_body::translate_body; -pub fn read(rule: &clingo::ast::Rule, context: &mut Context) +use translate_body::translate_body; +use translate_head::determine_head_type; + +pub fn read(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crate::Error> { - println!("{:?}", translate_body(rule.body(), context)); + let test = translate_body(rule.body(), context)?; + + println!("{:?}", test); + + let test = determine_head_type(rule.head(), + |name, arity| context.find_or_create_predicate_declaration(name, arity))?; + + match test + { + translate_head::HeadType::ChoiceWithSingleAtom(_) => println!("choice single"), + translate_head::HeadType::IntegrityConstraint => println!("integrity"), + translate_head::HeadType::Trivial => println!("trivial"), + _ => (), + } + + Ok(()) } diff --git a/src/translate/verify_properties/translate_head.rs b/src/translate/verify_properties/translate_head.rs new file mode 100644 index 0000000..4e5b799 --- /dev/null +++ b/src/translate/verify_properties/translate_head.rs @@ -0,0 +1,97 @@ +pub struct HeadAtom<'a> +{ + predicate_declaration: std::rc::Rc, + arguments: &'a [clingo::ast::Term<'a>], +} + +pub enum HeadType<'a> +{ + SingleAtom(HeadAtom<'a>), + ChoiceWithSingleAtom(HeadAtom<'a>), + IntegrityConstraint, + Trivial, +} + +pub fn determine_head_type<'a, F>(head_literal: &'a clingo::ast::HeadLiteral, + mut find_or_create_predicate_declaration: F) + -> Result, crate::Error> +where + F: FnMut(&str, usize) -> std::rc::Rc +{ + let mut create_head_atom = |function: &'a clingo::ast::Function| -> Result<_, crate::Error> + { + let function_name = function.name() + .map_err(|error| crate::Error::new_decode_identifier(error))?; + + let predicate_declaration + = find_or_create_predicate_declaration(function_name, function.arguments().len()); + + Ok(HeadAtom + { + predicate_declaration, + arguments: function.arguments(), + }) + }; + + match head_literal.head_literal_type() + { + clingo::ast::HeadLiteralType::Aggregate(aggregate) => + { + if aggregate.left_guard().is_some() || aggregate.right_guard().is_some() + { + return Err(crate::Error::new_unsupported_language_feature("aggregates with guards")); + } + + let literal = match aggregate.elements().split_first() + { + Some((first, remainder)) if remainder.is_empty() => first.literal(), + _ => return Err(crate::Error::new_unsupported_language_feature("aggregates not containing exactly one element")), + }; + + if literal.sign() != clingo::ast::Sign::None + { + return Err(crate::Error::new_unsupported_language_feature("negated literals in aggregates")); + } + + let term = match literal.literal_type() + { + clingo::ast::LiteralType::Symbolic(term) => term, + _ => return Err(crate::Error::new_unsupported_language_feature("elements other than terms in aggregates")), + }; + + let function = match term.term_type() + { + clingo::ast::TermType::Function(function) => function, + _ => return Err(crate::Error::new_unsupported_language_feature("elements other than atoms in aggregates")), + }; + + return Ok(HeadType::ChoiceWithSingleAtom(create_head_atom(function)?)); + }, + clingo::ast::HeadLiteralType::Literal(literal) => + { + if literal.sign() != clingo::ast::Sign::None + { + return Err(crate::Error::new_unsupported_language_feature("negated head literals")); + } + + let term = match literal.literal_type() + { + clingo::ast::LiteralType::Boolean(true) => return Ok(HeadType::Trivial), + clingo::ast::LiteralType::Boolean(false) => return Ok(HeadType::IntegrityConstraint), + clingo::ast::LiteralType::Symbolic(term) => term, + _ => return Err(crate::Error::new_unsupported_language_feature("elements other than terms in rule head")), + }; + + let function = match term.term_type() + { + clingo::ast::TermType::Function(function) => function, + _ => return Err(crate::Error::new_unsupported_language_feature("elements other than atoms in rule head")), + }; + + return Ok(HeadType::ChoiceWithSingleAtom(create_head_atom(function)?)); + }, + _ => (), + } + + Ok(HeadType::Annotation) +}