smtlib-lowlevel 0.1.1

A low-level API for interacting with SMT solvers
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350

---
source: lowlevel/src/tests.rs
expression: "Script::parse(include_str!(\"../../examples/bubble_sort.smt2\"))"
---
Ok(Script([
  DeclareConst(Symbol("dim"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("A0"), Parametric(Simple(Symbol("Array")), [
    Sort(Simple(Symbol("Int"))),
    Sort(Simple(Symbol("Int"))),
  ])),
  DeclareConst(Symbol("A1"), Parametric(Simple(Symbol("Array")), [
    Sort(Simple(Symbol("Int"))),
    Sort(Simple(Symbol("Int"))),
  ])),
  DeclareConst(Symbol("A2"), Parametric(Simple(Symbol("Array")), [
    Sort(Simple(Symbol("Int"))),
    Sort(Simple(Symbol("Int"))),
  ])),
  DeclareConst(Symbol("A3"), Parametric(Simple(Symbol("Array")), [
    Sort(Simple(Symbol("Int"))),
    Sort(Simple(Symbol("Int"))),
  ])),
  DeclareConst(Symbol("i0"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("i1"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("i2"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("i3"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("j0"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("j1"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("j2"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("j3"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("tmp0"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("tmp1"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("tmp2"), Sort(Simple(Symbol("Int")))),
  DeclareConst(Symbol("l0"), Parametric(Simple(Symbol("List")), [
    Sort(Simple(Symbol("Int"))),
  ])),
  DeclareConst(Symbol("l1"), Parametric(Simple(Symbol("List")), [
    Sort(Simple(Symbol("Int"))),
  ])),
  DeclareConst(Symbol("l2"), Parametric(Simple(Symbol("List")), [
    Sort(Simple(Symbol("Int"))),
  ])),
  DeclareConst(Symbol("l3"), Parametric(Simple(Symbol("List")), [
    Sort(Simple(Symbol("Int"))),
  ])),
  DeclareConst(Symbol("l4"), Parametric(Simple(Symbol("List")), [
    Sort(Simple(Symbol("Int"))),
  ])),
  DefineFun(FunctionDef(Symbol("init_indexes"), [
    SortedVar(Symbol("_i"), Sort(Simple(Symbol("Int")))),
    SortedVar(Symbol("_j"), Sort(Simple(Symbol("Int")))),
  ], Sort(Simple(Symbol("Bool"))), Application(Identifier(Simple(Symbol("and"))), [
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("_i")))),
      SpecConstant(Numeral(Numeral("0"))),
    ]),
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("_j")))),
      SpecConstant(Numeral(Numeral("0"))),
    ]),
  ]))),
  DefineFun(FunctionDef(Symbol("inner_loop"), [
    SortedVar(Symbol("_A0"), Parametric(Simple(Symbol("Array")), [
      Sort(Simple(Symbol("Int"))),
      Sort(Simple(Symbol("Int"))),
    ])),
    SortedVar(Symbol("_A1"), Parametric(Simple(Symbol("Array")), [
      Sort(Simple(Symbol("Int"))),
      Sort(Simple(Symbol("Int"))),
    ])),
    SortedVar(Symbol("tmp"), Sort(Simple(Symbol("Int")))),
    SortedVar(Symbol("_i0"), Sort(Simple(Symbol("Int")))),
    SortedVar(Symbol("_dim"), Sort(Simple(Symbol("Int")))),
  ], Sort(Simple(Symbol("Bool"))), Application(Identifier(Simple(Symbol("ite"))), [
    Application(Identifier(Simple(Symbol(">"))), [
      Application(Identifier(Simple(Symbol("select"))), [
        Identifier(Identifier(Simple(Symbol("_A0")))),
        Identifier(Identifier(Simple(Symbol("_i0")))),
      ]),
      Application(Identifier(Simple(Symbol("select"))), [
        Identifier(Identifier(Simple(Symbol("_A0")))),
        Application(Identifier(Simple(Symbol("+"))), [
          Identifier(Identifier(Simple(Symbol("_i0")))),
          SpecConstant(Numeral(Numeral("1"))),
        ]),
      ]),
    ]),
    Application(Identifier(Simple(Symbol("and"))), [
      Application(Identifier(Simple(Symbol("="))), [
        Identifier(Identifier(Simple(Symbol("tmp")))),
        Application(Identifier(Simple(Symbol("select"))), [
          Identifier(Identifier(Simple(Symbol("_A0")))),
          Identifier(Identifier(Simple(Symbol("_i0")))),
        ]),
      ]),
      Application(Identifier(Simple(Symbol("="))), [
        Identifier(Identifier(Simple(Symbol("_A1")))),
        Application(Identifier(Simple(Symbol("store"))), [
          Identifier(Identifier(Simple(Symbol("_A0")))),
          Identifier(Identifier(Simple(Symbol("_i0")))),
          Application(Identifier(Simple(Symbol("select"))), [
            Identifier(Identifier(Simple(Symbol("_A0")))),
            Application(Identifier(Simple(Symbol("+"))), [
              Identifier(Identifier(Simple(Symbol("_i0")))),
              SpecConstant(Numeral(Numeral("1"))),
            ]),
          ]),
        ]),
      ]),
      Application(Identifier(Simple(Symbol("="))), [
        Identifier(Identifier(Simple(Symbol("_A1")))),
        Application(Identifier(Simple(Symbol("store"))), [
          Identifier(Identifier(Simple(Symbol("_A0")))),
          Application(Identifier(Simple(Symbol("+"))), [
            Identifier(Identifier(Simple(Symbol("_i0")))),
            SpecConstant(Numeral(Numeral("1"))),
          ]),
          Identifier(Identifier(Simple(Symbol("tmp")))),
        ]),
      ]),
    ]),
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("_A1")))),
      Identifier(Identifier(Simple(Symbol("_A0")))),
    ]),
  ]))),
  DefineFun(FunctionDef(Symbol("bsort_step"), [
    SortedVar(Symbol("_A0"), Parametric(Simple(Symbol("Array")), [
      Sort(Simple(Symbol("Int"))),
      Sort(Simple(Symbol("Int"))),
    ])),
    SortedVar(Symbol("_A1"), Parametric(Simple(Symbol("Array")), [
      Sort(Simple(Symbol("Int"))),
      Sort(Simple(Symbol("Int"))),
    ])),
    SortedVar(Symbol("tmp"), Sort(Simple(Symbol("Int")))),
    SortedVar(Symbol("_i0"), Sort(Simple(Symbol("Int")))),
    SortedVar(Symbol("_j0"), Sort(Simple(Symbol("Int")))),
    SortedVar(Symbol("_i1"), Sort(Simple(Symbol("Int")))),
    SortedVar(Symbol("_j1"), Sort(Simple(Symbol("Int")))),
    SortedVar(Symbol("_dim"), Sort(Simple(Symbol("Int")))),
  ], Sort(Simple(Symbol("Bool"))), Application(Identifier(Simple(Symbol("ite"))), [
    Application(Identifier(Simple(Symbol("<"))), [
      Identifier(Identifier(Simple(Symbol("_j0")))),
      Application(Identifier(Simple(Symbol("-"))), [
        Identifier(Identifier(Simple(Symbol("_dim")))),
        SpecConstant(Numeral(Numeral("1"))),
      ]),
    ]),
    Application(Identifier(Simple(Symbol("and"))), [
      Application(Identifier(Simple(Symbol("ite"))), [
        Application(Identifier(Simple(Symbol("<"))), [
          Identifier(Identifier(Simple(Symbol("_i0")))),
          Application(Identifier(Simple(Symbol("-"))), [
            Identifier(Identifier(Simple(Symbol("_dim")))),
            SpecConstant(Numeral(Numeral("1"))),
          ]),
        ]),
        Application(Identifier(Simple(Symbol("and"))), [
          Application(Identifier(Simple(Symbol("inner_loop"))), [
            Identifier(Identifier(Simple(Symbol("_A0")))),
            Identifier(Identifier(Simple(Symbol("_A1")))),
            Identifier(Identifier(Simple(Symbol("tmp")))),
            Identifier(Identifier(Simple(Symbol("_i0")))),
            Identifier(Identifier(Simple(Symbol("_dim")))),
          ]),
          Application(Identifier(Simple(Symbol("="))), [
            Identifier(Identifier(Simple(Symbol("_i1")))),
            Application(Identifier(Simple(Symbol("+"))), [
              Identifier(Identifier(Simple(Symbol("_i0")))),
              SpecConstant(Numeral(Numeral("1"))),
            ]),
          ]),
        ]),
        Application(Identifier(Simple(Symbol("="))), [
          Identifier(Identifier(Simple(Symbol("_j1")))),
          Application(Identifier(Simple(Symbol("+"))), [
            Identifier(Identifier(Simple(Symbol("_j0")))),
            SpecConstant(Numeral(Numeral("1"))),
          ]),
        ]),
      ]),
      Application(Identifier(Simple(Symbol("="))), [
        Identifier(Identifier(Simple(Symbol("_j1")))),
        Application(Identifier(Simple(Symbol("+"))), [
          Identifier(Identifier(Simple(Symbol("_j0")))),
          SpecConstant(Numeral(Numeral("1"))),
        ]),
      ]),
    ]),
    Application(Identifier(Simple(Symbol("and"))), [
      Application(Identifier(Simple(Symbol("="))), [
        Identifier(Identifier(Simple(Symbol("_j1")))),
        Application(Identifier(Simple(Symbol("+"))), [
          Identifier(Identifier(Simple(Symbol("_j0")))),
          SpecConstant(Numeral(Numeral("1"))),
        ]),
      ]),
      Application(Identifier(Simple(Symbol("="))), [
        Identifier(Identifier(Simple(Symbol("_A1")))),
        Identifier(Identifier(Simple(Symbol("_A0")))),
      ]),
    ]),
  ]))),
  DefineFunRec(FunctionDef(Symbol("check"), [
    SortedVar(Symbol("_l"), Parametric(Simple(Symbol("List")), [
      Sort(Simple(Symbol("Int"))),
    ])),
  ], Sort(Simple(Symbol("Bool"))), Application(Identifier(Simple(Symbol("ite"))), [
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("_l")))),
      Identifier(Identifier(Simple(Symbol("nil")))),
    ]),
    Identifier(Identifier(Simple(Symbol("true")))),
    Application(Identifier(Simple(Symbol("ite"))), [
      Application(Identifier(Simple(Symbol("not"))), [
        Application(Identifier(Simple(Symbol("="))), [
          Application(Identifier(Simple(Symbol("tail"))), [
            Identifier(Identifier(Simple(Symbol("_l")))),
          ]),
          Identifier(Identifier(Simple(Symbol("nil")))),
        ]),
      ]),
      Application(Identifier(Simple(Symbol("and"))), [
        Application(Identifier(Simple(Symbol(">="))), [
          Application(Identifier(Simple(Symbol("head"))), [
            Identifier(Identifier(Simple(Symbol("_l")))),
          ]),
          Application(Identifier(Simple(Symbol("head"))), [
            Application(Identifier(Simple(Symbol("tail"))), [
              Identifier(Identifier(Simple(Symbol("_l")))),
            ]),
          ]),
        ]),
        Application(Identifier(Simple(Symbol("check"))), [
          Application(Identifier(Simple(Symbol("tail"))), [
            Identifier(Identifier(Simple(Symbol("_l")))),
          ]),
        ]),
      ]),
      Identifier(Identifier(Simple(Symbol("true")))),
    ]),
  ]))),
  Assert(Application(Identifier(Simple(Symbol("="))), [
    Identifier(Identifier(Simple(Symbol("dim")))),
    SpecConstant(Numeral(Numeral("4"))),
  ])),
  Assert(Application(Identifier(Simple(Symbol("init_indexes"))), [
    Identifier(Identifier(Simple(Symbol("i0")))),
    Identifier(Identifier(Simple(Symbol("j0")))),
  ])),
  Assert(Application(Identifier(Simple(Symbol("bsort_step"))), [
    Identifier(Identifier(Simple(Symbol("A0")))),
    Identifier(Identifier(Simple(Symbol("A1")))),
    Identifier(Identifier(Simple(Symbol("tmp0")))),
    Identifier(Identifier(Simple(Symbol("i0")))),
    Identifier(Identifier(Simple(Symbol("j0")))),
    Identifier(Identifier(Simple(Symbol("i1")))),
    Identifier(Identifier(Simple(Symbol("j1")))),
    Identifier(Identifier(Simple(Symbol("dim")))),
  ])),
  Assert(Application(Identifier(Simple(Symbol("bsort_step"))), [
    Identifier(Identifier(Simple(Symbol("A1")))),
    Identifier(Identifier(Simple(Symbol("A2")))),
    Identifier(Identifier(Simple(Symbol("tmp1")))),
    Identifier(Identifier(Simple(Symbol("i1")))),
    Identifier(Identifier(Simple(Symbol("j1")))),
    Identifier(Identifier(Simple(Symbol("i2")))),
    Identifier(Identifier(Simple(Symbol("j2")))),
    Identifier(Identifier(Simple(Symbol("dim")))),
  ])),
  Assert(Application(Identifier(Simple(Symbol("bsort_step"))), [
    Identifier(Identifier(Simple(Symbol("A2")))),
    Identifier(Identifier(Simple(Symbol("A3")))),
    Identifier(Identifier(Simple(Symbol("tmp2")))),
    Identifier(Identifier(Simple(Symbol("i2")))),
    Identifier(Identifier(Simple(Symbol("j2")))),
    Identifier(Identifier(Simple(Symbol("i3")))),
    Identifier(Identifier(Simple(Symbol("j3")))),
    Identifier(Identifier(Simple(Symbol("dim")))),
  ])),
  Assert(Application(Identifier(Simple(Symbol("and"))), [
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("l0")))),
      Identifier(Identifier(Simple(Symbol("nil")))),
    ]),
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("l1")))),
      Application(Identifier(Simple(Symbol("insert"))), [
        Application(Identifier(Simple(Symbol("select"))), [
          Identifier(Identifier(Simple(Symbol("A3")))),
          SpecConstant(Numeral(Numeral("0"))),
        ]),
        Identifier(Identifier(Simple(Symbol("l0")))),
      ]),
    ]),
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("l2")))),
      Application(Identifier(Simple(Symbol("insert"))), [
        Application(Identifier(Simple(Symbol("select"))), [
          Identifier(Identifier(Simple(Symbol("A3")))),
          SpecConstant(Numeral(Numeral("1"))),
        ]),
        Identifier(Identifier(Simple(Symbol("l1")))),
      ]),
    ]),
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("l3")))),
      Application(Identifier(Simple(Symbol("insert"))), [
        Application(Identifier(Simple(Symbol("select"))), [
          Identifier(Identifier(Simple(Symbol("A3")))),
          SpecConstant(Numeral(Numeral("2"))),
        ]),
        Identifier(Identifier(Simple(Symbol("l2")))),
      ]),
    ]),
    Application(Identifier(Simple(Symbol("="))), [
      Identifier(Identifier(Simple(Symbol("l4")))),
      Application(Identifier(Simple(Symbol("insert"))), [
        Application(Identifier(Simple(Symbol("select"))), [
          Identifier(Identifier(Simple(Symbol("A3")))),
          SpecConstant(Numeral(Numeral("3"))),
        ]),
        Identifier(Identifier(Simple(Symbol("l3")))),
      ]),
    ]),
  ])),
  Echo("\"BUBBLE SORT\""),
  Push(Numeral("1")),
  Assert(Application(Identifier(Simple(Symbol("not"))), [
    Application(Identifier(Simple(Symbol("check"))), [
      Identifier(Identifier(Simple(Symbol("l4")))),
    ]),
  ])),
  Echo("\"Testing the validity of the algorithm; `unsat` expected: \""),
  CheckSat,
  Echo("\"---------------------\""),
  Pop(Numeral("1")),
  Assert(Application(Identifier(Simple(Symbol("check"))), [
    Identifier(Identifier(Simple(Symbol("l4")))),
  ])),
  Echo("\"Getting a model; `sat` expected: \""),
  CheckSat,
  Echo("\"---------------------\""),
  Echo("\"Model: \""),
  GetValue([
    Identifier(Identifier(Simple(Symbol("A3")))),
  ]),
  Exit,
]))