smtlib_syntax/
sorts.rs

1//! From the spec:
2//! > 3.5 Sorts
3//! > A major subset of the SMT-LIB language is the language of well-sorted terms, used to represent
4//! > logical expressions. Such terms are typed, or sorted in logical terminology; that is, each is
5//! > associated with a (unique) sort. The set of sorts consists itself of sort terms. In essence, a sort
6//! > term is a sort symbol, a sort parameter, or a sort symbol applied to a sequence of sort terms.
7//! > Syntactically, a sort symbol can be either the distinguished symbol Bool or any 〈identier 〉.
8//! > A sort parameter can be any 〈symbol 〉 (which in turn, is an 〈identier 〉).
9//! > ```
10//! > 〈sort〉 ::= 〈identier 〉 | ( 〈identier 〉 〈sort〉+ )
11//! > ```
12
13use std::fmt::Display;
14
15use super::{identifiers::Identifier, sexprs::Sexpr};
16
17#[derive(Debug, Clone)]
18pub struct Sort {
19    identifier: Identifier,
20    parameters: Vec<Sort>,
21}
22
23impl From<Sort> for Sexpr {
24    fn from(value: Sort) -> Self {
25        let Sort {
26            identifier,
27            parameters,
28        } = value;
29        if parameters.is_empty() {
30            identifier.into()
31        } else {
32            let mut elems: Vec<Sexpr> = vec![identifier.into()];
33            elems.extend(parameters.into_iter().map(|param| param.into()));
34            Sexpr::Sequence(elems)
35        }
36    }
37}
38
39impl Display for Sort {
40    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
41        if self.parameters.is_empty() {
42            self.identifier.fmt(f)
43        } else {
44            write!(f, "({id}", id = self.identifier)?;
45
46            for param in &self.parameters {
47                write!(f, " {param}")?;
48            }
49
50            write!(f, ")")
51        }
52    }
53}
smtlib_syntax/sorts.rs

smtlib_syntax/
sorts.rs
