diff --git a/src/parse.rs b/src/parse.rs
index 5f72668..5632474 100644
--- a/src/parse.rs
+++ b/src/parse.rs
@@ -9,23 +9,3 @@ pub(crate) use literals::{boolean, integer, special_integer, string};
 pub(crate) use names::{function_or_predicate_name, variable_name};
 pub use terms::term;
 pub use formulas::formula;
-
-pub struct Declarations
-{
-	function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
-	predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
-	free_variable_declarations: std::cell::RefCell<crate::VariableDeclarations>,
-}
-
-impl Declarations
-{
-	pub fn new() -> Self
-	{
-		Self
-		{
-			function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
-			predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
-			free_variable_declarations: std::cell::RefCell::new(vec![]),
-		}
-	}
-}
diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs
index 8885935..7d2869d 100644
--- a/src/parse/formulas.rs
+++ b/src/parse/formulas.rs
@@ -9,10 +9,12 @@ use nom::
 	sequence::{delimited, pair, preceded, terminated, tuple},
 };
 
-use super::{Declarations, boolean, word_boundary};
+use super::{boolean, word_boundary};
 
-pub fn predicate<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+pub fn predicate<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Predicate>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map
 	(
@@ -25,34 +27,17 @@ pub fn predicate<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDec
 				None => vec![],
 			};
 
-			let mut predicate_declarations = d.predicate_declarations.borrow_mut();
-
-			let declaration = match predicate_declarations.iter()
-				.find(|x| x.name == name && x.arity == arguments.len())
-			{
-				Some(declaration) => std::rc::Rc::clone(&declaration),
-				None =>
-				{
-					let declaration = crate::PredicateDeclaration
-					{
-						name: name.to_string(),
-						arity: arguments.len(),
-					};
-					let declaration = std::rc::Rc::new(declaration);
-
-					predicate_declarations.insert(std::rc::Rc::clone(&declaration));
-
-					declaration
-				},
-			};
+			let declaration = d.find_or_create_predicate_declaration(name, arguments.len());
 
 			crate::Predicate::new(declaration, arguments)
 		},
 	)(i)
 }
 
-fn not<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn not<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map
 	(
@@ -69,8 +54,10 @@ fn not<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationSt
 	)(i)
 }
 
-fn and<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn and<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formulas>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map_res
 	(
@@ -102,8 +89,10 @@ fn and<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationSt
 	)(i)
 }
 
-fn or<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn or<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formulas>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map_res
 	(
@@ -135,9 +124,10 @@ fn or<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationSta
 	)(i)
 }
 
-fn implies_left_to_right<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn implies_left_to_right<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map
 	(
@@ -165,9 +155,10 @@ fn implies_left_to_right<'i, 'v>(i: &'i str, d: &Declarations,
 	)(i)
 }
 
-fn implies_right_to_left<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn implies_right_to_left<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map
 	(
@@ -195,8 +186,10 @@ fn implies_right_to_left<'i, 'v>(i: &'i str, d: &Declarations,
 	)(i)
 }
 
-fn if_and_only_if<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn if_and_only_if<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formulas>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map_res
 	(
@@ -224,9 +217,11 @@ fn if_and_only_if<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDe
 	)(i)
 }
 
-fn quantified_formula<'i, 'b, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer, keyword: &'b str)
+fn quantified_formula<'i, 'b, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer,
+	keyword: &'b str)
 	-> IResult<&'i str, crate::QuantifiedFormula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	preceded
 	(
@@ -280,8 +275,10 @@ fn quantified_formula<'i, 'b, 'v>(i: &'i str, d: &Declarations,
 	)(i)
 }
 
-fn compare<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn compare<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Compare>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map
 	(
@@ -335,21 +332,26 @@ fn compare<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarati
 	)(i)
 }
 
-fn exists<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn exists<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::QuantifiedFormula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	quantified_formula(i, d, v, "exists")
 }
 
-fn for_all<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn for_all<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::QuantifiedFormula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	quantified_formula(i, d, v, "forall")
 }
 
-fn formula_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn formula_parenthesized<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	delimited
 	(
@@ -367,9 +369,10 @@ fn formula_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
 	)(i)
 }
 
