Add graph coloring example

With this patch, properties specific to variable, function, and
predicate declarations are directly stored within those objects rather
than external maps that need to be queried via traits. This greatly
simplifies many parts of the logic.

This is made possible by implementing a custom foliage flavor, which
makes it possible to swap the built-in declaration types for extended
versions of those types that fulfill certain requirements.

Cargo.toml

@@ -1,15 +1,18 @@
 [package]
 name = "anthem"
-version = "0.4.0-beta.1"
+version = "0.4.0-beta.3"
 authors = ["Patrick Lühne <patrick@luehne.de>"]
 edition = "2018"
 
 [dependencies]
+atty = "0.2"
 foliage = {git = "https://github.com/pluehne/foliage", branch = "parser-new"}
+itertools = "0.9"
 log = "0.4"
 pretty_env_logger = "0.4"
 regex = "1"
 structopt = "0.3"
+termcolor = "1.1"
 
 [dependencies.clingo]
 git = "https://github.com/potassco/clingo-rs"

examples/coloring-1.lp

@@ -0,0 +1,12 @@
+% After eliminating the super-easy aggregate expression from the rule
+%
+% {color(X,Z) : color(Z)} = 1 :- vertex(X).
+%
+% we get 4 rules:
+
+{color(X,Z)} :- vertex(X), color(Z).
+:- color(X,Z1), color(X,Z2), vertex(X), color(Z1), color(Z2), Z1 != Z2.
+aux(X) :- vertex(X), color(Z), color(X,Z).
+:- vertex(X), not aux(X).
+
+:- edge(X,Y), color(X,Z), color(Y,Z).

examples/coloring.spec

@@ -0,0 +1,14 @@
+input: vertex/1, edge/2, color/1.
+
+output: color/2.
+
+# edge/2 is a set of pairs of vertices
+assume: forall X, Y (edge(X,Y) -> vertex(X) and vertex(Y)).
+
+# color/2 is a function from vertices to colors
+spec: forall X, Z (color(X,Z) -> vertex(X) and color(Z)).
+spec: forall X (vertex(X) -> exists Z color(X,Z)).
+spec: forall X, Z1, Z2 (color(X,Z1) and color(X,Z2) -> Z1 = Z2).
+
+# adjacent vertices have different colors
+spec: not exists X, Y, Z (edge(X,Y) and color(X,Z) and color(Y,Z)).

examples/exact-cover.lp

@@ -1,5 +0,0 @@
-{in(1..n)}.
-
-:- I != J, in(I), in(J), s(X, I), s(X, J).
-covered(X) :- in(I), s(X, I).
-:- s(X, Y), not covered(X).

examples/exact-cover.spec

@@ -1,10 +0,0 @@
-axiom: forall X (is_int(X) <-> exists N X = N).
-
-input: n -> integer, s/2, is_int/1.
-
-assume: n >= 0.
-assume: forall X, Y (s(X, Y) -> is_int(Y)).
-
-assert: forall X (in(X) -> X >= 1 and X <= n).
-assert: forall X (exists I s(X, I) -> exists I (in(I) and s(X, I))).
-assert: forall I, J (exists X (s(X, I) and s(X, J)) and in(I) and in(J) -> I = J).

examples/example-0.spec

@@ -0,0 +1,3 @@
+input: p/2.
+
+spec: exists X, Y p(X, Y) <-> exists X q(X).

examples/example-1.spec

@@ -0,0 +1,8 @@
+input: p/1.
+
+spec:
+	forall N
+	(
+		forall X (p(X) -> exists I exists M (I = M and I = X and I <= N))
+		-> forall X (q(X) -> exists I exists M (I = M and I = X and I <= 2 * N))
+	).

examples/example-2-deadlock.spec

@@ -1,20 +0,0 @@
-axiom: forall X (isint(X) <-> exists N X = N).
-axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
-
-axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)).
-
-input: n -> integer.
-
-assumption: n >= 0.
-
-assertion: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
-
-
-
-lemma(forward): forall N N * N >= N.
-lemma(forward): forall X (q(X) -> exists N X = N).
-lemma(forward): forall X (p(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n)).
-lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and not p(N2 + 1))).
-lemma(forward): forall N2 (N2 >= 0 and not p(N2 + 1) -> (N2 + 1) * (N2 + 1) > n).
-lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)).
-lemma(forward): exists N2 (forall X (X = N2 -> (q(X) <-> N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n))).

examples/example-2.lemmas

@@ -0,0 +1,18 @@
+# Induction principle instantiated for p.
+# This axiom is necessary because we use Vampire without higher-order reasoning
+axiom: p(0) and forall N (N >= 0 and p(N) -> p(N + 1)) -> forall N (N >= 0 -> p(N)).
+
+lemma(forward): forall X (p(X) <-> exists N (X = N and N >= 0 and N * N <= n)).
+lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)).
+lemma(forward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 < N2 -> N1 * N1 < N2 * N2).
+lemma(forward): forall N (N >= 0 and p(N + 1) -> p(N)).
+lemma(forward): not p(n + 1).
+lemma(forward): forall N1, N2 (q(N1) and N2 > N1 -> not q(N2)).
+lemma(forward): forall N (N >= 0 and not p(N + 1) -> (N + 1) * (N + 1) > n).
+
+lemma(backward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 * N1 <= N2 * N2 -> N1 <= N2).
+lemma(backward): forall N (p(N) <-> 0 <= N and N <= n and N * N <= n).
+lemma(backward): forall N (not p(N) and N >= 0 -> N * N > n).
+lemma(backward): forall N (N >= 0 -> N * N < (N + 1) * (N + 1)).
+lemma(backward): forall N1, N2 (p(N1) and not p(N2) and N2 >= 0 -> N1 < N2).
+lemma(backward): forall N1, N2 (p(N1) and not p(N1 + 1) and p(N2) and not p(N2 + 1) -> N1 = N2).

examples/example-2.spec

@@ -1,30 +1,9 @@
+# Perform the proofs under the assumption that n is a nonnegative integer input constant
 input: n -> integer.
-
-axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
-axiom: (p(0) and forall N (N >= 0 and p(N) -> p(N + 1))) -> (forall N p(N)).
-
 assume: n >= 0.
 
-assert: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).
+# p/1 is an auxiliary predicate
+output: q/1.
 
-
-
-lemma(forward): forall N N * N >= N.
-lemma(forward): forall X (q(X) -> exists N X = N).
-lemma(forward): forall X (p(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n)).
-lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and not p(N2 + 1))).
-lemma(forward): forall N2 (N2 >= 0 and not p(N2 + 1) -> (N2 + 1) * (N2 + 1) > n).
-lemma(forward): forall X (q(X) <-> exists N2 (X = N2 and N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n)).
-
-
-lemma(forward): exists N2 (forall X (X = N2 -> (q(X) <-> N2 >= 0 and N2 * N2 <= n and (N2 + 1) * (N2 + 1) > n))).
-lemma(forward): exists N2 p(N2).
-lemma(forward): forall N1, N2 (N1 >= 0 and N2 >= 0 and N1 < N2 -> N1 * N1 < N2 * N2).
-lemma(forward): forall N (N >= 0 and p(N + 1) -> p(N)).
-
-lemma(forward): not p(n + 1).
-lemma(forward): forall N1, N2 (N2 > N1 and N1 >= 0 and p(N2) -> p(N1)).
-
-lemma(forward): forall N (N >= 0 -> p(N)).
-
-lemma(forward): forall N2, N3 (q(N2) and N3 > N2 -> not q(N3)).
+# Verify that q computes the floor of the square root of n
+spec: exists N (forall X (q(X) <-> X = N) and N >= 0 and N * N <= n and (N + 1) * (N + 1) > n).

examples/example-exact-cover.lp

@@ -0,0 +1,5 @@
+{in_cover(1..n)}.
+
+:- I != J, in_cover(I), in_cover(J), s(X, I), s(X, J).
+covered(X) :- in_cover(I), s(X, I).
+:- s(X, I), not covered(X).

examples/example-exact-cover.spec

@@ -0,0 +1,22 @@
+# Perform the proofs under the assumption that n is a nonnegative integer input constant. n stands
+# for the total number of input sets
+input: n -> integer.
+assume: n >= 0.
+
+# s/2 is the input predicate defining the sets for which the program searches for exact covers
+input: s/2.
+
+# Only the in/1 predicate is an actual output, s/2 is an input and covered/1 and is_int/1 are
+# auxiliary
+output: in_cover/1.
+
+# Perform the proofs under the assumption that the second parameter of s/2 (the number of the set)
+# is always an integer
+assume: forall Y (exists X s(X, Y) -> exists I (Y = I and I >= 1 and I <= n)).
+
+# Only valid sets can be included in the solution
+spec: forall Y (in_cover(Y) -> exists I (Y = I and I >= 1 and I <= n)).
+# If an element is contained in an input set, it must be covered by all solutions
+spec: forall X (exists Y s(X, Y) -> exists Y (s(X, Y) and in_cover(Y))).
+# Elements may not be covered by two input sets
+spec: forall Y, Z (exists X (s(X, Y) and s(X, Z)) and in_cover(Y) and in_cover(Z) -> Y = Z).

examples/example-prime.lemmas

@@ -0,0 +1 @@
+lemma(backward): forall N (composite(N) <-> N > 1 and N <= n and exists I, J (I > 1 and J > 1 and I * J = N)).

examples/example-prime.lp

@@ -0,0 +1,3 @@
+% Prime numbers from 1 to n.
+composite(N) :- N = 1..n, I = 2..(N - 1), N \ I = 0.
+prime(N) :- N = 2..n, not composite(N).

examples/example-prime.spec

@@ -0,0 +1,7 @@
+input: n -> integer.
+output: prime/1.
+
+assume: n >= 1.
+
+spec: forall X (prime(X) -> exists N (X = N)).
+spec: forall N (prime(N) <-> N > 1 and N <= n and not exists I, J (I > 1 and J > 1 and I * J = N)).

src/ast.rs

@@ -0,0 +1,563 @@
+pub struct FoliageFlavor;
+
+pub struct FunctionDeclaration
+{
+	pub declaration: foliage::FunctionDeclaration,
+	pub domain: std::cell::RefCell<crate::Domain>,
+	pub is_input: std::cell::RefCell<bool>,
+}
+
+impl FunctionDeclaration
+{
+	pub fn is_built_in(&self) -> bool
+	{
+		self.declaration.name.starts_with("f__") && self.declaration.name.ends_with("__")
+	}
+}
+
+impl std::cmp::PartialEq for FunctionDeclaration
+{
+	#[inline(always)]
+	fn eq(&self, other: &Self) -> bool
+	{
+		self.declaration.eq(&other.declaration)
+	}
+}
+
+impl std::cmp::Eq for FunctionDeclaration
+{
+}
+
+impl std::cmp::PartialOrd for FunctionDeclaration
+{
+	#[inline(always)]
+	fn partial_cmp(&self, other: &FunctionDeclaration) -> Option<std::cmp::Ordering>
+	{
+		self.declaration.partial_cmp(&other.declaration)
+	}
+}
+
+impl std::cmp::Ord for FunctionDeclaration
+{
+	#[inline(always)]
+	fn cmp(&self, other: &FunctionDeclaration) -> std::cmp::Ordering
+	{
+		self.declaration.cmp(&other.declaration)
+	}
+}
+
+impl std::hash::Hash for FunctionDeclaration
+{
+	#[inline(always)]
+	fn hash<H: std::hash::Hasher>(&self, state: &mut H)
+	{
+		self.declaration.hash(state)
+	}
+}
+
+impl foliage::flavor::FunctionDeclaration for FunctionDeclaration
+{
+	fn new(name: String, arity: usize) -> Self
+	{
+		Self
+		{
+			declaration: foliage::FunctionDeclaration::new(name, arity),
+			domain: std::cell::RefCell::new(crate::Domain::Program),
+			is_input: std::cell::RefCell::new(false),
+		}
+	}
+
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		self.declaration.display_name(formatter)
+	}
+
+	fn arity(&self) -> usize
+	{
+		self.declaration.arity
+	}
+
+	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
+	{
+		self.declaration.matches_signature(other_name, other_arity)
+	}
+}
+
+#[derive(Copy, Clone, Eq, PartialEq)]
+pub enum PredicateDependencySign
+{
+	OnlyPositive,
+	OnlyNegative,
+	PositiveAndNegative,
+}
+
+impl PredicateDependencySign
+{
+	pub fn and_positive(self) -> Self
+	{
+		match self
+		{
+			Self::OnlyPositive => Self::OnlyPositive,
+			Self::OnlyNegative
+			| Self::PositiveAndNegative => Self::PositiveAndNegative,
+		}
+	}
+
+	pub fn and_negative(self) -> Self
+	{
+		match self
+		{
+			Self::OnlyNegative => Self::OnlyNegative,
+			Self::OnlyPositive
+			| Self::PositiveAndNegative => Self::PositiveAndNegative,
+		}
+	}
+
+	pub fn is_positive(&self) -> bool
+	{
+		match self
+		{
+			Self::OnlyPositive
+			| Self::PositiveAndNegative => true,
+			Self::OnlyNegative => false,
+		}
+	}
+
+	pub fn is_negative(&self) -> bool
+	{
+		match self
+		{
+			Self::OnlyPositive => false,
+			Self::OnlyNegative
+			| Self::PositiveAndNegative => true,
+		}
+	}
+}
+
+pub type PredicateDependencies =
+	std::collections::BTreeMap<std::rc::Rc<PredicateDeclaration>, PredicateDependencySign>;
+
+#[derive(Clone, Copy, Eq, PartialEq)]
+pub enum PredicateDeclarationSource
+{
+	Program,
+	Specification,
+	ProgramAndSpecification,
+}
+
+impl PredicateDeclarationSource
+{
+	pub fn and(self, other: Self) -> Self
+	{
+		match (self, other)
+		{
+			(Self::ProgramAndSpecification, _)
+			| (_, Self::ProgramAndSpecification) => Self::ProgramAndSpecification,
+			(Self::Program, Self::Program) => Self::Program,
+			(Self::Specification, Self::Specification) => Self::Specification,
+			(Self::Program, Self::Specification)
+			| (Self::Specification, Self::Program) => Self::ProgramAndSpecification,
+		}
+	}
+
+	pub fn and_specification(self) -> Self
+	{
+		match self
+		{
+			Self::Program
+			| Self::ProgramAndSpecification => Self::ProgramAndSpecification,
+			Self::Specification => Self::Specification,
+		}
+	}
+
+	pub fn is_program(&self) -> bool
+	{
+		match self
+		{
+			Self::Program
+			| Self::ProgramAndSpecification => true,
+			Self::Specification => false,
+		}
+	}
+
+	pub fn is_specification(&self) -> bool
+	{
+		match self
+		{
+			Self::Program => false,
+			Self::Specification
+			| Self::ProgramAndSpecification => true,
+		}
+	}
+}
+
+pub struct PredicateDeclaration
+{
+	pub declaration: foliage::PredicateDeclaration,
+	pub source: std::cell::RefCell<PredicateDeclarationSource>,
+	pub dependencies: std::cell::RefCell<Option<PredicateDependencies>>,
+	pub is_input: std::cell::RefCell<bool>,
+	pub is_output: std::cell::RefCell<bool>,
+}
+
+impl PredicateDeclaration
+{
+	pub fn tptp_statement_name(&self) -> String
+	{
+		format!("{}_{}", self.declaration.name, self.declaration.arity)
+	}
+
+	pub fn is_built_in(&self) -> bool
+	{
+		self.declaration.name.starts_with("p__") && self.declaration.name.ends_with("__")
+	}
+
+	pub fn is_public(&self) -> bool
+	{
+		*self.is_input.borrow() || *self.is_output.borrow()
+	}
+
+	fn collect_positive_dependencies(&self,
+		mut positive_dependencies: &mut std::collections::BTreeSet<
+			std::rc::Rc<crate::PredicateDeclaration>>)
+	{
+		let dependencies = self.dependencies.borrow();
+		let dependencies = match *dependencies
+		{
+			Some(ref dependencies) => dependencies,
+			// Input predicates don’t have completed definitions and no dependencies, so ignore them
+			None => return,
+		};
+
+		for (dependency, sign) in dependencies.iter()
+		{
+			if positive_dependencies.contains(&*dependency)
+				|| dependency.is_built_in()
+				|| !sign.is_positive()
+			{
+				continue;
+			}
+
+			positive_dependencies.insert(std::rc::Rc::clone(dependency));
+
+			dependency.collect_positive_dependencies(&mut positive_dependencies);
+		}
+	}
+
+	fn collect_private_dependencies(&self,
+		mut private_dependencies: &mut std::collections::BTreeSet<
+			std::rc::Rc<crate::PredicateDeclaration>>)
+	{
+		let dependencies = self.dependencies.borrow();
+		let dependencies = match *dependencies
+		{
+			Some(ref dependencies) => dependencies,
+			// Input predicates don’t have completed definitions and no dependencies, so ignore them
+			None => return,
+		};
+
+		for dependency in dependencies.keys()
+		{
+			if private_dependencies.contains(&*dependency)
+				|| dependency.is_public()
+				|| dependency.is_built_in()
+			{
+				continue;
+			}
+
+			private_dependencies.insert(std::rc::Rc::clone(dependency));
+
+			dependency.collect_private_dependencies(&mut private_dependencies);
+		}
+	}
+
+	pub fn has_positive_dependency_cycle(&self) -> bool
+	{
+		if self.is_built_in()
+		{
+			return false;
+		}
+
+		let mut positive_dependencies = std::collections::BTreeSet::new();
+		self.collect_positive_dependencies(&mut positive_dependencies);
+
+		positive_dependencies.contains(self)
+	}
+
+	pub fn has_private_dependency_cycle(&self) -> bool
+	{
+		if self.is_public() || self.is_built_in()
+		{
+			return false;
+		}
+
+		let mut private_dependencies = std::collections::BTreeSet::new();
+		self.collect_private_dependencies(&mut private_dependencies);
+
+		private_dependencies.contains(self)
+	}
+}
+
+impl std::cmp::PartialEq for PredicateDeclaration
+{
+	#[inline(always)]
+	fn eq(&self, other: &Self) -> bool
+	{
+		self.declaration.eq(&other.declaration)
+	}
+}
+
+impl std::cmp::Eq for PredicateDeclaration
+{
+}
+
+impl std::cmp::PartialOrd for PredicateDeclaration
+{
+	#[inline(always)]
+	fn partial_cmp(&self, other: &PredicateDeclaration) -> Option<std::cmp::Ordering>
+	{
+		self.declaration.partial_cmp(&other.declaration)
+	}
+}
+
+impl std::cmp::Ord for PredicateDeclaration
+{
+	#[inline(always)]
+	fn cmp(&self, other: &PredicateDeclaration) -> std::cmp::Ordering
+	{
+		self.declaration.cmp(&other.declaration)
+	}
+}
+
+impl std::hash::Hash for PredicateDeclaration
+{
+	#[inline(always)]
+	fn hash<H: std::hash::Hasher>(&self, state: &mut H)
+	{
+		self.declaration.hash(state)
+	}
+}
+
+impl foliage::flavor::PredicateDeclaration for PredicateDeclaration
+{
+	fn new(name: String, arity: usize) -> Self
+	{
+		Self
+		{
+			declaration: foliage::PredicateDeclaration::new(name, arity),
+			source: std::cell::RefCell::new(PredicateDeclarationSource::Specification),
+			dependencies: std::cell::RefCell::new(None),
+			is_input: std::cell::RefCell::new(false),
+			is_output: std::cell::RefCell::new(false),
+		}
+	}
+
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		self.declaration.display_name(formatter)
+	}
+
+	fn arity(&self) -> usize
+	{
+		self.declaration.arity
+	}
+
+	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
+	{
+		self.declaration.matches_signature(other_name, other_arity)
+	}
+}
+
+#[derive(Clone)]
+pub struct GeneratedVariableName
+{
+	pub domain: crate::Domain,
+	pub id: Option<usize>,
+}
+
+#[derive(Clone)]
+pub enum VariableName
+{
+	UserDefined(String),
+	Generated(GeneratedVariableName),
+}
+
+#[derive(Clone)]
+pub struct VariableDeclaration
+{
+	pub name: std::cell::RefCell<VariableName>,
+}
+
+impl VariableDeclaration
+{
+	pub fn new_generated(domain: crate::Domain) -> Self
+	{
+		let generated_variable_name = GeneratedVariableName
+		{
+			domain,
+			id: None,
+		};
+
+		Self
+		{
+			name: std::cell::RefCell::new(VariableName::Generated(generated_variable_name)),
+		}
+	}
+
+	pub fn domain(&self) -> Result<crate::Domain, crate::Error>
+	{
+		match *self.name.borrow()
+		{
+			VariableName::UserDefined(ref name) =>
+			{
+				let mut name_characters = name.chars();
+
+				loop
+				{
+					match name_characters.next()
+					{
+						Some('I')
+						| Some('J')
+						| Some('K')
+						| Some('L')
+						| Some('M')
+						| Some('N') => return Ok(crate::Domain::Integer),
+						Some('U')
+						| Some('V')
+						| Some('W')
+						| Some('X')
+						| Some('Y')
+						| Some('Z') => return Ok(crate::Domain::Program),
+						Some('_') => continue,
+						_ => return Err(
+							crate::Error::new_variable_name_not_allowed(name.to_string())),
+					}
+				}
+			},
+			VariableName::Generated(ref generated_variable_name) =>
+				Ok(generated_variable_name.domain),
+		}
+	}
+}
+
+impl std::cmp::PartialEq for VariableDeclaration
+{
+	#[inline(always)]
+	fn eq(&self, other: &Self) -> bool
+	{
+		let l = self as *const Self;
+		let r = other as *const Self;
+
+		l.eq(&r)
+	}
+}
+
+impl std::cmp::Eq for VariableDeclaration
+{
+}
+
+impl std::cmp::PartialOrd for VariableDeclaration
+{
+	#[inline(always)]
+	fn partial_cmp(&self, other: &VariableDeclaration) -> Option<std::cmp::Ordering>
+	{
+		let l = self as *const VariableDeclaration;
+		let r = other as *const VariableDeclaration;
+
+		l.partial_cmp(&r)
+	}
+}
+
+impl std::cmp::Ord for VariableDeclaration
+{
+	#[inline(always)]
+	fn cmp(&self, other: &VariableDeclaration) -> std::cmp::Ordering
+	{
+		let l = self as *const VariableDeclaration;
+		let r = other as *const VariableDeclaration;
+
+		l.cmp(&r)
+	}
+}
+
+impl std::hash::Hash for VariableDeclaration
+{
+	#[inline(always)]
+	fn hash<H: std::hash::Hasher>(&self, state: &mut H)
+	{
+		let p = self as *const VariableDeclaration;
+
+		p.hash(state);
+	}
+}
+
+impl foliage::flavor::VariableDeclaration for VariableDeclaration
+{
+	fn new(name: String) -> Self
+	{
+		Self
+		{
+			name: std::cell::RefCell::new(VariableName::UserDefined(name)),
+		}
+	}
+
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match *self.name.borrow()
+		{
+			VariableName::UserDefined(ref name) => write!(formatter, "{}", name),
+			VariableName::Generated(ref generated_variable_name) =>
+			{
+				let variable_name_prefix = match generated_variable_name.domain
+				{
+					crate::Domain::Program => "X",
+					crate::Domain::Integer => "N",
+				};
+
+				let variable_id = match generated_variable_name.id
+				{
+					Some(id) => id,
+					None => unreachable!("all variable IDs should be assigned at this point"),
+				};
+
+				match variable_id
+				{
+					0 => write!(formatter, "{}", variable_name_prefix),
+					_ => write!(formatter, "{}{}", variable_name_prefix, variable_id),
+				}
+			},
+		}
+	}
+
+	fn matches_name(&self, other_name: &str) -> bool
+	{
+		match *self.name.borrow()
+		{
+			VariableName::UserDefined(ref name) => name == other_name,
+			// Generated variable declarations never match user-defined variables by name
+			VariableName::Generated(_) => false,
+		}
+	}
+}
+
+impl foliage::flavor::Flavor for FoliageFlavor
+{
+	type FunctionDeclaration = FunctionDeclaration;
+	type PredicateDeclaration = PredicateDeclaration;
+	type VariableDeclaration = VariableDeclaration;
+}
+
+pub type BinaryOperation = foliage::BinaryOperation<FoliageFlavor>;
+pub type Formula = foliage::Formula<FoliageFlavor>;
+pub type Formulas = foliage::Formulas<FoliageFlavor>;
+pub type FunctionDeclarations = foliage::FunctionDeclarations<FoliageFlavor>;
+pub type OpenFormula = foliage::OpenFormula<FoliageFlavor>;
+pub type Predicate = foliage::Predicate<FoliageFlavor>;
+pub type PredicateDeclarations = foliage::PredicateDeclarations<FoliageFlavor>;
+pub type QuantifiedFormula = foliage::QuantifiedFormula<FoliageFlavor>;
+pub type Term = foliage::Term<FoliageFlavor>;
+pub type UnaryOperation = foliage::UnaryOperation<FoliageFlavor>;
+pub type Variable = foliage::Variable<FoliageFlavor>;
+pub type VariableDeclarationStackLayer<'p> =
+	foliage::VariableDeclarationStackLayer<'p, FoliageFlavor>;
+pub type VariableDeclarations = foliage::VariableDeclarations<FoliageFlavor>;

