smtlib_syntax/
identifiers.rs

1//! From the spec:
2//! > 3.3 Identifiers
3//! >
4//! > Identifiers are used mostly as function and sort symbols. When defining certain SMT-LIB
5//! > theories it is convenient to have indexed identifiers as well. Instead of having a special token
6//! > syntax for that, indexed identifiers are defined more systematically as the application of the
7//! > reserved word _ to a symbol and one or more indices. Indices can be numerals or symbols.(8)
8//! > ```
9//! >  〈index 〉      ::= 〈numeral 〉 | 〈symbol 〉
10//! >  〈identifier 〉 ::= 〈symbol 〉 | ( _ 〈symbol 〉 〈index 〉+ )
11//! > ```
12
13use std::fmt::Display;
14
15use super::{
16    lexicon::{Reserved, Symbol},
17    sexprs::{Sexpr, SpecialConstant::Numeral},
18};
19
20#[derive(Debug, Clone)]
21pub enum Index {
22    Numeral(i64),
23    Symbol(Symbol),
24}
25
26impl From<Index> for Sexpr {
27    fn from(value: Index) -> Self {
28        match value {
29            Index::Numeral(num) => Sexpr::SpecialConstant(Numeral(num)),
30            Index::Symbol(sym) => Sexpr::Symbol(sym),
31        }
32    }
33}
34
35impl Display for Index {
36    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
37        match self {
38            Index::Numeral(num) => num.fmt(f),
39            Index::Symbol(sym) => sym.fmt(f),
40        }
41    }
42}
43
44#[derive(Debug, Clone)]
45pub struct Identifier {
46    symbol: Symbol,
47    indexes: Vec<Index>,
48}
49
50impl From<Identifier> for Sexpr {
51    fn from(value: Identifier) -> Self {
52        let Identifier { symbol, indexes } = value;
53        if indexes.is_empty() {
54            Sexpr::Symbol(symbol)
55        } else {
56            let mut elems = vec![Sexpr::Reserved(Reserved::Underscore), Sexpr::Symbol(symbol)];
57
58            elems.extend(indexes.into_iter().map(|index| index.into()));
59
60            Sexpr::Sequence(elems)
61        }
62    }
63}
64
65impl Display for Identifier {
66    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
67        if self.indexes.is_empty() {
68            self.symbol.fmt(f)
69        } else {
70            write!(f, "(_ {sym}", sym = self.symbol)?;
71
72            for index in &self.indexes {
73                write!(f, " {index}")?;
74            }
75
76            write!(f, ")")
77        }
78    }
79}
smtlib_syntax/identifiers.rs

smtlib_syntax/
identifiers.rs
