From 0714bed2cc10a09d0a800c2c7f5334eadfbdec4d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sun, 2 Feb 2020 20:27:30 +0100 Subject: [PATCH] Start supporting TPTP output --- src/lib.rs | 1 + src/output.rs | 1 + src/output/tptp.rs | 251 +++++++++++++++++++++++++++++ src/translate/verify_properties.rs | 8 +- 4 files changed, 258 insertions(+), 3 deletions(-) create mode 100644 src/output.rs create mode 100644 src/output/tptp.rs diff --git a/src/lib.rs b/src/lib.rs index 947a9ed..6c457ec 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,7 @@ #![feature(trait_alias)] pub mod error; +pub(crate) mod output; pub mod translate; pub use error::Error; diff --git a/src/output.rs b/src/output.rs new file mode 100644 index 0000000..09538d1 --- /dev/null +++ b/src/output.rs @@ -0,0 +1 @@ +pub(crate) mod tptp; diff --git a/src/output/tptp.rs b/src/output/tptp.rs new file mode 100644 index 0000000..4c5a847 --- /dev/null +++ b/src/output/tptp.rs @@ -0,0 +1,251 @@ +pub(crate) struct VariableDeclarationDisplay<'a> +{ + variable_declaration: &'a foliage::VariableDeclaration, +} + +pub(crate) struct TermDisplay<'a> +{ + term: &'a foliage::Term, +} + +pub(crate) struct FormulaDisplay<'a> +{ + formula: &'a foliage::Formula, +} + +pub(crate) fn display_variable_declaration<'a>(variable_declaration: &'a foliage::VariableDeclaration) + -> VariableDeclarationDisplay<'a> +{ + VariableDeclarationDisplay + { + variable_declaration, + } +} + +pub(crate) fn display_term<'a>(term: &'a foliage::Term) -> TermDisplay<'a> +{ + TermDisplay + { + term, + } +} + +pub(crate) fn display_formula<'a>(formula: &'a foliage::Formula) + -> FormulaDisplay<'a> +{ + FormulaDisplay + { + formula, + } +} + +impl<'a> std::fmt::Debug for VariableDeclarationDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{}", &self.variable_declaration.name) + } +} + +impl<'a> std::fmt::Display for VariableDeclarationDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", &self) + } +} + +impl<'a> std::fmt::Debug for TermDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + 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() + { + true => write!(format, "$uminus({})", -value), + false => write!(format, "{}", 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) => + { + write!(format, "{}", function.declaration.name)?; + + assert!(function.declaration.arity == function.arguments.len(), + "function has a different number of arguments than declared (expected {}, got {})", + function.declaration.arity, function.arguments.len()); + + if function.arguments.len() > 0 + { + write!(format, "{}(", function.declaration.name)?; + + let mut separator = ""; + + for argument in &function.arguments + { + write!(format, "{}{:?}", separator, display_term(&argument))?; + + separator = ", "; + } + + write!(format, ")")?; + } + + 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"), + } + } +} + +impl<'term> std::fmt::Display for TermDisplay<'term> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", self) + } +} + +impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match &self.formula + { + foliage::Formula::Exists(exists) => + { + write!(format, "?[")?; + + let mut separator = ""; + + for parameter in exists.parameters.iter() + { + write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?; + + separator = ", " + } + + write!(format, "]: {:?}", display_formula(&exists.argument))?; + }, + foliage::Formula::ForAll(for_all) => + { + write!(format, "![")?; + + let mut separator = ""; + + for parameter in for_all.parameters.iter() + { + write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?; + + separator = ", " + } + + write!(format, "]: {:?}", display_formula(&for_all.argument))?; + }, + foliage::Formula::Not(argument) => write!(format, "~{:?}", display_formula(argument))?, + foliage::Formula::And(arguments) => + { + write!(format, "(")?; + + let mut separator = ""; + + assert!(!arguments.is_empty()); + + for argument in arguments + { + write!(format, "{}{:?}", separator, display_formula(argument))?; + + separator = " & " + } + + write!(format, ")")?; + }, + foliage::Formula::Or(arguments) => + { + write!(format, "(")?; + + let mut separator = ""; + + assert!(!arguments.is_empty()); + + for argument in arguments + { + write!(format, "{}{:?}", separator, display_formula(argument))?; + + separator = " | " + } + + write!(format, ")")?; + }, + foliage::Formula::Implies(foliage::Implies{antecedent, implication}) + => write!(format, "({:?} => {:?})", display_formula(antecedent), display_formula(implication))?, + foliage::Formula::IfAndOnlyIf(foliage::IfAndOnlyIf{left, right}) + => write!(format, "({:?} <=> {:?})", display_formula(left), display_formula(right))?, + foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right}) + => write!(format, "$less({:?}, {:?})", display_term(left), display_term(right))?, + foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::LessOrEqual, left, right}) + => write!(format, "$lesseq({:?}, {:?})", display_term(left), display_term(right))?, + foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Greater, left, right}) + => write!(format, "$greater({:?}, {:?})", display_term(left), display_term(right))?, + foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::GreaterOrEqual, left, right}) + => write!(format, "$greatereq({:?}, {:?})", display_term(left), display_term(right))?, + foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Equal, left, right}) + => write!(format, "({:?} = {:?})", display_term(left), display_term(right))?, + foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::NotEqual, left, right}) + => write!(format, "({:?} ~= {:?})", display_term(left), display_term(right))?, + foliage::Formula::Boolean(true) => write!(format, "$true")?, + foliage::Formula::Boolean(false) => write!(format, "$false")?, + foliage::Formula::Predicate(predicate) => + { + write!(format, "{}", predicate.declaration.name)?; + + if !predicate.arguments.is_empty() + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in &predicate.arguments + { + write!(format, "{}{:?}", separator, display_term(argument))?; + + separator = ", " + } + + write!(format, ")")?; + } + }, + } + + Ok(()) + } +} + +impl<'formula> std::fmt::Display for FormulaDisplay<'formula> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", self) + } +} diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index 1b94720..5a85bab 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -179,13 +179,15 @@ where for (predicate_declaration, completed_definition) in completed_definitions { - println!("completion({}/{}): {}.", predicate_declaration.name, - predicate_declaration.arity, completed_definition); + println!("tff(completion_{}_{}, axiom, {}).", predicate_declaration.name, + predicate_declaration.arity, + crate::output::tptp::display_formula(&completed_definition)); } for integrity_constraint in integrity_constraints { - println!("axiom: {}.", integrity_constraint); + println!("tff(integrity_constraint, axiom, {}).", + crate::output::tptp::display_formula(&integrity_constraint)); } Ok(())