src/commands/verify_program.rs

@@ -1,57 +1,76 @@
-pub fn run<P>(program_path: P, specification_path: P, proof_direction: crate::ProofDirection)
+pub fn run<P1, P2>(program_path: P1, specification_paths: &[P2],
+	proof_direction: crate::problem::ProofDirection, no_simplify: bool,
+	color_choice: crate::output::ColorChoice)
 where
-	P: AsRef<std::path::Path>
+	P1: AsRef<std::path::Path>,
+	P2: AsRef<std::path::Path>,
 {
-	//let context = crate::translate::verify_properties::Context::new();
-	let mut problem = crate::Problem::new();
+	let mut problem = crate::Problem::new(color_choice);
 
-	log::info!("reading specification “{}”", specification_path.as_ref().display());
-
-	let specification_content = match std::fs::read_to_string(specification_path.as_ref())
+	for specification_path in specification_paths
 	{
-		Ok(specification_content) => specification_content,
-		Err(error) =>
-		{
-			log::error!("could not access specification file: {}", error);
-			std::process::exit(1)
-		},
-	};
+		log::info!("reading specification file “{}”", specification_path.as_ref().display());
 
-	// TODO: rename to read_specification
-	match crate::input::parse_specification(&specification_content, &mut problem)
-	{
-		Ok(_) => (),
-		Err(error) =>
+		let specification_content = match std::fs::read_to_string(specification_path.as_ref())
 		{
-			log::error!("could not read specification: {}", error);
+			Ok(specification_content) => specification_content,
+			Err(error) =>
+			{
+				log::error!("could not access specification file: {}", error);
+				std::process::exit(1)
+			},
+		};
+
+		// TODO: rename to read_specification
+		if let Err(error) = crate::input::parse_specification(&specification_content, &mut problem)
+		{
+			log::error!("could not read specification file: {}", error);
 			std::process::exit(1)
 		}
+
+		log::info!("read specification “{}”", specification_path.as_ref().display());
 	}
 
-	log::info!("read specification “{}”", specification_path.as_ref().display());
+	problem.process_output_predicates();
 
 	log::info!("reading input program “{}”", program_path.as_ref().display());
 
 	// TODO: make consistent with specification call (path vs. content)
-	match crate::translate::verify_properties::Translator::new(&mut problem).translate(program_path)
+	if let Err(error) = crate::translate::verify_properties::Translator::new(&mut problem)
+		.translate(program_path)
 	{
-		Ok(_) => (),
-		Err(error) =>
+		log::error!("could not translate input program: {}", error);
+		std::process::exit(1)
+	}
+
+	if let Err(error) = problem.check_consistency(proof_direction)
+	{
+		match error.kind
 		{
-			log::error!("could not translate input program: {}", error);
+			// In forward proofs, it’s okay to use private predicates in the specification, but
+			// issue a warning regardless
+			crate::error::Kind::PrivatePredicateInSpecification(_)
+				if !proof_direction.requires_backward_proof() => log::warn!("{}", error),
+			_ =>
+			{
+				log::error!("{}", error);
+				std::process::exit(1)
+			},
+		}
+	}
+
+	if !no_simplify
+	{
+		if let Err(error) = problem.simplify()
+		{
+			log::error!("could not simplify translated program: {}", error);
 			std::process::exit(1)
 		}
 	}
 
-	match problem.prove(proof_direction)
+	if let Err(error) = problem.prove(proof_direction)
 	{
-		Ok(()) => (),
-		Err(error) =>
-		{
-			log::error!("could not verify program: {}", error);
-			std::process::exit(1)
-		}
+		log::error!("could not verify program: {}", error);
+		std::process::exit(1)
 	}
-
-	log::info!("done");
 }

src/error.rs

@@ -1,3 +1,5 @@
+use foliage::flavor::VariableDeclaration as _;
+
 pub type Source = Box<dyn std::error::Error>;
 
 pub enum Kind
@@ -15,16 +17,23 @@ pub enum Kind
 	MissingStatementTerminator,
 	ParseFormula,
 	ExpectedIdentifier,
+	ExpectedPredicateSpecifier,
 	ParsePredicateDeclaration,
 	//ParseConstantDeclaration,
 	UnknownProofDirection(String),
 	UnknownDomainIdentifier(String),
+	UnknownColorChoice(String),
 	VariableNameNotAllowed(String),
-	WriteTPTPProgram,
+	FormulaNotClosed(std::rc::Rc<crate::VariableDeclarations>),
+	ProgramNotTight(std::rc::Rc<crate::PredicateDeclaration>),
+	PrivatePredicateCycle(std::rc::Rc<crate::PredicateDeclaration>),
+	NoninputPredicateInAssumption(std::rc::Rc<crate::PredicateDeclaration>),
+	PrivatePredicateInSpecification(std::rc::Rc<crate::PredicateDeclaration>),
 	RunVampire,
 	// TODO: rename to something Vampire-specific
 	ProveProgram(Option<i32>, String, String),
 	ParseVampireOutput(String, String),
+	IO,
 }
 
 pub struct Error
@@ -115,6 +124,11 @@ impl Error
 		Self::new(Kind::ExpectedIdentifier)
 	}
 
+	pub(crate) fn new_expected_predicate_specifier() -> Self
+	{
+		Self::new(Kind::ExpectedPredicateSpecifier)
+	}
+
 	pub(crate) fn new_parse_predicate_declaration() -> Self
 	{
 		Self::new(Kind::ParsePredicateDeclaration)
@@ -130,14 +144,48 @@ impl Error
 		Self::new(Kind::UnknownDomainIdentifier(domain_identifier))
 	}
 
+	pub(crate) fn new_unknown_color_choice(color_choice: String) -> Self
+	{
+		Self::new(Kind::UnknownColorChoice(color_choice))
+	}
+
 	pub(crate) fn new_variable_name_not_allowed(variable_name: String) -> Self
 	{
 		Self::new(Kind::VariableNameNotAllowed(variable_name))
 	}
 
-	pub(crate) fn new_write_tptp_program<S: Into<Source>>(source: S) -> Self
+	pub(crate) fn new_formula_not_closed(free_variables: std::rc::Rc<crate::VariableDeclarations>)
+		-> Self
 	{
-		Self::new(Kind::WriteTPTPProgram).with(source)
+		Self::new(Kind::FormulaNotClosed(free_variables))
+	}
+
+	pub(crate) fn new_program_not_tight(
+		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::ProgramNotTight(predicate_declaration))
+	}
+
+	pub(crate) fn new_private_predicate_cycle(
+		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::PrivatePredicateCycle(predicate_declaration))
+	}
+
+	pub(crate) fn new_noninput_predicate_in_assumption(
+		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::NoninputPredicateInAssumption(predicate_declaration))
+	}
+
+	pub(crate) fn new_private_predicate_in_specification(
+		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::PrivatePredicateInSpecification(predicate_declaration))
 	}
 
 	pub(crate) fn new_run_vampire<S: Into<Source>>(source: S) -> Self
@@ -154,6 +202,11 @@ impl Error
 	{
 		Self::new(Kind::ParseVampireOutput(stdout, stderr))
 	}
+
+	pub(crate) fn new_io<S: Into<Source>>(source: S) -> Self
+	{
+		Self::new(Kind::IO).with(source)
+	}
 }
 
 impl std::fmt::Debug for Error
@@ -178,22 +231,53 @@ impl std::fmt::Debug for Error
 				"unknown statement “{}” (allowed: axiom, assert, assume, input, lemma)",
 				statement_name),
 			Kind::UnmatchedParenthesis => write!(formatter, "unmatched parenthesis"),
-			Kind::ParsePredicateDeclaration => write!(formatter,
-				"could not parse predicate declaration"),
 			Kind::ParseFormula => write!(formatter, "could not parse formula"),
 			Kind::ExpectedIdentifier => write!(formatter, "expected constant or predicate name"),
+			Kind::ExpectedPredicateSpecifier =>
+				write!(formatter, "expected predicate specifier (examples: p/0, q/2)"),
 			Kind::ParsePredicateDeclaration => write!(formatter,
 				"could not parse predicate declaration"),
+			// TODO: rename to ExpectedStatementTerminator
 			Kind::MissingStatementTerminator => write!(formatter,
 				"statement not terminated with ‘.’ character"),
 			Kind::UnknownProofDirection(ref proof_direction) => write!(formatter,
 				"unknown proof direction “{}” (allowed: integer, program)", proof_direction),
 			Kind::UnknownDomainIdentifier(ref domain_identifier) => write!(formatter,
 				"unknown domain identifier “{}” (allowed: int, program)", domain_identifier),
+			Kind::UnknownColorChoice(ref color_choice) => write!(formatter,
+				"unknown color choice “{}” (allowed: auto, always, never)", color_choice),
 			Kind::VariableNameNotAllowed(ref variable_name) => write!(formatter,
 				"variable name “{}” not allowed (program variables must start with X, Y, or Z and integer variables with I, J, K, L, M, or N)",
 				variable_name),
-			Kind::WriteTPTPProgram => write!(formatter, "error writing TPTP program"),
+			Kind::FormulaNotClosed(free_variable_declarations) =>
+			{
+				write!(formatter, "formula may not contain free variables (free variables in this formula: ")?;
+
+				let mut separator = "";
+
+				for free_variable_declaration in &**free_variable_declarations
+				{
+					write!(formatter, "{}", separator)?;
+					free_variable_declaration.display_name(formatter)?;
+					separator = ", ";
+				}
+
+				write!(formatter, ")")
+			},
+			Kind::ProgramNotTight(ref predicate_declaration) =>
+				write!(formatter, "program not tight (positive recursion involving {})",
+					predicate_declaration.declaration),
+			Kind::PrivatePredicateCycle(ref predicate_declaration) =>
+				write!(formatter, "private recursion involving {}",
+					predicate_declaration.declaration),
+			Kind::NoninputPredicateInAssumption(ref predicate_declaration) =>
+				write!(formatter,
+					"assumption includes {}, which is not an input predicate (consider declaring {} an input predicate)",
+					predicate_declaration.declaration, predicate_declaration.declaration),
+			Kind::PrivatePredicateInSpecification(ref predicate_declaration) =>
+				write!(formatter,
+					"private predicate {} should not occur in specification (consider declaring {} an input or output predicate)",
+					predicate_declaration.declaration, predicate_declaration.declaration),
 			Kind::RunVampire => write!(formatter, "could not run Vampire"),
 			Kind::ProveProgram(exit_code, ref stdout, ref stderr) =>
 			{
@@ -216,6 +300,7 @@ impl std::fmt::Debug for Error
 				{}\
 				==== stderr ===========================================================\n\
 				{}", stdout, stderr),
+			Kind::IO => write!(formatter, "input/output error"),
 		}?;
 
 		if let Some(source) = &self.source
@@ -246,3 +331,11 @@ impl std::error::Error for Error
 		}
 	}
 }
+
+impl From<std::io::Error> for Error
+{
+	fn from(error: std::io::Error) -> Self
+	{
+		Self::new_io(error)
+	}
+}

src/input/specification.rs

@@ -1,97 +1,8 @@
-// TODO: refactor
-fn term_assign_variable_declaration_domains<D>(term: &foliage::Term, declarations: &D)
-	-> Result<(), crate::Error>
+fn open_formula<'i, D>(input: &'i str, declarations: &D)
+	-> Result<(crate::OpenFormula, &'i str), crate::Error>
 where
-	D: crate::traits::AssignVariableDeclarationDomain,
-{
-	match term
-	{
-		foliage::Term::BinaryOperation(binary_operation) =>
-		{
-			term_assign_variable_declaration_domains(&binary_operation.left, declarations)?;
-			term_assign_variable_declaration_domains(&binary_operation.right, declarations)?;
-		},
-		foliage::Term::Function(function) =>
-			for argument in &function.arguments
-			{
-				term_assign_variable_declaration_domains(&argument, declarations)?;
-			},
-		foliage::Term::UnaryOperation(unary_operation) =>
-			term_assign_variable_declaration_domains(&unary_operation.argument, declarations)?,
-		foliage::Term::Variable(variable) =>
-		{
-			let domain =  match variable.declaration.name.chars().next()
-			{
-				Some('X')
-				| Some('Y')
-				| Some('Z') => crate::Domain::Program,
-				Some('I')
-				| Some('J')
-				| Some('K')
-				| Some('L')
-				| Some('M')
-				| Some('N') => crate::Domain::Integer,
-				// TODO: improve error handling
-				Some(other) => return Err(
-					crate::Error::new_variable_name_not_allowed(variable.declaration.name.clone())),
-				None => unreachable!(),
-			};
-
-			declarations.assign_variable_declaration_domain(&variable.declaration, domain);
-		},
-		_ => (),
-	}
-
-	Ok(())
-}
-
-fn formula_assign_variable_declaration_domains<D>(formula: &foliage::Formula, declarations: &D)
-	-> Result<(), crate::Error>
-where
-	D: crate::traits::AssignVariableDeclarationDomain,
-{
-	match formula
-	{
-		foliage::Formula::And(arguments)
-		| foliage::Formula::Or(arguments)
-		| foliage::Formula::IfAndOnlyIf(arguments) =>
-			for argument in arguments
-			{
-				formula_assign_variable_declaration_domains(&argument, declarations)?;
-			},
-		foliage::Formula::Compare(compare) =>
-		{
-			term_assign_variable_declaration_domains(&compare.left, declarations)?;
-			term_assign_variable_declaration_domains(&compare.right, declarations)?;
-		},
-		foliage::Formula::Exists(quantified_formula)
-		| foliage::Formula::ForAll(quantified_formula) =>
-			formula_assign_variable_declaration_domains(&quantified_formula.argument,
-				declarations)?,
-		foliage::Formula::Implies(implies) =>
-		{
-			formula_assign_variable_declaration_domains(&implies.antecedent, declarations)?;
-			formula_assign_variable_declaration_domains(&implies.implication, declarations)?;
-		}
-		foliage::Formula::Not(argument) =>
-			formula_assign_variable_declaration_domains(&argument, declarations)?,
-		foliage::Formula::Predicate(predicate) =>
-			for argument in &predicate.arguments
-			{
-				term_assign_variable_declaration_domains(&argument, declarations)?;
-			},
-		_ => (),
-	}
-
-	Ok(())
-}
-
-fn closed_formula<'i, D>(input: &'i str, declarations: &D)
-	-> Result<(crate::ScopedFormula, &'i str), crate::Error>
-where
-	D: foliage::FindOrCreateFunctionDeclaration
-		+ foliage::FindOrCreatePredicateDeclaration
-		+ crate::traits::AssignVariableDeclarationDomain,
+	D: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>
+		+ foliage::FindOrCreatePredicateDeclaration<crate::FoliageFlavor>
 {
 	let terminator_position = match input.find('.')
 	{
@@ -104,176 +15,114 @@ 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)?;
-
-	// TODO: get rid of ScopedFormula
-	let scoped_formula = crate::ScopedFormula
+	let open_formula = crate::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))
 }
 
