Work in progress

src/ast.rs

@@ -1,76 +1,150 @@
-#[derive(Eq, Hash, PartialEq)]
+// Operators
+
+pub enum BinaryOperator
+{
+	Addition,
+	Subtraction,
+	Multiplication,
+	Division,
+	Modulo,
+	Exponentiation,
+}
+
+pub enum ComparisonOperator
+{
+	Greater,
+	Less,
+	LessOrEqual,
+	GreaterOrEqual,
+	NotEqual,
+	Equal,
+}
+
+pub enum UnaryOperator
+{
+	AbsoluteValue,
+	Negation,
+}
+
+// Primitives
+
+pub struct FunctionDeclaration
+{
+	pub name: String,
+	pub arity: usize,
+}
+
 pub struct PredicateDeclaration
 {
 	pub name: String,
 	pub arity: usize,
 }
 
-#[derive(PartialEq)]
-pub struct Predicate
-{
-	pub declaration: PredicateDeclaration,
-	pub arguments: Vec<Term>,
-}
-
-#[derive(PartialEq)]
-pub struct Exists
-{
-	pub parameters: Vec<VariableDeclaration>,
-	pub argument: Box<Formula>,
-}
-
-#[derive(PartialEq)]
-pub struct ForAll
-{
-	pub parameters: Vec<VariableDeclaration>,
-	pub argument: Box<Formula>,
-}
-
-#[derive(PartialEq)]
-pub enum Formula
-{
-	Exists(Exists),
-	ForAll(ForAll),
-	Not(Box<Formula>),
-	And(Vec<Box<Formula>>),
-	Or(Vec<Box<Formula>>),
-	Implies(Box<Formula>, Box<Formula>),
-	Biconditional(Box<Formula>, Box<Formula>),
-	Less(Term, Term),
-	LessOrEqual(Term, Term),
-	Greater(Term, Term),
-	GreaterOrEqual(Term, Term),
-	Equal(Term, Term),
-	NotEqual(Term, Term),
-	Boolean(bool),
-	Predicate(Predicate),
-}
-
-#[derive(PartialEq)]
-pub enum Domain
-{
-	Program,
-	Integer,
-}
-
-#[derive(PartialEq)]
 pub struct VariableDeclaration
 {
 	pub name: String,
-	pub domain: Domain,
 }
 
-#[derive(PartialEq)]
+// Terms
-pub enum Term
+
+pub struct BinaryOperation
+{
+	pub operator: BinaryOperator,
+	pub left: Box<Term>,
+	pub right: Box<Term>,
+}
+
+pub struct Function
+{
+	pub declaration: std::rc::Rc<FunctionDeclaration>,
+	pub arguments: Vec<Box<Term>>,
+}
+
+pub enum SpecialInteger
 {
 	Infimum,
 	Supremum,
-	Integer(i64),
-	Symbolic(String),
-	String(String),
-	Variable(VariableDeclaration),
-	Add(Box<Term>, Box<Term>),
-	Subtract(Box<Term>, Box<Term>),
-	Multiply(Box<Term>, Box<Term>),
-	Negative(Box<Term>),
 }
+
+pub struct UnaryOperation
+{
+	pub operator: UnaryOperator,
+	pub argument: Box<Term>,
+}
+
+pub struct Variable
+{
+	pub declaration: std::rc::Rc<VariableDeclaration>,
+}
+
+// Formulas
+
+pub struct Biconditional
+{
+	pub left: Box<Formula>,
+	pub right: Box<Formula>,
+}
+
+pub struct Comparison
+{
+	pub operator: ComparisonOperator,
+	pub left: Box<Term>,
+	pub right: Box<Term>,
+}
+
+pub struct Exists
+{
+	pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
+	pub argument: Box<Formula>,
+}
+
+pub struct ForAll
+{
+	pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
+	pub argument: Box<Formula>,
+}
+
+pub struct Implies
+{
+	pub antecedent: Box<Formula>,
+	pub implication: Box<Formula>,
+}
+
+pub struct Predicate
+{
+	pub declaration: std::rc::Rc<PredicateDeclaration>,
+	pub arguments: Vec<Box<Term>>,
+}
+
+// Variants
+
+pub enum Term
+{
+	BinaryOperation(BinaryOperation),
+	Boolean(bool),
+	Function(Function),
+	Integer(i32),
+	SpecialInteger(SpecialInteger),
+	String(String),
+	Symbolic(String),
+	UnaryOperation(UnaryOperation),
+	Variable(Variable),
+}
+
+pub type Terms = Vec<Box<Term>>;
+
+pub enum Formula
+{
+	And(Formulas),
+	Biconditional(Biconditional),
+	Boolean(bool),
+	Comparison(Comparison),
+	Exists(Exists),
+	ForAll(ForAll),
+	Implies(Implies),
+	Not(Box<Formula>),
+	Or(Formulas),
+	Predicate(Predicate),
+}
+
+pub type Formulas = Vec<Box<Formula>>;

