smtlib_syntax/
scripts.rs

1use super::lexicon::{Keyword, Reserved, StringConstant, Symbol};
2use super::sexprs::Sexpr;
3use super::sorts::Sort;
4use super::terms::{SortedVar, Term};
5
6#[derive(Clone, Debug)]
7pub struct SortDec(pub Symbol, pub i64);
8
9impl From<SortDec> for Sexpr {
10    fn from(value: SortDec) -> Self {
11        let SortDec(symbol, numeral) = value;
12        Sexpr::Sequence(vec![symbol.into(), numeral.into()])
13    }
14}
15
16#[derive(Clone, Debug)]
17pub struct SelectorDec {
18    pub name: Symbol,
19    pub sort: Sort,
20}
21
22impl From<SelectorDec> for Sexpr {
23    fn from(value: SelectorDec) -> Self {
24        let SelectorDec { name, sort } = value;
25        Sexpr::Sequence(vec![name.into(), sort.into()])
26    }
27}
28
29#[derive(Clone, Debug)]
30pub struct ConstructorDec {
31    pub name: Symbol,
32    pub selectors: Vec<SelectorDec>,
33}
34
35impl From<ConstructorDec> for Sexpr {
36    fn from(value: ConstructorDec) -> Self {
37        let ConstructorDec { name, selectors } = value;
38        Sexpr::Sequence(
39            vec![name.into()]
40                .into_iter()
41                .chain(selectors.into_iter().map(|sel_dec| sel_dec.into()))
42                .collect(),
43        )
44    }
45}
46
47#[derive(Clone, Debug)]
48pub struct DatatypeDec {
49    par: Vec<Symbol>,
50    constructors: Vec<ConstructorDec>,
51}
52
53impl From<DatatypeDec> for Sexpr {
54    fn from(value: DatatypeDec) -> Self {
55        let DatatypeDec { par, constructors } = value;
56        if par.is_empty() {
57            Sexpr::Sequence(
58                constructors
59                    .into_iter()
60                    .map(|sel_dec| sel_dec.into())
61                    .collect(),
62            )
63        } else {
64            todo!()
65        }
66    }
67}
68
69#[derive(Clone, Debug)]
70pub struct FunctionDec {
71    name: Symbol,
72    args: Vec<SortedVar>,
73    sort: Sort,
74}
75
76impl From<FunctionDec> for Sexpr {
77    fn from(value: FunctionDec) -> Self {
78        let FunctionDec { name, args, sort } = value;
79
80        Sexpr::Sequence(vec![
81            name.into(),
82            Sexpr::Sequence(args.into_iter().map(|arg| arg.into()).collect()),
83            sort.into(),
84        ])
85    }
86}
87
88#[derive(Clone, Debug)]
89pub struct FunctionDef {
90    name: Symbol,
91    args: Vec<SortedVar>,
92    sort: Sort,
93    body: Term,
94}
95
96impl From<FunctionDef> for Vec<Sexpr> {
97    fn from(value: FunctionDef) -> Self {
98        let FunctionDef {
99            name,
100            args,
101            sort,
102            body,
103        } = value;
104
105        vec![
106            name.into(),
107            Sexpr::Sequence(args.into_iter().map(|arg| arg.into()).collect()),
108            sort.into(),
109            body.into(),
110        ]
111    }
112}
113
114#[derive(Clone, Debug)]
115pub struct PropLiteral {
116    negate: bool,
117    symbol: Symbol,
118}
119
120impl From<PropLiteral> for Sexpr {
121    fn from(value: PropLiteral) -> Self {
122        let PropLiteral { negate, symbol } = value;
123        if negate {
124            Sexpr::Sequence(vec![
125                Symbol::new("not".to_string()).unwrap().into(),
126                symbol.into(),
127            ])
128        } else {
129            symbol.into()
130        }
131    }
132}
133
134#[derive(Debug, Clone)]
135pub enum CommandType {
136    Assert,
137    CheckSat,
138    CheckSatAssuming,
139    DeclareConst,
140    DeclareDatatype,
141    DeclareDatatypes,
142    DeclareFun,
143    DeclareSort,
144    DefineFun,
145    DefineFunRec,
146    DefineFunsRec,
147    DefineSort,
148    Echo,
149    Exit,
150    GetAssertions,
151    GetAssignment,
152    //GetInfo
153    GetModel,
154    GetOption,
155    GetProof,
156    GetUnsatAssumptions,
157    GetUnsatCore,
158    GetValue,
159    Pop,
160    Push,
161    Reset,
162    ResetAssertions,
163    //SetInfo
164    SetLogic,
165    //SetOption /* not implemented */
166}
167
168impl From<CommandType> for Reserved {
169    fn from(value: CommandType) -> Self {
170        Reserved::Command(value)
171    }
172}
173
174impl From<CommandType> for Sexpr {
175    fn from(value: CommandType) -> Self {
176        let r: Reserved = value.into();
177        r.into()
178    }
179}
180
181#[derive(Debug, Clone)]
182pub enum Command {
183    Assert(Term),
184    CheckSat,
185    CheckSatAssuming(Vec<PropLiteral>),
186    DeclareConst(Symbol, Sort),
187    DeclareDatatype(Symbol, DatatypeDec),
188    DeclareDatatypes(Vec<(SortDec, DatatypeDec)>),
189    DeclareFun(Symbol, Vec<Sort>, Sort),
190    DeclareSort(Symbol, i64),
191    DefineFun(FunctionDef),
192    DefineFunRec(FunctionDef),
193    DefineFunsRec(Vec<(FunctionDec, Term)>),
194    DefineSort(Symbol, Vec<Symbol>, Sort),
195    Echo(StringConstant),
196    Exit,
197    GetAssertions,
198    GetAssignment,
199    //GetInfo(InfoFlag /* not implementd */),
200    GetModel,
201    GetOption(Keyword),
202    GetProof,
203    GetUnsatAssumptions,
204    GetUnsatCore,
205    GetValue(Vec<Term>),
206    Pop(i64),
207    Push(i64),
208    Reset,
209    ResetAssertions,
210    //SetInfo( /* not implemented */)
211    SetLogic(Symbol),
212    //SetOption(Option) /* not implemented */
213}
214
215fn to_seq<S: Into<Sexpr>>(items: Vec<S>) -> Sexpr {
216    Sexpr::Sequence(items.into_iter().map(|prop| prop.into()).collect())
217}
218
219impl From<Command> for Sexpr {
220    fn from(value: Command) -> Self {
221        let command_type = value.command_type();
222        let inner = match value {
223            Command::Exit
224            | Command::GetAssertions
225            | Command::GetAssignment
226            | Command::GetModel
227            | Command::GetProof
228            | Command::GetUnsatAssumptions
229            | Command::GetUnsatCore
230            | Command::Reset
231            | Command::ResetAssertions
232            | Command::CheckSat => vec![command_type.into()],
233            Command::Assert(term) => vec![command_type.into(), term.into()],
234            Command::CheckSatAssuming(props) => {
235                let props = to_seq(props);
236                vec![command_type.into(), props]
237            }
238            Command::DeclareConst(name, sort) => {
239                vec![command_type.into(), name.into(), sort.into()]
240            }
241            Command::DeclareDatatype(name, datatype_dec) => {
242                vec![command_type.into(), name.into(), datatype_dec.into()]
243            }
244            Command::DeclareDatatypes(entries) => {
245                let count = entries.len();
246                let (sort_decs, datatype_decs) = entries.into_iter().fold(
247                    (Vec::with_capacity(count), Vec::with_capacity(count)),
248                    |mut acc, (sort_dec, datatype_dec)| {
249                        acc.0.push(sort_dec.into());
250                        acc.1.push(datatype_dec.into());
251                        acc
252                    },
253                );
254
255                let sort_decs = Sexpr::Sequence(sort_decs);
256                let datatype_decs = Sexpr::Sequence(datatype_decs);
257
258                vec![command_type.into(), sort_decs, datatype_decs]
259            }
260            Command::DeclareFun(name, arg_sorts, ret_sort) => {
261                let arg_sorts = to_seq(arg_sorts);
262                vec![command_type.into(), name.into(), arg_sorts, ret_sort.into()]
263            }
264            Command::DeclareSort(name, num) => {
265                vec![command_type.into(), name.into(), num.into()]
266            }
267            Command::DefineFun(fun_def) | Command::DefineFunRec(fun_def) => {
268                let fun_def_sexprs: Vec<Sexpr> = fun_def.into();
269                vec![command_type.into()]
270                    .into_iter()
271                    .chain(fun_def_sexprs.into_iter())
272                    .collect()
273            }
274            Command::DefineFunsRec(entries) => {
275                let count = entries.len();
276                let (fun_decs, terms) = entries.into_iter().fold(
277                    (Vec::with_capacity(count), Vec::with_capacity(count)),
278                    |mut acc, (fun_dec, term)| {
279                        acc.0.push(fun_dec.into());
280                        acc.1.push(term.into());
281                        acc
282                    },
283                );
284
285                let fun_decs = Sexpr::Sequence(fun_decs);
286                let terms = Sexpr::Sequence(terms);
287
288                vec![command_type.into(), fun_decs, terms]
289            }
290            Command::DefineSort(name, syms, sort) => {
291                vec![command_type.into(), name.into(), to_seq(syms), sort.into()]
292            }
293            Command::Echo(string) => vec![command_type.into(), string.into()],
294            Command::GetOption(kw) => vec![command_type.into(), kw.into()],
295            Command::GetValue(terms) => vec![command_type.into(), to_seq(terms)],
296            Command::Pop(num) | Command::Push(num) => vec![command_type.into(), num.into()],
297            Command::SetLogic(sym) => vec![command_type.into(), sym.into()],
298        };
299
300        Sexpr::Sequence(inner)
301    }
302}
303
304impl Command {
305    fn command_type(&self) -> CommandType {
306        match self {
307            Command::Assert(_) => CommandType::Assert,
308            Command::CheckSat => CommandType::CheckSat,
309            Command::CheckSatAssuming(_) => CommandType::CheckSatAssuming,
310            Command::DeclareConst(_, _) => CommandType::DeclareConst,
311            Command::DeclareDatatype(_, _) => CommandType::DeclareDatatype,
312            Command::DeclareDatatypes(_) => CommandType::DeclareDatatypes,
313            Command::DeclareFun(_, _, _) => CommandType::DeclareFun,
314            Command::DeclareSort(_, _) => CommandType::DeclareSort,
315            Command::DefineFun(_) => CommandType::DefineFun,
316            Command::DefineFunRec(_) => CommandType::DefineFunRec,
317            Command::DefineFunsRec(_) => CommandType::DefineFunsRec,
318            Command::DefineSort(_, _, _) => CommandType::DefineSort,
319            Command::Echo(_) => CommandType::Echo,
320            Command::Exit => CommandType::Exit,
321            Command::GetAssertions => CommandType::GetAssertions,
322            Command::GetAssignment => CommandType::GetAssignment,
323            Command::GetModel => CommandType::GetModel,
324            Command::GetOption(_) => CommandType::GetOption,
325            Command::GetProof => CommandType::GetProof,
326            Command::GetUnsatAssumptions => CommandType::GetUnsatAssumptions,
327            Command::GetUnsatCore => CommandType::GetUnsatCore,
328            Command::GetValue(_) => CommandType::GetValue,
329            Command::Pop(_) => CommandType::Pop,
330            Command::Push(_) => CommandType::Push,
331            Command::Reset => CommandType::Reset,
332            Command::ResetAssertions => CommandType::ResetAssertions,
333            Command::SetLogic(_) => CommandType::SetLogic,
334        }
335    }
336}
337
338pub struct Script(pub Vec<Command>);
smtlib_syntax/scripts.rs

smtlib_syntax/
scripts.rs