-fn variable_free_formula<'i, D>(input: &'i str, declarations: &D)
-	-> Result<(foliage::Formula, &'i str), crate::Error>
+fn formula<'i, D>(mut input: &'i str, declarations: &D)
+	-> Result<(crate::Formula, &'i str), crate::Error>
 where
-	D: foliage::FindOrCreateFunctionDeclaration
-		+ foliage::FindOrCreatePredicateDeclaration
-		+ crate::traits::AssignVariableDeclarationDomain,
+	D: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>
+		+ foliage::FindOrCreatePredicateDeclaration<crate::FoliageFlavor>
 {
-	let (closed_formula, input) = closed_formula(input, declarations)?;
-
-	if !closed_formula.free_variable_declarations.is_empty()
-	{
-		// TODO: improve
-		panic!("formula may not contain free variables");
-	}
-
-	Ok((closed_formula.formula, input))
-}
-
-fn formula_statement_body<'i>(input: &'i str, problem: &crate::Problem)
-	-> Result<(foliage::Formula, &'i str), crate::Error>
-{
-	let input = input.trim_start();
-
-	let mut input_characters = input.chars();
-
-	let remaining_input = match input_characters.next()
-	{
-		Some(':') => input_characters.as_str(),
-		_ => return Err(crate::Error::new_expected_colon()),
-	};
-
-	let input = remaining_input;
-
-	variable_free_formula(input, problem)
-}
-
-fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
-	-> Result<&'i str, crate::Error>
-{
-	input = input.trim_start();
-
-	let mut input_characters = input.chars();
-
-	let remaining_input = match input_characters.next()
-	{
-		Some(':') => input_characters.as_str(),
-		_ => return Err(crate::Error::new_expected_colon()),
-	};
+	let (open_formula, remaining_input) = open_formula(input, declarations)?;
 
 	input = remaining_input;
 
-	loop
+	if !open_formula.free_variable_declarations.is_empty()
 	{
-		input = input.trim_start();
+		return Err(crate::Error::new_formula_not_closed(open_formula.free_variable_declarations));
+	}
 
-		let (constant_or_predicate_name, remaining_input) =
+	Ok((open_formula.formula, input))
+}
+
+fn formula_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
+	-> Result<(crate::Formula, &'i str), crate::Error>
+{
+	input = foliage::parse::tokens::trim_start(input);
+
+	let mut input_characters = input.chars();
+
+	input = match input_characters.next()
+	{
+		Some(':') => input_characters.as_str(),
+		_ => return Err(crate::Error::new_expected_colon()),
+	};
+
+	formula(input, problem)
+}
+
+fn domain_specifier<'i>(mut input: &'i str)
+	-> Result<(Option<crate::Domain>, &'i str), crate::Error>
+{
+	let original_input = input;
+	input = foliage::parse::tokens::trim_start(input);
+
+	if input.starts_with("->")
+	{
+		let mut input_characters = input.chars();
+		input_characters.next();
+		input_characters.next();
+
+		input = foliage::parse::tokens::trim_start(input_characters.as_str());
+
+		let (identifier, remaining_input) =
 			foliage::parse::tokens::identifier(input)
 				.ok_or_else(|| crate::Error::new_expected_identifier())?;
 
-		input = remaining_input.trim_start();
+		input = remaining_input;
 
-		let mut input_characters = input.chars();
-
-		match input_characters.next()
+		match identifier
 		{
-			// Parse input predicate specifiers
-			Some('/') =>
-			{
-				input = input_characters.as_str().trim_start();
-
-				let (arity, remaining_input) = foliage::parse::tokens::number(input)
-					.map_err(|error| crate::Error::new_parse_predicate_declaration().with(error))?
-					.ok_or_else(|| crate::Error::new_parse_predicate_declaration())?;
-
-				input = remaining_input.trim_start();
-
-				let mut input_predicate_declarations =
-					problem.input_predicate_declarations.borrow_mut();
-
-				use foliage::FindOrCreatePredicateDeclaration;
-
-				let predicate_declaration =
-					problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity);
-
-				input_predicate_declarations.insert(predicate_declaration);
-
-				let mut input_characters = input.chars();
-
-				match input_characters.next()
-				{
-					Some(',') => input = input_characters.as_str(),
-					_ => break,
-				}
-			},
-			// Parse input constant specifiers
-			Some(_)
-			| None =>
-			{
-				let domain =
-					if input.starts_with("->")
-					{
-						let mut input_characters = input.chars();
-						input_characters.next();
-						input_characters.next();
-
-						input = input_characters.as_str().trim_start();
-
-						let (identifier, remaining_input) =
-							foliage::parse::tokens::identifier(input)
-								.ok_or_else(|| crate::Error::new_expected_identifier())?;
-
-						input = remaining_input;
-
-						match identifier
-						{
-							"integer" => crate::Domain::Integer,
-							"program" => crate::Domain::Program,
-							_ => return Err(crate::Error::new_unknown_domain_identifier(
-								identifier.to_string())),
-						}
-					}
-					else
-					{
-						crate::Domain::Program
-					};
-
-				log::debug!("domain: {:?}", domain);
-
-				let mut input_constant_declarations =
-					problem.input_constant_declarations.borrow_mut();
-
-				use foliage::FindOrCreateFunctionDeclaration;
-
-				let constant_declaration =
-					problem.find_or_create_function_declaration(constant_or_predicate_name, 0);
-
-				input_constant_declarations.insert(std::rc::Rc::clone(&constant_declaration));
-
-				let mut input_constant_declaration_domains =
-					problem.input_constant_declaration_domains.borrow_mut();
-
-				input_constant_declaration_domains.insert(constant_declaration, domain);
-
-				let mut input_characters = input.chars();
-
-				match input_characters.next()
-				{
-					Some(',') => input = input_characters.as_str(),
-					_ => break,
-				}
-			}
+			"integer" => Ok((Some(crate::Domain::Integer), input)),
+			"program" => Ok((Some(crate::Domain::Program), input)),
+			_ => return Err(crate::Error::new_unknown_domain_identifier(identifier.to_string())),
 		}
 	}
+	else
+	{
+		Ok((None, original_input))
+	}
+}
 
-	input = input.trim_start();
+fn predicate_arity_specifier<'i>(mut input: &'i str)
+	-> Result<(Option<usize>, &'i str), crate::Error>
+{
+	let original_input = input;
+	input = foliage::parse::tokens::trim_start(input);
+
+	let mut input_characters = input.chars();
+
+	if input_characters.next() == Some('/')
+	{
+		input = foliage::parse::tokens::trim_start(input_characters.as_str());
+
+		let (arity, remaining_input) = foliage::parse::tokens::number(input)
+			.map_err(|error| crate::Error::new_parse_predicate_declaration().with(error))?
+			.ok_or_else(|| crate::Error::new_parse_predicate_declaration())?;
+
+		input = remaining_input;
+
+		Ok((Some(arity), input))
+	}
+	else
+	{
+		Ok((None, original_input))
+	}
+}
+
+fn expect_statement_terminator<'i>(mut input: &'i str) -> Result<&'i str, crate::Error>
+{
+	input = foliage::parse::tokens::trim_start(input);
 
 	let mut input_characters = input.chars();
 
@@ -287,12 +136,134 @@ fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
 	Ok(input)
 }
 
+fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
+	-> Result<&'i str, crate::Error>
+{
+	input = foliage::parse::tokens::trim_start(input);
+
+	let mut input_characters = input.chars();
+
+	let remaining_input = match input_characters.next()
+	{
+		Some(':') => input_characters.as_str(),
+		_ => return Err(crate::Error::new_expected_colon()),
+	};
+
+	input = remaining_input;
+
+	loop
+	{
+		input = foliage::parse::tokens::trim_start(input);
+
+		let (constant_or_predicate_name, remaining_input) =
+			foliage::parse::tokens::identifier(input)
+				.ok_or_else(|| crate::Error::new_expected_identifier())?;
+
+		input = foliage::parse::tokens::trim_start(remaining_input);
+
+		// Parse input predicate specifiers
+		if let (Some(arity), remaining_input) = predicate_arity_specifier(input)?
+		{
+			input = remaining_input;
+
+			let predicate_declaration =
+				problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity,
+					crate::PredicateDeclarationSource::Specification);
+
+			*predicate_declaration.is_input.borrow_mut() = true;
+		}
+		// Parse input constant specifiers
+		else
+		{
+			// TODO: detect conflicting domain specifiers (for example: n -> program, n -> integer)
+			let (domain, remaining_input) = match domain_specifier(input)?
+			{
+				(Some(domain), remaining_input) => (domain, remaining_input),
+				(None, remaining_input) => (crate::Domain::Program, remaining_input),
+			};
+
+			input = remaining_input;
+
+			use foliage::FindOrCreateFunctionDeclaration as _;
+
+			let constant_declaration =
+				problem.find_or_create_function_declaration(constant_or_predicate_name, 0);
+
+			*constant_declaration.is_input.borrow_mut() = true;
+			*constant_declaration.domain.borrow_mut() = domain;
+		}
+
+		let mut input_characters = input.chars();
+
+		match input_characters.next()
+		{
+			Some(',') => input = input_characters.as_str(),
+			_ => break,
+		}
+	}
+
+	expect_statement_terminator(input)
+}
+
+fn output_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
+	-> Result<&'i str, crate::Error>
+{
+	input = foliage::parse::tokens::trim_start(input);
+
+	let mut input_characters = input.chars();
+
+	let remaining_input = match input_characters.next()
+	{
+		Some(':') => input_characters.as_str(),
+		_ => return Err(crate::Error::new_expected_colon()),
+	};
+
+	input = remaining_input;
+
+	loop
+	{
+		input = foliage::parse::tokens::trim_start(input);
+
+		let (constant_or_predicate_name, remaining_input) =
+			foliage::parse::tokens::identifier(input)
+				.ok_or_else(|| crate::Error::new_expected_identifier())?;
+
+		input = foliage::parse::tokens::trim_start(remaining_input);
+
+		// Only accept output predicate specifiers
+		if let (Some(arity), remaining_input) = predicate_arity_specifier(input)?
+		{
+			input = remaining_input;
+
+			let predicate_declaration =
+				problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity,
+					crate::PredicateDeclarationSource::Specification);
+
+			*predicate_declaration.is_output.borrow_mut() = true;
+		}
+		else
+		{
+			return Err(crate::Error::new_expected_predicate_specifier());
+		}
+
+		let mut input_characters = input.chars();
+
+		match input_characters.next()
+		{
+			Some(',') => input = input_characters.as_str(),
+			_ => break,
+		}
+	}
+
+	expect_statement_terminator(input)
+}
+
 pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
 	-> Result<(), crate::Error>
 {
 	loop
 	{
-		input = input.trim_start();
+		input = foliage::parse::tokens::trim_start(input);
 
 		if input.is_empty()
 		{
@@ -335,7 +306,7 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
 			},
 			"lemma" =>
 			{
-				input = input.trim_start();
+				input = foliage::parse::tokens::trim_start(input);
 
 				let mut input_characters = input.chars();
 
@@ -344,24 +315,24 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
 					Some('(') =>
 					{
 						// TODO: refactor
-						input = input_characters.as_str().trim_start();
+						input = foliage::parse::tokens::trim_start(input_characters.as_str());
 
 						let (proof_direction, remaining_input) = match
 							foliage::parse::tokens::identifier(input)
 						{
 							Some(("forward", remaining_input)) =>
-								(crate::ProofDirection::Forward, remaining_input),
+								(crate::problem::ProofDirection::Forward, remaining_input),
 							Some(("backward", remaining_input)) =>
-								(crate::ProofDirection::Backward, remaining_input),
+								(crate::problem::ProofDirection::Backward, remaining_input),
 							Some(("both", remaining_input)) =>
-								(crate::ProofDirection::Both, remaining_input),
+								(crate::problem::ProofDirection::Both, remaining_input),
 							Some((identifier, _)) =>
 								return Err(crate::Error::new_unknown_proof_direction(
 									identifier.to_string())),
-							None => (crate::ProofDirection::Both, input),
+							None => (crate::problem::ProofDirection::Both, input),
 						};
 
-						input = remaining_input.trim_start();
+						input = foliage::parse::tokens::trim_start(remaining_input);
 
 						let mut input_characters = input.chars();
 
@@ -375,7 +346,7 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
 						(proof_direction, input)
 					},
 					Some(_)
-					| None => (crate::ProofDirection::Both, remaining_input),
+					| None => (crate::problem::ProofDirection::Both, remaining_input),
 				};
 
 				input = remaining_input;
@@ -391,20 +362,21 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
 
 				continue;
 			},
-			"assert" =>
+			"spec" =>
 			{
 				let (formula, remaining_input) = formula_statement_body(input, problem)?;
 
 				input = remaining_input;
 
 				let statement = crate::problem::Statement::new(
-					crate::problem::StatementKind::Assertion, formula);
+					crate::problem::StatementKind::Spec, formula);
 
-				problem.add_statement(crate::problem::SectionKind::Assertions, statement);
+				problem.add_statement(crate::problem::SectionKind::Specs, statement);
 
 				continue;
 			},
 			"input" => input = input_statement_body(input, problem)?,
+			"output" => input = output_statement_body(input, problem)?,
 			identifier => return Err(crate::Error::new_unknown_statement(identifier.to_string())),
 		}
 	}

src/lib.rs

@@ -1,15 +1,19 @@
 #![feature(trait_alias)]
+#![feature(vec_remove_item)]
 
+mod ast;
 pub mod commands;
 pub mod error;
 pub mod input;
 pub mod output;
 pub mod problem;
-pub(crate) mod traits;
+pub mod simplify;
 pub mod translate;
 mod utils;
 
+pub use crate::ast::*;
 pub use error::Error;
 pub use problem::Problem;
+pub(crate) use simplify::*;
 pub(crate) use utils::*;
-pub use utils::{Domain, InputConstantDeclarationDomains, ProofDirection};
+pub use utils::Domain;

src/main.rs

@@ -13,12 +13,20 @@ enum Command
 		program_path: std::path::PathBuf,
 
 		#[structopt(name = "specification", parse(from_os_str), required(true))]
-		/// Specification file path
-		specification_path: std::path::PathBuf,
+		/// One or more specification file paths
+		specification_paths: Vec<std::path::PathBuf>,
 
 		/// Proof direction (forward, backward, both)
-		#[structopt(long, default_value = "forward")]
-		proof_direction: anthem::ProofDirection,
+		#[structopt(long, default_value = "both")]
+		proof_direction: anthem::problem::ProofDirection,
+
+		/// Do not simplify translated program
+		#[structopt(long)]
+		no_simplify: bool,
+
+		/// Whether to use colors in the output (auto, always, never)
+		#[structopt(name = "color", long, default_value = "auto")]
+		color_choice: anthem::output::ColorChoice,
 	}
 }
 
@@ -33,10 +41,12 @@ fn main()
 		Command::VerifyProgram
 		{
 			program_path,
-			specification_path,
+			specification_paths,
 			proof_direction,
+			no_simplify,
+			color_choice,
 		}
-			=> anthem::commands::verify_program::run(&program_path, &specification_path,
-				proof_direction),
+			=> anthem::commands::verify_program::run(&program_path, specification_paths.as_slice(),
+				proof_direction, no_simplify, color_choice),
 	}
 }

src/output.rs

@@ -1,6 +1,9 @@
-pub(crate) mod human_readable;
+pub(crate) mod shell;
 pub(crate) mod tptp;
 
+pub use shell::ColorChoice;
+pub(crate) use shell::Shell;
+
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
 pub enum Format
 {

src/output/human_readable.rs

@@ -1,18 +0,0 @@
-/*pub(crate) fn display_variable_declaration<C>(context: &C, formatter: &mut std::fmt::Formatter,
-	variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-	-> std::fmt::Result
-where C:
-	crate::traits::VariableDeclarationDomain + crate::traits::VariableDeclarationID
-{
-	let id = context.variable_declaration_id(variable_declaration);
-	let domain = context.variable_declaration_domain(variable_declaration)
-		.expect("unspecified variable domain");
-
-	let prefix = match domain
-	{
-		crate::Domain::Integer => "N",
-		crate::Domain::Program => "X",
-	};
-
-	write!(formatter, "{}{}", prefix, id + 1)
-}*/

src/output/shell.rs

@@ -0,0 +1,149 @@
+pub struct Shell
+{
+	output: ShellOutput,
+}
+
+enum ShellOutput
+{
+	Basic(Box<dyn std::io::Write>),
+	WithColorSupport(termcolor::StandardStream),
+}
+
+#[derive(Clone, Copy, Eq, PartialEq)]
+pub enum ColorChoice
+{
+	Always,
+	Never,
+	Auto,
+}
+
+impl Shell
+{
+	pub fn from_stdout(color_choice: ColorChoice) -> Self
+	{
+		Self
+		{
+			output: match color_choice
+			{
+				ColorChoice::Never => ShellOutput::Basic(Box::new(std::io::stdout())),
+				_ => ShellOutput::WithColorSupport(termcolor::StandardStream::stdout(
+					color_choice.to_termcolor_color_choice())),
+			},
+		}
+	}
+
+	pub fn print(&mut self, text: &dyn std::fmt::Display, color: &termcolor::ColorSpec)
+		-> std::io::Result<()>
+	{
+		self.output.print(text, color)
+	}
+
+	pub fn println(&mut self, text: &dyn std::fmt::Display, color: &termcolor::ColorSpec)
+		-> std::io::Result<()>
+	{
+		self.output.println(text, color)
+	}
+
+	pub fn erase_line(&mut self)
+	{
+		self.output.erase_line();
+	}
+}
+
+impl ShellOutput
+{
+	fn print(&mut self, text: &dyn std::fmt::Display, color: &termcolor::ColorSpec)
+		-> std::io::Result<()>
+	{
+		use std::io::Write as _;
+		use termcolor::WriteColor as _;
+
+		match *self
+		{
+			Self::Basic(ref mut write) => write!(write, "{}", text),
+			Self::WithColorSupport(ref mut stream) =>
+			{
+				stream.reset()?;
+				stream.set_color(color)?;
+
+				write!(stream, "{}", text)?;
+
+				stream.reset()
+			},
+		}
+	}
+
+	fn println(&mut self, text: &dyn std::fmt::Display, color: &termcolor::ColorSpec)
+		-> std::io::Result<()>
+	{
+		self.print(text, color)?;
+
+		use std::io::Write as _;
+
+		match *self
+		{
+			Self::Basic(ref mut write) => writeln!(write, ""),
+			Self::WithColorSupport(ref mut stream) => writeln!(stream, ""),
+		}
+	}
+
+	#[cfg(unix)]
+	pub fn erase_line(&mut self)
+	{
+		let erase_sequence = b"\x1b[2K";
+
+		use std::io::Write as _;
+
+		let _ = match *self
+		{
+			Self::Basic(ref mut write) => write.write_all(erase_sequence),
+			Self::WithColorSupport(ref mut stream) => stream.write_all(erase_sequence),
+		};
+	}
+}
+
+impl ColorChoice
+{
+	fn to_termcolor_color_choice(self) -> termcolor::ColorChoice
+	{
+		match self
+		{
+			Self::Always => termcolor::ColorChoice::Always,
+			Self::Never => termcolor::ColorChoice::Never,
+			Self::Auto => match atty::is(atty::Stream::Stdout)
+			{
+				true => termcolor::ColorChoice::Auto,
+				false => termcolor::ColorChoice::Never,
+			},
+		}
+	}
+}
+
+impl std::fmt::Debug for ColorChoice
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match self
+		{
+			ColorChoice::Always => write!(formatter, "always"),
+			ColorChoice::Never => write!(formatter, "never"),
+			ColorChoice::Auto => write!(formatter, "auto"),
+		}
+	}
+}
+
+impl std::str::FromStr for ColorChoice
+{
+	type Err = crate::Error;
+
+	fn from_str(s: &str) -> Result<Self, Self::Err>
+	{
+		match s
+		{
+			"always" => Ok(ColorChoice::Always),
+			"never" => Ok(ColorChoice::Never),
+			"auto" => Ok(ColorChoice::Auto),
+			_ => Err(crate::Error::new_unknown_color_choice(s.to_string())),
+		}
+	}
+}

src/output/tptp.rs

@@ -1,3 +1,6 @@
+use foliage::flavor::{FunctionDeclaration as _, PredicateDeclaration as _,
+	 VariableDeclaration as _};
+
 pub(crate) struct DomainDisplay
 {
 	domain: crate::Domain,
@@ -13,7 +16,7 @@ pub(crate) fn display_domain(domain: crate::Domain) -> DomainDisplay
 
 impl std::fmt::Debug for DomainDisplay
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
 		let domain_name = match self.domain
 		{
@@ -21,49 +24,34 @@ impl std::fmt::Debug for DomainDisplay
 			crate::Domain::Program => "object",
 		};
 
-		write!(format, "{}", domain_name)
+		write!(formatter, "{}", domain_name)
 	}
 }
 
 impl std::fmt::Display for DomainDisplay
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", &self)
+		write!(formatter, "{:?}", &self)
 	}
 }
 
-pub(crate) struct FunctionDeclarationDisplay<'a, 'b, C>
-where
-	C: crate::traits::InputConstantDeclarationDomain
+pub(crate) struct FunctionDeclarationDisplay<'a>(&'a crate::FunctionDeclaration);
+
+pub(crate) fn display_function_declaration<'a>(function_declaration: &'a crate::FunctionDeclaration)
+	-> FunctionDeclarationDisplay<'a>
 {
-	function_declaration: &'a std::rc::Rc<foliage::FunctionDeclaration>,
-	context: &'b C,
+	FunctionDeclarationDisplay(function_declaration)
 }
 
-pub(crate) fn display_function_declaration<'a, 'b, C>(
-	function_declaration: &'a std::rc::Rc<foliage::FunctionDeclaration>, context: &'b C)
-	-> FunctionDeclarationDisplay<'a, 'b, C>
-where
-	C: crate::traits::InputConstantDeclarationDomain
+impl<'a> std::fmt::Debug for FunctionDeclarationDisplay<'a>
 {
-	FunctionDeclarationDisplay
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		function_declaration,
-		context,
-	}
-}
+		self.0.display_name(formatter)?;
+		write!(formatter, ":")?;
 
-impl<'a, 'b, C> std::fmt::Debug for FunctionDeclarationDisplay<'a, 'b, C>
-where
-	C: crate::traits::InputConstantDeclarationDomain
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(format, "{}:", self.function_declaration.name)?;
-
-		let domain = self.context.input_constant_declaration_domain(self.function_declaration);
-		let domain_identifier = match domain
+		let domain_identifier = match *self.0.domain.borrow()
 		{
 			crate::Domain::Integer => "$int",
 			crate::Domain::Program => "object",
@@ -71,37 +59,35 @@ where
 
 		let mut separator = "";
 
-		if self.function_declaration.arity > 0
+		if self.0.arity() > 0
 		{
-			write!(format, " (")?;
+			write!(formatter, " (")?;
 
-			for _ in 0..self.function_declaration.arity
+			for _ in 0..self.0.arity()
 			{
-				write!(format, "{}object", separator)?;
+				write!(formatter, "{}object", separator)?;
 				separator = " * ";
 			}
 
-			write!(format, ") >")?;
+			write!(formatter, ") >")?;
 		}
 
-		write!(format, " {}", domain_identifier)
+		write!(formatter, " {}", domain_identifier)
 	}
 }
 
-impl<'a, 'b, C> std::fmt::Display for FunctionDeclarationDisplay<'a, 'b, C>
-where
-	C: crate::traits::InputConstantDeclarationDomain
+impl<'a> std::fmt::Display for FunctionDeclarationDisplay<'a>
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", &self)
+		write!(formatter, "{:?}", &self)
 	}
 }
 