src/format.rs

@@ -1,16 +1,16 @@
 struct TermDisplay<'term>
 {
-	parent_precedence: u64,
+	parent_precedence: i32,
 	term: &'term crate::Term,
 }
 
 struct FormulaDisplay<'formula>
 {
-	parent_precedence: u64,
+	parent_precedence: i32,
 	formula: &'formula crate::Formula,
 }
 
-fn display_term<'term>(term: &'term crate::Term, parent_precedence: u64) -> TermDisplay<'term>
+fn display_term<'term>(term: &'term crate::Term, parent_precedence: i32) -> TermDisplay<'term>
 {
 	TermDisplay
 	{
@@ -19,7 +19,7 @@ fn display_term<'term>(term: &'term crate::Term, parent_precedence: u64) -> Term
 	}
 }
 
-fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: u64)
+fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: i32)
 	-> FormulaDisplay<'formula>
 {
 	FormulaDisplay
@@ -29,28 +29,66 @@ fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedenc
 	}
 }
 
-fn term_precedence(term: &crate::Term) -> u64
+trait Precedence
 {
-	match term
+	fn precedence(&self) -> i32;
+}
+
+impl Precedence for crate::Term
+{
+	fn precedence(&self) -> i32
 	{
-		crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0,
+		match &self
-		crate::Term::Negative(_) => 1,
+		{
-		crate::Term::Multiply(_, _) => 2,
+			Self::Boolean(_)
-		crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3,
+			| Self::Function(_)
+			| Self::SpecialInteger(_)
+			| Self::Integer(_)
+			| Self::Symbolic(_)
+			| Self::String(_)
+			| Self::Variable(_)
+				=> 0,
+			Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negation, ..})
+				=> 1,
+			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiation, ..})
+				=> 2,
+			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiplication, ..})
+			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Division, ..})
+			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
+				=> 3,
+			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Addition, ..})
+			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtraction, ..})
+				=> 4,
+			Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
+				=> 5,
+		}
 	}
 }
 
-fn formula_precedence(formula: &crate::Formula) -> u64
+impl Precedence for crate::Formula
 {
-	match formula
+	fn precedence(&self) -> i32
 	{
-		crate::Formula::Predicate(_) | crate::Formula::Boolean(_) | crate::Formula::Less(_, _) | crate::Formula::LessOrEqual(_, _) | crate::Formula::Greater(_, _) | crate::Formula::GreaterOrEqual(_, _) | crate::Formula::Equal(_, _) | crate::Formula::NotEqual(_, _) => 0,
+		match &self
-		crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1,
+		{
-		crate::Formula::Not(_) => 2,
+			Self::Predicate(_)
-		crate::Formula::And(_) => 3,
+			| Self::Boolean(_)
-		crate::Formula::Or(_) => 4,
+			| Self::Comparison(_)
-		crate::Formula::Implies(_, _) => 5,
+				=> 0,
-		crate::Formula::Biconditional(_, _) => 6,
+			Self::Exists(_)
+			| Self::ForAll(_)
+				=> 1,
+			Self::Not(_)
+				=> 2,
+			Self::And(_)
+				=> 3,
+			Self::Or(_)
+				=> 4,
+			Self::Implies(_)
+				=> 5,
+			Self::Biconditional(_)
+				=> 6,
+		}
 	}
 }
 
@@ -58,12 +96,6 @@ impl std::fmt::Debug for crate::VariableDeclaration
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		match &self.domain
-		{
-			crate::Domain::Program => write!(format, "X")?,
-			crate::Domain::Integer => write!(format, "N")?,
-		};
-
 		write!(format, "{}", &self.name)
 	}
 }
