From ab7c6d18285fd76b476841453947cbf74291414f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Mon, 11 May 2020 03:58:30 +0200 Subject: [PATCH] Rename ScopedFormula to OpenFormula --- src/input/specification.rs | 23 +++++++++++------------ src/translate/verify_properties.rs | 16 ++++++++-------- src/utils.rs | 6 ------ src/utils/closures.rs | 20 ++++++++++---------- 4 files changed, 29 insertions(+), 36 deletions(-) diff --git a/src/input/specification.rs b/src/input/specification.rs index c42ecc2..f41135f 100644 --- a/src/input/specification.rs +++ b/src/input/specification.rs @@ -85,8 +85,8 @@ where Ok(()) } -fn closed_formula<'i, D>(input: &'i str, declarations: &D) - -> Result<(crate::ScopedFormula, &'i str), crate::Error> +fn open_formula<'i, D>(input: &'i str, declarations: &D) + -> Result<(foliage::OpenFormula, &'i str), crate::Error> where D: foliage::FindOrCreateFunctionDeclaration + foliage::FindOrCreatePredicateDeclaration @@ -103,19 +103,18 @@ where remaining_input_characters.next(); let remaining_input = remaining_input_characters.as_str(); - let closed_formula = foliage::parse::formula(formula_input, declarations) + let open_formula = foliage::parse::formula(formula_input, declarations) .map_err(|error| crate::Error::new_parse_formula(error))?; - formula_assign_variable_declaration_domains(&closed_formula.formula, declarations)?; + formula_assign_variable_declaration_domains(&open_formula.formula, declarations)?; - // TODO: get rid of ScopedFormula - let scoped_formula = crate::ScopedFormula + let open_formula = foliage::OpenFormula { - free_variable_declarations: closed_formula.free_variable_declarations, - formula: closed_formula.formula, + free_variable_declarations: open_formula.free_variable_declarations, + formula: open_formula.formula, }; - Ok((scoped_formula, remaining_input)) + Ok((open_formula, remaining_input)) } // TODO: rename @@ -126,15 +125,15 @@ where + foliage::FindOrCreatePredicateDeclaration + crate::traits::AssignVariableDeclarationDomain, { - let (closed_formula, input) = closed_formula(input, declarations)?; + let (open_formula, input) = open_formula(input, declarations)?; - if !closed_formula.free_variable_declarations.is_empty() + if !open_formula.free_variable_declarations.is_empty() { // TODO: improve panic!("formula may not contain free variables"); } - Ok((closed_formula.formula, input)) + Ok((open_formula.formula, input)) } fn formula_statement_body<'i>(input: &'i str, problem: &crate::Problem) diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index e3442c1..fee701a 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -8,7 +8,7 @@ use crate::traits::AssignVariableDeclarationDomain as _; struct PredicateDefinitions { pub parameters: std::rc::Rc, - pub definitions: Vec, + pub definitions: Vec, } type Definitions = @@ -99,13 +99,13 @@ impl<'p> Translator<'p> let completed_definition = foliage::Formula::if_and_only_if(vec![head_predicate, or]); - let scoped_formula = crate::ScopedFormula + let open_formula = foliage::OpenFormula { free_variable_declarations: predicate_definitions.parameters, formula: completed_definition, }; - crate::universal_closure(scoped_formula) + crate::universal_closure(open_formula) }, // This predicate has no definitions, so universally falsify it None => @@ -130,13 +130,13 @@ impl<'p> Translator<'p> let not = foliage::Formula::not(Box::new(head_predicate)); - let scoped_formula = crate::ScopedFormula + let open_formula = foliage::OpenFormula { free_variable_declarations: parameters, formula: not, }; - crate::universal_closure(scoped_formula) + crate::universal_closure(open_formula) }, } }; @@ -255,7 +255,7 @@ impl<'p> Translator<'p> _ => foliage::Formula::and(definition_arguments), }; - let definition = crate::ScopedFormula + let definition = foliage::OpenFormula { free_variable_declarations: std::rc::Rc::new(free_variable_declarations), formula: definition, @@ -286,13 +286,13 @@ impl<'p> Translator<'p> _ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))), }; - let scoped_formula = crate::ScopedFormula + let open_formula = foliage::OpenFormula { free_variable_declarations: std::rc::Rc::new(free_variable_declarations), formula, }; - let integrity_constraint = crate::universal_closure(scoped_formula); + let integrity_constraint = crate::universal_closure(open_formula); let statement = crate::problem::Statement::new( crate::problem::StatementKind::Program, integrity_constraint) diff --git a/src/utils.rs b/src/utils.rs index 7427ed0..28519ee 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -37,9 +37,3 @@ impl std::fmt::Display for Domain write!(formatter, "{:?}", self) } } - -pub(crate) struct ScopedFormula -{ - pub free_variable_declarations: std::rc::Rc, - pub formula: foliage::Formula, -} diff --git a/src/utils/closures.rs b/src/utils/closures.rs index c8e67ee..ce8b5b4 100644 --- a/src/utils/closures.rs +++ b/src/utils/closures.rs @@ -1,19 +1,19 @@ -pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula +pub(crate) fn existential_closure(open_formula: foliage::OpenFormula) -> foliage::Formula { - match scoped_formula.free_variable_declarations.is_empty() + match open_formula.free_variable_declarations.is_empty() { - true => scoped_formula.formula, - false => foliage::Formula::exists(scoped_formula.free_variable_declarations, - Box::new(scoped_formula.formula)), + true => open_formula.formula, + false => foliage::Formula::exists(open_formula.free_variable_declarations, + Box::new(open_formula.formula)), } } -pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula +pub(crate) fn universal_closure(open_formula: foliage::OpenFormula) -> foliage::Formula { - match scoped_formula.free_variable_declarations.is_empty() + match open_formula.free_variable_declarations.is_empty() { - true => scoped_formula.formula, - false => foliage::Formula::for_all(scoped_formula.free_variable_declarations, - Box::new(scoped_formula.formula)), + true => open_formula.formula, + false => foliage::Formula::for_all(open_formula.free_variable_declarations, + Box::new(open_formula.formula)), } }