-pub(crate) struct PredicateDeclarationDisplay<'a>(&'a std::rc::Rc<foliage::PredicateDeclaration>);
+pub(crate) struct PredicateDeclarationDisplay<'a>(&'a crate::PredicateDeclaration);
 
 pub(crate) fn display_predicate_declaration<'a>(
-	predicate_declaration: &'a std::rc::Rc<foliage::PredicateDeclaration>)
+	predicate_declaration: &'a crate::PredicateDeclaration)
 	-> PredicateDeclarationDisplay<'a>
 {
 	PredicateDeclarationDisplay(predicate_declaration)
@@ -109,235 +95,142 @@ pub(crate) fn display_predicate_declaration<'a>(
 
 impl<'a> std::fmt::Debug for PredicateDeclarationDisplay<'a>
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{}:", self.0.name)?;
+		self.0.display_name(formatter)?;
+		write!(formatter, ":")?;
 
 		let mut separator = "";
 
-		if self.0.arity > 0
+		if self.0.arity() > 0
 		{
-			write!(format, " (")?;
+			write!(formatter, " (")?;
 
-			for _ in 0..self.0.arity
+			for _ in 0..self.0.arity()
 			{
-				write!(format, "{}object", separator)?;
+				write!(formatter, "{}object", separator)?;
 				separator = " * ";
 			}
 
-			write!(format, ") >")?;
+			write!(formatter, ") >")?;
 		}
 
-		write!(format, " $o")
+		write!(formatter, " $o")
 	}
 }
 
 impl<'a> std::fmt::Display for PredicateDeclarationDisplay<'a>
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", &self)
+		write!(formatter, "{:?}", &self)
 	}
 }
 
-pub(crate) struct VariableDeclarationDisplay<'a, 'b, C>
-where
-	C: crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
+pub(crate) struct TermDisplay<'a>(&'a crate::Term);
+
+pub(crate) fn display_term<'a>(term: &'a crate::Term) -> TermDisplay<'a>
 {
-	variable_declaration: &'a std::rc::Rc<foliage::VariableDeclaration>,
-	context: &'b C,
+	TermDisplay(term)
 }
 
-pub(crate) fn display_variable_declaration<'a, 'b, C>(
-	variable_declaration: &'a std::rc::Rc<foliage::VariableDeclaration>, context: &'b C)
-	-> VariableDeclarationDisplay<'a, 'b, C>
-where
-	C: crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
+impl<'a> std::fmt::Debug for TermDisplay<'a>
 {
-	VariableDeclarationDisplay
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		variable_declaration,
-		context,
-	}
-}
+		use foliage::*;
 
-impl<'a, 'b, C> std::fmt::Debug for VariableDeclarationDisplay<'a, 'b, C>
-where
-	C: crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		let id = self.context.variable_declaration_id(self.variable_declaration);
-		let domain = self.context.variable_declaration_domain(self.variable_declaration)
-			.expect("unspecified variable domain");
-
-		let prefix = match domain
+		match &self.0
 		{
-			crate::Domain::Integer => "N",
-			crate::Domain::Program => "X",
-		};
-
-		write!(format, "{}{}", prefix, id + 1)
-	}
-}
-
-impl<'a, 'b, C> std::fmt::Display for VariableDeclarationDisplay<'a, 'b, C>
-where
-	C: crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(format, "{:?}", &self)
-	}
-}
-
-pub(crate) struct TermDisplay<'a, 'b, C>
-{
-	term: &'a foliage::Term,
-	context: &'b C,
-}
-
-pub(crate) fn display_term<'a, 'b, C>(term: &'a foliage::Term, context: &'b C)
-	-> TermDisplay<'a, 'b, C>
-where
-	C: crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
-{
-	TermDisplay
-	{
-		term,
-		context,
-	}
-}
-
-impl<'a, 'b, C> std::fmt::Debug for TermDisplay<'a, 'b, C>
-where
-	C: crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		let display_variable_declaration = |variable_declaration|
-			display_variable_declaration(variable_declaration, self.context);
-		let display_term = |term| display_term(term, self.context);
-
-		match &self.term
-		{
-			foliage::Term::Boolean(true) => write!(format, "$true"),
-			foliage::Term::Boolean(false) => write!(format, "$false"),
-			foliage::Term::SpecialInteger(foliage::SpecialInteger::Infimum) => write!(format, "c__infimum__"),
-			foliage::Term::SpecialInteger(foliage::SpecialInteger::Supremum) => write!(format, "c__supremum__"),
-			foliage::Term::Integer(value) => match value.is_negative()
+			Term::Boolean(true) => write!(formatter, "$true"),
+			Term::Boolean(false) => write!(formatter, "$false"),
+			Term::SpecialInteger(SpecialInteger::Infimum) => write!(formatter, "c__infimum__"),
+			Term::SpecialInteger(SpecialInteger::Supremum) => write!(formatter, "c__supremum__"),
+			Term::Integer(value) => match value.is_negative()
 			{
-				true => write!(format, "$uminus({})", -value),
-				false => write!(format, "{}", value),
+				true => write!(formatter, "$uminus({})", -value),
+				false => write!(formatter, "{}", value),
 			},
-			foliage::Term::String(_) => panic!("strings not supported in TPTP"),
-			foliage::Term::Variable(variable) =>
-				write!(format, "{:?}", display_variable_declaration(&variable.declaration)),
-			foliage::Term::Function(function) =>
+			Term::String(_) => panic!("strings not supported in TPTP"),
+			Term::Variable(variable) => variable.declaration.display_name(formatter),
+			Term::Function(function) =>
 			{
-				write!(format, "{}", function.declaration.name)?;
+				function.declaration.display_name(formatter)?;
 
-				assert!(function.declaration.arity == function.arguments.len(),
+				assert!(function.declaration.arity() == function.arguments.len(),
 					"function has a different number of arguments than declared (expected {}, got {})",
-					function.declaration.arity, function.arguments.len());
+					function.declaration.arity(), function.arguments.len());
 
 				if function.arguments.len() > 0
 				{
-					write!(format, "{}(", function.declaration.name)?;
+					function.declaration.display_name(formatter)?;
+					write!(formatter, "(")?;
 
 					let mut separator = "";
 
 					for argument in &function.arguments
 					{
-						write!(format, "{}{:?}", separator, display_term(&argument))?;
+						write!(formatter, "{}{:?}", separator, display_term(&argument))?;
 
 						separator = ", ";
 					}
 
-					write!(format, ")")?;
+					write!(formatter, ")")?;
 				}
 
 				Ok(())
 			},
-			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Add, left, right})
-				=> write!(format, "$sum({:?}, {:?})", display_term(left), display_term(right)),
-			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Subtract, left, right})
-				=> write!(format, "$difference({:?}, {:?})", display_term(left), display_term(right)),
-			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Multiply, left, right})
-				=> write!(format, "$product({:?}, {:?})", display_term(left), display_term(right)),
-			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Divide, ..})
-				=> panic!("division not supported with TPTP output"),
-			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Modulo, ..})
-				=> panic!("modulo not supported with TPTP output"),
-			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Exponentiate, ..})
-				=> panic!("exponentiation not supported with TPTP output"),
-			foliage::Term::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::Negative, argument})
-				=> write!(format, "$uminus({:?})", display_term(argument)),
-			foliage::Term::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::AbsoluteValue, ..})
-				=> panic!("absolute value not supported with TPTP output"),
+			Term::BinaryOperation(BinaryOperation{operator: BinaryOperator::Add, left, right}) =>
+				write!(formatter, "$sum({:?}, {:?})", display_term(left), display_term(right)),
+			Term::BinaryOperation(BinaryOperation{operator: BinaryOperator::Subtract, left, right})
+				=>
+				write!(formatter, "$difference({:?}, {:?})", display_term(left),
+					display_term(right)),
+			Term::BinaryOperation(BinaryOperation{operator: BinaryOperator::Multiply, left, right})
+				=>
+				write!(formatter, "$product({:?}, {:?})", display_term(left), display_term(right)),
+			Term::BinaryOperation(BinaryOperation{operator: BinaryOperator::Divide, ..}) =>
+				panic!("division not supported with TPTP output"),
+			Term::BinaryOperation(BinaryOperation{operator: BinaryOperator::Modulo, ..}) =>
+				panic!("modulo not supported with TPTP output"),
+			Term::BinaryOperation(BinaryOperation{operator: BinaryOperator::Exponentiate, ..}) =>
+				panic!("exponentiation not supported with TPTP output"),
+			Term::UnaryOperation(UnaryOperation{operator: UnaryOperator::Negative, argument}) =>
+				write!(formatter, "$uminus({:?})", display_term(argument)),
+			Term::UnaryOperation(UnaryOperation{operator: UnaryOperator::AbsoluteValue, ..}) =>
+				panic!("absolute value not supported with TPTP output"),
 		}
 	}
 }
 
-impl<'a, 'b, C> std::fmt::Display for TermDisplay<'a, 'b, C>
-where
-	C: crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
+impl<'a> std::fmt::Display for TermDisplay<'a>
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", self)
+		write!(formatter, "{:?}", self)
 	}
 }
 
-pub(crate) struct FormulaDisplay<'a, 'b, C>
+pub(crate) struct FormulaDisplay<'a>(&'a crate::Formula);
+
+pub(crate) fn display_formula<'a>(formula: &'a crate::Formula) -> FormulaDisplay<'a>
 {
-	formula: &'a foliage::Formula,
-	context: &'b C,
+	FormulaDisplay(formula)
 }
 
-pub(crate) fn display_formula<'a, 'b, C>(formula: &'a foliage::Formula, context: &'b C)
-	-> FormulaDisplay<'a, 'b, C>
-where
-	C: crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
+impl<'a> std::fmt::Debug for FormulaDisplay<'a>
 {
-	FormulaDisplay
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		formula,
-		context,
-	}
-}
-
-impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C>
-where
-	C: crate::traits::InputConstantDeclarationDomain
-		+ crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
-{
-	// TODO: rename format to formatter
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		let display_variable_declaration = |variable_declaration|
-			display_variable_declaration(variable_declaration, self.context);
-		let display_term = |term| display_term(term, self.context);
-		let display_formula = |formula| display_formula(formula, self.context);
-
 		let mut display_compare = |left, right, notation, integer_operator_name,
 			auxiliary_predicate_name| -> std::fmt::Result
 		{
 			let mut notation = notation;
 			let mut operation_identifier = integer_operator_name;
 
-			let is_left_term_arithmetic = crate::is_term_arithmetic(left, self.context)
+			let is_left_term_arithmetic = crate::is_term_arithmetic(left)
 				.expect("could not determine whether term is arithmetic");
-			let is_right_term_arithmetic = crate::is_term_arithmetic(right, self.context)
+			let is_right_term_arithmetic = crate::is_term_arithmetic(right)
 				.expect("could not determine whether term is arithmetic");
 
 			match (!is_left_term_arithmetic || !is_right_term_arithmetic, auxiliary_predicate_name)
@@ -352,79 +245,77 @@ where
 
 			if notation == crate::OperatorNotation::Prefix
 			{
-				write!(format, "{}(", operation_identifier)?;
+				write!(formatter, "{}(", operation_identifier)?;
 			}
 
 			match is_left_term_arithmetic && !is_right_term_arithmetic
 			{
-				true => write!(format, "f__integer__({})", display_term(left))?,
-				false => write!(format, "{}", display_term(left))?,
+				true => write!(formatter, "f__integer__({})", display_term(left))?,
+				false => write!(formatter, "{}", display_term(left))?,
 			}
 
 			match notation
 			{
-				crate::OperatorNotation::Prefix => write!(format, ", ")?,
-				crate::OperatorNotation::Infix => write!(format, " {} ", operation_identifier)?,
+				crate::OperatorNotation::Prefix => write!(formatter, ", ")?,
+				crate::OperatorNotation::Infix => write!(formatter, " {} ", operation_identifier)?,
 			}
 
 			match is_right_term_arithmetic && !is_left_term_arithmetic
 			{
-				true => write!(format, "f__integer__({})", display_term(right))?,
-				false => write!(format, "{}", display_term(right))?,
+				true => write!(formatter, "f__integer__({})", display_term(right))?,
+				false => write!(formatter, "{}", display_term(right))?,
 			}
 
 			if notation == crate::OperatorNotation::Prefix
 			{
-				write!(format, ")")?;
+				write!(formatter, ")")?;
 			}
 
 			Ok(())
 		};
 
-		match &self.formula
+		use foliage::*;
+
+		match &self.0
 		{
-			foliage::Formula::Exists(exists) =>
+			// TODO: handle cases with 0 parameters properly
+			Formula::Exists(quantified_formula)
+			| Formula::ForAll(quantified_formula) =>
 			{
-				write!(format, "?[")?;
+				let operator_symbol = match &self.0
+				{
+					Formula::Exists(_) => "?",
+					Formula::ForAll(_) => "!",
+					_ => unreachable!(),
+				};
+
+				write!(formatter, "{}[", operator_symbol)?;
 
 				let mut separator = "";
 
-				for parameter in exists.parameters.iter()
+				for parameter in quantified_formula.parameters.iter()
 				{
-					let parameter_domain = self.context.variable_declaration_domain(parameter)
-						.expect("unspecified variable domain");
+					let domain = match parameter.domain()
+					{
+						Ok(domain) => domain,
+						Err(_) => unreachable!(
+							"all variable domains should have been checked at this point"),
+					};
 
-					write!(format, "{}{:?}: {}", separator, display_variable_declaration(parameter),
-						display_domain(parameter_domain))?;
+					write!(formatter, "{}", separator)?;
+					parameter.display_name(formatter)?;
+					write!(formatter, ": {}", display_domain(domain))?;
 
 					separator = ", "
 				}
 
-				write!(format, "]: ({:?})", display_formula(&exists.argument))?;
+				write!(formatter, "]: ({:?})", display_formula(&quantified_formula.argument))?;
 			},
-			foliage::Formula::ForAll(for_all) =>
+			Formula::Not(argument) => write!(formatter, "~{:?}", display_formula(argument))?,
+			// TODO: handle cases with < 2 arguments properly
+			Formula::And(arguments) =>
 			{
-				write!(format, "![")?;
-
-				let mut separator = "";
-
-				for parameter in for_all.parameters.iter()
-				{
-					let parameter_domain = self.context.variable_declaration_domain(parameter)
-						.expect("unspecified variable domain");
-
-					write!(format, "{}{:?}: {}", separator, display_variable_declaration(parameter),
-						display_domain(parameter_domain))?;
-
-					separator = ", "
-				}
-
-				write!(format, "]: ({:?})", display_formula(&for_all.argument))?;
-			},
-			foliage::Formula::Not(argument) => write!(format, "~{:?}", display_formula(argument))?,
-			foliage::Formula::And(arguments) =>
-			{
-				write!(format, "(")?;
+				write!(formatter, "(")?;
 
 				let mut separator = "";
 
@@ -432,16 +323,17 @@ where
 
 				for argument in arguments
 				{
-					write!(format, "{}{:?}", separator, display_formula(argument))?;
+					write!(formatter, "{}{:?}", separator, display_formula(argument))?;
 
 					separator = " & "
 				}
 
-				write!(format, ")")?;
+				write!(formatter, ")")?;
 			},
-			foliage::Formula::Or(arguments) =>
+			// TODO: handle cases with < 2 arguments properly
+			Formula::Or(arguments) =>
 			{
-				write!(format, "(")?;
+				write!(formatter, "(")?;
 
 				let mut separator = "";
 
@@ -449,43 +341,44 @@ where
 
 				for argument in arguments
 				{
-					write!(format, "{}{:?}", separator, display_formula(argument))?;
+					write!(formatter, "{}{:?}", separator, display_formula(argument))?;
 
 					separator = " | "
 				}
 
-				write!(format, ")")?;
+				write!(formatter, ")")?;
 			},
-			foliage::Formula::Implies(foliage::Implies{antecedent, implication, ..})
-				=> write!(format, "({:?} => {:?})", display_formula(antecedent),
+			Formula::Implies(Implies{antecedent, implication, ..}) =>
+				write!(formatter, "({:?} => {:?})", display_formula(antecedent),
 					display_formula(implication))?,
-			foliage::Formula::IfAndOnlyIf(arguments) => match arguments.len()
+			// TODO: handle cases with < 2 arguments properly
+			Formula::IfAndOnlyIf(arguments) => match arguments.len()
 			{
-				0 => write!(format, "$true")?,
+				0 => write!(formatter, "$true")?,
 				_ =>
 				{
-					let mut separator = "";
 					let parentheses_required = arguments.len() > 2;
 
 					let mut argument_iterator = arguments.iter().peekable();
+					let mut separator = "";
 
 					while let Some(argument) = argument_iterator.next()
 					{
 						if let Some(next_argument) = argument_iterator.peek()
 						{
-							write!(format, "{}", separator)?;
+							write!(formatter, "{}", separator)?;
 
 							if parentheses_required
 							{
-								write!(format, "(")?;
+								write!(formatter, "(")?;
 							}
 
-							write!(format, "{:?} <=> {:?}", display_formula(argument),
+							write!(formatter, "{:?} <=> {:?}", display_formula(argument),
 								display_formula(next_argument))?;
 
 							if parentheses_required
 							{
-								write!(format, ")")?;
+								write!(formatter, ")")?;
 							}
 
 							separator = " & ";
@@ -493,58 +386,51 @@ where
 					}
 				},
 			},
-			foliage::Formula::Compare(
-				foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right})
-				=> display_compare(left, right, crate::OperatorNotation::Prefix, "$less",
+			Formula::Compare(Compare{operator: ComparisonOperator::Less, left, right}) =>
+				display_compare(left, right, crate::OperatorNotation::Prefix, "$less",
 					Some("p__less__"))?,
-			foliage::Formula::Compare(
-				foliage::Compare{operator: foliage::ComparisonOperator::LessOrEqual, left, right})
-				=> display_compare(left, right, crate::OperatorNotation::Prefix, "$lesseq",
+			Formula::Compare(Compare{operator: ComparisonOperator::LessOrEqual, left, right}) =>
+				display_compare(left, right, crate::OperatorNotation::Prefix, "$lesseq",
 					Some("p__less_equal__"))?,
-			foliage::Formula::Compare(
-				foliage::Compare{operator: foliage::ComparisonOperator::Greater, left, right})
-				=> display_compare(left, right, crate::OperatorNotation::Prefix, "$greater",
+			Formula::Compare(Compare{operator: ComparisonOperator::Greater, left, right}) =>
+				display_compare(left, right, crate::OperatorNotation::Prefix, "$greater",
 					Some("p__greater__"))?,
-			foliage::Formula::Compare(
-				foliage::Compare{operator: foliage::ComparisonOperator::GreaterOrEqual, left, right})
-				=> display_compare(left, right, crate::OperatorNotation::Prefix, "$greatereq",
+			Formula::Compare(Compare{operator: ComparisonOperator::GreaterOrEqual, left, right}) =>
+				display_compare(left, right, crate::OperatorNotation::Prefix, "$greatereq",
 					Some("p__greater_equal__"))?,
-			foliage::Formula::Compare(
-				foliage::Compare{operator: foliage::ComparisonOperator::Equal, left, right})
-				=> display_compare(left, right, crate::OperatorNotation::Infix, "=", None)?,
-			foliage::Formula::Compare(
-				foliage::Compare{operator: foliage::ComparisonOperator::NotEqual, left, right})
-				=> display_compare(left, right, crate::OperatorNotation::Infix, "!=", None)?,
-			foliage::Formula::Boolean(true) => write!(format, "$true")?,
-			foliage::Formula::Boolean(false) => write!(format, "$false")?,
-			foliage::Formula::Predicate(predicate) =>
+			Formula::Compare(Compare{operator: ComparisonOperator::Equal, left, right}) =>
+				display_compare(left, right, crate::OperatorNotation::Infix, "=", None)?,
+			Formula::Compare(Compare{operator: ComparisonOperator::NotEqual, left, right}) =>
+				display_compare(left, right, crate::OperatorNotation::Infix, "!=", None)?,
+			Formula::Boolean(true) => write!(formatter, "$true")?,
+			Formula::Boolean(false) => write!(formatter, "$false")?,
+			Formula::Predicate(predicate) =>
 			{
-				write!(format, "{}", predicate.declaration.name)?;
+				predicate.declaration.display_name(formatter)?;
 
 				if !predicate.arguments.is_empty()
 				{
-					write!(format, "(")?;
+					write!(formatter, "(")?;
 
 					let mut separator = "";
 
 					for argument in &predicate.arguments
 					{
-						write!(format, "{}", separator)?;
+						write!(formatter, "{}", separator)?;
 
-						let is_argument_arithmetic =
-							crate::is_term_arithmetic(argument, self.context)
-								.expect("could not determine whether term is arithmetic");
+						let is_argument_arithmetic = crate::is_term_arithmetic(argument)
+							.expect("could not determine whether term is arithmetic");
 
 						match is_argument_arithmetic
 						{
-							true => write!(format, "f__integer__({})", display_term(argument))?,
-							false => write!(format, "{}", display_term(argument))?,
+							true => write!(formatter, "f__integer__({})", display_term(argument))?,
+							false => write!(formatter, "{}", display_term(argument))?,
 						}
 
 						separator = ", "
 					}
 
-					write!(format, ")")?;
+					write!(formatter, ")")?;
 				}
 			},
 		}
@@ -553,14 +439,10 @@ where
 	}
 }
 
-impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C>
-where
-	C: crate::traits::InputConstantDeclarationDomain
-		+ crate::traits::VariableDeclarationDomain
-		+ crate::traits::VariableDeclarationID
+impl<'a> std::fmt::Display for FormulaDisplay<'a>
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", self)
+		write!(formatter, "{:?}", self)
 	}
 }

src/problem/proof_direction.rs

@@ -0,0 +1,85 @@
+#[derive(Clone, Copy, Eq, Hash, PartialEq)]
+pub enum ProofDirection
+{
+	Forward,
+	Backward,
+	Both,
+}
+
+impl ProofDirection
+{
+	pub fn requires_forward_proof(&self) -> bool
+	{
+		match self
+		{
+			Self::Forward
+			| Self::Both => true,
+			Self::Backward => false,
+		}
+	}
+
+	pub fn requires_backward_proof(&self) -> bool
+	{
+		match self
+		{
+			Self::Forward => false,
+			Self::Backward
+			| Self::Both => true,
+		}
+	}
+}
+
+impl std::fmt::Debug for ProofDirection
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match self
+		{
+			ProofDirection::Forward => write!(formatter, "forward"),
+			ProofDirection::Backward => write!(formatter, "backward"),
+			ProofDirection::Both => write!(formatter, "both"),
+		}
+	}
+}
+
+impl std::fmt::Display for ProofDirection
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "{:?}", self)
+	}
+}
+
+pub struct InvalidProofDirectionError;
+
+impl std::fmt::Debug for InvalidProofDirectionError
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "invalid proof direction")
+	}
+}
+
+impl std::fmt::Display for InvalidProofDirectionError
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "{:?}", self)
+	}
+}
+
+impl std::str::FromStr for ProofDirection
+{
+	type Err = InvalidProofDirectionError;
+
+	fn from_str(s: &str) -> Result<Self, Self::Err>
+	{
+		match s
+		{
+			"forward" => Ok(ProofDirection::Forward),
+			"backward" => Ok(ProofDirection::Backward),
+			"both" => Ok(ProofDirection::Both),
+			_ => Err(InvalidProofDirectionError),
+		}
+	}
+}

