Support hiding auxiliary predicates

examples/exact-cover.spec

@@ -1,6 +1,4 @@
-# Auxiliary predicate to determine whether a variable is integer. is_int/1 is declared as an input
-# predicate so that anthem doesn’t generate its completed definition
-input: is_int/1.
+# Auxiliary predicate to determine whether a variable is integer
 axiom: forall X (is_int(X) <-> exists N X = N).
 
 # Perform the proofs under the assumption that n is a nonnegative integer input constant. n stands
@@ -11,6 +9,10 @@ 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/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 X, Y (s(X, Y) -> is_int(Y)).

examples/example-0.spec

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

examples/example-1.spec

@@ -1,3 +1,5 @@
+input: p/1.
+
 assert:
 	forall N
 	(

src/commands/verify_program.rs

@@ -44,6 +44,16 @@ where
 		}
 	}
 
+	match problem.restrict_to_output_predicates()
+	{
+		Ok(_) => (),
+		Err(error) =>
+		{
+			log::error!("could not restrict problem to output predicates: {}", error);
+			std::process::exit(1)
+		}
+	}
+
 	match problem.prove(proof_direction)
 	{
 		Ok(()) => (),

src/error.rs

@@ -22,6 +22,9 @@ pub enum Kind
 	UnknownDomainIdentifier(String),
 	VariableNameNotAllowed(String),
 	FormulaNotClosed(std::rc::Rc<foliage::VariableDeclarations>),
+	NoCompletedDefinitionFound(std::rc::Rc<foliage::PredicateDeclaration>),
+	CannotHidePredicate(std::rc::Rc<foliage::PredicateDeclaration>,
+		std::rc::Rc<foliage::PredicateDeclaration>),
 	WriteTPTPProgram,
 	RunVampire,
 	// TODO: rename to something Vampire-specific
@@ -148,6 +151,21 @@ impl Error
 		Self::new(Kind::FormulaNotClosed(free_variables))
 	}
 
+	pub(crate) fn new_no_completed_definition_found(
+		predicate_declaration: std::rc::Rc<foliage::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::NoCompletedDefinitionFound(predicate_declaration))
+	}
+
+	pub(crate) fn new_cannot_hide_predicate(
+		predicate_declaration_1: std::rc::Rc<foliage::PredicateDeclaration>,
+		predicate_declaration_2: std::rc::Rc<foliage::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::CannotHidePredicate(predicate_declaration_1, predicate_declaration_2))
+	}
+
 	pub(crate) fn new_write_tptp_program<S: Into<Source>>(source: S) -> Self
 	{
 		Self::new(Kind::WriteTPTPProgram).with(source)
@@ -219,6 +237,11 @@ impl std::fmt::Debug for Error
 				write!(formatter, "formula may not contain free variables (free variables in this formula: {})",
 					free_variable_names_output)
 			},
