use nom::
{
	IResult,
	bytes::complete::{take_while, take_while_m_n, is_not},
	character::complete::{digit1, multispace0},
	sequence::{preceded, delimited, pair},
	combinator::{map, map_res},
	multi::{many0, separated_list},
	branch::alt,
	bytes::complete::tag,
};

struct Declarations
{
	//function_declarations:,
	//predicate_declarations:,
	variable_declaration_stack: VariableDeclarationStack,
}

enum TermOperator
{
	Add,
	Subtract,
	Multiply,
}

fn infimum<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	map
	(
		delimited(multispace0, tag("#inf"), multispace0),
		|_| crate::Term::SpecialInteger(crate::SpecialInteger::Infimum)
	)(i)
}

fn supremum<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	map
	(
		delimited(multispace0, tag("#sup"), multispace0),
		|_| crate::Term::SpecialInteger(crate::SpecialInteger::Supremum)
	)(i)
}

fn integer<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	map
	(
		map_res
		(
			delimited(multispace0, digit1, multispace0),
			std::str::FromStr::from_str
		),
		crate::Term::Integer
	)(i)
}

fn is_lowercase_alphanumeric(c: char) -> bool
{
	c.is_alphanumeric() && c.is_lowercase()
}

fn symbolic_identifier<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, String>
{
	let (i, symbolic_identifier) = map
	(
		pair
		(
			take_while_m_n(1, 1, is_lowercase_alphanumeric),
			take_while(char::is_alphanumeric)
		),
		|(s0, s1)| format!("{}{}", s0, s1)
	)(i)?;

	Ok((i, symbolic_identifier))
}

fn symbolic<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	map
	(
		delimited(multispace0, |i| symbolic_identifier(i, declarations), multispace0),
		crate::Term::Symbolic
	)(i)
}

fn string<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	map
	(
		delimited
		(
			multispace0,
			delimited
			(
				tag("\""),
				is_not("\""),
				tag("\""),
			),
			multispace0
		),
		|s: &str| crate::Term::String(s.to_string())
	)(i)
}

fn variable_identifier<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, String>
{
	map
	(
		delimited
		(
			multispace0,
			preceded
			(
				take_while_m_n(1, 1, |c| char::is_alphabetic(c) && char::is_uppercase(c)),
				take_while(char::is_alphanumeric)
			),
			multispace0
		),
		|s: &str| s.to_string()
	)(i)
}

fn variable_declaration<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::VariableDeclaration>
{
	map
	(
		|i| variable_identifier(i, declarations),
		|s| crate::VariableDeclaration{name: s},
	)(i)
}

fn program_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	map
	(
		|i| program_variable_identifier(i, declarations),
		|s|
		{
			let declaration = declarations.variable_declaration_stack.get(s.as_ref());

			crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program})
		},
	)(i)
}

fn integer_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	map
	(
		|i| integer_variable_identifier,
		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}),
	)(i)
}

fn variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	alt
	((
		|i| program_variable(i, declarations),
		|i| integer_variable(i, declarations),
	))(i)
}

fn predicate_0_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		delimited(multispace0, symbolic_identifier, multispace0),
		|name| crate::Formula::Predicate(
			crate::Predicate
			{
				declaration:
					crate::PredicateDeclaration
					{
						name: name,
						arity: 0,
					},
				arguments: vec![],
			})
	)(i)
}

fn predicate_n_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			delimited(multispace0, symbolic_identifier, multispace0),
			delimited
			(
				multispace0,
				delimited
				(
					tag("("),
					separated_list(tag(","), term),
					tag(")")
				),
				multispace0
			)
		),
		|(name, arguments)| crate::Formula::Predicate(
				crate::Predicate
				{
					declaration:
						crate::PredicateDeclaration
						{
							name: name,
							arity: arguments.len(),
						},
					arguments: arguments,
				})
	)(i)
}

fn predicate<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		predicate_n_ary,
		predicate_0_ary
	))(i)
}