src/problem/section_kind.rs

@@ -0,0 +1,35 @@
+// TODO: remove if possible
+#[derive(Clone, Copy, Eq, Ord, PartialEq, PartialOrd)]
+pub enum SectionKind
+{
+	Axioms,
+	Assumptions,
+	Lemmas,
+	CompletedDefinitions,
+	IntegrityConstraints,
+	Specs,
+}
+
+impl std::fmt::Debug for SectionKind
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match self
+		{
+			Self::CompletedDefinitions => write!(formatter, "completed definition"),
+			Self::IntegrityConstraints => write!(formatter, "integrity constraint"),
+			Self::Axioms => write!(formatter, "axiom"),
+			Self::Assumptions => write!(formatter, "assumption"),
+			Self::Lemmas => write!(formatter, "lemma"),
+			Self::Specs => write!(formatter, "spec"),
+		}
+	}
+}
+
+impl std::fmt::Display for SectionKind
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "{:?}", self)
+	}
+}

src/problem/statement.rs

@@ -0,0 +1,77 @@
+use super::ProofDirection;
+
+#[derive(Eq, PartialEq)]
+pub(crate) enum StatementKind
+{
+	Axiom,
+	Assumption,
+	CompletedDefinition(std::rc::Rc<crate::PredicateDeclaration>),
+	IntegrityConstraint,
+	Lemma(ProofDirection),
+	Spec,
+}
+
+impl std::fmt::Debug for StatementKind
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match self
+		{
+			Self::Axiom => write!(formatter, "axiom"),
+			Self::Assumption => write!(formatter, "assumption"),
+			Self::CompletedDefinition(ref predicate_declaration) =>
+				write!(formatter, "completed definition of {}", predicate_declaration.declaration),
+			Self::IntegrityConstraint => write!(formatter, "integrity constraint"),
+			Self::Lemma(_) => write!(formatter, "lemma"),
+			Self::Spec => write!(formatter, "spec"),
+		}
+	}
+}
+
+impl std::fmt::Display for StatementKind
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "{:?}", self)
+	}
+}
+
+#[derive(Copy, Clone, Eq, PartialEq)]
+pub(crate) enum ProofStatus
+{
+	AssumedProven,
+	Proven,
+	NotProven,
+	Disproven,
+	ToProveNow,
+	ToProveLater,
+	Ignored,
+}
+
+pub(crate) struct Statement
+{
+	pub kind: StatementKind,
+	pub name: Option<String>,
+	pub formula: crate::Formula,
+	pub proof_status: ProofStatus,
+}
+
+impl Statement
+{
+	pub fn new(kind: StatementKind, formula: crate::Formula) -> Self
+	{
+		Self
+		{
+			kind,
+			name: None,
+			formula,
+			proof_status: ProofStatus::ToProveLater,
+		}
+	}
+
+	pub fn with_name(mut self, name: String) -> Self
+	{
+		self.name = Some(name);
+		self
+	}
+}

src/simplify.rs

@@ -0,0 +1,355 @@
+#[derive(Clone, Copy, Eq, PartialEq)]
+enum SimplificationResult
+{
+	Simplified,
+	NotSimplified,
+}
+
+impl SimplificationResult
+{
+	fn or(&self, other: SimplificationResult) -> SimplificationResult
+	{
+		match (self, other)
+		{
+			(SimplificationResult::NotSimplified, SimplificationResult::NotSimplified)
+				=> SimplificationResult::NotSimplified,
+			_ => SimplificationResult::Simplified,
+		}
+	}
+}
+
+fn remove_unnecessary_exists_parameters(formula: &mut crate::Formula)
+	-> Result<SimplificationResult, crate::Error>
+{
+	use crate::{Formula, Term};
+
+	match formula
+	{
+		Formula::And(ref mut arguments)
+		| Formula::IfAndOnlyIf(ref mut arguments)
+		| Formula::Or(ref mut arguments) =>
+		{
+			let mut simplification_result = SimplificationResult::NotSimplified;
+
+			for argument in arguments
+			{
+				simplification_result = simplification_result.or(
+					remove_unnecessary_exists_parameters(argument)?);
+			}
+
+			Ok(simplification_result)
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_)
+		| Formula::Predicate(_) => Ok(SimplificationResult::NotSimplified),
+		Formula::Exists(ref mut quantified_formula) =>
+		{
+			let mut simplification_result =
+				remove_unnecessary_exists_parameters(&mut quantified_formula.argument)?;
+
+			let arguments = match *quantified_formula.argument
+			{
+				Formula::And(ref mut arguments) => arguments,
+				_ => return remove_unnecessary_exists_parameters(&mut quantified_formula.argument),
+			};
+
+			// TODO: do not copy parameters, use std::vec::Vec::retain instead
+			quantified_formula.parameters =
+				std::rc::Rc::new(quantified_formula.parameters.iter().filter_map(
+					|parameter|
+					{
+						let assignment = arguments.iter().enumerate().find_map(
+							|(argument_index, argument)|
+							{
+								let (left, right) = match argument
+								{
+									Formula::Compare(foliage::Compare{
+										operator: foliage::ComparisonOperator::Equal, ref left,
+										ref right})
+										=> (left, right),
+									_ => return None,
+								};
+
+								let assigned_term = match (&**left, &**right)
+								{
+									(Term::Variable(ref variable), right)
+										if variable.declaration == *parameter =>
+										right,
+									(left, Term::Variable(ref variable))
+										if variable.declaration == *parameter =>
+										left,
+									_ => return None,
+								};
+
+								let parameter_domain = match parameter.domain()
+								{
+									Ok(domain) => domain,
+									Err(_) =>
+										unreachable!("all variable domains should be assigned at this point"),
+								};
+
+								let is_parameter_integer =
+									parameter_domain == crate::Domain::Integer;
+
+								let is_assigned_term_arithmetic =
+									match crate::is_term_arithmetic(assigned_term)
+									{
+										Ok(is_term_arithmetic) => is_term_arithmetic,
+										Err(error) => return Some(Err(error)),
+									};
+
+								let is_assignment_narrowing = is_parameter_integer
+									&& !is_assigned_term_arithmetic;
+
+								if crate::term_contains_variable(assigned_term, parameter)
+									|| is_assignment_narrowing
+								{
+									return None;
+								}
+
+								// TODO: avoid copy
+								Some(Ok((argument_index, crate::copy_term(assigned_term))))
+							});
+
+						if let Some(assignment) = assignment
+						{
+							let (assignment_index, assigned_term) = match assignment
+							{
+								Err(error) => return Some(Err(error)),
+								Ok(assignment) => assignment,
+							};
+
+							arguments.remove(assignment_index);
+
+							for argument in arguments.iter_mut()
+							{
+								crate::replace_variable_in_formula_with_term(argument, parameter,
+									&assigned_term);
+							}
+
+							simplification_result = SimplificationResult::Simplified;
+
+							return None;
+						}
+
+						Some(Ok(std::rc::Rc::clone(parameter)))
+					})
+					.collect::<Result<_, _>>()?);
+
+			Ok(simplification_result)
+		}
+		Formula::ForAll(ref mut quantified_formula) =>
+			remove_unnecessary_exists_parameters(&mut quantified_formula.argument),
+		Formula::Implies(ref mut implies) =>
+			remove_unnecessary_exists_parameters(&mut implies.antecedent)
+				.or(remove_unnecessary_exists_parameters(&mut implies.implication)),
+		Formula::Not(ref mut argument) =>
+			remove_unnecessary_exists_parameters(argument),
+	}
+}
+
+fn simplify_quantified_formulas_without_parameters(formula: &mut crate::Formula)
+	-> SimplificationResult
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+		{
+			let mut simplification_result = SimplificationResult::NotSimplified;
+
+			for mut argument in arguments
+			{
+				simplification_result = simplification_result.or(
+					simplify_quantified_formulas_without_parameters(&mut argument));
+			}
+
+			simplification_result
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_)
+		| Formula::Predicate(_) => SimplificationResult::NotSimplified,
+		Formula::Exists(quantified_formula)
+		| Formula::ForAll(quantified_formula) =>
+		{
+			if quantified_formula.parameters.is_empty()
+			{
+				// TODO: remove workaround
+				let mut argument = crate::Formula::false_();
+				std::mem::swap(&mut argument, &mut quantified_formula.argument);
+
+				*formula = argument;
+
+				return SimplificationResult::Simplified;
+			}
+
+			simplify_quantified_formulas_without_parameters(&mut quantified_formula.argument)
+		},
+		Formula::Implies(ref mut implies) =>
+			simplify_quantified_formulas_without_parameters(&mut implies.antecedent)
+				.or(simplify_quantified_formulas_without_parameters(&mut implies.implication)),
+		Formula::Not(ref mut argument) =>
+			simplify_quantified_formulas_without_parameters(argument),
+	}
+}
+
+fn join_nested_quantified_formulas_of_same_type(formula: &mut crate::Formula)
+	-> SimplificationResult
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+		{
+			let mut simplification_result = SimplificationResult::NotSimplified;
+
+			for mut argument in arguments
+			{
+				simplification_result = simplification_result.or(
+					join_nested_quantified_formulas_of_same_type(&mut argument));
+			}
+
+			simplification_result
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_)
+		| Formula::Predicate(_) => SimplificationResult::NotSimplified,
+		Formula::Exists(ref mut quantified_formula) =>
+		{
+			let mut simplification_result =
+				join_nested_quantified_formulas_of_same_type(&mut quantified_formula.argument);
+
+			if let Formula::Exists(ref mut nested_quantified_formula) = *quantified_formula.argument
+			{
+				// TODO: remove workaround
+				let mut argument = crate::Formula::false_();
+				std::mem::swap(&mut argument, &mut nested_quantified_formula.argument);
+
+				let joined_parameters =
+					[&quantified_formula.parameters[..], &nested_quantified_formula.parameters[..]]
+					.concat()
+					.iter()
+					.map(|x| std::rc::Rc::clone(x))
+					.collect::<Vec<_>>();
+
+				quantified_formula.parameters = std::rc::Rc::new(joined_parameters);
+				*quantified_formula.argument = argument;
+
+				simplification_result = SimplificationResult::Simplified;
+			}
+
+			simplification_result
+		},
+		Formula::ForAll(ref mut quantified_formula) =>
+		{
+			let mut simplification_result =
+				join_nested_quantified_formulas_of_same_type(&mut quantified_formula.argument);
+
+			if let Formula::ForAll(ref mut nested_quantified_formula) = *quantified_formula.argument
+			{
+				// TODO: remove workaround
+				let mut argument = crate::Formula::false_();
+				std::mem::swap(&mut argument, &mut nested_quantified_formula.argument);
+
+				let joined_parameters =
+					[&quantified_formula.parameters[..], &nested_quantified_formula.parameters[..]]
+					.concat()
+					.iter()
+					.map(|x| std::rc::Rc::clone(x))
+					.collect::<Vec<_>>();
+
+				quantified_formula.parameters = std::rc::Rc::new(joined_parameters);
+				*quantified_formula.argument = argument;
+
+				simplification_result = SimplificationResult::Simplified;
+			}
+
+			simplification_result
+		},
+		Formula::Implies(ref mut implies) =>
+			join_nested_quantified_formulas_of_same_type(&mut implies.antecedent)
+				.or(join_nested_quantified_formulas_of_same_type(&mut implies.implication)),
+		Formula::Not(ref mut argument) =>
+			join_nested_quantified_formulas_of_same_type(argument),
+	}
+}
+
+fn simplify_trivial_n_ary_formulas(formula: &mut crate::Formula) -> SimplificationResult
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments) if arguments.is_empty() =>
+		{
+			*formula = crate::Formula::true_();
+
+			return SimplificationResult::Simplified;
+		},
+		| Formula::Or(arguments) if arguments.is_empty() =>
+		{
+			*formula = crate::Formula::false_();
+
+			return SimplificationResult::Simplified;
+		},
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+		{
+			if arguments.len() == 1
+			{
+				*formula = arguments.remove(0);
+
+				return SimplificationResult::Simplified;
+			}
+
+			let mut simplification_result = SimplificationResult::NotSimplified;
+
+			for mut argument in arguments
+			{
+				simplification_result = simplification_result.or(
+					simplify_trivial_n_ary_formulas(&mut argument));
+			}
+
+			simplification_result
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_)
+		| Formula::Predicate(_) => SimplificationResult::NotSimplified,
+		Formula::Exists(ref mut quantified_formula)
+		| Formula::ForAll(ref mut quantified_formula) =>
+			simplify_trivial_n_ary_formulas(&mut quantified_formula.argument),
+		Formula::Implies(ref mut implies) =>
+			simplify_trivial_n_ary_formulas(&mut implies.antecedent)
+				.or(simplify_trivial_n_ary_formulas(&mut implies.implication)),
+		Formula::Not(ref mut argument) =>
+			simplify_trivial_n_ary_formulas(argument),
+	}
+}
+
+pub(crate) fn simplify(formula: &mut crate::Formula) -> Result<(), crate::Error>
+{
+	loop
+	{
+		if remove_unnecessary_exists_parameters(formula)? == SimplificationResult::Simplified
+			|| simplify_quantified_formulas_without_parameters(formula)
+				== SimplificationResult::Simplified
+			|| join_nested_quantified_formulas_of_same_type(formula)
+				== SimplificationResult::Simplified
+			|| simplify_trivial_n_ary_formulas(formula) == SimplificationResult::Simplified
+		{
+			continue;
+		}
+
+		break;
+	}
+
+	Ok(())
+}

src/specification.rs

@@ -1,36 +0,0 @@
-/*#[derive(Clone, Copy, Eq, Hash, PartialEq)]
-pub enum ProofDirection
-{
-	Forward,
-	Backward,
-}
-
-#[derive(Eq, Hash, PartialEq)]
-pub enum CompletionTarget
-{
-	Predicate(std::rc::Rc<foliage::PredicateDeclaration>),
-	Constraint,
-}
-
-pub struct CompletionFormula
-{
-	pub target: CompletionTarget,
-	pub formula: foliage::Formula,
-}
-
-pub struct Lemma
-{
-	pub direction: Option<ProofDirection>,
-	pub formula: foliage::Formula,
-}
-
-pub struct Specification
-{
-	pub axioms: foliage::Formulas,
-	pub lemmas: Vec<Lemma>,
-	pub assumptions: foliage::Formulas,
-	pub assertions: foliage::Formulas,
-
-	pub input_constants: foliage::FunctionDeclarations,
-	pub input_predicates: foliage::PredicateDeclarations,
-}*/

src/traits.rs

@@ -1,23 +0,0 @@
-pub(crate) trait InputConstantDeclarationDomain
-{
-	fn input_constant_declaration_domain(&self,
-		declaration: &std::rc::Rc<foliage::FunctionDeclaration>) -> crate::Domain;
-}
-
-pub(crate) trait AssignVariableDeclarationDomain
-{
-	fn assign_variable_declaration_domain(&self,
-		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>, domain: crate::Domain);
-}
-
-pub(crate) trait VariableDeclarationDomain
-{
-	fn variable_declaration_domain(&self,
-		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>) -> Option<crate::Domain>;
-}
-
-pub(crate) trait VariableDeclarationID
-{
-	fn variable_declaration_id(&self,
-		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>) -> usize;
-}

src/translate/common/choose_value_in_term.rs

@@ -1,19 +1,18 @@
-pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
-	variable_declaration: std::rc::Rc<foliage::VariableDeclaration>)
-	-> foliage::Formula
+pub(crate) fn choose_value_in_primitive(term: Box<crate::Term>,
+	variable_declaration: std::rc::Rc<crate::VariableDeclaration>)
+	-> crate::Formula
 {
-	let variable = foliage::Term::variable(variable_declaration);
+	let variable = crate::Term::variable(variable_declaration);
 
-	foliage::Formula::equal(Box::new(variable), term)
+	crate::Formula::equal(Box::new(variable), term)
 }
 
 pub(crate) fn choose_value_in_term<C>(term: &clingo::ast::Term,
-	variable_declaration: std::rc::Rc<foliage::VariableDeclaration>, context: &C,
-	variable_declaration_stack: &foliage::VariableDeclarationStackLayer)
-	-> Result<foliage::Formula, crate::Error>
+	variable_declaration: std::rc::Rc<crate::VariableDeclaration>, context: &C,
+	variable_declaration_stack: &crate::VariableDeclarationStackLayer)
+	-> Result<crate::Formula, crate::Error>
 where
-	C: foliage::FindOrCreateFunctionDeclaration
-		+ crate::traits::AssignVariableDeclarationDomain
+	C: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>,
 {
 	match term.term_type()
 	{
@@ -21,15 +20,15 @@ where
 			.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
 		{
 			clingo::SymbolType::Number => Ok(choose_value_in_primitive(
-				Box::new(foliage::Term::integer(symbol.number()
+				Box::new(crate::Term::integer(symbol.number()
 					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?)),
 				variable_declaration)),
 			clingo::SymbolType::Infimum => Ok(choose_value_in_primitive(
-				Box::new(foliage::Term::infimum()), variable_declaration)),
+				Box::new(crate::Term::infimum()), variable_declaration)),
 			clingo::SymbolType::Supremum => Ok(choose_value_in_primitive(
-				Box::new(foliage::Term::supremum()), variable_declaration)),
+				Box::new(crate::Term::supremum()), variable_declaration)),
 			clingo::SymbolType::String => Ok(choose_value_in_primitive(
-				Box::new(foliage::Term::string(symbol.string()
+				Box::new(crate::Term::string(symbol.string()
 					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
 					.to_string())),
 				variable_declaration)),
@@ -51,7 +50,7 @@ where
 
 				let constant_declaration =
 					context.find_or_create_function_declaration(constant_name, 0);
-				let function = foliage::Term::function(constant_declaration, vec![]);
+				let function = crate::Term::function(constant_declaration, vec![]);
 
 				Ok(choose_value_in_primitive(Box::new(function), variable_declaration))
 			}
@@ -60,14 +59,14 @@ where
 		{
 			let other_variable_declaration = match variable_name
 			{
-				// TODO: check
 				// Every occurrence of anonymous variables is treated as if it introduced a fresh
 				// variable declaration
 				"_" => variable_declaration_stack.free_variable_declarations_do_mut(
 					|free_variable_declarations|
 					{
+						// TODO: check domain type
 						let variable_declaration = std::rc::Rc::new(
-							foliage::VariableDeclaration::new("_".to_owned()));
+							crate::VariableDeclaration::new_generated(crate::Domain::Program));
 
 						free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration));
 
@@ -75,9 +74,7 @@ where
 					}),
 				_ => variable_declaration_stack.find_or_create(variable_name),
 			};
-			context.assign_variable_declaration_domain(&other_variable_declaration,
-				crate::Domain::Program);
-			let other_variable = foliage::Term::variable(other_variable_declaration);
+			let other_variable = crate::Term::variable(other_variable_declaration);
 
 			Ok(choose_value_in_primitive(Box::new(other_variable), variable_declaration))
 		},
