Skip to content

Commit

Permalink
formatting all variables with trailing _<SORT> for TPTP compliance (r…
Browse files Browse the repository at this point in the history 
…eplacing $i, $s convention)
  • Loading branch information
@ZachJHansen @teiesti
ZachJHansen authored and teiesti committed Nov 28, 2024
1 parent d53ef72 commit b77a2ce
Showing 1 changed file with 69 additions and 25 deletions.
94 changes: 69 additions & 25 deletions src/formatting/fol/tptp.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,8 @@ impl Display for Format<'_, IntegerTerm> {

Ok(())
}
IntegerTerm::Variable(v) => write!(f, "{v}$i"),
IntegerTerm::FunctionConstant(c) => write!(f, "{c}$i"),
IntegerTerm::Variable(v) => write!(f, "{v}_i"),
IntegerTerm::FunctionConstant(c) => write!(f, "{c}_i"),
IntegerTerm::UnaryOperation { op, arg } => {
let op = Format(op);
let arg = Format(arg.as_ref());
Expand All @@ -67,8 +67,8 @@ impl Display for Format<'_, SymbolicTerm> {
fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
match self.0 {
SymbolicTerm::Symbol(s) => write!(f, "{s}"),
SymbolicTerm::FunctionConstant(c) => write!(f, "{c}$s"),
SymbolicTerm::Variable(v) => write!(f, "{v}$s"),
SymbolicTerm::FunctionConstant(c) => write!(f, "{c}_s"),
SymbolicTerm::Variable(v) => write!(f, "{v}_s"),
}
}
}
Expand All @@ -78,8 +78,8 @@ impl Display for Format<'_, GeneralTerm> {
match self.0 {
GeneralTerm::Infimum => write!(f, "c__infimum__"),
GeneralTerm::Supremum => write!(f, "c__supremum__"),
GeneralTerm::FunctionConstant(c) => write!(f, "{c}$g"),
GeneralTerm::Variable(v) => write!(f, "{v}"),
GeneralTerm::FunctionConstant(c) => write!(f, "{c}_g"),
GeneralTerm::Variable(v) => write!(f, "{v}_g"),
GeneralTerm::IntegerTerm(t) => write!(f, "f__integer__({})", Format(t)),
GeneralTerm::SymbolicTerm(t) => write!(f, "f__symbolic__({})", Format(t)),
}
Expand Down Expand Up @@ -206,9 +206,9 @@ impl Display for Format<'_, FunctionConstant> {
let sort = &self.0.sort;

match sort {
Sort::General => write!(f, "{name}$g"),
Sort::Integer => write!(f, "{name}$i"),
Sort::Symbol => write!(f, "{name}$s"),
Sort::General => write!(f, "{name}_g"),
Sort::Integer => write!(f, "{name}_i"),
Sort::Symbol => write!(f, "{name}_s"),
}
}
}
Expand All @@ -219,9 +219,9 @@ impl Display for Format<'_, Variable> {
let sort = &self.0.sort;

match sort {
Sort::General => write!(f, "{name}"),
Sort::Integer => write!(f, "{name}$i"),
Sort::Symbol => write!(f, "{name}$s"),
Sort::General => write!(f, "{name}_g"),
Sort::Integer => write!(f, "{name}_i"),
Sort::Symbol => write!(f, "{name}_s"),
}
}
}
Expand Down Expand Up @@ -337,7 +337,7 @@ mod tests {
);
assert_eq!(
Format(&IntegerTerm::Variable("A".into())).to_string(),
"A$i"
"A_i"
);
assert_eq!(
Format(&IntegerTerm::BinaryOperation {
Expand All @@ -355,7 +355,7 @@ mod tests {
rhs: IntegerTerm::Variable("N".into()).into(),
})
.to_string(),
"$sum(10, N$i)"
"$sum(10, N_i)"
);
assert_eq!(
Format(&IntegerTerm::BinaryOperation {
Expand All @@ -368,7 +368,7 @@ mod tests {
.into(),
})
.to_string(),
"$difference($uminus(195), $uminus(N$i))"
"$difference($uminus(195), $uminus(N_i))"
);
}

Expand All @@ -377,7 +377,7 @@ mod tests {
assert_eq!(Format(&SymbolicTerm::Symbol("p".into())).to_string(), "p");
assert_eq!(
Format(&SymbolicTerm::Variable("X".into())).to_string(),
"X$s"
"X_s"
)
}

Expand All @@ -387,7 +387,7 @@ mod tests {
assert_eq!(Format(&GeneralTerm::Supremum).to_string(), "c__supremum__");
assert_eq!(
Format(&GeneralTerm::Variable("N1".into())).to_string(),
"N1"
"N1_g"
);
assert_eq!(
Format(&GeneralTerm::SymbolicTerm(SymbolicTerm::Symbol("p".into()))).to_string(),
Expand All @@ -414,7 +414,7 @@ mod tests {
]
})
.to_string(),
"prime(f__integer__($sum(N1$i, 3)), f__integer__(5))"
"prime(f__integer__($sum(N1_i, 3)), f__integer__(5))"
)
}

