smtlib-lowlevel 0.1.2

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

;   File name:    bubble_sort.smt2
;
;   BUBBLESORT  -  Copyright (c) March, 2021 - Matteo Nicoli
;
;   An example of bounded model checking of the classic bubble sort algorithm.
;   we will copy the array values into a list in order to check whether the
;   array is ordered or not. That's because:
;       - it's easier to walk recursively through a list
;       - it gives an example of how list and sequences work in Z3
;


; size of the array
(declare-const dim Int)

; arrays declaration
(declare-const A0 (Array Int Int))
(declare-const A1 (Array Int Int))
(declare-const A2 (Array Int Int))
(declare-const A3 (Array Int Int))

; indexes declaration
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i3 Int)

(declare-const j0 Int)
(declare-const j1 Int)
(declare-const j2 Int)
(declare-const j3 Int)

(declare-const tmp0 Int)
(declare-const tmp1 Int)
(declare-const tmp2 Int)

; lists declaration (for post condition)
(declare-const l0 (List Int))
(declare-const l1 (List Int))
(declare-const l2 (List Int))
(declare-const l3 (List Int))
(declare-const l4 (List Int))

(define-fun init_indexes ((_i Int) (_j Int)) Bool
    (and
        (= _i 0)
        (= _j 0)
    )
)

(define-fun inner_loop
                        (
                            (_A0 (Array Int Int))
                            (_A1 (Array Int Int))
                            (tmp Int)
                            (_i0 Int)
                            (_dim Int)
                        ) Bool
    (ite
        (> (select _A0 _i0) (select _A0 (+ _i0 1)))
        (and
            (= tmp (select _A0 _i0))
            (= _A1 (store _A0 _i0 (select _A0 (+ _i0 1))))
            (= _A1 (store _A0 (+ _i0 1) tmp))
        )
        (= _A1 _A0)
    )
)

; the body of the bubblesort algorithm
(define-fun bsort_step
                        (
                            (_A0 (Array Int Int))
                            (_A1 (Array Int Int))
                            (tmp Int)
                            (_i0 Int)
                            (_j0 Int)
                            (_i1 Int)
                            (_j1 Int)
                            (_dim Int)
                        ) Bool
    (ite
        (< _j0 (- _dim 1))
        (and
            (ite
                (< _i0 (- _dim 1))
                (and
                    (inner_loop _A0 _A1 tmp _i0 _dim)
                    (= _i1 (+ _i0 1))
                )
                (= _j1 (+ _j0 1))
            )
            (= _j1 (+ _j0 1))
        )
        (and
            (= _j1 (+ _j0 1))
            (= _A1 _A0)
        )
    )
)

; the function by which we check whether the list is ordered
(define-fun-rec check ((_l (List Int))) Bool
    (ite
        (= _l nil)
        true
        (ite
            (not (= (tail _l) nil))
            (and
                (>= (head _l) (head (tail _l)))
                (check (tail _l))
            )
            true
        )
    )
)

; sets the size of the array
(assert (= dim 4))

; initialization of the counters
(assert (init_indexes i0 j0))

; the first step of the sorting algorithm
(assert (bsort_step A0 A1 tmp0 i0 j0 i1 j1 dim))
(assert (bsort_step A1 A2 tmp1 i1 j1 i2 j2 dim))
(assert (bsort_step A2 A3 tmp2 i2 j2 i3 j3 dim))

; filling the list for test
(assert
    (and
        (= l0 nil)
        (= l1 (insert (select A3 0) l0))
        (= l2 (insert (select A3 1) l1))
        (= l3 (insert (select A3 2) l2))
        (= l4 (insert (select A3 3) l3))
    )
)

(echo "BUBBLE SORT")

(push 1)

; (negated) post-condition
(assert (not (check l4)))

(echo "Testing the validity of the algorithm; `unsat` expected: ")

; `unsat` expected
(check-sat)

(echo "---------------------")

(pop 1)

; post-condition
(assert (check l4))

(echo "Getting a model; `sat` expected: ")

; `sat` expected
(check-sat)

(echo "---------------------")

(echo "Model: ")
(get-value (A3))
(exit)