@@ -92,26 +89,21 @@ where
 				| foliage::BinaryOperator::Multiply
 					=>
 				{
-					let parameters = (0..2).map(|_|
-						{
-							let variable_declaration = std::rc::Rc::new(
-								foliage::VariableDeclaration::new("<anonymous>".to_string()));
-							context.assign_variable_declaration_domain(&variable_declaration,
-								crate::Domain::Integer);
-							variable_declaration
-						})
-						.collect::<foliage::VariableDeclarations>();
+					let parameters = (0..2).map(
+						|_| std::rc::Rc::new(crate::VariableDeclaration::new_generated(
+							crate::Domain::Integer)))
+						.collect::<crate::VariableDeclarations>();
 					let parameters = std::rc::Rc::new(parameters);
 
 					let parameter_1 = &parameters[0];
 					let parameter_2 = &parameters[1];
 
-					let translated_binary_operation = foliage::Term::binary_operation(operator,
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(&parameter_1))),
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(&parameter_2))));
+					let translated_binary_operation = crate::Term::binary_operation(operator,
+						Box::new(crate::Term::variable(std::rc::Rc::clone(&parameter_1))),
+						Box::new(crate::Term::variable(std::rc::Rc::clone(&parameter_2))));
 
-					let equals = foliage::Formula::equal(
-						Box::new(foliage::Term::variable(variable_declaration)),
+					let equals = crate::Formula::equal(
+						Box::new(crate::Term::variable(variable_declaration)),
 						Box::new(translated_binary_operation));
 
 					let choose_value_from_left_argument = choose_value_in_term(
@@ -122,24 +114,19 @@ where
 						binary_operation.right(), std::rc::Rc::clone(&parameter_2), context,
 							variable_declaration_stack)?;
 
-					let and = foliage::Formula::And(vec![equals, choose_value_from_left_argument,
+					let and = crate::Formula::And(vec![equals, choose_value_from_left_argument,
 						choose_value_from_right_argument]);
 
-					Ok(foliage::Formula::exists(parameters, Box::new(and)))
+					Ok(crate::Formula::exists(parameters, Box::new(and)))
 				},
 				foliage::BinaryOperator::Divide
 				| foliage::BinaryOperator::Modulo
 					=>
 				{
-					let parameters = (0..4).map(|_|
-						{
-							let variable_declaration = std::rc::Rc::new(
-								foliage::VariableDeclaration::new("<anonymous>".to_string()));
-							context.assign_variable_declaration_domain(&variable_declaration,
-								crate::Domain::Integer);
-							variable_declaration
-						})
-						.collect::<foliage::VariableDeclarations>();
+					let parameters = (0..4).map(
+						|_| std::rc::Rc::new(crate::VariableDeclaration::new_generated(
+							crate::Domain::Integer)))
+						.collect::<crate::VariableDeclarations>();
 					let parameters = std::rc::Rc::new(parameters);
 
 					let parameter_i = &parameters[0];
@@ -147,43 +134,43 @@ where
 					let parameter_q = &parameters[2];
 					let parameter_r = &parameters[3];
 
-					let j_times_q = foliage::Term::multiply(
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))),
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q))));
+					let j_times_q = crate::Term::multiply(
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_j))),
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_q))));
 
-					let j_times_q_plus_r = foliage::Term::add(Box::new(j_times_q),
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))));
+					let j_times_q_plus_r = crate::Term::add(Box::new(j_times_q),
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_r))));
 
-					let i_equals_j_times_q_plus_r = foliage::Formula::equal(
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))),
+					let i_equals_j_times_q_plus_r = crate::Formula::equal(
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_i))),
 						Box::new(j_times_q_plus_r));
 
 					let choose_i_in_t1 = choose_value_in_term(binary_operation.left(),
 						std::rc::Rc::clone(parameter_i), context, variable_declaration_stack)?;
 
-					let choose_i_in_t2 = choose_value_in_term(binary_operation.left(),
+					let choose_j_in_t2 = choose_value_in_term(binary_operation.right(),
 						std::rc::Rc::clone(parameter_j), context, variable_declaration_stack)?;
 
-					let j_not_equal_to_0 = foliage::Formula::not_equal(
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))),
-						Box::new(foliage::Term::integer(0)));
+					let j_not_equal_to_0 = crate::Formula::not_equal(
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_j))),
+						Box::new(crate::Term::integer(0)));
 
-					let r_greater_or_equal_to_0 = foliage::Formula::greater_or_equal(
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))),
-						Box::new(foliage::Term::integer(0)));
+					let r_greater_or_equal_to_0 = crate::Formula::greater_or_equal(
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_r))),
+						Box::new(crate::Term::integer(0)));
 
-					let r_less_than_q = foliage::Formula::less(
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))),
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q))));
+					let r_less_than_q = crate::Formula::less(
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_r))),
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_q))));
 
-					let z_equal_to_q = foliage::Formula::equal(
+					let z_equal_to_q = crate::Formula::equal(
 						Box::new(
-							foliage::Term::variable(std::rc::Rc::clone(&variable_declaration))),
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_q))));
+							crate::Term::variable(std::rc::Rc::clone(&variable_declaration))),
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_q))));
 
-					let z_equal_to_r = foliage::Formula::equal(
-						Box::new(foliage::Term::variable(variable_declaration)),
-						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_r))));
+					let z_equal_to_r = crate::Formula::equal(
+						Box::new(crate::Term::variable(variable_declaration)),
+						Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_r))));
 
 					let last_argument = match operator
 					{
@@ -192,11 +179,11 @@ where
 						_ => return Err(crate::Error::new_logic("unreachable code")),
 					};
 
-					let and = foliage::Formula::and(vec![i_equals_j_times_q_plus_r, choose_i_in_t1,
-						choose_i_in_t2, j_not_equal_to_0, r_greater_or_equal_to_0, r_less_than_q,
+					let and = crate::Formula::and(vec![i_equals_j_times_q_plus_r, choose_i_in_t1,
+						choose_j_in_t2, j_not_equal_to_0, r_greater_or_equal_to_0, r_less_than_q,
 						last_argument]);
 
-					Ok(foliage::Formula::exists(parameters, Box::new(and)))
+					Ok(crate::Formula::exists(parameters, Box::new(and)))
 				},
 				foliage::BinaryOperator::Exponentiate =>
 					Err(crate::Error::new_unsupported_language_feature("exponentiation")),
@@ -210,41 +197,34 @@ where
 					return Err(crate::Error::new_unsupported_language_feature("absolute value")),
 				clingo::ast::UnaryOperator::Minus =>
 				{
-					let parameter_z_prime = std::rc::Rc::new(foliage::VariableDeclaration::new(
-						"<anonymous>".to_string()));
-					context.assign_variable_declaration_domain(&parameter_z_prime,
-						crate::Domain::Integer);
+					let parameter_z_prime = std::rc::Rc::new(
+						crate::VariableDeclaration::new_generated(crate::Domain::Integer));
 
-					let negative_z_prime = foliage::Term::negative(Box::new(
-						foliage::Term::variable(std::rc::Rc::clone(&parameter_z_prime))));
-					let equals = foliage::Formula::equal(
-						Box::new(foliage::Term::variable(variable_declaration)),
+					let negative_z_prime = crate::Term::negative(Box::new(
+						crate::Term::variable(std::rc::Rc::clone(&parameter_z_prime))));
+					let equals = crate::Formula::equal(
+						Box::new(crate::Term::variable(variable_declaration)),
 						Box::new(negative_z_prime));
 
 					let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(),
 						std::rc::Rc::clone(&parameter_z_prime), context,
 						variable_declaration_stack)?;
 
-					let and = foliage::Formula::and(vec![equals, choose_z_prime_in_t_prime]);
+					let and = crate::Formula::and(vec![equals, choose_z_prime_in_t_prime]);
 
 					let parameters = std::rc::Rc::new(vec![parameter_z_prime]);
 
-					Ok(foliage::Formula::exists(parameters, Box::new(and)))
+					Ok(crate::Formula::exists(parameters, Box::new(and)))
 				},
 				_ => Err(crate::Error::new_not_yet_implemented("todo")),
 			}
 		},
 		clingo::ast::TermType::Interval(interval) =>
 		{
-			let parameters = (0..3).map(|_|
-				{
-					let variable_declaration = std::rc::Rc::new(
-						foliage::VariableDeclaration::new("<anonymous>".to_string()));
-					context.assign_variable_declaration_domain(&variable_declaration,
-						crate::Domain::Integer);
-					variable_declaration
-				})
-				.collect::<foliage::VariableDeclarations>();
+			let parameters = (0..3).map(
+				|_| std::rc::Rc::new(crate::VariableDeclaration::new_generated(
+					crate::Domain::Integer)))
+				.collect::<crate::VariableDeclarations>();
 			let parameters = std::rc::Rc::new(parameters);
 
 			let parameter_i = &parameters[0];
@@ -257,22 +237,22 @@ where
 			let choose_j_in_t_2 = choose_value_in_term(interval.right(),
 				std::rc::Rc::clone(parameter_j), context, variable_declaration_stack)?;
 
-			let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal(
-				Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_i))),
-				Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k))));
+			let i_less_than_or_equal_to_k = crate::Formula::less_or_equal(
+				Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_i))),
+				Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_k))));
 
-			let k_less_than_or_equal_to_j = foliage::Formula::less_or_equal(
-				Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k))),
-				Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))));
+			let k_less_than_or_equal_to_j = crate::Formula::less_or_equal(
+				Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_k))),
+				Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_j))));
 
-			let z_equals_k = foliage::Formula::equal(
-				Box::new(foliage::Term::variable(variable_declaration)),
-				Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_k))));
+			let z_equals_k = crate::Formula::equal(
+				Box::new(crate::Term::variable(variable_declaration)),
+				Box::new(crate::Term::variable(std::rc::Rc::clone(parameter_k))));
 