fn boolean<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		delimited
		(
			multispace0,
			alt
			((
				map(tag("#true"), |_| true),
				map(tag("#false"), |_| false)
			)),
			multispace0
		),
		|value| crate::Formula::Boolean(value)
	)(i)
}

fn less<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			term,
			preceded(tag("<"), term)
		),
		|(left, right)| crate::Formula::Less(left, right)
	)(i)
}

fn less_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			term,
			preceded(tag("<="), term)
		),
		|(left, right)| crate::Formula::LessOrEqual(left, right)
	)(i)
}

fn greater<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			term,
			preceded(tag(">"), term)
		),
		|(left, right)| crate::Formula::Greater(left, right)
	)(i)
}

fn greater_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			term,
			preceded(tag(">="), term)
		),
		|(left, right)| crate::Formula::GreaterOrEqual(left, right)
	)(i)
}

fn equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			term,
			preceded(tag("="), term)
		),
		|(left, right)| crate::Formula::Equal(left, right)
	)(i)
}

fn not_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			term,
			preceded(tag("!="), term)
		),
		|(left, right)| crate::Formula::NotEqual(left, right)
	)(i)
}

fn comparison<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		less,
		less_or_equal,
		greater,
		greater_or_equal,
		equal,
		not_equal
	))(i)
}

fn term_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	delimited
	(
		multispace0,
		delimited
		(
			tag("("),
			term,
			tag(")")
		),
		multispace0
	)(i)
}

fn fold_terms(initial: crate::Term, remainder: Vec<(TermOperator, crate::Term)>) -> crate::Term
{
	remainder.into_iter().fold(initial,
		|accumulator, pair|
		{
			let (term_operator, term) = pair;

			match term_operator
			{
				TermOperator::Add => crate::Term::Add(Box::new(accumulator), Box::new(term)),
				TermOperator::Subtract => crate::Term::Subtract(Box::new(accumulator), Box::new(term)),
				TermOperator::Multiply => crate::Term::Multiply(Box::new(accumulator), Box::new(term)),
			}
		})
}

fn term_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	alt
	((
		infimum,
		supremum,
		integer,
		symbolic,
		string,
		variable,
		term_parenthesized
	))(i)
}

fn term_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	alt
	((
		map
		(
			delimited
			(
				multispace0,
				preceded(tag("-"), term_precedence_0),
				multispace0
			),
			|term| crate::Term::Negative(Box::new(term))
		),
		term_precedence_0
	))(i)
}

fn term_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	let (i, initial) = term_precedence_1(i)?;
	let (i, remainder) =
		many0
		(
			|i|
			{
				let (i, term) = preceded(tag("*"), term_precedence_1)(i)?;
				Ok((i, (TermOperator::Multiply, term)))
			}
		)(i)?;

	Ok((i, fold_terms(initial, remainder)))
}

fn term_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	let (i, initial) = term_precedence_2(i)?;
	let (i, remainder) =
		many0
		(
			alt
			((
				|i|
				{
					let (i, term) = preceded(tag("+"), term_precedence_2)(i)?;
					Ok((i, (TermOperator::Add, term)))
				},
				|i|
				{
					let (i, term) = preceded(tag("-"), term_precedence_2)(i)?;
					Ok((i, (TermOperator::Subtract, term)))
				}
			))
		)(i)?;

	Ok((i, fold_terms(initial, remainder)))
}

pub fn term<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
{
	term_precedence_3(i)
}

fn formula_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	delimited
	(
		multispace0,
		delimited
		(
			tag("("),
			formula,
			tag(")")
		),
		multispace0
	)(i)
}

fn formula_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		comparison,
		predicate,
		boolean,
		formula_parenthesized
	))(i)
}

fn exists<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		delimited
		(
			multispace0,
			preceded
			(
				tag("exists "),
				pair
				(
					separated_list
					(
						tag(","),
						variable_declaration
					),
					formula_precedence_1
				)
			),
			multispace0
		),
		|(parameters, argument)| crate::Formula::Exists(
			crate::Exists
			{
				parameters: parameters,
				argument: Box::new(argument),
			})
	)(i)
}

