smtlib_syntax/
terms.rs

1use std::fmt::Display;
2
3use super::identifiers::Identifier;
4use super::lexicon::{Reserved, Symbol};
5use super::sexprs::{Sexpr, SpecialConstant};
6use super::sorts::Sort;
7
8#[derive(Debug, Clone)]
9pub struct QualifiedIdentifier(Identifier, Option<Sort>);
10impl From<QualifiedIdentifier> for super::sexprs::Sexpr {
11    fn from(value: QualifiedIdentifier) -> Self {
12        let QualifiedIdentifier(id, sort) = value;
13
14        match sort {
15            Some(sort) => {
16                Sexpr::Sequence(vec![Sexpr::Reserved(Reserved::As), id.into(), sort.into()])
17            }
18            None => id.into(),
19        }
20    }
21}
22impl Display for QualifiedIdentifier {
23    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
24        let QualifiedIdentifier(id, sort) = self;
25
26        match sort {
27            Some(sort) => write!(f, "(as {id} {sort})"),
28            None => write!(f, "{id}"),
29        }
30    }
31}
32
33#[derive(Debug, Clone)]
34pub struct VarBinding(Symbol, Term);
35
36impl From<VarBinding> for Sexpr {
37    fn from(value: VarBinding) -> Self {
38        let VarBinding(name, term) = value;
39
40        Sexpr::Sequence(vec![name.into(), term.into()])
41    }
42}
43
44#[derive(Debug, Clone)]
45pub struct SortedVar(Symbol, Sort);
46
47impl From<SortedVar> for Sexpr {
48    fn from(value: SortedVar) -> Self {
49        let SortedVar(name, sort) = value;
50
51        Sexpr::Sequence(vec![name.into(), sort.into()])
52    }
53}
54
55#[derive(Debug, Clone)]
56pub enum Term {
57    SpecialConstant(SpecialConstant),
58    QualifiedIdentifier(QualifiedIdentifier),
59    Application(QualifiedIdentifier, Vec<Term>),
60    Let(Vec<VarBinding>, Box<Term>),
61    Forall(Vec<SortedVar>, Box<Term>),
62    Exists(Vec<SortedVar>, Box<Term>),
63    // TODO:
64    // - match
65    // - ! (term attributes)
66}
67
68impl From<Term> for Sexpr {
69    fn from(value: Term) -> Self {
70        match value {
71            Term::SpecialConstant(sc) => sc.into(),
72            Term::QualifiedIdentifier(qi) => qi.into(),
73            Term::Application(name, args) => Sexpr::Sequence({
74                vec![name.into()]
75                    .into_iter()
76                    .chain(args.into_iter().map(|e| e.into()))
77                    .collect()
78            }),
79            Term::Let(bindings, body) => Sexpr::Sequence(vec![
80                Reserved::Let.into(),
81                Sexpr::Sequence(bindings.into_iter().map(|e| e.into()).collect()),
82                (*body).into(),
83            ]),
84            Term::Forall(quants, body) => Sexpr::Sequence(vec![
85                Reserved::Forall.into(),
86                Sexpr::Sequence(quants.into_iter().map(|e| e.into()).collect()),
87                (*body).into(),
88            ]),
89            Term::Exists(quants, body) => Sexpr::Sequence(vec![
90                Reserved::Exists.into(),
91                Sexpr::Sequence(quants.into_iter().map(|e| e.into()).collect()),
92                (*body).into(),
93            ]),
94        }
95    }
96}
smtlib_syntax/terms.rs

smtlib_syntax/
terms.rs