@@ -80,7 +112,7 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		let precedence = term_precedence(self.term);
+		let precedence = self.term.precedence();
 		let requires_parentheses = precedence > self.parent_precedence;
 
 		if requires_parentheses
@@ -88,18 +120,58 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 			write!(format, "(")?;
 		}
 
-		match self.term
+		match &self.term
 		{
-			crate::Term::Infimum => write!(format, "#inf"),
+			crate::Term::Boolean(true) => write!(format, "true"),
-			crate::Term::Supremum => write!(format, "#sup"),
+			crate::Term::Boolean(false) => write!(format, "false"),
+			crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) => write!(format, "#inf"),
+			crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) => write!(format, "#sup"),
 			crate::Term::Integer(value) => write!(format, "{}", value),
-			crate::Term::Symbolic(ref value) => write!(format, "{}", value),
+			crate::Term::Symbolic(value) => write!(format, "{}", value),
-			crate::Term::String(ref value) => write!(format, "\"{}\"", value),
+			crate::Term::String(value) => write!(format, "\"{}\"", value),
-			crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
+			crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
-			crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::Function(function) =>
-			crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
+			{
-			crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
+				write!(format, "{}", function.declaration.name)?;
-			crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, precedence)),
+
+				assert!(function.declaration.arity == function.arguments.len(),
+					"function has a different number of arguments than declared (expected {}, got {})",
+					function.declaration.arity, function.arguments.len());
+
+				if function.arguments.len() > 0
+				{
+					write!(format, "{}(", function.declaration.name)?;
+
+					let mut separator = "";
+
+					for argument in &function.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(&argument, 1000))?;
+
+						separator = ", ";
+					}
+
+					write!(format, ")")?;
+				}
+
+				Ok(())
+			},
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Addition, left, right})
+				=> write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtraction, left, right})
+				=> write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiplication, left, right})
+				=> write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Division, left, right})
+				=> write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
+				=> write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiation, left, right})
+				=> write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negation, argument})
+				=> write!(format, "-{:?}", display_term(argument, precedence)),
+			crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
+				=> write!(format, "|{:?}|", display_term(argument, precedence)),
 		}?;
 
 		if requires_parentheses
@@ -123,7 +195,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		let precedence = formula_precedence(self.formula);
+		let precedence = self.formula.precedence();
 		let requires_parentheses = precedence > self.parent_precedence;
 
 		if requires_parentheses
@@ -131,9 +203,9 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			write!(format, "(")?;
 		}
 
-		match self.formula
+		match &self.formula
 		{
-			crate::Formula::Exists(ref exists) =>
+			crate::Formula::Exists(exists) =>
 			{
 				write!(format, "exists")?;
 
@@ -148,7 +220,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 				write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
 			},
-			crate::Formula::ForAll(ref for_all) =>
+			crate::Formula::ForAll(for_all) =>
 			{
 				write!(format, "forall")?;
 
@@ -163,8 +235,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 				write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
 			},
-			crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
+			crate::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
-			crate::Formula::And(ref arguments) =>
+			crate::Formula::And(arguments) =>
 			{
 				let mut separator = "";
 
@@ -175,7 +247,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					separator = " and "
 				}
 			},
-			crate::Formula::Or(ref arguments) =>
+			crate::Formula::Or(arguments) =>
 			{
 				let mut separator = "";
 
@@ -186,21 +258,25 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					separator = " or "
 				}
 			},
