From 84bec338ae8e3ceb16c664e5a5ee949ff6608d8d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 17 Apr 2020 01:44:16 +0200 Subject: [PATCH] =?UTF-8?q?Use=20foliage=E2=80=99s=20built-in=20variable?= =?UTF-8?q?=20declaration=20stack?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/translate/verify_properties.rs | 5 +- src/translate/verify_properties/context.rs | 4 +- src/utils.rs | 2 - src/utils/variable_declaration_stack.rs | 70 ---------------------- 4 files changed, 5 insertions(+), 76 deletions(-) delete mode 100644 src/utils/variable_declaration_stack.rs diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index d5cdcda..44675fc 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -371,7 +371,8 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E let definitions = definitions.get_mut(&head_atom.predicate_declaration).unwrap(); let head_atom_parameters = std::rc::Rc::clone(&definitions.head_atom_parameters); - context.variable_declaration_stack.borrow_mut().push(head_atom_parameters); + let variable_declaration_stack_guard = foliage::VariableDeclarationStack::push( + &context.variable_declaration_stack, head_atom_parameters); let mut definition_arguments = translate_body(rule.body(), context)?; @@ -401,7 +402,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E definition_arguments.push(translated_head_term); } - context.variable_declaration_stack.borrow_mut().pop()?; + drop(variable_declaration_stack_guard); let free_variable_declarations = std::mem::replace( &mut context.variable_declaration_stack.borrow_mut().free_variable_declarations, diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs index 1e20050..a0a9a80 100644 --- a/src/translate/verify_properties/context.rs +++ b/src/translate/verify_properties/context.rs @@ -22,7 +22,7 @@ pub(crate) struct Context pub function_declarations: std::cell::RefCell, pub predicate_declarations: std::cell::RefCell, - pub variable_declaration_stack: std::cell::RefCell, + pub variable_declaration_stack: std::cell::RefCell, pub variable_declaration_domains: std::cell::RefCell, pub program_variable_declaration_ids: std::cell::RefCell, pub integer_variable_declaration_ids: std::cell::RefCell, @@ -45,7 +45,7 @@ impl Context function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()), predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()), variable_declaration_stack: - std::cell::RefCell::new(crate::VariableDeclarationStack::new()), + std::cell::RefCell::new(foliage::VariableDeclarationStack::new()), variable_declaration_domains: std::cell::RefCell::new(VariableDeclarationDomains::new()), program_variable_declaration_ids: diff --git a/src/utils.rs b/src/utils.rs index 2439369..f8cb111 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -1,8 +1,6 @@ mod arithmetic_terms; -mod variable_declaration_stack; pub(crate) use arithmetic_terms::*; -pub(crate) use variable_declaration_stack::*; #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)] pub(crate) enum OperatorNotation diff --git a/src/utils/variable_declaration_stack.rs b/src/utils/variable_declaration_stack.rs deleted file mode 100644 index 7728cec..0000000 --- a/src/utils/variable_declaration_stack.rs +++ /dev/null @@ -1,70 +0,0 @@ -pub(crate) struct VariableDeclarationStack -{ - pub free_variable_declarations: foliage::VariableDeclarations, - bound_variable_declaration_stack: Vec>, -} - -impl VariableDeclarationStack -{ - pub fn new() -> Self - { - Self - { - free_variable_declarations: foliage::VariableDeclarations::new(), - bound_variable_declaration_stack: vec![], - } - } - - pub fn find(&self, variable_name: &str) -> Option> - { - for variable_declarations in self.bound_variable_declaration_stack.iter().rev() - { - if let Some(variable_declaration) = variable_declarations.iter().find(|x| x.name == variable_name) - { - return Some(std::rc::Rc::clone(&variable_declaration)); - } - } - - if let Some(variable_declaration) = self.free_variable_declarations.iter().find(|x| x.name == variable_name) - { - return Some(std::rc::Rc::clone(&variable_declaration)); - } - - None - } - - pub fn find_or_create(&mut self, variable_name: &str) -> std::rc::Rc - { - if let Some(variable_declaration) = self.find(variable_name) - { - return variable_declaration; - } - - let variable_declaration = foliage::VariableDeclaration - { - name: variable_name.to_owned(), - }; - let variable_declaration = std::rc::Rc::new(variable_declaration); - - self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration)); - - variable_declaration - } - - pub fn is_empty(&self) -> bool - { - self.free_variable_declarations.is_empty() - && self.bound_variable_declaration_stack.is_empty() - } - - pub fn push(&mut self, bound_variable_declarations: std::rc::Rc) - { - self.bound_variable_declaration_stack.push(bound_variable_declarations); - } - - pub fn pop(&mut self) -> Result<(), crate::Error> - { - self.bound_variable_declaration_stack.pop().map(|_| ()) - .ok_or(crate::Error::new_logic("variable stack not in expected state")) - } -}