Make all terms compatible in TPTP

src/output/tptp.rs

@@ -210,7 +210,8 @@ where
 
 impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C>
 where
-	C: crate::traits::VariableDeclarationDomain
+	C: crate::traits::InputConstantDeclarationDomain
+		+ crate::traits::VariableDeclarationDomain
 		+ crate::traits::VariableDeclarationID
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
@@ -220,6 +221,59 @@ where
 		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)
+				.expect("could not determine whether term is arithmetic");
+			let is_right_term_arithmetic = crate::is_term_arithmetic(right, self.context)
+				.expect("could not determine whether term is arithmetic");
+
+			match (!is_left_term_arithmetic && !is_right_term_arithmetic,
+				auxiliary_predicate_name)
+			{
+				(true, Some(auxiliary_predicate_name)) =>
+				{
+					notation = crate::OperatorNotation::Prefix;
+					operation_identifier = auxiliary_predicate_name;
+				},
+				_ => (),
+			}
+
+			if notation == crate::OperatorNotation::Prefix
+			{
+				write!(format, "{}(", 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))?,
+			}
+
+			match notation
+			{
+				crate::OperatorNotation::Prefix => write!(format, ", ")?,
+				crate::OperatorNotation::Infix => write!(format, " {} ", 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))?,
+			}
+
+			if notation == crate::OperatorNotation::Prefix
+			{
+				write!(format, ")")?;
+			}
+
+			write!(format, ")")
+		};
+
 		match &self.formula
 		{
 			foliage::Formula::Exists(exists) =>
@@ -299,19 +353,30 @@ where
 				=> write!(format, "({:?} => {:?})", display_formula(antecedent),
 					display_formula(implication))?,
 			foliage::Formula::IfAndOnlyIf(foliage::IfAndOnlyIf{left, right})
-				=> write!(format, "({:?} <=> {:?})", display_formula(left), display_formula(right))?,
+				=> write!(format, "({:?} <=> {:?})", display_formula(left),
-			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right})
+					display_formula(right))?,
-				=> write!(format, "$less({:?}, {:?})", display_term(left), display_term(right))?,
+			foliage::Formula::Compare(
-			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::LessOrEqual, left, right})
+				foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right})
-				=> write!(format, "$lesseq({:?}, {:?})", display_term(left), display_term(right))?,
+				=> display_compare(left, right, crate::OperatorNotation::Prefix, "$less",
-			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Greater, left, right})
+					Some("p__less__"))?,
-				=> write!(format, "$greater({:?}, {:?})", display_term(left), display_term(right))?,
+			foliage::Formula::Compare(
-			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::GreaterOrEqual, left, right})
+				foliage::Compare{operator: foliage::ComparisonOperator::LessOrEqual, left, right})
-				=> write!(format, "$greatereq({:?}, {:?})", display_term(left), display_term(right))?,
+				=> display_compare(left, right, crate::OperatorNotation::Prefix, "$lesseq",
-			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Equal, left, right})
+					Some("p__less_equal__"))?,
-				=> write!(format, "({:?} = {:?})", display_term(left), display_term(right))?,
+			foliage::Formula::Compare(
-			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::NotEqual, left, right})
+				foliage::Compare{operator: foliage::ComparisonOperator::Greater, left, right})
-				=> write!(format, "({:?} ~= {:?})", display_term(left), display_term(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",
+					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) =>
@@ -342,7 +407,8 @@ where
 
 impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C>
 where
-	C: crate::traits::VariableDeclarationDomain
+	C: crate::traits::InputConstantDeclarationDomain
+		+ crate::traits::VariableDeclarationDomain
 		+ crate::traits::VariableDeclarationID
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result

src/traits.rs

@@ -1,3 +1,10 @@
+pub(crate) trait InputConstantDeclarationDomain
+{
+	fn input_constant_declaration_domain(&self,
+		declaration: &std::rc::Rc<foliage::FunctionDeclaration>)
+		-> Option<crate::Domain>;
+}
+
 pub(crate) trait AssignVariableDeclarationDomain
 {
 	fn assign_variable_declaration_domain(&self,

src/translate/verify_properties.rs

@@ -195,8 +195,8 @@ where
 			for (predicate_declaration, completed_definition) in completed_definitions
 			{
 				println!("tff(completion_{}_{}, axiom, {}).", predicate_declaration.name,
-					predicate_declaration.arity, crate::output::human_readable::display_formula(
+					predicate_declaration.arity, crate::output::tptp::display_formula(
-						&completed_definition, None, &context));
+						&completed_definition, &context));
 			}
 
 			if !context.integrity_constraints.borrow().is_empty()
@@ -207,8 +207,7 @@ where
 			for integrity_constraint in context.integrity_constraints.borrow().iter()
 			{
 				println!("tff(integrity_constraint, axiom, {}).",
-					crate::output::human_readable::display_formula(&integrity_constraint, None,
+					crate::output::tptp::display_formula(&integrity_constraint, &context));
-						&context));
 			}
 		},
 	}

