|
|
|
@ -66,24 +66,40 @@ pub fn is_formula_statement_ignored(formula_statement: &crate::project::FormulaS
|
|
|
|
|
false |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
fn is_arithmetic_term(term: &foliage::Term) -> bool |
|
|
|
|
fn is_integer_input_constant(constant_name: &str, |
|
|
|
|
input_constants: &std::collections::HashSet<crate::project::InputConstantDeclaration>) -> bool |
|
|
|
|
{ |
|
|
|
|
let input_constant = crate::project::InputConstantDeclaration |
|
|
|
|
{ |
|
|
|
|
// TODO: avoid unnecessary allocation
|
|
|
|
|
name: constant_name.to_owned(), |
|
|
|
|
domain: foliage::Domain::Integer, |
|
|
|
|
}; |
|
|
|
|
|
|
|
|
|
input_constants.contains(&input_constant) |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
fn is_arithmetic_term(term: &foliage::Term, input_constants: &std::collections::HashSet<crate::project::InputConstantDeclaration>) -> bool |
|
|
|
|
{ |
|
|
|
|
match term |
|
|
|
|
{ |
|
|
|
|
foliage::Term::Infimum => false, |
|
|
|
|
foliage::Term::Supremum => false, |
|
|
|
|
foliage::Term::Integer(_) => true, |
|
|
|
|
foliage::Term::Symbolic(_) => false, |
|
|
|
|
foliage::Term::Symbolic(ref name) => |
|
|
|
|
{ |
|
|
|
|
is_integer_input_constant(name, input_constants) |
|
|
|
|
}, |
|
|
|
|
foliage::Term::String(_) => false, |
|
|
|
|
foliage::Term::Variable(ref declaration) => match declaration.domain |
|
|
|
|
{ |
|
|
|
|
foliage::Domain::Program => false, |
|
|
|
|
foliage::Domain::Integer => true, |
|
|
|
|
}, |
|
|
|
|
foliage::Term::Add(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right), |
|
|
|
|
foliage::Term::Subtract(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right), |
|
|
|
|
foliage::Term::Multiply(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right), |
|
|
|
|
foliage::Term::Negative(ref argument) => is_arithmetic_term(argument), |
|
|
|
|
foliage::Term::Add(ref left, ref right) => is_arithmetic_term(left, input_constants) && is_arithmetic_term(right, input_constants), |
|
|
|
|
foliage::Term::Subtract(ref left, ref right) => is_arithmetic_term(left, input_constants) && is_arithmetic_term(right, input_constants), |
|
|
|
|
foliage::Term::Multiply(ref left, ref right) => is_arithmetic_term(left, input_constants) && is_arithmetic_term(right, input_constants), |
|
|
|
|
foliage::Term::Negative(ref argument) => is_arithmetic_term(argument, input_constants), |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
@ -284,11 +300,16 @@ fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project)
|
|
|
|
|
struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration); |
|
|
|
|
struct PredicateDeclarationDisplay<'a>(&'a foliage::PredicateDeclaration); |
|
|
|
|
struct TermDisplay<'a>(&'a foliage::Term); |
|
|
|
|
struct FormulaDisplay<'a>(&'a foliage::Formula); |
|
|
|
|
struct FormulaStatementDisplay<'a> |
|
|
|
|
struct FormulaDisplay<'a, 'project> |
|
|
|
|
{ |
|
|
|
|
formula: &'a foliage::Formula, |
|
|
|
|
input_constants: &'project std::collections::HashSet<crate::project::InputConstantDeclaration>, |
|
|
|
|
} |
|
|
|
|
struct FormulaStatementDisplay<'a, 'project> |
|
|
|
|
{ |
|
|
|
|
formula_statement: &'a crate::project::FormulaStatement, |
|
|
|
|
proof_direction: crate::project::ProofDirection, |
|
|
|
|
input_constants: &'project std::collections::HashSet<crate::project::InputConstantDeclaration>, |
|
|
|
|
} |
|
|
|
|
pub struct ProjectDisplay<'a> |
|
|
|
|
{ |
|
|
|
@ -321,22 +342,26 @@ impl<'a> DisplayTPTP<'a, TermDisplay<'a>> for foliage::Term
|
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula |
|
|
|
|
fn display_formula_tptp<'a, 'project>(formula: &'a foliage::Formula, |
|
|
|
|
input_constants: &'project std::collections::HashSet<crate::project::InputConstantDeclaration>) |
|
|
|
|
-> FormulaDisplay<'a, 'project> |
|
|
|
|
{ |
|
|
|
|
fn display_tptp(&'a self) -> FormulaDisplay<'a> |
|
|
|
|
FormulaDisplay |
|
|
|
|
{ |
|
|
|
|
FormulaDisplay(self) |
|
|
|
|
formula, |
|
|
|
|
input_constants, |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
fn display_formula_statement_tptp<'a>(formula_statement: &'a crate::project::FormulaStatement, |
|
|
|
|
proof_direction: crate::project::ProofDirection) |
|
|
|
|
-> FormulaStatementDisplay<'a> |
|
|
|
|
fn display_formula_statement_tptp<'a, 'project>(formula_statement: &'a crate::project::FormulaStatement, |
|
|
|
|
proof_direction: crate::project::ProofDirection, input_constants: &'project std::collections::HashSet<crate::project::InputConstantDeclaration>,) |
|
|
|
|
-> FormulaStatementDisplay<'a, 'project> |
|
|
|
|
{ |
|
|
|
|
FormulaStatementDisplay |
|
|
|
|
{ |
|
|
|
|
formula_statement, |
|
|
|
|
proof_direction, |
|
|
|
|
input_constants, |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
@ -430,7 +455,7 @@ impl<'a> std::fmt::Display for TermDisplay<'a>
|
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
impl<'a> std::fmt::Debug for FormulaDisplay<'a> |
|
|
|
|
impl<'a, 'project> std::fmt::Debug for FormulaDisplay<'a, 'project> |
|
|
|
|
{ |
|
|
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result |
|
|
|
|
{ |
|
|
|
@ -448,8 +473,8 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
let mut notation = notation; |
|
|
|
|
let mut operator_identifier = operator_identifier; |
|
|
|
|
|
|
|
|
|
let left_is_arithmetic_term = is_arithmetic_term(left); |
|
|
|
|
let right_is_arithmetic_term = is_arithmetic_term(right); |
|
|
|
|
let left_is_arithmetic_term = is_arithmetic_term(left, self.input_constants); |
|
|
|
|
let right_is_arithmetic_term = is_arithmetic_term(right, self.input_constants); |
|
|
|
|
|
|
|
|
|
if let Some(operator_identifier_fallback) = operator_identifier_fallback |
|
|
|
|
{ |
|
|
|
@ -497,7 +522,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
write!(format, ")") |
|
|
|
|
}; |
|
|
|
|
|
|
|
|
|
match self.0 |
|
|
|
|
match self.formula |
|
|
|
|
{ |
|
|
|
|
foliage::Formula::Exists(ref exists) => |
|
|
|
|
{ |
|
|
|
@ -512,7 +537,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
separator = ", " |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
write!(format, "]: ({:?})", exists.argument.display_tptp()) |
|
|
|
|
write!(format, "]: ({:?})", display_formula_tptp(&exists.argument, self.input_constants)) |
|
|
|
|
}, |
|
|
|
|
foliage::Formula::ForAll(ref for_all) => |
|
|
|
|
{ |
|
|
|
@ -527,9 +552,9 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
separator = ", " |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
write!(format, "]: ({:?})", for_all.argument.display_tptp()) |
|
|
|
|
write!(format, "]: ({:?})", display_formula_tptp(&for_all.argument, self.input_constants)) |
|
|
|
|
}, |
|
|
|
|
foliage::Formula::Not(ref argument) => write!(format, "~({:?})", argument.display_tptp()), |
|
|
|
|
foliage::Formula::Not(ref argument) => write!(format, "~({:?})", display_formula_tptp(argument, self.input_constants)), |
|
|
|
|
foliage::Formula::And(ref arguments) => |
|
|
|
|
{ |
|
|
|
|
write!(format, "(")?; |
|
|
|
@ -538,7 +563,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
|
|
|
|
|
for argument in arguments |
|
|
|
|
{ |
|
|
|
|
write!(format, "{}{:?}", separator, argument.display_tptp())?; |
|
|
|
|
write!(format, "{}{:?}", separator, display_formula_tptp(argument, self.input_constants))?; |
|
|
|
|
|
|
|
|
|
separator = " & " |
|
|
|
|
} |
|
|
|
@ -553,7 +578,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
|
|
|
|
|
for argument in arguments |
|
|
|
|
{ |
|
|
|
|
write!(format, "{}{:?}", separator, argument.display_tptp())?; |
|
|
|
|
write!(format, "{}{:?}", separator, display_formula_tptp(argument, self.input_constants))?; |
|
|
|
|
|
|
|
|
|
separator = " | " |
|
|
|
|
} |
|
|
|
@ -562,10 +587,10 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
}, |
|
|
|
|
foliage::Formula::Implies(ref left, ref right, implication_direction) => match implication_direction |
|
|
|
|
{ |
|
|
|
|
foliage::ImplicationDirection::LeftToRight => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()), |
|
|
|
|
foliage::ImplicationDirection::RightToLeft => write!(format, "({:?} <= {:?})", left.display_tptp(), right.display_tptp()), |
|
|
|
|
foliage::ImplicationDirection::LeftToRight => write!(format, "({:?} => {:?})", display_formula_tptp(left, self.input_constants), display_formula_tptp(right, self.input_constants)), |
|
|
|
|
foliage::ImplicationDirection::RightToLeft => write!(format, "({:?} <= {:?})", display_formula_tptp(left, self.input_constants), display_formula_tptp(right, self.input_constants)), |
|
|
|
|
}, |
|
|
|
|
foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", left.display_tptp(), right.display_tptp()), |
|
|
|
|
foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", display_formula_tptp(left, self.input_constants), display_formula_tptp(right, self.input_constants)), |
|
|
|
|
foliage::Formula::Less(ref left, ref right) => display_comparison(Notation::Prefix, "$less", Some("p__less__"), left, right), |
|
|
|
|
foliage::Formula::LessOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$lesseq", Some("p__less_equal__"), left, right), |
|
|
|
|
foliage::Formula::Greater(ref left, ref right) => display_comparison(Notation::Prefix, "$greater", Some("p__greater__"), left, right), |
|
|
|
@ -590,7 +615,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
|
|
|
|
|
for argument in &predicate.arguments |
|
|
|
|
{ |
|
|
|
|
let argument_is_arithmetic_term = is_arithmetic_term(argument); |
|
|
|
|
let argument_is_arithmetic_term = is_arithmetic_term(argument, self.input_constants); |
|
|
|
|
|
|
|
|
|
write!(format, "{}", separator)?; |
|
|
|
|
|
|
|
|
@ -618,7 +643,7 @@ impl<'a> std::fmt::Debug for FormulaDisplay<'a>
|
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
impl<'a> std::fmt::Display for FormulaDisplay<'a> |
|
|
|
|
impl<'a, 'project> std::fmt::Display for FormulaDisplay<'a, 'project> |
|
|
|
|
{ |
|
|
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result |
|
|
|
|
{ |
|
|
|
@ -626,7 +651,7 @@ impl<'a> std::fmt::Display for FormulaDisplay<'a>
|
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
impl<'a> std::fmt::Debug for FormulaStatementDisplay<'a> |
|
|
|
|
impl<'a, 'project> std::fmt::Debug for FormulaStatementDisplay<'a, 'project> |
|
|
|
|
{ |
|
|
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result |
|
|
|
|
{ |
|
|
|
@ -657,11 +682,11 @@ impl<'a> std::fmt::Debug for FormulaStatementDisplay<'a>
|
|
|
|
|
panic!("expected formula statement to be either theorem, lemma, or axiom, please report to bug tracker"); |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
write!(format, ", {:?}).", self.formula_statement.formula.display_tptp()) |
|
|
|
|
write!(format, ", {:?}).", display_formula_tptp(&self.formula_statement.formula, self.input_constants)) |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
impl<'a> std::fmt::Display for FormulaStatementDisplay<'a> |
|
|
|
|
impl<'a, 'project> std::fmt::Display for FormulaStatementDisplay<'a, 'project> |
|
|
|
|
{ |
|
|
|
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result |
|
|
|
|
{ |
|
|
|
@ -704,7 +729,11 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a>
|
|
|
|
|
|
|
|
|
|
for symbolic_constant in symbolic_constants |
|
|
|
|
{ |
|
|
|
|
write!(format, "\ntff(type, type, {}: object).", symbolic_constant)?; |
|
|
|
|
match is_integer_input_constant(symbolic_constant, &self.project.input_constants) |
|
|
|
|
{ |
|
|
|
|
true => write!(format, "\ntff(type, type, {}: $int).", symbolic_constant)?, |
|
|
|
|
false => write!(format, "\ntff(type, type, {}: object).", symbolic_constant)?, |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
@ -732,12 +761,12 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a>
|
|
|
|
|
|
|
|
|
|
for axiom in axioms |
|
|
|
|
{ |
|
|
|
|
write!(format, "\n{}", display_formula_statement_tptp(&axiom, self.proof_direction))?; |
|
|
|
|
write!(format, "\n{}", display_formula_statement_tptp(&axiom, self.proof_direction, &self.project.input_constants))?; |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
write_title(format, "\n\n", "assertion")?; |
|
|
|
|
|
|
|
|
|
write!(format, "\n{}", display_formula_statement_tptp(&self.conjecture, self.proof_direction)) |
|
|
|
|
write!(format, "\n{}", display_formula_statement_tptp(&self.conjecture, self.proof_direction, &self.project.input_constants)) |
|
|
|
|
} |
|
|
|
|
} |
|
|
|
|
|
|
|
|
|