-			let and = foliage::Formula::and(vec![choose_i_in_t_1, choose_j_in_t_2,
+			let and = crate::Formula::and(vec![choose_i_in_t_1, choose_j_in_t_2,
 				i_less_than_or_equal_to_k, k_less_than_or_equal_to_j, z_equals_k]);
 
-			Ok(foliage::Formula::exists(parameters, Box::new(and)))
+			Ok(crate::Formula::exists(parameters, Box::new(and)))
 		},
 		clingo::ast::TermType::Function(_) =>
 			Err(crate::Error::new_unsupported_language_feature("symbolic functions")),

src/translate/verify_properties.rs

@@ -3,20 +3,21 @@ mod translate_body;
 
 use head_type::*;
 use translate_body::*;
-use crate::traits::AssignVariableDeclarationDomain as _;
+
+use foliage::flavor::{PredicateDeclaration as _};
 
 struct PredicateDefinitions
 {
-	pub parameters: std::rc::Rc<foliage::VariableDeclarations>,
-	pub definitions: Vec<crate::ScopedFormula>,
+	pub parameters: std::rc::Rc<crate::VariableDeclarations>,
+	pub definitions: Vec<crate::OpenFormula>,
 }
 
 type Definitions =
-	std::collections::BTreeMap::<std::rc::Rc<foliage::PredicateDeclaration>, PredicateDefinitions>;
+	std::collections::BTreeMap::<std::rc::Rc<crate::PredicateDeclaration>, PredicateDefinitions>;
 
 pub(crate) struct Translator<'p>
 {
-	problem: &'p mut crate::Problem,// TODO: refactor
+	problem: &'p mut crate::Problem,
 	definitions: Definitions,
 }
 
@@ -64,7 +65,7 @@ impl<'p> Translator<'p>
 
 	pub fn translate<P>(&mut self, program_path: P) -> Result<(), crate::Error>
 	where
-		P: AsRef<std::path::Path>
+		P: AsRef<std::path::Path>,
 	{
 		// Read input program
 		let program = std::fs::read_to_string(program_path.as_ref())
@@ -76,20 +77,7 @@ impl<'p> Translator<'p>
 
 		log::info!("read input program “{}”", program_path.as_ref().display());
 
-		// TODO: reimplement
-		/*
-		for (predicate_declaration, predicate_definitions) in self.definitions.iter()
-		{
-			for definition in predicate_definitions.definitions.iter()
-			{
-				log::debug!("definition({}/{}): {}.", predicate_declaration.name,
-					predicate_declaration.arity,
-					foliage::format::display_formula(&definition.formula, self.problem));
-			}
-		}*/
-
-		let completed_definition = |predicate_declaration, definitions: &mut Definitions,
-			problem: &crate::Problem|
+		let completed_definition = |predicate_declaration, definitions: &mut Definitions|
 		{
 			match definitions.remove(predicate_declaration)
 			{
@@ -99,77 +87,73 @@ impl<'p> Translator<'p>
 					let or_arguments = predicate_definitions.definitions.into_iter()
 						.map(|x| crate::existential_closure(x))
 						.collect::<Vec<_>>();
-					let or = foliage::Formula::or(or_arguments);
+					let or = crate::Formula::or(or_arguments);
 
 					let head_arguments = predicate_definitions.parameters.iter()
-						.map(|x| foliage::Term::variable(std::rc::Rc::clone(x)))
+						.map(|x| crate::Term::variable(std::rc::Rc::clone(x)))
 						.collect::<Vec<_>>();
 
-					let head_predicate = foliage::Formula::predicate(
+					let head_predicate = crate::Formula::predicate(
 						std::rc::Rc::clone(predicate_declaration), head_arguments);
 
 					let completed_definition =
-						foliage::Formula::if_and_only_if(vec![head_predicate, or]);
+						crate::Formula::if_and_only_if(vec![head_predicate, or]);
 
-					let scoped_formula = crate::ScopedFormula
+					let open_formula = crate::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 =>
 				{
-					let parameters = std::rc::Rc::new((0..predicate_declaration.arity)
-						.map(|_|
-						{
-							let variable_declaration = std::rc::Rc::new(
-								foliage::VariableDeclaration::new("<anonymous>".to_string()));
-							problem.assign_variable_declaration_domain(&variable_declaration,
-								crate::Domain::Program);
-							variable_declaration
-						})
+					let parameters = std::rc::Rc::new((0..predicate_declaration.arity()).map(
+						|_| std::rc::Rc::new(crate::VariableDeclaration::new_generated(
+							crate::Domain::Program)))
 						.collect::<Vec<_>>());
 
 					let head_arguments = parameters.iter()
-						.map(|x| foliage::Term::variable(std::rc::Rc::clone(x)))
+						.map(|x| crate::Term::variable(std::rc::Rc::clone(x)))
 						.collect();
 
-					let head_predicate = foliage::Formula::predicate(
+					let head_predicate = crate::Formula::predicate(
 						std::rc::Rc::clone(predicate_declaration), head_arguments);
 
-					let not = foliage::Formula::not(Box::new(head_predicate));
+					let not = crate::Formula::not(Box::new(head_predicate));
 
-					let scoped_formula = crate::ScopedFormula
+					let open_formula = crate::OpenFormula
 					{
 						free_variable_declarations: parameters,
 						formula: not,
 					};
 
-					crate::universal_closure(scoped_formula)
+					crate::universal_closure(open_formula)
 				},
 			}
 		};
 
-		for predicate_declaration in self.problem.predicate_declarations.borrow().iter()
+		for predicate_declaration in self.problem.predicate_declarations.borrow_mut().iter()
 		{
-			// Don’t perform completion for input predicates
-			if self.problem.input_predicate_declarations.borrow().contains(predicate_declaration)
+			// Don’t perform completion for input predicates and built-in predicates
+			if *predicate_declaration.is_input.borrow() || predicate_declaration.is_built_in()
 			{
 				continue;
 			}
 
-			let completed_definition =
-				completed_definition(predicate_declaration, &mut self.definitions, self.problem);
+			let statement_kind = crate::problem::StatementKind::CompletedDefinition(
+				std::rc::Rc::clone(&predicate_declaration));
 
-			let statement = crate::problem::Statement::new(
-				crate::problem::StatementKind::Program, completed_definition)
-				.with_name(format!("completed_definition_{}_{}", predicate_declaration.name,
-					predicate_declaration.arity))
-				.with_description(format!("completed definition of {}/{}",
-						predicate_declaration.name, predicate_declaration.arity));
+			let completed_definition = completed_definition(predicate_declaration,
+				&mut self.definitions);
+
+			let statement_name =
+				format!("completed_definition_{}", predicate_declaration.tptp_statement_name());
+
+			let statement = crate::problem::Statement::new(statement_kind, completed_definition)
+				.with_name(statement_name);
 
 			self.problem.add_statement(crate::problem::SectionKind::CompletedDefinitions,
 				statement);
@@ -190,15 +174,10 @@ impl<'p> Translator<'p>
 			{
 				if !self.definitions.contains_key(&head_atom.predicate_declaration)
 				{
-					let parameters = std::rc::Rc::new((0..head_atom.predicate_declaration.arity)
-						.map(|_|
-						{
-							let variable_declaration = std::rc::Rc::new(
-								foliage::VariableDeclaration::new("<anonymous>".to_string()));
-							self.problem.assign_variable_declaration_domain(&variable_declaration,
-								crate::Domain::Program);
-							variable_declaration
-						})
+					let parameters = std::rc::Rc::new((0..head_atom.predicate_declaration.arity())
+						.map(
+							|_| std::rc::Rc::new(crate::VariableDeclaration::new_generated(
+								crate::Domain::Program)))
 						.collect());
 
 					self.definitions.insert(
@@ -217,12 +196,24 @@ impl<'p> Translator<'p>
 				let parameters = std::rc::Rc::clone(&predicate_definitions.parameters);
 				let free_variable_declarations = std::cell::RefCell::new(vec![]);
 				let free_layer =
-					foliage::VariableDeclarationStackLayer::Free(free_variable_declarations);
+					crate::VariableDeclarationStackLayer::Free(free_variable_declarations);
 				let parameters_layer =
-					foliage::VariableDeclarationStackLayer::bound(&free_layer, parameters);
+					crate::VariableDeclarationStackLayer::bound(&free_layer, parameters);
+
+				let mut predicate_dependencies =
+					head_atom.predicate_declaration.dependencies.borrow_mut();
+
+				if predicate_dependencies.is_none()
+				{
+					*predicate_dependencies = Some(crate::PredicateDependencies::new());
+				}
+
+				// The conditional assignment above ensures unwrapping to be safe
+				let mut dependencies = predicate_dependencies.as_mut().unwrap();
 
 				let mut definition_arguments =
-					translate_body(rule.body(), self.problem, &parameters_layer)?;
+					translate_body(rule.body(), self.problem, &parameters_layer,
+						&mut Some(&mut dependencies))?;
 
 				// TODO: refactor
 				assert_eq!(predicate_definitions.parameters.len(), head_atom.arguments.len());
@@ -230,10 +221,10 @@ impl<'p> Translator<'p>
 				if let HeadType::ChoiceWithSingleAtom(_) = head_type
 				{
 					let head_arguments = predicate_definitions.parameters.iter()
-						.map(|x| foliage::Term::variable(std::rc::Rc::clone(x)))
+						.map(|x| crate::Term::variable(std::rc::Rc::clone(x)))
 						.collect::<Vec<_>>();
 
-					let head_predicate = foliage::Formula::predicate(
+					let head_predicate = crate::Formula::predicate(
 						std::rc::Rc::clone(&head_atom.predicate_declaration), head_arguments);
 
 					definition_arguments.push(head_predicate);
@@ -255,7 +246,7 @@ impl<'p> Translator<'p>
 				// TODO: refactor
 				let free_variable_declarations = match free_layer
 				{
-					foliage::VariableDeclarationStackLayer::Free(free_variable_declarations)
+					crate::VariableDeclarationStackLayer::Free(free_variable_declarations)
 						=> free_variable_declarations.into_inner(),
 					_ => unreachable!(),
 				};
@@ -263,67 +254,53 @@ impl<'p> Translator<'p>
 				let definition = match definition_arguments.len()
 				{
 					1 => definition_arguments.pop().unwrap(),
-					0 => foliage::Formula::true_(),
-					_ => foliage::Formula::and(definition_arguments),
+					0 => crate::Formula::true_(),
+					_ => crate::Formula::and(definition_arguments),
 				};
 
-				let definition = crate::ScopedFormula
+				let definition = crate::OpenFormula
 				{
 					free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
 					formula: definition,
 				};
 
-				// TODO: refactor
-				// TODO: reimplement
-				/*
-				log::debug!("translated rule with single atom in head: {}",
-					foliage::format::display_formula(&definition.formula, self.problem));
-				*/
-
 				predicate_definitions.definitions.push(definition);
 			},
 			HeadType::IntegrityConstraint =>
 			{
 				let free_variable_declarations = std::cell::RefCell::new(vec![]);
 				let free_layer =
-					foliage::VariableDeclarationStackLayer::Free(free_variable_declarations);
+					crate::VariableDeclarationStackLayer::Free(free_variable_declarations);
 
-				let mut arguments = translate_body(rule.body(), self.problem, &free_layer)?;
+				let mut arguments = translate_body(rule.body(), self.problem, &free_layer,
+					&mut None)?;
 
 				// TODO: refactor
 				let free_variable_declarations = match free_layer
 				{
-					foliage::VariableDeclarationStackLayer::Free(free_variable_declarations)
+					crate::VariableDeclarationStackLayer::Free(free_variable_declarations)
 						=> free_variable_declarations.into_inner(),
 					_ => unreachable!(),
 				};
 
 				let formula = match arguments.len()
 				{
-					1 => foliage::Formula::not(Box::new(arguments.pop().unwrap())),
-					0 => foliage::Formula::false_(),
-					_ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))),
+					1 => crate::Formula::not(Box::new(arguments.pop().unwrap())),
+					0 => crate::Formula::false_(),
+					_ => crate::Formula::not(Box::new(crate::Formula::and(arguments))),
 				};
 
-				let scoped_formula = crate::ScopedFormula
+				let open_formula = crate::OpenFormula
 				{
 					free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
 					formula,
 				};
 
-				let integrity_constraint = crate::universal_closure(scoped_formula);
-
-				// TODO: refactor
-				// TODO: reimplement
-				/*
-				log::debug!("translated integrity constraint: {}",
-					foliage::format::display_formula(&integrity_constraint, self.problem));
-				*/
+				let integrity_constraint = crate::universal_closure(open_formula);
 
 				let statement = crate::problem::Statement::new(
-					crate::problem::StatementKind::Program, integrity_constraint)
-					.with_name("integrity_constraint".to_string())
-					.with_description("integrity constraint".to_string());
+					crate::problem::StatementKind::IntegrityConstraint, integrity_constraint)
+					.with_name("integrity_constraint".to_string());
 
 				self.problem.add_statement(crate::problem::SectionKind::IntegrityConstraints,
 					statement);

src/translate/verify_properties/context.rs

@@ -1,195 +0,0 @@
-/*pub(crate) struct Definitions
-{
-	pub head_atom_parameters: std::rc::Rc<foliage::VariableDeclarations>,
-	pub definitions: Vec<crate::ScopedFormula>,
-}
-
-type VariableDeclarationDomains
-	= std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>;
-
-type VariableDeclarationIDs
-	= std::collections::BTreeMap::<std::rc::Rc<foliage::VariableDeclaration>, usize>;
-
-pub(crate) struct Context
-{
-	pub definitions: std::cell::RefCell<std::collections::BTreeMap::<
-		std::rc::Rc<foliage::PredicateDeclaration>, Definitions>>,
-	pub integrity_constraints: std::cell::RefCell<foliage::Formulas>,
-
-	pub input_constant_declaration_domains: std::cell::RefCell<
-		crate::InputConstantDeclarationDomains>,
-	pub input_predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
-
-	pub function_declarations: std::cell::RefCell<foliage::FunctionDeclarations>,
-	pub predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
-	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>,
-}
-
-impl Context
-{
-	pub(crate) fn new() -> Self
-	{
-		Self
-		{
-			definitions: std::cell::RefCell::new(std::collections::BTreeMap::<_, _>::new()),
-			integrity_constraints: std::cell::RefCell::new(vec![]),
-
-			input_constant_declaration_domains:
-				std::cell::RefCell::new(crate::InputConstantDeclarationDomains::new()),
-			input_predicate_declarations:
-				std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
-
-			function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()),
-			predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
-			variable_declaration_domains:
-				std::cell::RefCell::new(VariableDeclarationDomains::new()),
-			program_variable_declaration_ids:
-				std::cell::RefCell::new(VariableDeclarationIDs::new()),
-			integer_variable_declaration_ids:
-				std::cell::RefCell::new(VariableDeclarationIDs::new()),
-		}
-	}
-}
-
-impl crate::traits::InputConstantDeclarationDomain for Context
-{
-	fn input_constant_declaration_domain(&self,
-		declaration: &std::rc::Rc<foliage::FunctionDeclaration>) -> crate::Domain
-	{
-		let input_constant_declaration_domains = self.input_constant_declaration_domains.borrow();
-
-		// Assume the program domain if not specified otherwise
-		input_constant_declaration_domains.get(declaration).map(|x| *x)
-			.unwrap_or(crate::Domain::Program)
-	}
-}
-
-impl foliage::FindOrCreateFunctionDeclaration for Context
-{
-	fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<foliage::FunctionDeclaration>
-	{
-		let mut function_declarations = self.function_declarations.borrow_mut();
-
-		match function_declarations.iter()
-			.find(|x| x.name == name && x.arity == arity)
-		{
-			Some(value) => std::rc::Rc::clone(value),
-			None =>
-			{
-				let declaration = std::rc::Rc::new(foliage::FunctionDeclaration::new(
-					name.to_string(), arity));
-
-				function_declarations.insert(std::rc::Rc::clone(&declaration));
-
-				log::debug!("new function declaration: {}/{}", name, arity);
-
-				declaration
-			},
-		}
-	}
-}
-
-impl foliage::FindOrCreatePredicateDeclaration for Context
-{
-	fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<foliage::PredicateDeclaration>
-	{
-		let mut predicate_declarations = self.predicate_declarations.borrow_mut();
-
-		match predicate_declarations.iter()
-			.find(|x| x.name == name && x.arity == arity)
-		{
-			Some(value) => std::rc::Rc::clone(value),
-			None =>
-			{
-				let declaration = std::rc::Rc::new(foliage::PredicateDeclaration::new(
-					name.to_string(), arity));
-
-				predicate_declarations.insert(std::rc::Rc::clone(&declaration));
-
-				log::debug!("new predicate declaration: {}/{}", name, arity);
-
-				declaration
-			},
-		}
-	}
-}
-
-impl crate::traits::AssignVariableDeclarationDomain for Context
-{
-	fn assign_variable_declaration_domain(&self,
-		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>, domain: crate::Domain)
-	{
-		let mut variable_declaration_domains = self.variable_declaration_domains.borrow_mut();
-
-		match variable_declaration_domains.get(variable_declaration)
-		{
-			Some(current_domain) => assert_eq!(*current_domain, domain,
-				"inconsistent variable declaration domain"),
-			None =>
-			{
-				variable_declaration_domains
-					.insert(std::rc::Rc::clone(variable_declaration).into(), domain);
-			},
-		}
-	}
-}
-
-impl crate::traits::VariableDeclarationDomain for Context
-{
-	fn variable_declaration_domain(&self,
-		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-		-> Option<crate::Domain>
-	{
-		let variable_declaration_domains = self.variable_declaration_domains.borrow();
-
-		variable_declaration_domains.get(variable_declaration)
-			.map(|x| *x)
-	}
-}
-
-impl crate::traits::VariableDeclarationID for Context
-{
-	fn variable_declaration_id(&self,
-		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-		-> usize
-	{
-		use crate::traits::VariableDeclarationDomain;
-
-		let mut variable_declaration_ids = match self.variable_declaration_domain(
-			variable_declaration)
-		{
-			Some(crate::Domain::Program) => self.program_variable_declaration_ids.borrow_mut(),
-			Some(crate::Domain::Integer) => self.integer_variable_declaration_ids.borrow_mut(),
-			None => panic!("all variables should be declared at this point"),
-		};
-
-		match variable_declaration_ids.get(variable_declaration)
-		{
-			Some(id) =>
-			{
-				*id
-			}
-			None =>
-			{
-				let id = variable_declaration_ids.len();
-				variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id);
-				id
-			},
-		}
-	}
-}
-
-impl foliage::format::Format for Context
-{
-	fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter,
-		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
-		-> std::fmt::Result
-	{
-		crate::output::human_readable::display_variable_declaration(self, formatter,
-			variable_declaration)
-	}
-}*/

src/translate/verify_properties/head_type.rs

@@ -1,6 +1,6 @@
 pub(crate) struct HeadAtom<'a>
 {
-	pub predicate_declaration: std::rc::Rc<foliage::PredicateDeclaration>,
+	pub predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>,
 	pub arguments: &'a [clingo::ast::Term<'a>],
 }
 
@@ -15,7 +15,7 @@ pub(crate) enum HeadType<'a>
 pub(crate) fn determine_head_type<'a, C>(head_literal: &'a clingo::ast::HeadLiteral, context: &C)
 	-> Result<HeadType<'a>, crate::Error>
 where
-	C: foliage::FindOrCreatePredicateDeclaration
+	C: foliage::FindOrCreatePredicateDeclaration<crate::FoliageFlavor>
 {
 	let create_head_atom = |function: &'a clingo::ast::Function| -> Result<_, crate::Error>
 	{

src/translate/verify_properties/translate_body.rs

@@ -1,11 +1,11 @@
 // TODO: rename context
 pub(crate) fn translate_body_term<C>(body_term: &clingo::ast::Term, sign: clingo::ast::Sign,
-	context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer)
-	-> Result<foliage::Formula, crate::Error>
+	context: &C, variable_declaration_stack: &crate::VariableDeclarationStackLayer,
+	head_predicate_dependencies: &mut Option<&mut crate::PredicateDependencies>)
+	-> Result<crate::Formula, crate::Error>
 where
-	C: foliage::FindOrCreateFunctionDeclaration
-		+ foliage::FindOrCreatePredicateDeclaration
-		+ crate::traits::AssignVariableDeclarationDomain
+	C: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>
+		+ foliage::FindOrCreatePredicateDeclaration<crate::FoliageFlavor>,
 {
 	let function = match body_term.term_type()
 	{
@@ -18,22 +18,42 @@ where
 	let predicate_declaration = context.find_or_create_predicate_declaration(function_name,
 		function.arguments().len());
 
-	let parameters = function.arguments().iter().map(|_|
-		{
-			let variable_declaration = std::rc::Rc::new(
-				foliage::VariableDeclaration::new("<anonymous>".to_string()));
-			context.assign_variable_declaration_domain(&variable_declaration,
-				crate::Domain::Program);
-			variable_declaration
-		})
-		.collect::<foliage::VariableDeclarations>();
+	let parameters = function.arguments().iter().map(
+		|_| std::rc::Rc::new(crate::VariableDeclaration::new_generated(crate::Domain::Program)))
+		.collect::<crate::VariableDeclarations>();
 	let parameters = std::rc::Rc::new(parameters);
 
 	let predicate_arguments = parameters.iter().map(
-		|parameter| foliage::Term::variable(std::rc::Rc::clone(parameter)))
+		|parameter| crate::Term::variable(std::rc::Rc::clone(parameter)))
 		.collect::<Vec<_>>();
 
-	let predicate = foliage::Formula::predicate(predicate_declaration, predicate_arguments);
+	if let Some(head_predicate_dependencies) = head_predicate_dependencies
+	{
+		match head_predicate_dependencies.get_mut(&predicate_declaration)
+		{
+			None =>
+			{
+				let predicate_dependency_sign = match sign
+				{
+					clingo::ast::Sign::None
+					| clingo::ast::Sign::DoubleNegation => crate::PredicateDependencySign::OnlyPositive,
+					clingo::ast::Sign::Negation => crate::PredicateDependencySign::OnlyNegative,
+				};
+
+				head_predicate_dependencies.insert(
+					std::rc::Rc::clone(&predicate_declaration), predicate_dependency_sign);
+			},
+			Some(predicate_dependency_sign) =>
+				*predicate_dependency_sign = match sign
+				{
+					clingo::ast::Sign::None
+					| clingo::ast::Sign::DoubleNegation => predicate_dependency_sign.and_positive(),
+					clingo::ast::Sign::Negation => predicate_dependency_sign.and_negative(),
+				},
+		}
+	}
+
+	let predicate = crate::Formula::predicate(predicate_declaration, predicate_arguments);
 
 	let predicate_literal = match sign
 	{
@@ -41,7 +61,7 @@ where
 		| clingo::ast::Sign::DoubleNegation
 			=> predicate,
 		clingo::ast::Sign::Negation
-			=> foliage::Formula::not(Box::new(predicate)),
+			=> crate::Formula::not(Box::new(predicate)),
 	};
 
 	if function.arguments().is_empty()
@@ -60,18 +80,18 @@ where
 
 	arguments.push(predicate_literal);
 
-	let and = foliage::Formula::and(arguments);
+	let and = crate::Formula::and(arguments);
 
-	Ok(foliage::Formula::exists(parameters, Box::new(and)))
+	Ok(crate::Formula::exists(parameters, Box::new(and)))
 }
 
 pub(crate) fn translate_body_literal<C>(body_literal: &clingo::ast::BodyLiteral,
-	context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer)
-	-> Result<foliage::Formula, crate::Error>
+	context: &C, variable_declaration_stack: &crate::VariableDeclarationStackLayer,
+	head_predicate_dependencies: &mut Option<&mut crate::PredicateDependencies>)
+	-> Result<crate::Formula, crate::Error>
 where
-	C: foliage::FindOrCreateFunctionDeclaration
-		+ foliage::FindOrCreatePredicateDeclaration
-		+ crate::traits::AssignVariableDeclarationDomain
+	C: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>
+		+ foliage::FindOrCreatePredicateDeclaration<crate::FoliageFlavor>,
 {
 	match body_literal.sign()
 	{
@@ -97,21 +117,16 @@ where
 				_ => return Err(crate::Error::new_logic("unexpected negated Boolean value")),
 			}
 
-			Ok(foliage::Formula::Boolean(value))
+			Ok(crate::Formula::Boolean(value))
 		},
 		clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(),
-			context, variable_declaration_stack),
+			context, variable_declaration_stack, head_predicate_dependencies),
 		clingo::ast::LiteralType::Comparison(comparison) =>
 		{
-			let parameters = (0..2).map(|_|
-				{
-					let variable_declaration = std::rc::Rc::new(
-						foliage::VariableDeclaration::new("<anonymous>".to_string()));
-					context.assign_variable_declaration_domain(&variable_declaration,
-						crate::Domain::Program);
-					variable_declaration
-				})
-				.collect::<foliage::VariableDeclarations>();
+			let parameters = (0..2).map(
+				|_| std::rc::Rc::new(crate::VariableDeclaration::new_generated(
+					crate::Domain::Program)))
+				.collect::<crate::VariableDeclarations>();
 			let parameters = std::rc::Rc::new(parameters);
 
 			let mut parameters_iterator = parameters.iter();
@@ -123,19 +138,19 @@ where
 			let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(),
 				std::rc::Rc::clone(parameter_z2), context, variable_declaration_stack)?;
 
-			let variable_1 = foliage::Term::variable(std::rc::Rc::clone(parameter_z1));
-			let variable_2 = foliage::Term::variable(std::rc::Rc::clone(parameter_z2));
+			let variable_1 = crate::Term::variable(std::rc::Rc::clone(parameter_z1));
+			let variable_2 = crate::Term::variable(std::rc::Rc::clone(parameter_z2));
 
 			let operator = crate::translate::common::translate_comparison_operator(
 				comparison.comparison_type());
 
-			let compare_z1_and_z2 = foliage::Formula::compare(operator, Box::new(variable_1),
+			let compare_z1_and_z2 = crate::Formula::compare(operator, Box::new(variable_1),
 				Box::new(variable_2));
 
 			let and =
-				foliage::Formula::and(vec![choose_z1_in_t1, choose_z2_in_t2, compare_z1_and_z2]);
+				crate::Formula::and(vec![choose_z1_in_t1, choose_z2_in_t2, compare_z1_and_z2]);
 
-			Ok(foliage::Formula::exists(parameters, Box::new(and)))
+			Ok(crate::Formula::exists(parameters, Box::new(and)))
 		},
 		_ => Err(crate::Error::new_unsupported_language_feature(
 			"body literals other than Booleans, terms, or comparisons")),
@@ -143,15 +158,16 @@ where
 }
 
 pub(crate) fn translate_body<C>(body_literals: &[clingo::ast::BodyLiteral], context: &C,
-	variable_declaration_stack: &foliage::VariableDeclarationStackLayer)
-	-> Result<foliage::Formulas, crate::Error>
+	variable_declaration_stack: &crate::VariableDeclarationStackLayer,
+	// TODO: refactor
+	mut head_predicate_dependencies: &mut Option<&mut crate::PredicateDependencies>)
+	-> Result<crate::Formulas, crate::Error>
 where
-	C: foliage::FindOrCreateFunctionDeclaration
-		+ foliage::FindOrCreatePredicateDeclaration
-		+ crate::traits::AssignVariableDeclarationDomain
+	C: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>
+		+ foliage::FindOrCreatePredicateDeclaration<crate::FoliageFlavor>,
 {
 	body_literals.iter()
 		.map(|body_literal| translate_body_literal(body_literal, context,
-			variable_declaration_stack))
-		.collect::<Result<foliage::Formulas, crate::Error>>()
+			variable_declaration_stack, &mut head_predicate_dependencies))
+		.collect::<Result<crate::Formulas, crate::Error>>()
 }

src/utils.rs

@@ -1,6 +1,18 @@
 mod arithmetic_terms;
+mod autoname_variables;
+mod closures;
+mod copy_formula;
+mod fold_predicates;
+mod formula_contains_predicate;
+mod variables_in_terms;
 
+pub(crate) use autoname_variables::*;
 pub(crate) use arithmetic_terms::*;
+pub(crate) use closures::*;
+pub(crate) use copy_formula::*;
+pub(crate) use fold_predicates::*;
+pub(crate) use formula_contains_predicate::*;
+pub(crate) use variables_in_terms::*;
 
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
 pub(crate) enum OperatorNotation
@@ -35,155 +47,3 @@ impl std::fmt::Display for Domain
 		write!(formatter, "{:?}", self)
 	}
 }
-
-#[derive(Clone, Copy, Eq, Hash, PartialEq)]
-pub enum ProofDirection
-{
-	Forward,
-	Backward,
-	Both,
-}
-
-impl std::fmt::Debug for ProofDirection
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match self
-		{
-			ProofDirection::Forward => write!(formatter, "forward"),
-			ProofDirection::Backward => write!(formatter, "backward"),
-			ProofDirection::Both => write!(formatter, "both"),
-		}
-	}
-}
-
-impl std::fmt::Display for ProofDirection
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(formatter, "{:?}", self)
-	}
-}
-
-pub struct InvalidProofDirectionError;
-
-impl std::fmt::Debug for InvalidProofDirectionError
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(formatter, "invalid proof direction")
-	}
-}
-
-impl std::fmt::Display for InvalidProofDirectionError
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(formatter, "{:?}", self)
-	}
-}
-
-impl std::str::FromStr for ProofDirection
-{
-	type Err = InvalidProofDirectionError;
-
-	fn from_str(s: &str) -> Result<Self, Self::Err>
-	{
-		match s
-		{
-			"forward" => Ok(ProofDirection::Forward),
-			"backward" => Ok(ProofDirection::Backward),
-			"both" => Ok(ProofDirection::Both),
-			_ => Err(InvalidProofDirectionError),
-		}
-	}
-}
-
-pub(crate) struct ScopedFormula
-{
-	pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,
-	pub formula: foliage::Formula,
-}
-
-pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
-{
-	match scoped_formula.free_variable_declarations.is_empty()
-	{
-		true => scoped_formula.formula,
-		false => foliage::Formula::exists(scoped_formula.free_variable_declarations,
-			Box::new(scoped_formula.formula)),
-	}
-}
-
-pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
-{
-	match scoped_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)),
-	}
-}
-
-/*pub fn parse_predicate_declaration(input: &str)
-	-> Result<std::rc::Rc<foliage::PredicateDeclaration>, crate::Error>
-{
-	let mut parts = input.split("/");
-
-	let name = parts.next().ok_or(crate::Error::new_parse_predicate_declaration())?;
-
-	use std::str::FromStr;
-
-	let arity = match parts.next()
-	{
-		Some(arity)
-			=> usize::from_str(arity).map_err(|_| crate::Error::new_parse_predicate_declaration())?,
-		None => 0,
-	};
-
-	if parts.next().is_some()
-	{
-		return Err(crate::Error::new_parse_predicate_declaration());
-	}
-
-	Ok(std::rc::Rc::new(foliage::PredicateDeclaration
-	{
-		name: name.to_string(),
-		arity,
-	}))
-}*/
-
-pub type InputConstantDeclarationDomains
-	= std::collections::BTreeMap<std::rc::Rc<foliage::FunctionDeclaration>, Domain>;
-
-/*pub fn parse_constant_declaration(input: &str)
-	-> Result<(std::rc::Rc<foliage::FunctionDeclaration>, crate::Domain), crate::Error>
-{
-	let mut parts = input.split(":");
-
-	let name = parts.next().ok_or(crate::Error::new_parse_constant_declaration())?.trim();
-
-	let domain = match parts.next()
-	{
-		None => crate::Domain::Program,
-		Some(value) => match value.trim()
-		{
-			"program" => crate::Domain::Program,
-			"integer" => crate::Domain::Integer,
-			_ => return Err(crate::Error::new_parse_constant_declaration()),
-		},
-	};
-
-	if parts.next().is_some()
-	{
-		return Err(crate::Error::new_parse_constant_declaration());
-	}
-
-	let constant_declaration = std::rc::Rc::new(foliage::FunctionDeclaration
-	{
-		name: name.to_string(),
-		arity: 0,
-	});
-
-	Ok((constant_declaration, domain))
-}*/

src/utils/arithmetic_terms.rs