-fn formula_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn formula_precedence_0<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -392,9 +395,10 @@ fn formula_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn formula_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn formula_precedence_1<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -412,9 +416,10 @@ fn formula_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn formula_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn formula_precedence_2<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -423,9 +428,10 @@ fn formula_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn formula_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn formula_precedence_3<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -438,9 +444,10 @@ fn formula_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn formula_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn formula_precedence_4<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -453,9 +460,10 @@ fn formula_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn formula_precedence_5<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn formula_precedence_5<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -465,9 +473,10 @@ fn formula_precedence_5<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn formula_precedence_6<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn formula_precedence_6<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -480,8 +489,10 @@ fn formula_precedence_6<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-pub fn formula<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+pub fn formula<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Formula>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	formula_precedence_6(i, d, v)
 }
@@ -489,9 +500,9 @@ pub fn formula<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDecla
 #[cfg(test)]
 mod tests
 {
-	use crate::parse::formulas::*;
-	use crate::parse::formulas as original;
 	use crate::{Formula, ImplicationDirection, Term, VariableDeclarationStackLayer};
+	use crate::parse::formulas as original;
+	use crate::utils::*;
 
 	fn formula(i: &str) -> Formula
 	{
diff --git a/src/parse/terms.rs b/src/parse/terms.rs
index 64f24f1..8bdb366 100644
--- a/src/parse/terms.rs
+++ b/src/parse/terms.rs
@@ -9,11 +9,12 @@ use nom::
 	sequence::{delimited, pair, preceded, terminated},
 };
 
-use super::{Declarations, boolean, function_or_predicate_name, integer, special_integer, string,
-	variable_name};
+use super::{boolean, function_or_predicate_name, integer, special_integer, string, variable_name};
 
-fn negative<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn negative<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map
 	(
@@ -37,8 +38,10 @@ fn negative<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarat
 	)(i)
 }
 
-fn absolute_value<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn absolute_value<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map
 	(
@@ -60,9 +63,11 @@ fn absolute_value<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDe
 	)(i)
 }
 
-pub(crate) fn function_or_predicate<'i, 'v>(i: &'i str, d: &Declarations,
+pub(crate) fn function_or_predicate<'i, 'v, D>(i: &'i str, d: &D,
 	v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, (&'i str, Option<crate::Terms>)>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	pair
 	(
@@ -97,8 +102,10 @@ pub(crate) fn function_or_predicate<'i, 'v>(i: &'i str, d: &Declarations,
 	)(i)
 }
 
-fn function<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+fn function<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Function>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	map
 	(
@@ -111,26 +118,7 @@ fn function<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarat
 				None => vec![],
 			};
 
-			let mut function_declarations = d.function_declarations.borrow_mut();
-
-			let declaration = match function_declarations.iter()
-				.find(|x| x.name == name && x.arity == arguments.len())
-			{
-				Some(declaration) => std::rc::Rc::clone(&declaration),
-				None =>
-				{
-					let declaration = crate::FunctionDeclaration
-					{
-						name: name.to_string(),
-						arity: arguments.len(),
-					};
-					let declaration = std::rc::Rc::new(declaration);
-
-					function_declarations.insert(std::rc::Rc::clone(&declaration));
-
-					declaration
-				},
-			};
+			let declaration = d.find_or_create_function_declaration(name, arguments.len());
 
 			crate::Function::new(declaration, arguments)
 		},
@@ -161,9 +149,10 @@ fn variable<'i, 'v>(i: &'i str, v: &'v crate::VariableDeclarationStackLayer)
 	)(i)
 }
 
-fn term_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn term_parenthesized<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	delimited
 	(
@@ -181,9 +170,10 @@ fn term_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
 	)(i)
 }
 
-fn term_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn term_precedence_0<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -222,9 +212,10 @@ fn term_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn term_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn term_precedence_1<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -233,9 +224,10 @@ fn term_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn term_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn term_precedence_2<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -266,9 +258,10 @@ fn term_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn term_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer)
+fn term_precedence_3<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -311,8 +304,10 @@ fn term_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-fn term_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
-	v: &'v crate::VariableDeclarationStackLayer) -> IResult<&'i str, crate::Term>
+fn term_precedence_4<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	alt
 	((
@@ -353,8 +348,10 @@ fn term_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
 	))(i)
 }
 