+			Kind::NoCompletedDefinitionFound(ref predicate_declaration) =>
+				write!(formatter, "no completed definition found for {}", predicate_declaration),
+			Kind::CannotHidePredicate(ref predicate_declaration_1, ref predicate_declaration_2) =>
+				write!(formatter, "cannot hide predicate {} because it depends on {}",
+					predicate_declaration_1, predicate_declaration_2),
 			Kind::RunVampire => write!(formatter, "could not run Vampire"),
 			Kind::ProveProgram(exit_code, ref stdout, ref stderr) =>
 			{

src/lib.rs

@@ -1,4 +1,5 @@
 #![feature(trait_alias)]
+#![feature(vec_remove_item)]
 
 pub mod commands;
 pub mod error;

src/problem.rs

@@ -20,6 +20,9 @@ type VariableDeclarationIDs
 type InputConstantDeclarationDomains
 	= std::collections::BTreeMap<std::rc::Rc<foliage::FunctionDeclaration>, crate::Domain>;
 
+type VariableDeclarationDomains
+	= std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>;
+
 struct FormatContext<'a, 'b>
 {
 	pub program_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
@@ -28,9 +31,6 @@ struct FormatContext<'a, 'b>
 	pub variable_declaration_domains: &'b VariableDeclarationDomains,
 }
 
-type VariableDeclarationDomains
-	= std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>;
-
 pub struct Problem
 {
 	function_declarations: std::cell::RefCell<foliage::FunctionDeclarations>,
@@ -82,6 +82,64 @@ impl Problem
 		section.push(statement);
 	}
 
+	pub(crate) fn restrict_to_output_predicates(&mut self) -> Result<(), crate::Error>
+	{
+		let predicate_declarations = self.predicate_declarations.borrow();
+		let input_predicate_declarations = self.input_predicate_declarations.borrow();
+		let output_predicate_declarations = self.output_predicate_declarations.borrow();
+
+		// If no output statements were provided, show all predicates by default
+		if output_predicate_declarations.is_empty()
+		{
+			return Ok(());
+		}
+
+		let hidden_predicate_declarations =
+			predicate_declarations.iter().filter(|x| !output_predicate_declarations.contains(*x)
+				&& !input_predicate_declarations.contains(*x));
+
+		let mut statements = self.statements.borrow_mut();
+
+		for hidden_predicate_declaration in hidden_predicate_declarations
+		{
+			let matches_completed_definition =
+				|(_, statement): &(_, &Statement)| match statement.kind
+				{
+					StatementKind::CompletedDefinition(ref predicate_declaration) =>
+						predicate_declaration == hidden_predicate_declaration,
+					_ => false,
+				};
+
+			let completed_definitions = match statements.get_mut(&SectionKind::CompletedDefinitions)
+			{
+				Some(completed_definitions) => completed_definitions,
+				None => return Ok(()),
+			};
+
+			let completed_definition = match completed_definitions.iter().enumerate()
+				.find(matches_completed_definition)
+			{
+				Some((completed_definition_index, _)) =>
+					completed_definitions.remove(completed_definition_index).formula,
+				None => return Err(crate::Error::new_no_completed_definition_found(
+					std::rc::Rc::clone(hidden_predicate_declaration))),
+			};
+
+			drop(completed_definitions);
+
+			for (_, statements) in statements.iter_mut()
+			{
+				for statement in statements.iter_mut()
+				{
+					crate::utils::replace_predicate_in_formula_with_completed_definition(
+						&mut statement.formula, &completed_definition, self)?;
+				}
+			}
+		}
+
+		Ok(())
+	}
+
 	fn print_step_title(&self, step_title: &str, color: &termcolor::ColorSpec)
 	{
 		let longest_possible_key = "    Finished";
@@ -216,17 +274,7 @@ impl Problem
 
 	fn prove_unproven_statements(&self) -> Result<ProofResult, crate::Error>
 	{
-		let format_context = FormatContext
-		{
-			program_variable_declaration_ids:
-				std::cell::RefCell::new(VariableDeclarationIDs::new()),
-			integer_variable_declaration_ids:
-				std::cell::RefCell::new(VariableDeclarationIDs::new()),
-			input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(),
-			variable_declaration_domains: &self.variable_declaration_domains.borrow(),
-		};
-
-		let display_statement = |statement: &Statement, format_context|
+		let display_statement = |statement: &Statement|
 		{
 			let step_title = match statement.proof_status
 			{
@@ -256,15 +304,17 @@ impl Problem
 			self.shell.borrow_mut().print(&format!("{}: ", statement.kind),
 				&termcolor::ColorSpec::new());
 
-			match statement.kind
+			let format_context = FormatContext
 			{
-				StatementKind::CompletedDefinition(_)
-				| StatementKind::IntegrityConstraint =>
-					print!("{}",
-						foliage::format::display_formula(&statement.formula, format_context)),
-				_ =>
-					print!("{}", statement.formula),
-			}
+				program_variable_declaration_ids:
+					std::cell::RefCell::new(VariableDeclarationIDs::new()),
+				integer_variable_declaration_ids:
+					std::cell::RefCell::new(VariableDeclarationIDs::new()),
+				input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(),
+				variable_declaration_domains: &self.variable_declaration_domains.borrow(),
+			};
+
+			print!("{}", foliage::format::display_formula(&statement.formula, &format_context));
 		};
 
 		// Show all statements that are assumed to be proven
@@ -273,7 +323,7 @@ impl Problem
 			for statement in statements.iter_mut()
 				.filter(|statement| statement.proof_status == ProofStatus::AssumedProven)
 			{
-				display_statement(statement, &format_context);
+				display_statement(statement);
 				println!("");
 			}
 		}
@@ -286,7 +336,7 @@ impl Problem
 					statement.proof_status = ProofStatus::ToProveNow;
 
 					print!("\x1b[s");
-					display_statement(statement, &format_context);
+					display_statement(statement);
 					print!("\x1b[u");
 
 					use std::io::Write as _;
@@ -309,7 +359,7 @@ impl Problem
 			// TODO: make configurable again
 			let (proof_result, proof_time_seconds) =
 				run_vampire(&tptp_problem_to_prove_next_statement,
-					Some(&["--mode", "casc", "--cores", "8", "--time_limit", "15"]))?;
+					Some(&["--mode", "casc", "--cores", "8", "--time_limit", "300"]))?;
 
 			match self.next_unproven_statement_do_mut(
 				|statement|
@@ -323,7 +373,7 @@ impl Problem
 
 					self.shell.borrow_mut().erase_line();
 
-					display_statement(statement, &format_context);
+					display_statement(statement);
 
 					match proof_result
 					{
@@ -591,6 +641,22 @@ impl crate::traits::AssignVariableDeclarationDomain for Problem
 	}
 }
 
+impl crate::traits::VariableDeclarationDomain for Problem
+{
+	fn variable_declaration_domain(&self,
+		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
+		-> Option<crate::Domain>
+	{
+		self.variable_declaration_domains.borrow().iter().find_map(
+			|(x, domain)|
+			match x == variable_declaration
+			{
+				true => Some(*domain),
+				false => None,
+			})
+	}
+}
+
 impl<'a, 'b> FormatContext<'a, 'b>
 {
 	fn variable_declaration_id(&self,

src/utils.rs

@@ -1,8 +1,12 @@
 mod arithmetic_terms;
 mod closures;
+mod copy_formula;
+mod output_predicates;
 
 pub(crate) use arithmetic_terms::*;
 pub(crate) use closures::*;
+pub(crate) use copy_formula::*;
+pub(crate) use output_predicates::*;
 
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
 pub(crate) enum OperatorNotation

src/utils/copy_formula.rs

@@ -0,0 +1,262 @@
+fn replace_variables_in_term(term: &mut foliage::Term,
+	old_variable_declarations: &foliage::VariableDeclarations,
+	new_variable_declarations: &foliage::VariableDeclarations)
+{
+	assert_eq!(old_variable_declarations.len(), new_variable_declarations.len());
+
+	use foliage::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 foliage::Formula,
+	old_variable_declarations: &foliage::VariableDeclarations,
+	new_variable_declarations: &foliage::VariableDeclarations)
+{
+	use foliage::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 foliage::Term,
+	variable_declaration: &foliage::VariableDeclaration, replacement_term: &foliage::Term)
+{
+	use foliage::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 foliage::Formula,
+	variable_declaration: &foliage::VariableDeclaration, replacement_term: &foliage::Term)
+{
+	use foliage::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(_) => (),
+	}
+}
+
+fn copy_term(term: &foliage::Term) -> foliage::Term
+{
+	use foliage::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<D>(quantified_expression: &foliage::QuantifiedFormula, declarations: &D)
+	-> foliage::QuantifiedFormula
+where
+	D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain,
+{
+	let copy_parameters =
+		quantified_expression.parameters.iter()
+			.map(
+				|parameter|
+				{
+					let copy_parameter = std::rc::Rc::new(
+						foliage::VariableDeclaration::new(parameter.name.clone()));
+
+					if let Some(domain) = declarations.variable_declaration_domain(parameter)
+					{
+						declarations.assign_variable_declaration_domain(&copy_parameter, domain);
+					}
+
+					copy_parameter
+				})
+			.collect();
+	let copy_parameters = std::rc::Rc::new(copy_parameters);
+
+	let mut copy_argument = copy_formula(&quantified_expression.argument, declarations);
+
+	replace_variables_in_formula(&mut copy_argument, &quantified_expression.parameters,
+		&copy_parameters);
+
+	foliage::QuantifiedFormula::new(copy_parameters, Box::new(copy_argument))
+}
+
+pub(crate) fn copy_formula<D>(formula: &foliage::Formula, declarations: &D) -> foliage::Formula
+where
+	D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain,
+{
+	use foliage::Formula;
+
+	match formula
+	{
+		Formula::And(arguments) =>
+			Formula::and(arguments.iter().map(
+				|argument| copy_formula(argument, declarations)).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, declarations)),
+		Formula::ForAll(quantified_formula) =>
+			Formula::ForAll(copy_quantified_formula(quantified_formula, declarations)),
+		Formula::IfAndOnlyIf(arguments) =>
+			Formula::if_and_only_if(
+				arguments.iter().map(|argument| copy_formula(argument, declarations)).collect()),
+		Formula::Implies(implies) =>
+			Formula::implies(implies.direction,
+				Box::new(copy_formula(&implies.antecedent, declarations)),
+				Box::new(copy_formula(&implies.implication, declarations))),
+		Formula::Not(argument) => Formula::not(Box::new(copy_formula(&argument, declarations))),
+		Formula::Or(arguments) =>
+			Formula::or(arguments.iter().map(
+				|argument| copy_formula(argument, declarations)).collect()),
+		Formula::Predicate(predicate) =>
+			Formula::predicate(std::rc::Rc::clone(&predicate.declaration),
+				predicate.arguments.iter().map(|argument| copy_term(argument)).collect()),
+	}
+}

src/utils/output_predicates.rs

@@ -0,0 +1,127 @@
+fn formula_contains_predicate(formula: &foliage::Formula,
+	predicate_declaration: &foliage::PredicateDeclaration)
+	-> bool
+{
+	unimplemented!()
+}
+
+fn replace_predicate_in_formula<D>(formula: &mut foliage::Formula,
+	predicate_to_replace: &foliage::Predicate, replacement_formula: &foliage::Formula,
+	declarations: &D)
+where
+	D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain,
+{
+	use foliage::{Formula, Term};
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+			for mut argument in arguments
+			{
+				replace_predicate_in_formula(&mut argument, predicate_to_replace,
+					replacement_formula, declarations);
+			},
+		Formula::Boolean(_)
+		| Formula::Compare(_) => (),
+		Formula::Exists(quantified_expression)
+		| Formula::ForAll(quantified_expression) =>
+			replace_predicate_in_formula(&mut quantified_expression.argument, predicate_to_replace,
+				replacement_formula, declarations),
+		Formula::Implies(implies) =>
+		{
+			replace_predicate_in_formula(&mut implies.antecedent, predicate_to_replace,
+				replacement_formula, declarations);
+			replace_predicate_in_formula(&mut implies.implication, predicate_to_replace,
+				replacement_formula, declarations);
+		},
+		Formula::Not(argument) =>
+			replace_predicate_in_formula(argument, predicate_to_replace, replacement_formula,
+				declarations),
+		Formula::Predicate(predicate) =>
+			if predicate.declaration == predicate_to_replace.declaration
+			{
+				let mut replacement_formula =
+					crate::utils::copy_formula(replacement_formula, declarations);
+
+				for (index, argument) in predicate.arguments.iter().enumerate()
+				{
+					let variable_declaration = match &predicate_to_replace.arguments[index]
+					{
+						Term::Variable(variable) => &variable.declaration,
+						_ => panic!("invalid completed definition"),
+					};
+
+					crate::utils::replace_variable_in_formula_with_term(&mut replacement_formula,
+						&variable_declaration, argument);
+				}
+
+				*formula = replacement_formula;
+			},
+	}
+}
+
+pub(crate) fn replace_predicate_in_formula_with_completed_definition<D>(
+	formula: &mut foliage::Formula, completed_definition: &foliage::Formula, declarations: &D)
+	-> Result<(), crate::Error>
+where
+	D: crate::traits::VariableDeclarationDomain + crate::traits::AssignVariableDeclarationDomain,
+{
+	let false_ = foliage::Formula::false_();
+
+	// TODO: refactor
+	let (completed_definition_predicate, completed_definition) = match completed_definition
+	{
+		foliage::Formula::ForAll(quantified_expression) => match *quantified_expression.argument
+		{
+			foliage::Formula::IfAndOnlyIf(ref arguments) =>
+			{
+				assert_eq!(arguments.len(), 2, "invalid completed definition");
+
+				match arguments[0]
+				{
+					foliage::Formula::Predicate(ref predicate) => (predicate, &arguments[1]),
+					_ => panic!("invalid completed definition"),
+				}
+			},
+			foliage::Formula::Not(ref argument) => match **argument
+			{
+				foliage::Formula::Predicate(ref predicate) => (predicate, &false_),
+				_ => panic!("invalid completed definition"),
+			},
+			_ => panic!("invalid completed definition"),
+		},
+		foliage::Formula::IfAndOnlyIf(ref arguments) =>
+		{
+			assert_eq!(arguments.len(), 2, "invalid completed definition");
+
+			match arguments[0]
+			{
+				foliage::Formula::Predicate(ref predicate) => (predicate, &arguments[1]),
+				_ => panic!("invalid completed definition"),
+			}
+		},
+		foliage::Formula::Not(ref argument) => match **argument
+		{
+			foliage::Formula::Predicate(ref predicate) => (predicate, &false_),
+			_ => panic!("invalid completed definition"),
+		},
+		_ => panic!("invalid completed definition"),
+	};
+
+	// Predicates can only be substituted by their completed definitions if there is no cycle.
+	// For example, if the completed definition of p/1 references q/1 and vice versa, neither can
+	// be replaced with the completed definition of the other
+	/*if formula_contains_predicate(completed_definition, predicate_declaration)
+	{
+		return Err(crate::Error::new())
+	}*/
+
+	// TODO: detect cycles and warn accordingly
+
+	replace_predicate_in_formula(formula, completed_definition_predicate, completed_definition,
+		declarations);
+
+	Ok(())
+}