patrick/anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Determine head type of input rules

Browse Source
This commit is contained in:
Patrick Lühne 2020-02-01 17:13:43 +01:00
parent aaea04d51b
commit 142531d334
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
3 changed files with 59 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
src/main.rs
View File

@ -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<dyn std::error::Error>>
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);
},
}
}

20
src/translate/verify_properties.rs
View File

@ -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(());
},
_ => (),
}

56
src/translate/verify_properties/translate_head.rs
View File

@ -1,7 +1,7 @@
pub struct HeadAtom<'a>
{
predicate_declaration: std::rc::Rc<foliage::PredicateDeclaration>,
arguments: &'a [clingo::ast::Term<'a>],
pub predicate_declaration: std::rc::Rc<foliage::PredicateDeclaration>,
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)
}