diff --git a/src/main.rs b/src/main.rs index 37b3752..70128d9 100644 --- a/src/main.rs +++ b/src/main.rs @@ -14,6 +14,7 @@ impl clingo::StatementHandler for StatementHandler<'_> if let Err(error) = anthem::translate::verify_properties::read(rule, self.context) { log::error!("could not translate input program: {}", error); + return false; } }, _ => log::debug!("read statement (other kind)"), @@ -33,17 +34,32 @@ impl clingo::Logger for Logger } } -fn main() -> Result<(), Box> +fn main() { pretty_env_logger::init(); - let program = std::fs::read_to_string("test.lp")?; + let program = match std::fs::read_to_string("test.lp") + { + Ok(value) => value, + Err(error) => + { + log::error!("could not read input program: {}", error); + std::process::exit(1); + }, + }; let mut context = anthem::translate::verify_properties::Context::new(); let mut statement_handler = StatementHandler { context: &mut context }; - clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)?; - Ok(()) + match clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX) + { + Ok(()) => (), + Err(error) => + { + log::error!("could not translate input program: {}", error); + std::process::exit(1); + }, + } } diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 8b455b9..16c2494 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -9,18 +9,22 @@ use translate_head::determine_head_type; pub fn read(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crate::Error> { - let test = translate_body(rule.body(), context)?; + let translated_body = translate_body(rule.body(), context)?; - println!("{:?}", test); - - let test = determine_head_type(rule.head(), + let head_type = determine_head_type(rule.head(), |name, arity| context.find_or_create_predicate_declaration(name, arity))?; - match test + match head_type { - translate_head::HeadType::ChoiceWithSingleAtom(_) => println!("choice single"), - translate_head::HeadType::IntegrityConstraint => println!("integrity"), - translate_head::HeadType::Trivial => println!("trivial"), + translate_head::HeadType::ChoiceWithSingleAtom(test) => + log::debug!("translating choice rule with single atom"), + translate_head::HeadType::IntegrityConstraint => + log::debug!("translating integrity constraint"), + translate_head::HeadType::Trivial => + { + log::debug!("skipping trivial rule"); + return Ok(()); + }, _ => (), } diff --git a/src/translate/verify_properties/translate_head.rs b/src/translate/verify_properties/translate_head.rs index 4e5b799..da8996d 100644 --- a/src/translate/verify_properties/translate_head.rs +++ b/src/translate/verify_properties/translate_head.rs @@ -1,7 +1,7 @@ pub struct HeadAtom<'a> { - predicate_declaration: std::rc::Rc, - arguments: &'a [clingo::ast::Term<'a>], + pub predicate_declaration: std::rc::Rc, + pub arguments: &'a [clingo::ast::Term<'a>], } pub enum HeadType<'a> @@ -35,6 +35,29 @@ where match head_literal.head_literal_type() { + 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")), + }; + + Ok(HeadType::SingleAtom(create_head_atom(function)?)) + }, clingo::ast::HeadLiteralType::Aggregate(aggregate) => { if aggregate.left_guard().is_some() || aggregate.right_guard().is_some() @@ -65,33 +88,8 @@ where _ => return Err(crate::Error::new_unsupported_language_feature("elements other than atoms in aggregates")), }; - return Ok(HeadType::ChoiceWithSingleAtom(create_head_atom(function)?)); + 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)?)); - }, - _ => (), + _ => Err(crate::Error::new_unsupported_language_feature("elements other than literals and aggregates in rule head")), } - - Ok(HeadType::Annotation) }