Expand Down Expand Up @@ -511,7 +511,7 @@ mod tests {
]
})
.to_string(),
"$less(1, 2) & p__less__(f__integer__(2), X)"
"$less(1, 2) & p__less__(f__integer__(2), X_g)"
);
assert_eq!(
Format(&Comparison {
Expand All @@ -522,7 +522,7 @@ mod tests {
},]
})
.to_string(),
"$less(1, N$i)"
"$less(1, N_i)"
);
assert_eq!(
Format(&Comparison {
Expand All @@ -534,7 +534,7 @@ mod tests {
})
.to_string(),
// "f__symbolic__(a) = f__symbolic__(B$s)"
"a = B$s"
"a = B_s"
);
assert_eq!(
Format(&Comparison {
Expand All @@ -545,7 +545,7 @@ mod tests {
},]
})
.to_string(),
"p__less__(f__symbolic__(a), f__symbolic__(B$s))"
"p__less__(f__symbolic__(a), f__symbolic__(B_s))"
);
}

Expand All @@ -566,7 +566,7 @@ mod tests {
]
})
.to_string(),
"![X1$i: $int, N2: general]"
"![X1_i: $int, N2_g: general]"
);
assert_eq!(
Format(&Quantification {
Expand All @@ -577,7 +577,7 @@ mod tests {
},]
})
.to_string(),
"?[X1$s: symbol]"
"?[X1_s: symbol]"
);
}

Expand Down Expand Up @@ -648,7 +648,51 @@ mod tests {
.into()
})
.to_string(),
"![X$i: $int, Y1: general]: (p & q)"
"![X_i: $int, Y1_g: general]: (p & q)"
);
assert_eq!(
Format(&Formula::QuantifiedFormula {
quantification: Quantification {
quantifier: Quantifier::Forall,
variables: vec![
Variable {
name: "X_i".into(),
sort: Sort::Symbol,
},
Variable {
name: "X".into(),
sort: Sort::Integer,
},
Variable {
name: "Y1".into(),
sort: Sort::General,
},
]
},
formula: Formula::BinaryFormula {
connective: BinaryConnective::Conjunction,
lhs: Formula::BinaryFormula {
connective: BinaryConnective::Conjunction,
lhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
predicate_symbol: "p".into(),
terms: vec![GeneralTerm::IntegerTerm(IntegerTerm::Variable("X".to_string()))],
}))
.into(),
rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
predicate_symbol: "q".into(),
terms: vec![GeneralTerm::Variable("Y1".to_string())],
}))
.into(),
}.into(),
rhs: Formula::AtomicFormula(AtomicFormula::Atom(Atom {
predicate_symbol: "t".into(),
terms: vec![GeneralTerm::SymbolicTerm(SymbolicTerm::Variable("X_i".into()))],
}))
.into(),
}.into()
})
.to_string(),
"![X_i_s: symbol, X_i: $int, Y1_g: general]: (p(f__integer__(X_i)) & q(Y1_g) & t(f__symbolic__(X_i_s)))"
);
}
}

0 comments on commit b77a2ce

Please sign in to comment.