smtlib-lowlevel 0.1.5

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

;   File name:    loop_unrolling_bitvec.smt2
;
;   Copyright (c) March, 2021 - Matteo Nicoli
;
;
;   Let's start considering a simple C program involving an iteration:
;
;       #define DIM 2
;
;       /* uninterpreted functions */
;       long get_number();
;       void fill_array(long *A);
;
;       int main()
;       {
;           long x = get_number();
;           long A[DIM];
;           long i = 0;
;           long found = 0;
;
;           fill_array(A);
;
;           while(i < DIM) {
;               if(x == A[i])
;                   found = 1;
;               i++;
;           }
;       }
;
;   Below, we can see its SSA representation in SMT-LIB2.
;   Our goal is to verify that, at the end of the program, the variable `found`
;   is equal to 1 if, and only if, `x` is an element of the array.
;   We define our custom sort `IntValue` that represents a 32-bit integer value.


(define-sort IntValue () (_ BitVec 32))
(declare-const x IntValue)
(declare-const A (Array IntValue IntValue))
(declare-const i_0 IntValue)
(declare-const found_0 IntValue)

(declare-const found_1 IntValue)
(declare-const found_2 IntValue)
(declare-const i_1 IntValue)
(declare-const i_2 IntValue)

; Pre-condition: variables initialization
(assert
    (and
        (= i_0 #x00000000)
        (= found_0 #x00000000)
    )
)

; Transition funcion
(define-fun body ((f_0 IntValue) (f IntValue) (i_0 IntValue) (i_1 IntValue)(_A (Array IntValue IntValue)) (_x IntValue)) Bool
    (and
        (= f (ite (= _x (select _A i_0)) #x00000001 f_0))
        (= i_1 (bvadd i_0 #x00000001))
    )
)

; Post-condition function
(define-fun post ((_f IntValue) (_i IntValue) (_x IntValue) (_A (Array IntValue IntValue))) Bool
    (=
        (= _f #x00000001)
        (= _x (select _A _i))
    )
)

; Transition function is called DIM times:
; for practical reasons, we are considering here DIM = 2
(assert (body found_0 found_1 i_0 i_1 A x))
(assert (body found_1 found_2 i_1 i_2 A x))

(push 1)

(echo "Bounded model checking with loop unrolling")

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

; Post-condition (negated) is called DIM times
(assert
    (not
        (or
            (post found_2 i_0 x A)
            (post found_2 i_1 x A)
        )
    )
)

(echo "Testing the validity of the post-condition: `unsat expected`")

; `unsat` expected
(check-sat)

(pop 1)

; Post-condition (called DIM times)
(assert
    (or
        (post found_2 i_0 x A)
        (post found_2 i_1 x A)
    )
)

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

; `sat` expected
(check-sat)

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

(echo "Model: ")
(get-value (x A found_2))
(exit)