add three smt2 examples and update one python example

examples/SMT-LIB2/bounded model checking/bubble_sort.smt2

@@ -0,0 +1,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)
+
+; (negated) post-condition
+(assert (not (check l4)))
+
+(echo "Testing the validity of the algorithm; `unsat` expected: ")
+
+; `unsat` expected
+(check-sat)
+
+(echo "---------------------")
+
+(pop)
+
+; post-condition
+(assert (check l4))
+
+(echo "Getting a model; `sat` expected: ")
+
+; `sat` expected
+(check-sat)
+
+(echo "---------------------")
+
+(echo "Model: ")
+(get-value (A3))
+(exit)

examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2

@@ -0,0 +1,114 @@
+;   File name:    loop_unrolling.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.
+
+
+(declare-const x Int)
+(declare-const A (Array Int Int))
+(declare-const i_0 Int)
+(declare-const found_0 Int)
+
+(declare-const found_1 Int)
+(declare-const found_2 Int)
+(declare-const i_1 Int)
+(declare-const i_2 Int)
+
+; Pre-condition: variables initialization
+(assert
+    (and
+        (= i_0 0)
+        (= found_0 0)
+    )
+)
+
+; Transition funcion
+(define-fun body ((f_0 Int) (f Int) (i_0 Int) (i_1 Int)(_A (Array Int Int)) (_x Int)) Bool
+    (and
+        (= f (ite (= _x (select _A i_0)) 1 f_0))
+        (= i_1 (+ i_0 1))
+    )
+)
+
+; Post-condition function
+(define-fun post ((_f Int) (_i Int) (_x Int) (_A (Array Int Int))) Bool
+    (=
+        (= _f 1)
+        (= _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)
+
+(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)
+
+; 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)