smtlib/
sorts.rs

1//! SMT sorts.
2//!
3//! From SMT-LIB reference:
4//!
5//! > A major subset of the SMT-LIB language is the language of well-sorted
6//! > terms, used to represent logical expressions. Such terms are typed, or
7//! > sorted in logical terminology; that is, each is associated with a (unique)
8//! > sort. The set of sorts consists itself of sort terms. In essence, a sort
9//! > term is a sort symbol, a sort parameter, or a sort symbol applied to a
10//! > sequence of sort terms.
11
12use itertools::Itertools;
13use smtlib_lowlevel::{
14    ast::{self, Identifier},
15    lexicon::{Numeral, Symbol},
16    Storage,
17};
18
19use crate::terms::{self, qual_ident, STerm};
20
21/// A SMT-LIB sort.
22#[derive(Debug, Clone, Copy, PartialEq, Eq)]
23pub enum Sort<'st> {
24    /// A built-in sort.
25    Static(ast::Sort<'st>),
26    /// A user-defined sort.
27    Dynamic {
28        /// smtlib storage
29        st: &'st Storage,
30        /// The name of the sort.
31        name: &'st str,
32        /// The index of the sort.
33        index: &'st [Index<'st>],
34        /// The parameters of the sort.
35        parameters: &'st [Sort<'st>],
36    },
37}
38
39impl std::fmt::Display for Sort<'_> {
40    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
41        self.ast().fmt(f)
42    }
43}
44
45impl<'st> From<ast::Sort<'st>> for Sort<'st> {
46    fn from(sort: ast::Sort<'st>) -> Self {
47        Sort::Static(sort)
48    }
49}
50
51/// An index of a sort.
52#[derive(Debug, Clone, Copy, PartialEq, Eq)]
53pub enum Index<'st> {
54    /// A numeral index.
55    Numeral(usize),
56    /// A symbol index.
57    Symbol(&'st str),
58}
59
60impl<'st> Index<'st> {
61    fn ast(&self) -> ast::Index<'st> {
62        match self {
63            Index::Numeral(n) => ast::Index::Numeral(Numeral::from_usize(*n)),
64            Index::Symbol(s) => ast::Index::Symbol(Symbol(s)),
65        }
66    }
67}
68
69pub(crate) fn is_built_in_sort(name: &str) -> bool {
70    matches!(name, "Int" | "Bool" | "Array" | "BitVec")
71}
72
73impl<'st> Sort<'st> {
74    /// Create a new dynamic sort.
75    pub fn new(st: &'st Storage, name: impl Into<String>) -> Self {
76        let mut name = name.into();
77        if !is_built_in_sort(&name) {
78            // HACK: how should we handle this? or should we event handle it?
79            name += "_xxx";
80        }
81        let name = st.alloc_str(&name);
82        Self::Dynamic {
83            st,
84            name,
85            index: &[],
86            parameters: &[],
87        }
88    }
89    /// Create a new dynamic sort with parameters.
90    pub fn new_parametric(
91        st: &'st Storage,
92        name: impl Into<String>,
93        parameters: &[Sort<'st>],
94    ) -> Self {
95        Self::Dynamic {
96            st,
97            name: st.alloc_str(&name.into()),
98            index: &[],
99            parameters: st.alloc_slice(parameters),
100        }
101    }
102    /// Create a new dynamic sort with index.
103    pub fn new_indexed(st: &'st Storage, name: impl Into<String>, index: &[Index<'st>]) -> Self {
104        Self::Dynamic {
105            st,
106            name: st.alloc_str(&name.into()),
107            index: st.alloc_slice(index),
108            parameters: &[],
109        }
110    }
111
112    /// Get the smtlib AST representation of the sort.
113    pub fn ast(self) -> ast::Sort<'st> {
114        match self {
115            Sort::Static(sort) => sort,
116            Sort::Dynamic {
117                st,
118                name,
119                index,
120                parameters,
121            } => {
122                let ident = if index.is_empty() {
123                    Identifier::Simple(Symbol(name))
124                } else {
125                    Identifier::Indexed(
126                        Symbol(name),
127                        st.alloc_slice(&index.iter().map(|idx| idx.ast()).collect_vec()),
128                    )
129                };
130                if parameters.is_empty() {
131                    ast::Sort::Sort(ident)
132                } else {
133                    ast::Sort::Parametric(
134                        ident,
135                        st.alloc_slice(&parameters.iter().map(|param| param.ast()).collect_vec()),
136                    )
137                }
138            }
139        }
140    }
141
142    /// Create a new constant of this sort.
143    pub fn new_const(
144        &self,
145        st: &'st Storage,
146        name: impl Into<String>,
147    ) -> terms::Const<'st, terms::Dynamic<'st>> {
148        let name = st.alloc_str(&name.into());
149        terms::Const(
150            name,
151            terms::Dynamic::from_term_sort(
152                STerm::new(
153                    st,
154                    ast::Term::Identifier(qual_ident(name, Some(self.ast()))),
155                ),
156                *self,
157            ),
158        )
159    }
160}
smtlib/sorts.rs

smtlib/
sorts.rs