-			crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
+			crate::Formula::Implies(crate::Implies{antecedent, implication})
-			crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
+				=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?,
-			crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, 1000), display_term(right, 1000))?,
+			crate::Formula::Biconditional(crate::Biconditional{left, right})
-			crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?,
+				=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
-			crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, 1000), display_term(right, 1000))?,
+			crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::Less, left, right})
-			crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, 1000), display_term(right, 1000))?,
+				=> write!(format, "{:?} < {:?}", display_term(left, 1000), display_term(right, 1000))?,
-			crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?,
+			crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::LessOrEqual, left, right})
-			crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, 1000), display_term(right, 1000))?,
+				=> write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?,
-			crate::Formula::Boolean(value) =>
+			crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::Greater, left, right})
-				match value
+				=> write!(format, "{:?} > {:?}", display_term(left, 1000), display_term(right, 1000))?,
-				{
+			crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
-					true => write!(format, "#true")?,
+				=> write!(format, "{:?} >= {:?}", display_term(left, 1000), display_term(right, 1000))?,
-					false => write!(format, "#false")?,
+			crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::Equal, left, right})
-				},
+				=> write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?,
-			crate::Formula::Predicate(ref predicate) =>
+			crate::Formula::Comparison(crate::Comparison{operator: crate::ComparisonOperator::NotEqual, left, right})
+				=> write!(format, "{:?} != {:?}", display_term(left, 1000), display_term(right, 1000))?,
+			crate::Formula::Boolean(true) => write!(format, "#true")?,
+			crate::Formula::Boolean(false) => write!(format, "#false")?,
+			crate::Formula::Predicate(predicate) =>
 			{
 				write!(format, "{}", predicate.declaration.name)?;
 

src/lib.rs

@@ -1,6 +1,6 @@
 mod ast;
 pub mod format;
-mod parse;
+//mod parse;
 
-pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term};
+pub use ast::*;
-pub use parse::{formula, formulas, term};
+//pub use parse::{formula, formulas, term};

src/parse.rs

@@ -10,6 +10,60 @@ use nom::
 	bytes::complete::tag,
 };
 
+type VariableDeclarations = std::collections::HashSet<std::rc::Rc<crate::VariableDeclaration>>;
+
+struct VariableDeclarationStack
+{
+	free_variable_declarations: VariableDeclarations,
+	bound_variable_declarations: Vec<std::rc::Rc<VariableDeclarations>>,
+}
+
+impl VariableDeclarationStack
+{
+	fn find(&self, variable_name: &str) -> Option<std::rc::Rc<crate::VariableDeclaration>>
+	{
+		for variable_declarations in self.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(crate) fn find_or_create(&mut self, variable_name: &str) -> std::rc::Rc<crate::VariableDeclaration>
+	{
+		if let Some(variable_declaration) = self.find(variable_name)
+		{
+			return variable_declaration;
+		}
+
+		let variable_declaration = crate::VariableDeclaration
+		{
+			name: variable_name.to_owned(),
+		};
+		let variable_declaration = std::rc::Rc::new(variable_declaration);
+
+		self.free_variable_declarations.insert(std::rc::Rc::clone(&variable_declaration));
+
+		variable_declaration
+	}
+}
+
+struct Declarations
+{
+	//function_declarations:,
+	//predicate_declarations:,
+	variable_declaration_stack: VariableDeclarationStack,
+}
+
 enum TermOperator
 {
 	Add,
@@ -17,25 +71,25 @@ enum TermOperator
 	Multiply,
 }
 
-fn infimum(i: &str) -> IResult<&str, crate::Term>
+fn infimum<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	map
 	(
 		delimited(multispace0, tag("#inf"), multispace0),
-		|_| crate::Term::Infimum
+		|_| crate::Term::SpecialInteger(crate::SpecialInteger::Infimum)
 	)(i)
 }
 
-fn supremum(i: &str) -> IResult<&str, crate::Term>
+fn supremum<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	map
 	(
 		delimited(multispace0, tag("#sup"), multispace0),
-		|_| crate::Term::Supremum
+		|_| crate::Term::SpecialInteger(crate::SpecialInteger::Supremum)
 	)(i)
 }
 
-fn integer(i: &str) -> IResult<&str, crate::Term>
+fn integer<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	map
 	(
@@ -53,7 +107,7 @@ fn is_lowercase_alphanumeric(c: char) -> bool
 	c.is_alphanumeric() && c.is_lowercase()
 }
 
-fn symbolic_identifier(i: &str) -> IResult<&str, String>
+fn symbolic_identifier<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, String>
 {
 	let (i, symbolic_identifier) = map
 	(
@@ -68,16 +122,16 @@ fn symbolic_identifier(i: &str) -> IResult<&str, String>
 	Ok((i, symbolic_identifier))
 }
 
-fn symbolic(i: &str) -> IResult<&str, crate::Term>
+fn symbolic<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	map
 	(
-		delimited(multispace0, symbolic_identifier, multispace0),
+		delimited(multispace0, |i| symbolic_identifier(i, declarations), multispace0),
 		crate::Term::Symbolic
 	)(i)
 }
 
-fn string(i: &str) -> IResult<&str, crate::Term>
+fn string<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	map
 	(
@@ -96,7 +150,7 @@ fn string(i: &str) -> IResult<&str, crate::Term>
 	)(i)
 }
 
