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

Move closure functions to utils module

Browse Source
This commit is contained in:
Patrick Lühne 2020-02-09 10:26:24 +07:00
parent c3860c1bf1
commit f83695b5dc
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 26 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
src/translate/verify_properties.rs
View File

@ -117,7 +117,7 @@ where
Some(definitions) =>
{
let or_arguments = definitions.definitions.into_iter()
.map(|x| existential_closure(x))
.map(|x| crate::existential_closure(x))
.collect::<Vec<_>>();
let or = foliage::Formula::or(or_arguments);
@ -137,7 +137,7 @@ where
formula: Box::new(completed_definition),
};
universal_closure(scoped_formula)
crate::universal_closure(scoped_formula)
},
// This predicate has no definitions, so universally falsify it
None =>
@ -168,7 +168,7 @@ where
formula: Box::new(not),
};
universal_closure(scoped_formula)
crate::universal_closure(scoped_formula)
},
}
};
@ -446,7 +446,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
formula: Box::new(formula),
};
let integrity_constraint = universal_closure(scoped_formula);
let integrity_constraint = crate::universal_closure(scoped_formula);
log::debug!("translated integrity constraint: {}",
crate::output::human_readable::display_formula(&integrity_constraint, None,
@ -459,23 +459,3 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
Ok(())
}
fn existential_closure(scoped_formula: crate::ScopedFormula) -> Box<foliage::Formula>
{
match scoped_formula.free_variable_declarations.is_empty()
{
true => scoped_formula.formula,
false => Box::new(foliage::Formula::exists(scoped_formula.free_variable_declarations,
scoped_formula.formula)),
}
}
fn universal_closure(scoped_formula: crate::ScopedFormula) -> Box<foliage::Formula>
{
match scoped_formula.free_variable_declarations.is_empty()
{
true => scoped_formula.formula,
false => Box::new(foliage::Formula::for_all(scoped_formula.free_variable_declarations,
scoped_formula.formula)),
}
}

24
src/utils.rs
View File

@ -44,8 +44,25 @@ pub(crate) struct ScopedFormula
pub formula: Box<foliage::Formula>,
}
pub type InputConstantDeclarationDomains
= std::collections::BTreeMap<std::rc::Rc<foliage::FunctionDeclaration>, Domain>;
pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> Box<foliage::Formula>
{
match scoped_formula.free_variable_declarations.is_empty()
{
true => scoped_formula.formula,
false => Box::new(foliage::Formula::exists(scoped_formula.free_variable_declarations,
scoped_formula.formula)),
}
}
pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> Box<foliage::Formula>
{
match scoped_formula.free_variable_declarations.is_empty()
{
true => scoped_formula.formula,
false => Box::new(foliage::Formula::for_all(scoped_formula.free_variable_declarations,
scoped_formula.formula)),
}
}
pub fn parse_predicate_declaration(input: &str)
-> Result<std::rc::Rc<foliage::PredicateDeclaration>, crate::Error>
@ -75,6 +92,9 @@ pub fn parse_predicate_declaration(input: &str)
}))
}
pub type InputConstantDeclarationDomains
= std::collections::BTreeMap<std::rc::Rc<foliage::FunctionDeclaration>, Domain>;
pub fn parse_constant_declaration(input: &str)
-> Result<(std::rc::Rc<foliage::FunctionDeclaration>, crate::Domain), crate::Error>
{