Use foliage’s built-in variable declaration stack

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,

src/translate/verify_properties/context.rs

@@ -22,7 +22,7 @@ pub(crate) struct Context
 
 	pub function_declarations: std::cell::RefCell<foliage::FunctionDeclarations>,
 	pub predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
-	pub variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
+	pub variable_declaration_stack: std::cell::RefCell<foliage::VariableDeclarationStack>,
 	pub variable_declaration_domains: std::cell::RefCell<VariableDeclarationDomains>,
 	pub program_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
 	pub integer_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
@@ -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:

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

src/utils/variable_declaration_stack.rs

@@ -1,70 +0,0 @@
-pub(crate) struct VariableDeclarationStack
-{
-	pub free_variable_declarations: foliage::VariableDeclarations,
-	bound_variable_declaration_stack: Vec<std::rc::Rc<foliage::VariableDeclarations>>,
-}
-
-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<std::rc::Rc<foliage::VariableDeclaration>>
-	{
-		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<foliage::VariableDeclaration>
-	{
-		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<foliage::VariableDeclarations>)
-	{
-		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"))
-	}
-}