-fn program_variable_identifier(i: &str) -> IResult<&str, String>
+fn variable_identifier<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, String>
 {
 	map
 	(
@@ -105,7 +159,7 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String>
 			multispace0,
 			preceded
 			(
-				tag("X"),
+				take_while_m_n(1, 1, |c| char::is_alphabetic(c) && char::is_uppercase(c)),
 				take_while(char::is_alphanumeric)
 			),
 			multispace0
@@ -114,79 +168,48 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String>
 	)(i)
 }
 
-fn integer_variable_identifier(i: &str) -> IResult<&str, String>
+fn variable_declaration<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::VariableDeclaration>
 {
 	map
 	(
-		delimited
+		|i| variable_identifier(i, declarations),
-		(
+		|s| crate::VariableDeclaration{name: s},
-			multispace0,
-			preceded
-			(
-				tag("N"),
-				take_while(char::is_alphanumeric)
-			),
-			multispace0
-		),
-		|s: &str| s.to_string()
 	)(i)
 }
 
-fn program_variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
+fn program_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	map
 	(
-		program_variable_identifier,
+		|i| program_variable_identifier(i, declarations),
-		|s| crate::VariableDeclaration{name: s, domain: crate::Domain::Program}
+		|s|
+		{
+			let declaration = declarations.variable_declaration_stack.get(s.as_ref());
+
+			crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program})
+		},
 	)(i)
 }
 
-fn integer_variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
+fn integer_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	map
 	(
-		integer_variable_identifier,
+		|i| integer_variable_identifier,
-		|s| crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}
+		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}),
 	)(i)
 }
 
-fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
+fn variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	alt
 	((
-		program_variable_declaration,
+		|i| program_variable(i, declarations),
-		integer_variable_declaration
+		|i| integer_variable(i, declarations),
 	))(i)
 }
 