fn for_all<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		delimited
		(
			multispace0,
			preceded
			(
				tag("forall "),
				pair
				(
					separated_list
					(
						tag(","),
						variable_declaration
					),
					formula_precedence_1
				)
			),
			multispace0
		),
		|(parameters, argument)| crate::Formula::ForAll(
			crate::ForAll
			{
				parameters: parameters,
				argument: Box::new(argument),
			})
	)(i)
}

fn formula_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		exists,
		for_all,
		formula_precedence_0
	))(i)
}

fn formula_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		map
		(
			delimited
			(
				multispace0,
				preceded(tag("not "), formula_precedence_1),
				multispace0
			),
			|argument| crate::Formula::Not(Box::new(argument))
		),
		formula_precedence_1
	))(i)
}

fn formula_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		map_res
		(
			separated_list(tag("and"), map(formula_precedence_2, |argument| Box::new(argument))),
			|arguments|
				match arguments.len()
				{
					// TODO: improve error handling
					0 | 1 => Err(nom::Err::Error("")),
					_ => Ok(crate::Formula::And(arguments)),
				}
		),
		formula_precedence_2
	))(i)
}

fn formula_precedence_4<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		map_res
		(
			separated_list(tag("or"), map(formula_precedence_3, |argument| Box::new(argument))),
			|arguments|
				match arguments.len()
				{
					// TODO: improve error handling
					0 | 1 => Err(nom::Err::Error("")),
					_ => Ok(crate::Formula::Or(arguments)),
				}
		),
		formula_precedence_3
	))(i)
}

fn formula_precedence_5<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	let (i, left) = formula_precedence_4(i)?;

	match preceded(tag("->"), formula_precedence_4)(i)
	{
		Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right)))),
		Err(_) => Ok((i, left)),
	}
}

fn formula_precedence_6<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	let (i, left) = formula_precedence_5(i)?;

	match preceded(tag("<->"), formula_precedence_5)(i)
	{
		Ok((i, right)) => Ok((i, crate::Formula::Biconditional(Box::new(left), Box::new(right)))),
		Err(_) => Ok((i, left)),
	}
}

pub fn formula<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
{
	formula_precedence_6(i)
}

pub fn formulas<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, Vec<crate::Formula>>
{
	many0(formula)(i)
}

#[cfg(test)]
mod tests
{
	#[test]
	fn parse_integer()
	{
		assert_eq!(crate::term("12345"), Ok(("", crate::Term::Integer(12345))));
	}