src/translate/verify_properties/context.rs

@@ -4,6 +4,9 @@ pub(crate) struct Definitions
 	pub definitions: Vec<crate::ScopedFormula>,
 }
 
+type InputConstantDeclarationDomains
+	= std::collections::BTreeMap<std::rc::Rc<foliage::FunctionDeclaration>, crate::Domain>;
+
 type VariableDeclarationDomains
 	= std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>;
 
@@ -16,6 +19,7 @@ pub(crate) struct Context
 		std::rc::Rc<foliage::PredicateDeclaration>, Definitions>>,
 	pub integrity_constraints: std::cell::RefCell<foliage::Formulas>,
 
+	pub input_constant_declaration_domains: std::cell::RefCell<InputConstantDeclarationDomains>,
 	pub function_declarations: std::cell::RefCell<foliage::FunctionDeclarations>,
 	pub predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
 	pub variable_declaration_stack: std::cell::RefCell<foliage::VariableDeclarationStack>,
@@ -32,15 +36,31 @@ impl Context
 			definitions: std::cell::RefCell::new(std::collections::BTreeMap::<_, _>::new()),
 			integrity_constraints: std::cell::RefCell::new(vec![]),
 
+			input_constant_declaration_domains:
+				std::cell::RefCell::new(InputConstantDeclarationDomains::new()),
 			function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()),
 			predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
-			variable_declaration_stack: std::cell::RefCell::new(foliage::VariableDeclarationStack::new()),
+			variable_declaration_stack:
-			variable_declaration_domains: std::cell::RefCell::new(VariableDeclarationDomains::new()),
+				std::cell::RefCell::new(foliage::VariableDeclarationStack::new()),
+			variable_declaration_domains:
+				std::cell::RefCell::new(VariableDeclarationDomains::new()),
 			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>)
+		-> Option<crate::Domain>
+	{
+		let input_constant_declaration_domains = self.input_constant_declaration_domains.borrow();
+
+		input_constant_declaration_domains.get(declaration).map(|x| *x)
+	}
+}
+
 impl crate::traits::GetOrCreateFunctionDeclaration for Context
 {
 	fn get_or_create_function_declaration(&self, name: &str, arity: usize)

src/utils.rs

@@ -1,4 +1,15 @@
-#[derive(Clone, Copy, Debug, PartialEq)]
+mod arithmetic_terms;
+
+pub(crate) use arithmetic_terms::*;
+
+#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
+pub(crate) enum OperatorNotation
+{
+	Prefix,
+	Infix,
+}
+
+#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
 pub(crate) enum Domain
 {
 	Program,

src/utils/arithmetic_terms.rs

@@ -0,0 +1,39 @@
+pub(crate) fn is_term_arithmetic<C>(term: &foliage::Term, context: &C) -> Result<bool, crate::Error>
+where
+	C: crate::traits::InputConstantDeclarationDomain
+		+ crate::traits::VariableDeclarationDomain
+{
+	match term
+	{
+		foliage::Term::Boolean(_)
+		| foliage::Term::SpecialInteger(_)
+		| foliage::Term::String(_)
+			=> Ok(false),
+		foliage::Term::Integer(_) => Ok(true),
+		foliage::Term::Function(ref function) =>
+		{
+			if !function.arguments.is_empty()
+			{
+				return Err(
+					crate::Error::new_unsupported_language_feature("functions with arguments"));
+			}
+
+			// Assume the program domain if not specified otherwise
+			let domain = context.input_constant_declaration_domain(&function.declaration)
+				.unwrap_or(crate::Domain::Program);
+
+			Ok(domain == crate::Domain::Integer)
+		},
+		foliage::Term::Variable(foliage::Variable{ref declaration}) =>
+			match context.variable_declaration_domain(declaration)
+			{
+				Some(crate::Domain::Program) => Ok(false),
+				Some(crate::Domain::Integer) => Ok(true),
+				None => Err(crate::Error::new_logic("unspecified variable declaration domain")),
+			},
+		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),
+	}
+}