/*
- Recuperăm pe 17 noiembrie de la 16 (ca principiu)
- 1 decembrie -> zi liberă
- 5 ianuarie -> (?)
- 12 ianuarie -> (?)
 */

// Aplicatii ale solver-elor SMT
// 1. Verificarea de Programe (azi)
// 2. Analiza Statica
/*
   void weird(int *a, int len) // len este dimensiunea lui a
   {
     int *b = a + 10;  // b pointeaza la al 10-lea element din a
     if (len > 20) {   // a are mai mult de 20 de elemente
       b[3] = 7;       // a[13] = 7
     }
     // daca len este dimensiunea lui a, codul de mai sus
     // nu face segmentation fault
   }

   // b = a + 10
   // len(a) > 20
   // ----------/
   // a + 0 < b + 3 < a + len(a)
   // ----------//

   Analizor static: citeste codul sursa (fara sa il execute)
   si se "uita" daca accesul la variabile de tip array/pointer
   risca sa depaseasca memoria alocata.

   MSVC: /analyze (analiza static)
   CLang: clang static analyzer
*/
// 3. Executie Simbolica
/*

   int max(int a, int b)
   {
     if (a > b) {
       return a;
     } else {
       return b;
     }
   }

   Executie concreta:
   max(3, 7) -> 7

   Executia simbolica:
             a>b
   max(a, b) ----> a
       |
       |a<b
       v
       b

   SMT solver: a > b (?)
   - unreachability code
   - test case generation
 */
// 4. Hardware verification (circuit equivalence)
// doua circuite C1, C2
// exists x1, ..., xn.C1(x1, ... xn) != C2(x1, ..., xn)
// 5. Security
// reverse engineering, implementari critografice
// 6. Optimization/Constraint Solving
// 7. AI/ML
//    - verify neural networks
//    - integrate w/ statistical reasoning
// 8. Interactive Theorem Proving
//    - SMT solver
// 9. Automotive: design SDV


// Verificarea de Programe
method min(a : int, b : int) returns (r : int)
  ensures r <= a && r <= b
  ensures r == a || r == b
{
  if (a < b) {
    return a;
  } else {
    return b;
  }
}

method test1()
{
  var x := min(3, 7);
  print "Expected: 3; got: ", x, "\n";
}

method test2()
{
  var x := min(5, 5);
  print "Expected: 5; got: ", x, "\n";
}

method test3()
{
  var x := min(10, 5);
  print "Expected: 5; got: ", x, "\n";
}

method min3(a : int, b : int, c : int) returns (r : int)
{
  if (a < b && a < c) {
    return a;
  } else if (b < a && b < c) {
    return b;
  } else {
    return c;
  }
}

method min3test()
{
  var x1 := min3(3, 7, 10);
  print "Expected: 3; got: ", x1, "\n";
  var x2 := min3(10, 7, 3);
  print "Expected: 3; got: ", x2, "\n";
  var x3 := min3(10, 2, 3);
  print "Expected: 2; got: ", x3, "\n";
  var x4 := min3(5, 5, 10);
  print "Expected: 5; got: ", x4, "\n";
}

/*
(declare-const a Int)
(declare-const b Int)
(declare-const r Int)

(assert
 (and (=> (< a b)
         (= r a))
      (=> (not (< a b))
         (= r b)))
 )
(assert (not
         (and
          (<= r a)
          (<= r b)
          (or (= r a)
              (= r b)))))

(check-sat)


   */

/*
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const r Int)

(assert
 (and (=> (and (< a b) (< a c))
         (= r a))
      (=> (and (not (and (< a b) (< a c))) (and (< b a) (< b c)))
         (= r b))
      (=> (and (not (and (< a b) (< a c))) (not (and (< b a) (< b c))))
         (= r c)))
)
(assert (not
         (and
          (<= r a)
          (<= r b)
          (<= r c)
          (or (= r a)
              (= r b)
              (= r c)))))
;; // min3(0, 0, 1) nu da raspunsul corect
(check-sat)
(get-model)



   */

method min3'(a : int, b : int, c : int) returns (r : int)
  ensures r <= a && r <= b && r <= c
  ensures r == a || r == b || r == c
{
  var temp1 := min(a, b);
  var temp2 := min(temp1, c);
  return temp2;
  // if (a <= b && a < c) {
  //   return a;
  // } else if (b < a && b < c) {
  //   return b;
  // } else {
  //   return c;
  // }
}

method Main()
{
  test1();
  test2();
  test3();
  min3test();
}

/*
(declare-fun |a#0| () Int)
(declare-fun |b#0| () Int)
(declare-fun |r#0@0| () Int)
(assert
(not
 (=>
 (and
 (< |a#0| |b#0|)
 (= |r#0@0| |a#0|)
 (<= |r#0@0| |a#0|)
 (<= |r#0@0| |b#0|)
 )
 (or
 (= |r#0@0| |a#0|)
 (= |r#0@0| |b#0|)))
))
(check-sat)





(assert (not
         (=>
          (and
           (< |a#0| |b#0|)
           (= |r#0@0| |a#0|)
           (<= |r#0@0| |a#0|))
          (<= |r#0@0| |b#0|)
          )))

   */

method search(s : seq<int>, x : int) returns (pos : int)
  ensures pos == -1 || (0 <= pos < |s|)
  ensures pos == -1 ==> forall i :: 0 <= i < |s| ==> s[i] != x
  ensures pos != -1 ==> s[pos] == x
{
  var i := 0;
  while (i < |s|)
    invariant 0 <= i <= |s| // adev inainte si dupa fiecare executie
    // a corpului buclei while (inclusiv dupa
    // ultima executie)
    invariant forall i' :: 0 <= i' < i ==> s[i'] != x
  {
    if (s[i] == x) {
      return i;
    }
    i := i + 1;
  }
  return -1;
}


/*
1. Invariantul este adevarat la intrarea in bucla:

s : seq<int>
x : int
pos : int
i : int
i == 0
i < |s|
-------------/
0 <= i <= |s| &&
forall i' :: 0 <= i' < i ==> s[i'] != x
----------//

2. Invariantul este pastrat de fiecare
executie a corpului buclei

s : seq<int>
x : int
pos : int
i : int
0 <= i <= |s|
forall i' :: 0 <= i' < i ==> s[i'] != x      (A)
s[i] != x                            (B)
i_next = i + 1
i < |s|
-----------------/
0 <= i_next <= |s| &&
forall i' :: 0 <= i' < i_next ==> s[i'] != x
-----------------//

0 <= i + 1 <= |s| done

forall i' :: 0 <= i' < i + 1 ==> s[i'] != x
     doua cazuri 0 <= i' < i ==> ipoteza (A)
                 i' == i ==> s[i] != x ipoteza (B)
   */