	#[test]
	fn parse_variable_declaration()
	{
		assert_eq!(crate::term(" X5 "), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))));
		assert_eq!(crate::term(" NX3 "), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))));
	}

	#[test]
	fn parse_variable()
	{
		assert_eq!(crate::term("X5"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))));
		assert_eq!(crate::term("NX3"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))));
	}

	#[test]
	fn parse_string()
	{
		assert_eq!(crate::term(" \"foobar\" "), Ok(("", crate::Term::String("foobar".to_string()))));
	}

	#[test]
	fn parse_boolean()
	{
		assert_eq!(crate::formula(" #true "), Ok(("", crate::Formula::Boolean(true))));
		assert_eq!(crate::formula(" #false "), Ok(("", crate::Formula::Boolean(false))));
	}

	#[test]
	fn parse_term()
	{
		assert_eq!(crate::term(" 5 + 3"), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Integer(3)),
			))));

		assert_eq!(crate::term(" -5"), Ok(("",
				crate::Term::Negative
				(
					Box::new(crate::Term::Integer(5))
				)
			)));

		assert_eq!(crate::term(" 5+3 * -(9+ 1)  + 2 "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Add
				(
					Box::new(crate::Term::Integer(5)),
					Box::new(crate::Term::Multiply
					(
						Box::new(crate::Term::Integer(3)),
						Box::new(crate::Term::Negative
						(
							Box::new(crate::Term::Add
							(
								Box::new(crate::Term::Integer(9)),
								Box::new(crate::Term::Integer(1)),
							))
						)),
					)),
				)),
				Box::new(crate::Term::Integer(2)),
			))));

		assert_eq!(crate::term(" 5 + a "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Symbolic("a".to_string())),
			))));

		assert_eq!(crate::term(" 5 + #sup "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Supremum),
			))));

		assert_eq!(crate::term(" 5 + #inf "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Infimum),
			))));

		assert_eq!(crate::term(" 5 + \" text \" "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::String(" text ".to_string())),
			))));

		assert_eq!(crate::term(" 5 + X1 "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "1".to_string()})),
			))));
	}

	#[test]
	fn parse_predicate()
	{
		assert_eq!(crate::formula(" p "), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]}))));

		assert_eq!(crate::formula(" p(5, 6, 7) "), Ok(("",
			crate::Formula::Predicate
			(
				crate::Predicate
				{
					declaration:
						crate::PredicateDeclaration
						{
							name: "p".to_string(),
							arity: 3,
						},
					arguments:
						vec!
						[
							crate::Term::Integer(5),
							crate::Term::Integer(6),
							crate::Term::Integer(7),
						],
				}
			))));

		assert_eq!(crate::formula(" p(1, 3+4*5+6, \"test\") "), Ok(("",
			crate::Formula::Predicate
			(
				crate::Predicate
				{
					declaration:
						crate::PredicateDeclaration
						{
							name: "p".to_string(),
							arity: 3,
						},
					arguments:
						vec!
						[
							crate::Term::Integer(1),
							crate::Term::Add
							(
								Box::new(crate::Term::Add
								(
									Box::new(crate::Term::Integer(3)),
									Box::new(crate::Term::Multiply
									(
										Box::new(crate::Term::Integer(4)),
										Box::new(crate::Term::Integer(5)),
									)),
								)),
								Box::new(crate::Term::Integer(6)),
							),
							crate::Term::String("test".to_string()),
						],
				}
			))));
	}

	#[test]
	fn parse_comparison()
	{
		assert_eq!(crate::formula("5 + 9 < #sup"), Ok(("",
			crate::Formula::Less
			(
				crate::Term::Add
				(
					Box::new(crate::Term::Integer(5)),
					Box::new(crate::Term::Integer(9)),
				),
				crate::Term::Supremum,
			))));

		assert_eq!(crate::formula("#inf != 6 * 9"), Ok(("",
			crate::Formula::NotEqual
			(
				crate::Term::Infimum,
				crate::Term::Multiply
				(
					Box::new(crate::Term::Integer(6)),
					Box::new(crate::Term::Integer(9)),
				),
			))));

		assert_eq!(crate::formula("n = 5"), Ok(("",
			crate::Formula::Equal
			(
				crate::Term::Symbolic("n".to_string()),
				crate::Term::Integer(5),
			))));
	}

	#[test]
	fn formula()
	{
		assert_eq!(crate::formula("p(1, a) or q(2)"), Ok(("",
			crate::Formula::Or
			(
				vec!
				[
					Box::new(crate::Formula::Predicate
					(
						crate::Predicate
						{
							declaration:
								crate::PredicateDeclaration
								{
									name: "p".to_string(),
									arity: 2,
								},
							arguments:
								vec!
								[
									crate::Term::Integer(1),
									crate::Term::Symbolic("a".to_string()),
								],
						}
					)),
					Box::new(crate::Formula::Predicate
					(
						crate::Predicate
						{
							declaration:
								crate::PredicateDeclaration
								{
									name: "q".to_string(),
									arity: 1,
								},
							arguments:
								vec!
								[
									crate::Term::Integer(2),
								],
						}
					)),
				]
			))));

		assert_eq!(crate::formula("#inf < 5 and p(1, a) or q(2)"), Ok(("",
			crate::Formula::Or
			(
				vec!
				[
					Box::new(crate::Formula::And
					(
						vec!
						[
							Box::new(crate::Formula::Less
							(
								crate::Term::Infimum,
								crate::Term::Integer(5),
							)),
							Box::new(crate::Formula::Predicate
							(
								crate::Predicate
								{
									declaration:
										crate::PredicateDeclaration
										{
											name: "p".to_string(),
											arity: 2,
										},
									arguments:
										vec!
										[
											crate::Term::Integer(1),
											crate::Term::Symbolic("a".to_string()),
										],
								}
							)),
						]
					)),
					Box::new(crate::Formula::Predicate
					(
						crate::Predicate
						{
							declaration:
								crate::PredicateDeclaration
								{
									name: "q".to_string(),
									arity: 1,
								},
							arguments:
								vec!
								[
									crate::Term::Integer(2),
								],
						}
					)),
				]
			))));

		assert_eq!(crate::formula("#inf < 5 and p(1, a) or q(2) -> #false"), Ok(("",
			crate::Formula::Implies
			(
				Box::new(crate::Formula::Or
				(
					vec!
					[
						Box::new(crate::Formula::And
						(
							vec!
							[
								Box::new(crate::Formula::Less
								(
									crate::Term::Infimum,
									crate::Term::Integer(5),
								)),
								Box::new(crate::Formula::Predicate
								(
									crate::Predicate
									{
										declaration:
											crate::PredicateDeclaration
											{
												name: "p".to_string(),
												arity: 2,
											},
										arguments:
											vec!
											[
												crate::Term::Integer(1),
												crate::Term::Symbolic("a".to_string()),
											],
									}
								)),
							]
						)),
						Box::new(crate::Formula::Predicate
						(
							crate::Predicate
							{
								declaration:
									crate::PredicateDeclaration
									{
										name: "q".to_string(),
										arity: 1,
									},
								arguments:
									vec!
									[
										crate::Term::Integer(2),
									],
							}
						)),
					]
				)),
				Box::new(crate::Formula::Boolean(false)),
			))));

		assert_eq!(crate::formula(" not #true"), Ok(("",
			crate::Formula::Not(Box::new(crate::Formula::Boolean(true))))));

		assert_eq!(crate::formula("exists X forall N1 p(1, 2) and #false"), Ok(("",
			crate::Formula::And
			(
				vec!
				[
					Box::new(crate::Formula::Exists
					(
						crate::Exists
						{
							parameters: vec![crate::VariableDeclaration{name: "".to_string(), domain: crate::Domain::Program}],
							argument:
								Box::new(crate::Formula::ForAll
								(
									crate::ForAll
									{
										parameters: vec![crate::VariableDeclaration{name: "1".to_string(), domain: crate::Domain::Integer}],
										argument:
											Box::new(crate::Formula::Predicate
											(
												crate::Predicate
												{
													declaration:
														crate::PredicateDeclaration
														{
															name: "p".to_string(),
															arity: 2,
														},
													arguments:
														vec!
														[
															crate::Term::Integer(1),
															crate::Term::Integer(2),
														],
												}
											)),
									}
								)),
						}
					)),
					Box::new(crate::Formula::Boolean(false)),
				]
			))));

		assert_eq!(crate::formula("exists X forall N1 (p(1, 2) and #false)"), Ok(("",
			crate::Formula::Exists
			(
				crate::Exists
				{
					parameters: vec![crate::VariableDeclaration{name: "".to_string(), domain: crate::Domain::Program}],
					argument:
						Box::new(crate::Formula::ForAll
						(
							crate::ForAll
							{
								parameters: vec![crate::VariableDeclaration{name: "1".to_string(), domain: crate::Domain::Integer}],
								argument:
									Box::new(crate::Formula::And
									(
										vec!
										[
											Box::new(crate::Formula::Predicate
											(
												crate::Predicate
												{
													declaration:
														crate::PredicateDeclaration
														{
															name: "p".to_string(),
															arity: 2,
														},
													arguments:
														vec!
														[
															crate::Term::Integer(1),
															crate::Term::Integer(2),
														],
												}
											)),
											Box::new(crate::Formula::Boolean(false)),
										]
									)),
							}
						)),
				}
			))));
	}
}