in smt2parser/src/concrete.rs [1189:1268]
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
use Term::*;
match self {
Constant(c) => {
// ⟨spec_constant⟩
write!(f, "{}", c)
}
QualIdentifier(id) => {
// ⟨qual_identifier⟩
write!(f, "{}", id)
}
Application {
qual_identifier,
arguments,
} => {
// ( ⟨qual_identifier ⟩ ⟨term⟩+ )
write!(f, "({} {})", qual_identifier, arguments.iter().format(" "))
}
Let { var_bindings, term } => {
// ( let ( ⟨var_binding⟩+ ) ⟨term⟩ )
write!(
f,
"(let ({}) {})",
var_bindings
.iter()
.format_with(" ", |(v, t), f| f(&format_args!("({} {})", v, t))),
term
)
}
Forall { vars, term } => {
// ( forall ( ⟨sorted_var⟩+ ) ⟨term⟩ )
write!(
f,
"(forall ({}) {})",
vars.iter()
.format_with(" ", |(v, s), f| f(&format_args!("({} {})", v, s))),
term
)
}
Exists { vars, term } => {
// ( exists ( ⟨sorted_var⟩+ ) ⟨term⟩ )
write!(
f,
"(exists ({}) {})",
vars.iter()
.format_with(" ", |(v, s), f| f(&format_args!("({} {})", v, s))),
term
)
}
Match { term, cases } => {
// ( match ⟨term⟩ ( ⟨match_case⟩+ ) )
write!(
f,
"(match {} ({}))",
term,
cases.iter().format_with(" ", |(pattern, term), f| {
if pattern.len() == 1 {
f(&format_args!("({} {})", &pattern[0], term))
} else {
f(&format_args!("(({}) {})", pattern.iter().format(" "), term))
}
})
)
}
Attributes { term, attributes } => {
// ( ! ⟨term⟩ ⟨attribute⟩+ )
write!(
f,
"(! {} {})",
term,
attributes
.iter()
.format_with(" ", |(key, value), f| match value {
AttributeValue::None => f(key),
_ => f(&format_args!("{} {}", key, value)),
})
)
}
}
}