-pub fn term<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+pub fn term<'i, 'v, D>(i: &'i str, d: &D, v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, crate::Term>
+where
+	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration
 {
 	term_precedence_4(i, d, v)
 }
@@ -362,9 +359,9 @@ pub fn term<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarat
 #[cfg(test)]
 mod tests
 {
-	use crate::parse::terms::*;
-	use crate::parse::terms as original;
 	use crate::{Term, VariableDeclaration, VariableDeclarationStackLayer};
+	use crate::parse::terms as original;
+	use crate::utils::*;
 
 	fn term(i: &str) -> Term
 	{
diff --git a/src/utils.rs b/src/utils.rs
index 8da8e48..422eba7 100644
--- a/src/utils.rs
+++ b/src/utils.rs
@@ -1,20 +1,15 @@
-pub trait FindFunctionDeclaration
+pub trait FindOrCreateFunctionDeclaration
 {
-	fn find_function_declaration(&self, name: &str, arity: usize)
+	fn find_or_create_function_declaration(&self, name: &str, arity: usize)
 		-> std::rc::Rc<crate::FunctionDeclaration>;
 }
 
-pub trait FindPredicateDeclaration
+pub trait FindOrCreatePredicateDeclaration
 {
-	fn find_predicate_declaration(&self, name: &str, arity: usize)
+	fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
 		-> std::rc::Rc<crate::PredicateDeclaration>;
 }
 
-pub trait FindVariableDeclaration
-{
-	fn find_variable_declaration(&self, name: &str) -> std::rc::Rc<crate::VariableDeclaration>;
-}
-
 pub struct BoundVariableDeclarations<'p>
 {
 	parent: &'p VariableDeclarationStackLayer<'p>,
@@ -144,3 +139,81 @@ impl<'p> VariableDeclarationStackLayer<'p>
 		}
 	}
 }
+
+#[cfg(test)]
+pub struct Declarations
+{
+	function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
+	predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
+	//free_variable_declarations: std::cell::RefCell<crate::VariableDeclarations>,
+}
+
+#[cfg(test)]
+impl Declarations
+{
+	pub fn new() -> Self
+	{
+		Self
+		{
+			function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
+			predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
+			//free_variable_declarations: std::cell::RefCell::new(vec![]),
+		}
+	}
+}
+
+#[cfg(test)]
+impl FindOrCreateFunctionDeclaration for Declarations
+{
+	fn find_or_create_function_declaration(&self, name: &str, arity: usize)
+		-> std::rc::Rc<crate::FunctionDeclaration>
+	{
+		let mut function_declarations = self.function_declarations.borrow_mut();
+
+		match function_declarations.iter().find(|x| x.name == name && x.arity == arity)
+		{
+			Some(declaration) => std::rc::Rc::clone(&declaration),
+			None =>
+			{
+				let declaration = crate::FunctionDeclaration
+				{
+					name: name.to_string(),
+					arity,
+				};
+				let declaration = std::rc::Rc::new(declaration);
+
+				function_declarations.insert(std::rc::Rc::clone(&declaration));
+
+				declaration
+			},
+		}
+	}
+}
+
+#[cfg(test)]
+impl FindOrCreatePredicateDeclaration for Declarations
+{
+	fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
+		-> std::rc::Rc<crate::PredicateDeclaration>
+	{
+		let mut predicate_declarations = self.predicate_declarations.borrow_mut();
+
+		match predicate_declarations.iter().find(|x| x.name == name && x.arity == arity)
+		{
+			Some(declaration) => std::rc::Rc::clone(&declaration),
+			None =>
+			{
+				let declaration = crate::PredicateDeclaration
+				{
+					name: name.to_string(),
+					arity,
+				};
+				let declaration = std::rc::Rc::new(declaration);
+
+				predicate_declarations.insert(std::rc::Rc::clone(&declaration));
+
+				declaration
+			},
+		}
+	}
+}