@@ -1,16 +1,15 @@
-pub(crate) fn is_term_arithmetic<C>(term: &foliage::Term, context: &C) -> Result<bool, crate::Error>
-where
-	C: crate::traits::InputConstantDeclarationDomain
-		+ crate::traits::VariableDeclarationDomain
+pub(crate) fn is_term_arithmetic(term: &crate::Term) -> Result<bool, crate::Error>
 {
+	use crate::Term;
+
 	match term
 	{
-		foliage::Term::Boolean(_)
-		| foliage::Term::SpecialInteger(_)
-		| foliage::Term::String(_)
+		Term::Boolean(_)
+		| Term::SpecialInteger(_)
+		| Term::String(_)
 			=> Ok(false),
-		foliage::Term::Integer(_) => Ok(true),
-		foliage::Term::Function(ref function) =>
+		Term::Integer(_) => Ok(true),
+		Term::Function(ref function) =>
 		{
 			if !function.arguments.is_empty()
 			{
@@ -18,20 +17,17 @@ where
 					crate::Error::new_unsupported_language_feature("functions with arguments"));
 			}
 
-			let domain = context.input_constant_declaration_domain(&function.declaration);
-
-			Ok(domain == crate::Domain::Integer)
+			Ok(*function.declaration.domain.borrow() == crate::Domain::Integer)
 		},
-		foliage::Term::Variable(foliage::Variable{ref declaration}) =>
-			match context.variable_declaration_domain(declaration)
+		Term::Variable(crate::Variable{ref declaration}) =>
+			match declaration.domain()?
 			{
-				Some(crate::Domain::Program) => Ok(false),
-				Some(crate::Domain::Integer) => Ok(true),
-				None => Err(crate::Error::new_logic("unspecified variable declaration domain")),
+				crate::Domain::Program => Ok(false),
+				crate::Domain::Integer => Ok(true),
 			},
-		foliage::Term::BinaryOperation(foliage::BinaryOperation{ref left, ref right, ..})
-			=> Ok(is_term_arithmetic(left, context)? && is_term_arithmetic(right, context)?),
-		foliage::Term::UnaryOperation(foliage::UnaryOperation{ref argument, ..})
-			=> is_term_arithmetic(argument, context),
+		Term::BinaryOperation(crate::BinaryOperation{ref left, ref right, ..})
+			=> Ok(is_term_arithmetic(left)? && is_term_arithmetic(right)?),
+		Term::UnaryOperation(crate::UnaryOperation{ref argument, ..})
+			=> is_term_arithmetic(argument),
 	}
 }

src/utils/autoname_variables.rs

@@ -0,0 +1,246 @@
+struct IDs
+{
+	program_variable_id: usize,
+	integer_variable_id: usize,
+}
+
+impl IDs
+{
+	pub fn new() -> Self
+	{
+		Self
+		{
+			program_variable_id: 1,
+			integer_variable_id: 1,
+		}
+	}
+}
+
+fn reset_variable_name(variable_declaration: &crate::VariableDeclaration)
+{
+	let domain = match variable_declaration.domain()
+	{
+		Ok(domain) => domain,
+		Err(_) => unreachable!("all variable domains should be assigned at this point"),
+	};
+
+	let ref mut variable_name = *variable_declaration.name.borrow_mut();
+
+	match variable_name
+	{
+		crate::VariableName::Generated(ref mut generated_variable_name) =>
+			generated_variable_name.id = None,
+		crate::VariableName::UserDefined(_) =>
+			*variable_name = crate::VariableName::Generated(
+				crate::GeneratedVariableName
+				{
+					domain,
+					id: None,
+				}),
+	}
+}
+
+fn reset_variable_names_in_term(term: &mut crate::Term)
+{
+	use foliage::Term;
+
+	match term
+	{
+		Term::BinaryOperation(ref mut binary_operation) =>
+		{
+			reset_variable_names_in_term(&mut *binary_operation.left);
+			reset_variable_names_in_term(&mut *binary_operation.right);
+		},
+		Term::Boolean(_)
+		| Term::Integer(_)
+		| Term::SpecialInteger(_)
+		| Term::String(_) => (),
+		Term::Function(ref mut function) =>
+			for mut argument in &mut function.arguments
+			{
+				reset_variable_names_in_term(&mut argument);
+			},
+		Term::UnaryOperation(ref mut unary_operation) =>
+			reset_variable_names_in_term(&mut *unary_operation.argument),
+		Term::Variable(ref mut variable) => reset_variable_name(&variable.declaration),
+	}
+}
+
+fn reset_variable_names_in_formula(formula: &mut crate::Formula)
+{
+	use foliage::Formula;
+
+	match formula
+	{
+		Formula::And(ref mut arguments)
+		| Formula::IfAndOnlyIf(ref mut arguments)
+		| Formula::Or(ref mut arguments) =>
+			for argument in arguments
+			{
+				reset_variable_names_in_formula(argument);
+			},
+		Formula::Boolean(_) => (),
+		Formula::Compare(ref mut compare) =>
+		{
+			reset_variable_names_in_term(&mut *compare.left);
+			reset_variable_names_in_term(&mut *compare.right);
+		},
+		Formula::Exists(ref mut quantified_formula)
+		| Formula::ForAll(ref mut quantified_formula) =>
+		{
+			for ref parameter in &*quantified_formula.parameters
+			{
+				reset_variable_name(&parameter);
+			}
+
+			reset_variable_names_in_formula(&mut *quantified_formula.argument);
+		},
+		Formula::Implies(ref mut implies) =>
+		{
+			reset_variable_names_in_formula(&mut *implies.antecedent);
+			reset_variable_names_in_formula(&mut *implies.implication);
+		},
+		Formula::Not(ref mut argument) => reset_variable_names_in_formula(argument),
+		Formula::Predicate(ref mut predicate) =>
+			for mut argument in &mut predicate.arguments
+			{
+				reset_variable_names_in_term(&mut argument);
+			},
+	}
+}
+
+fn set_variable_name(variable_declaration: &crate::VariableDeclaration, ids: &mut IDs)
+{
+	match *variable_declaration.name.borrow_mut()
+	{
+		crate::VariableName::Generated(ref mut generated_variable_name) =>
+		{
+			if generated_variable_name.id.is_some()
+			{
+				return;
+			}
+
+			match generated_variable_name.domain
+			{
+				crate::Domain::Program =>
+				{
+					generated_variable_name.id = Some(ids.program_variable_id);
+					ids.program_variable_id += 1;
+				},
+				crate::Domain::Integer =>
+				{
+					generated_variable_name.id = Some(ids.integer_variable_id);
+					ids.integer_variable_id += 1;
+				},
+			}
+		},
+		crate::VariableName::UserDefined(_) => (),
+	}
+}
+
+fn set_variable_names_in_term(term: &mut crate::Term, ids: &mut IDs)
+{
+	use foliage::Term;
+
+	match term
+	{
+		Term::BinaryOperation(ref mut binary_operation) =>
+		{
+			set_variable_names_in_term(&mut *binary_operation.left, ids);
+			set_variable_names_in_term(&mut *binary_operation.right, ids);
+		},
+		Term::Boolean(_)
+		| Term::Integer(_)
+		| Term::SpecialInteger(_)
+		| Term::String(_) => (),
+		Term::Function(ref mut function) =>
+			for mut argument in &mut function.arguments
+			{
+				set_variable_names_in_term(&mut argument, ids);
+			},
+		Term::UnaryOperation(ref mut unary_operation) =>
+			set_variable_names_in_term(&mut *unary_operation.argument, ids),
+		Term::Variable(ref mut variable) => set_variable_name(&variable.declaration, ids),
+	}
+}
+
+fn set_variable_names_in_formula(formula: &mut crate::Formula, ids: &mut IDs)
+{
+	use foliage::Formula;
+
+	match formula
+	{
+		Formula::And(ref mut arguments)
+		| Formula::IfAndOnlyIf(ref mut arguments)
+		| Formula::Or(ref mut arguments) =>
+			for argument in arguments
+			{
+				set_variable_names_in_formula(argument, ids);
+			},
+		Formula::Boolean(_) => (),
+		Formula::Compare(ref mut compare) =>
+		{
+			set_variable_names_in_term(&mut *compare.left, ids);
+			set_variable_names_in_term(&mut *compare.right, ids);
+		},
+		Formula::Exists(ref mut quantified_formula)
+		| Formula::ForAll(ref mut quantified_formula) =>
+		{
+			for ref parameter in &*quantified_formula.parameters
+			{
+				set_variable_name(&parameter, ids);
+			}
+
+			set_variable_names_in_formula(&mut *quantified_formula.argument, ids);
+		},
+		Formula::Implies(ref mut implies) =>
+			match implies.direction
+			{
+				foliage::ImplicationDirection::LeftToRight =>
+				{
+					set_variable_names_in_formula(&mut *implies.antecedent, ids);
+					set_variable_names_in_formula(&mut *implies.implication, ids);
+				},
+				foliage::ImplicationDirection::RightToLeft =>
+				{
+					set_variable_names_in_formula(&mut *implies.implication, ids);
+					set_variable_names_in_formula(&mut *implies.antecedent, ids);
+				},
+		},
+		Formula::Not(ref mut argument) => set_variable_names_in_formula(argument, ids),
+		Formula::Predicate(ref mut predicate) =>
+			for mut argument in &mut predicate.arguments
+			{
+				set_variable_names_in_term(&mut argument, ids);
+			},
+	}
+}
+
+pub(crate) fn autoname_variables(formula: &mut crate::Formula)
+{
+	// TODO: refactor, this is a bit hacky
+	reset_variable_names_in_formula(formula);
+
+	let mut ids = IDs::new();
+
+	set_variable_names_in_formula(formula, &mut ids);
+
+	// If there only exists exactly one program variable (which incremented the ID from 1 to 2),
+	// give it the special ID 0 on the second run
+	ids.program_variable_id = match ids.program_variable_id
+	{
+		2 => 0,
+		_ => 1,
+	};
+
+	// If there only exists exactly one integer variable (which incremented the ID from 1 to 2),
+	// give it the special ID 0 on the second run
+	ids.integer_variable_id = match ids.integer_variable_id
+	{
+		2 => 0,
+		_ => 1,
+	};
+
+	reset_variable_names_in_formula(formula);
+	set_variable_names_in_formula(formula, &mut ids);
+}

src/utils/closures.rs

@@ -0,0 +1,19 @@
+pub(crate) fn existential_closure(open_formula: crate::OpenFormula) -> crate::Formula
+{
+	match open_formula.free_variable_declarations.is_empty()
+	{
+		true => open_formula.formula,
+		false => crate::Formula::exists(open_formula.free_variable_declarations,
+			Box::new(open_formula.formula)),
+	}
+}
+
+pub(crate) fn universal_closure(open_formula: crate::OpenFormula) -> crate::Formula
+{
+	match open_formula.free_variable_declarations.is_empty()
+	{
+		true => open_formula.formula,
+		false => crate::Formula::for_all(open_formula.free_variable_declarations,
+			Box::new(open_formula.formula)),
+	}
+}

src/utils/copy_formula.rs

@@ -0,0 +1,245 @@
+fn replace_variables_in_term(term: &mut crate::Term,
+	old_variable_declarations: &crate::VariableDeclarations,
+	new_variable_declarations: &crate::VariableDeclarations)
+{
+	assert_eq!(old_variable_declarations.len(), new_variable_declarations.len());
+
+	use crate::Term;
+
+	match term
+	{
+		Term::BinaryOperation(binary_operation) =>
+		{
+			replace_variables_in_term(&mut binary_operation.left, old_variable_declarations,
+				new_variable_declarations);
+			replace_variables_in_term(&mut binary_operation.right, old_variable_declarations,
+				new_variable_declarations);
+		},
+		Term::Function(function) =>
+			for mut argument in &mut function.arguments
+			{
+				replace_variables_in_term(&mut argument, old_variable_declarations,
+					new_variable_declarations);
+			},
+		Term::UnaryOperation(unary_operation) =>
+			replace_variables_in_term(&mut unary_operation.argument, old_variable_declarations,
+				new_variable_declarations),
+		Term::Variable(variable) =>
+			if let Some(index) = old_variable_declarations.iter().enumerate()
+				.find_map(
+					|(index, variable_declaration)|
+					{
+						match *variable_declaration == variable.declaration
+						{
+							true => Some(index),
+							false => None,
+						}
+					})
+			{
+				variable.declaration = std::rc::Rc::clone(&new_variable_declarations[index]);
+			},
+		Term::Boolean(_)
+		| Term::Integer(_)
+		| Term::SpecialInteger(_)
+		| Term::String(_) => (),
+	}
+}
+
+fn replace_variables_in_formula(formula: &mut crate::Formula,
+	old_variable_declarations: &crate::VariableDeclarations,
+	new_variable_declarations: &crate::VariableDeclarations)
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+			for argument in arguments
+			{
+				replace_variables_in_formula(argument, old_variable_declarations,
+					new_variable_declarations);
+			},
+		Formula::Compare(compare) =>
+		{
+			replace_variables_in_term(&mut compare.left, old_variable_declarations,
+				new_variable_declarations);
+			replace_variables_in_term(&mut compare.right, old_variable_declarations,
+				new_variable_declarations);
+		},
+		Formula::Exists(quantified_formula)
+		| Formula::ForAll(quantified_formula) =>
+			replace_variables_in_formula(&mut quantified_formula.argument,
+				old_variable_declarations, new_variable_declarations),
+		Formula::Implies(implies) =>
+		{
+			replace_variables_in_formula(&mut implies.antecedent, old_variable_declarations,
+				new_variable_declarations);
+			replace_variables_in_formula(&mut implies.implication, old_variable_declarations,
+				new_variable_declarations);
+		},
+		Formula::Not(argument) =>
+			replace_variables_in_formula(argument, old_variable_declarations,
+				new_variable_declarations),
+		Formula::Predicate(predicate) =>
+			for mut argument in &mut predicate.arguments
+			{
+				replace_variables_in_term(&mut argument, old_variable_declarations,
+					new_variable_declarations);
+			},
+		Formula::Boolean(_) => (),
+	}
+}
+
+fn replace_variable_in_term_with_term(term: &mut crate::Term,
+	variable_declaration: &crate::VariableDeclaration, replacement_term: &crate::Term)
+{
+	use crate::Term;
+
+	match term
+	{
+		Term::BinaryOperation(binary_operation) =>
+		{
+			replace_variable_in_term_with_term(&mut binary_operation.left, variable_declaration,
+				replacement_term);
+			replace_variable_in_term_with_term(&mut binary_operation.right, variable_declaration,
+				replacement_term);
+		},
+		Term::Function(function) =>
+			for mut argument in &mut function.arguments
+			{
+				replace_variable_in_term_with_term(&mut argument, variable_declaration,
+					replacement_term);
+			},
+		Term::UnaryOperation(unary_operation) =>
+			replace_variable_in_term_with_term(&mut unary_operation.argument, variable_declaration,
+				replacement_term),
+		Term::Variable(variable) =>
+			if *variable.declaration == *variable_declaration
+			{
+				*term = copy_term(replacement_term);
+			},
+		Term::Boolean(_)
+		| Term::Integer(_)
+		| Term::SpecialInteger(_)
+		| Term::String(_) => (),
+	}
+}
+
+pub(crate) fn replace_variable_in_formula_with_term(formula: &mut crate::Formula,
+	variable_declaration: &crate::VariableDeclaration, replacement_term: &crate::Term)
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+			for argument in arguments
+			{
+				replace_variable_in_formula_with_term(argument, variable_declaration,
+					replacement_term);
+			},
+		Formula::Compare(compare) =>
+		{
+			replace_variable_in_term_with_term(&mut compare.left, variable_declaration,
+				replacement_term);
+			replace_variable_in_term_with_term(&mut compare.right, variable_declaration,
+				replacement_term);
+		},
+		Formula::Exists(quantified_formula)
+		| Formula::ForAll(quantified_formula) =>
+			replace_variable_in_formula_with_term(&mut quantified_formula.argument,
+				variable_declaration, replacement_term),
+		Formula::Implies(implies) =>
+		{
+			replace_variable_in_formula_with_term(&mut implies.antecedent, variable_declaration,
+				replacement_term);
+			replace_variable_in_formula_with_term(&mut implies.implication, variable_declaration,
+				replacement_term);
+		},
+		Formula::Not(argument) =>
+			replace_variable_in_formula_with_term(argument, variable_declaration, replacement_term),
+		Formula::Predicate(predicate) =>
+			for mut argument in &mut predicate.arguments
+			{
+				replace_variable_in_term_with_term(&mut argument, variable_declaration,
+					replacement_term);
+			},
+		Formula::Boolean(_) => (),
+	}
+}
+
+pub(crate) fn copy_term(term: &crate::Term) -> crate::Term
+{
+	use crate::Term;
+
+	match term
+	{
+		Term::BinaryOperation(binary_operation) =>
+			Term::binary_operation(binary_operation.operator,
+				Box::new(copy_term(&binary_operation.left)),
+				Box::new(copy_term(&binary_operation.right))),
+		Term::Boolean(value) => Term::boolean(*value),
+		Term::Function(function) => Term::function(std::rc::Rc::clone(&function.declaration),
+			function.arguments.iter().map(|argument| copy_term(argument)).collect()),
+		Term::Integer(value) => Term::integer(*value),
+		Term::SpecialInteger(value) => Term::special_integer(*value),
+		Term::String(value) => Term::string(value.clone()),
+		Term::UnaryOperation(unary_operation) => Term::unary_operation(unary_operation.operator,
+			Box::new(copy_term(&unary_operation.argument))),
+		Term::Variable(variable) => Term::variable(std::rc::Rc::clone(&variable.declaration)),
+	}
+}
+
+fn copy_quantified_formula(quantified_expression: &crate::QuantifiedFormula)
+	-> crate::QuantifiedFormula
+{
+	let copy_parameters =
+		quantified_expression.parameters.iter()
+			// TODO: check correctness of clone implementation
+			.map(|x| x.clone())
+			.collect();
+	let copy_parameters = std::rc::Rc::new(copy_parameters);
+
+	let mut copy_argument = copy_formula(&quantified_expression.argument);
+
+	replace_variables_in_formula(&mut copy_argument, &quantified_expression.parameters,
+		&copy_parameters);
+
+	crate::QuantifiedFormula::new(copy_parameters, Box::new(copy_argument))
+}
+
+#[allow(dead_code)]
+pub(crate) fn copy_formula(formula: &crate::Formula) -> crate::Formula
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments) =>
+			Formula::and(arguments.iter().map(|argument| copy_formula(argument)).collect()),
+		Formula::Boolean(value) => Formula::boolean(*value),
+		Formula::Compare(compare) =>
+			Formula::compare(compare.operator, Box::new(copy_term(&compare.left)),
+				Box::new(copy_term(&compare.right))),
+		Formula::Exists(quantified_formula) =>
+			Formula::Exists(copy_quantified_formula(quantified_formula)),
+		Formula::ForAll(quantified_formula) =>
+			Formula::ForAll(copy_quantified_formula(quantified_formula)),
+		Formula::IfAndOnlyIf(arguments) =>
+			Formula::if_and_only_if(
+				arguments.iter().map(|argument| copy_formula(argument)).collect()),
+		Formula::Implies(implies) =>
+			Formula::implies(implies.direction, Box::new(copy_formula(&implies.antecedent)),
+				Box::new(copy_formula(&implies.implication))),
+		Formula::Not(argument) => Formula::not(Box::new(copy_formula(&argument))),
+		Formula::Or(arguments) =>
+			Formula::or(arguments.iter().map(|argument| copy_formula(argument)).collect()),
+		Formula::Predicate(predicate) =>
+			Formula::predicate(std::rc::Rc::clone(&predicate.declaration),
+				predicate.arguments.iter().map(|argument| copy_term(argument)).collect()),
+	}
+}

src/utils/fold_predicates.rs

@@ -0,0 +1,36 @@
+pub(crate) fn fold_predicates<B, F>(formula: &crate::Formula, mut accumulator: B, functor: &mut F)
+	-> B
+where
+	F: FnMut(B, &crate::Predicate) -> B,
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+		{
+			for argument in arguments
+			{
+				accumulator = fold_predicates(argument, accumulator, functor);
+			}
+
+			accumulator
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_) => accumulator,
+		Formula::Exists(quantified_expression)
+		| Formula::ForAll(quantified_expression) =>
+			fold_predicates(&quantified_expression.argument, accumulator, functor),
+		Formula::Implies(implies) =>
+		{
+			accumulator = fold_predicates(&implies.antecedent, accumulator, functor);
+			accumulator = fold_predicates(&implies.implication, accumulator, functor);
+
+			accumulator
+		},
+		Formula::Not(argument) => fold_predicates(argument, accumulator, functor),
+		Formula::Predicate(predicate) => functor(accumulator, &predicate),
+	}
+}

src/utils/formula_contains_predicate.rs

@@ -0,0 +1,25 @@
+pub(crate) fn formula_contains_predicate(formula: &crate::Formula,
+	predicate_declaration: &crate::PredicateDeclaration)
+	-> bool
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+			arguments.iter().any(
+				|argument| formula_contains_predicate(argument, predicate_declaration)),
+		Formula::Boolean(_)
+		| Formula::Compare(_) => false,
+		Formula::Exists(quantified_expression)
+		| Formula::ForAll(quantified_expression) =>
+			formula_contains_predicate(&quantified_expression.argument, predicate_declaration),
+		Formula::Implies(implies) =>
+			formula_contains_predicate(&implies.antecedent, predicate_declaration)
+			|| formula_contains_predicate(&implies.implication, predicate_declaration),
+		Formula::Not(argument) => formula_contains_predicate(argument, predicate_declaration),
+		Formula::Predicate(predicate) => &*predicate.declaration == predicate_declaration,
+	}
+}

src/utils/variables_in_terms.rs

@@ -0,0 +1,21 @@
+pub(crate) fn term_contains_variable(term: &crate::Term,
+	variable_declaration: &crate::VariableDeclaration)
+	-> bool
+{
+	use crate::Term;
+
+	match term
+	{
+		Term::BinaryOperation(binary_operation) =>
+			term_contains_variable(&binary_operation.left, variable_declaration)
+				|| term_contains_variable(&binary_operation.right, variable_declaration),
+		Term::Boolean(_)
+		| Term::Function(_)
+		| Term::Integer(_)
+		| Term::SpecialInteger(_)
+		| Term::String(_) => false,
+		Term::UnaryOperation(unary_operation) =>
+			term_contains_variable(&unary_operation.argument, variable_declaration),
+		Term::Variable(variable) => *variable.declaration == *variable_declaration,
+	}
+}