smtlib_lowlevel/
ast_ext.rs

1use crate::{ast, lexicon};
2
3impl<'st> From<&'st str> for lexicon::Symbol<'st> {
4    fn from(s: &'st str) -> Self {
5        lexicon::Symbol(s)
6    }
7}
8
9impl<'st> ast::Identifier<'st> {
10    pub const fn simple(s: &'st str) -> Self {
11        ast::Identifier::Simple(lexicon::Symbol(s))
12    }
13    pub const fn indexed(s: &'st str, index: &'st [ast::Index<'st>]) -> Self {
14        ast::Identifier::Indexed(lexicon::Symbol(s), index)
15    }
16}
17
18impl<'st> ast::Sort<'st> {
19    pub const fn new_simple(name: &'st str) -> Self {
20        ast::Sort::Sort(ast::Identifier::simple(name))
21    }
22    pub const fn new_indexed(name: &'st str, index: &'st [ast::Index<'st>]) -> Self {
23        ast::Sort::Sort(ast::Identifier::Indexed(lexicon::Symbol(name), index))
24    }
25    pub const fn new_simple_parametric(name: &'st str, parameters: &'st [ast::Sort<'st>]) -> Self {
26        ast::Sort::Parametric(ast::Identifier::simple(name), parameters)
27    }
28    pub const fn new_indexed_parametric(
29        name: &'st str,
30        index: &'st [ast::Index<'st>],
31        parameters: &'st [ast::Sort<'st>],
32    ) -> Self {
33        ast::Sort::Parametric(
34            ast::Identifier::Indexed(lexicon::Symbol(name), index),
35            parameters,
36        )
37    }
38}
smtlib_lowlevel/ast_ext.rs

smtlib_lowlevel/
ast_ext.rs