-fn program_variable(i: &str) -> IResult<&str, crate::Term>
+fn predicate_0_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	map
-	(
-		program_variable_identifier,
-		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program})
-	)(i)
-}
-
-fn integer_variable(i: &str) -> IResult<&str, crate::Term>
-{
-	map
-	(
-		integer_variable_identifier,
-		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer})
-	)(i)
-}
-
-fn variable(i: &str) -> IResult<&str, crate::Term>
-{
-	alt
-	((
-		program_variable,
-		integer_variable
-	))(i)
-}
-
-fn predicate_0_ary(i: &str) -> IResult<&str, crate::Formula>
 {
 	map
 	(
@@ -205,7 +228,7 @@ fn predicate_0_ary(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn predicate_n_ary(i: &str) -> IResult<&str, crate::Formula>
+fn predicate_n_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -238,7 +261,7 @@ fn predicate_n_ary(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn predicate(i: &str) -> IResult<&str, crate::Formula>
+fn predicate<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	alt
 	((
@@ -247,7 +270,7 @@ fn predicate(i: &str) -> IResult<&str, crate::Formula>
 	))(i)
 }
 
-fn boolean(i: &str) -> IResult<&str, crate::Formula>
+fn boolean<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -265,7 +288,7 @@ fn boolean(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn less(i: &str) -> IResult<&str, crate::Formula>
+fn less<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -278,7 +301,7 @@ fn less(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn less_or_equal(i: &str) -> IResult<&str, crate::Formula>
+fn less_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -291,7 +314,7 @@ fn less_or_equal(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn greater(i: &str) -> IResult<&str, crate::Formula>
+fn greater<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -304,7 +327,7 @@ fn greater(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn greater_or_equal(i: &str) -> IResult<&str, crate::Formula>
+fn greater_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -317,7 +340,7 @@ fn greater_or_equal(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn equal(i: &str) -> IResult<&str, crate::Formula>
+fn equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -330,7 +353,7 @@ fn equal(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn not_equal(i: &str) -> IResult<&str, crate::Formula>
+fn not_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -343,7 +366,7 @@ fn not_equal(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn comparison(i: &str) -> IResult<&str, crate::Formula>
+fn comparison<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	alt
 	((
@@ -356,7 +379,7 @@ fn comparison(i: &str) -> IResult<&str, crate::Formula>
 	))(i)
 }
 
-fn term_parenthesized(i: &str) -> IResult<&str, crate::Term>
+fn term_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	delimited
 	(
@@ -387,7 +410,7 @@ fn fold_terms(initial: crate::Term, remainder: Vec<(TermOperator, crate::Term)>)
 		})
 }
 
-fn term_precedence_0(i: &str) -> IResult<&str, crate::Term>
+fn term_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	alt
 	((
@@ -401,7 +424,7 @@ fn term_precedence_0(i: &str) -> IResult<&str, crate::Term>
 	))(i)
 }
 
-fn term_precedence_1(i: &str) -> IResult<&str, crate::Term>
+fn term_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	alt
 	((
@@ -419,7 +442,7 @@ fn term_precedence_1(i: &str) -> IResult<&str, crate::Term>
 	))(i)
 }
 
-fn term_precedence_2(i: &str) -> IResult<&str, crate::Term>
+fn term_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	let (i, initial) = term_precedence_1(i)?;
 	let (i, remainder) =
@@ -435,7 +458,7 @@ fn term_precedence_2(i: &str) -> IResult<&str, crate::Term>
 	Ok((i, fold_terms(initial, remainder)))
 }
 
-fn term_precedence_3(i: &str) -> IResult<&str, crate::Term>
+fn term_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	let (i, initial) = term_precedence_2(i)?;
 	let (i, remainder) =
@@ -459,12 +482,12 @@ fn term_precedence_3(i: &str) -> IResult<&str, crate::Term>
 	Ok((i, fold_terms(initial, remainder)))
 }
 
-pub fn term(i: &str) -> IResult<&str, crate::Term>
+pub fn term<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
 {
 	term_precedence_3(i)
 }
 
-fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula>
+fn formula_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	delimited
 	(
@@ -479,7 +502,7 @@ fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn formula_precedence_0(i: &str) -> IResult<&str, crate::Formula>
+fn formula_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	alt
 	((
@@ -490,7 +513,7 @@ fn formula_precedence_0(i: &str) -> IResult<&str, crate::Formula>
 	))(i)
 }
 
-fn exists(i: &str) -> IResult<&str, crate::Formula>
+fn exists<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -521,7 +544,7 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn for_all(i: &str) -> IResult<&str, crate::Formula>
+fn for_all<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -552,7 +575,7 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula>
 	)(i)
 }
 
-fn formula_precedence_1(i: &str) -> IResult<&str, crate::Formula>
+fn formula_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	alt
 	((
@@ -562,7 +585,7 @@ fn formula_precedence_1(i: &str) -> IResult<&str, crate::Formula>
 	))(i)
 }
 
-fn formula_precedence_2(i: &str) -> IResult<&str, crate::Formula>
+fn formula_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	alt
 	((
@@ -580,7 +603,7 @@ fn formula_precedence_2(i: &str) -> IResult<&str, crate::Formula>
 	))(i)
 }
 
-fn formula_precedence_3(i: &str) -> IResult<&str, crate::Formula>
+fn formula_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	alt
 	((
@@ -599,7 +622,7 @@ fn formula_precedence_3(i: &str) -> IResult<&str, crate::Formula>
 	))(i)
 }
 
-fn formula_precedence_4(i: &str) -> IResult<&str, crate::Formula>
+fn formula_precedence_4<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	alt
 	((
@@ -618,7 +641,7 @@ fn formula_precedence_4(i: &str) -> IResult<&str, crate::Formula>
 	))(i)
 }
 
-fn formula_precedence_5(i: &str) -> IResult<&str, crate::Formula>
+fn formula_precedence_5<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	let (i, left) = formula_precedence_4(i)?;
 
@@ -629,7 +652,7 @@ fn formula_precedence_5(i: &str) -> IResult<&str, crate::Formula>
 	}
 }
 
-fn formula_precedence_6(i: &str) -> IResult<&str, crate::Formula>
+fn formula_precedence_6<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	let (i, left) = formula_precedence_5(i)?;
 
@@ -640,12 +663,12 @@ fn formula_precedence_6(i: &str) -> IResult<&str, crate::Formula>
 	}
 }
 
-pub fn formula(i: &str) -> IResult<&str, crate::Formula>
+pub fn formula<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	formula_precedence_6(i)
 }
 
-pub fn formulas(i: &str) -> IResult<&str, Vec<crate::Formula>>
+pub fn formulas<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, Vec<crate::Formula>>
 {
 	many0(formula)(i)
 }