/*

NOTE: For me, using the carbon backend did not work (exit with 1 error, but
      did not list anything in the problems tab). However, it also failed
      for all other files including the solutions of exercises from the
      lectures. So, it probably stems from a faulty installation or such.
      I used viper 2.2.2 and then deinstalled it and installed 2.2.3, without
      any success. However, they all verified successfully using the silicon
      backend. I'm using Manjaro 21.0.1 with Linux Kernel 5.10.26.

*/

// TODO: remember to add your definition of trees from task 4
domain Tree {
    // Task (1)

    // Constructors
    function Leaf(): Tree
    function Node(v: Int, lft: Tree, rgt: Tree): Tree

    function isLeaf(t: Tree): Bool
    function isNode(t: Tree): Bool

    axiom type_is_leaf {
        forall t: Tree ::
            isLeaf(t) == (type(t) == type_Leaf())
    }

    axiom construct_over_destruct_Leaf {
        forall t: Tree ::
            isLeaf(t) ==>
                t == Leaf()
    }

    axiom type_is_node {
        forall t: Tree ::
            isNode(t) == (type(t) == type_Node())
    }

    axiom construct_over_destruct_Node {
        forall t: Tree ::   
            isNode(t) ==>
                t == Node(getVal(t), getLeft(t), getRight(t))
    }

    // Deconstructors
    function getVal(t: Tree): Int
    function getLeft(t: Tree): Tree
    function getRight(t: Tree): Tree

    axiom destruct_over_construct {
        forall v: Int, lft: Tree, rgt: Tree ::
            getVal(Node(v, lft, rgt)) == v
         && getLeft(Node(v, lft, rgt)) == lft
         && getRight(Node(v, lft, rgt)) == rgt
    }

    // Types
    function type(t: Tree): Int
    unique function type_Leaf(): Int
    unique function type_Node(): Int

    axiom type_of_Leaf {
        type(Leaf()) == type_Leaf()
    }

    axiom type_of_Node {
        forall v: Int, lft: Tree, rgt: Tree ::
            type(Node(v, lft, rgt)) == type_Node()
    }

    axiom all_types {
        forall t: Tree ::
            (type(t) == type_Leaf() && t == Leaf())
         || (type(t) == type_Node() && exists v: Int, lft: Tree, rgt: Tree :: t == Node(v, lft, rgt))
    }
}

// Above is from task (4)

// Task (1)

function height(t: Tree): Int
{
  isLeaf(t) ? 0 :
    (height(getLeft(t)) > height(getRight(t)) ? height(getLeft(t)) + 1 : height(getRight(t)) + 1)
}

// Task (2)

method computeTreeHeight(t: Tree) returns (res: Int)
  // Show computeTreeHeight always returns the same result as the recursive
  // height function
  ensures res == height(t)
{
  if (isLeaf(t)){
    res := 0
  }else{
    var current: Seq[Tree]
    var next: Seq[Tree]
    current := Seq(t)
    next := Seq[Tree]()
    res := 0
    
    while (|current| > 0)
      invariant |current| == 0 ==> res == height(t)
      // 'res' increases by 1 for each level of the tree, thus it is always
      // equal to the total height minus the height of the highest sub-tree when
      // cutting off at the current level. In the end the height of the highest
      // sub-tree will be 0 and thus it follows 'res == height(t)'. The 
      // following invariant formalizes this, but it is actually not needed for
      // the verifier to succeed.
      // invariant forall i: Int :: i >= 0 && i < |current| &&
      //   (forall k: Int :: k >= 0 && k < |current| &&
      //     height(current[i]) > height(current[k])) 
      //       ==> res == height(t) - height(current[i])
    {
      res := res + 1
      next := Seq[Tree]()

      while (|current| > 0)
        // The highest tree in 'current' is higher by 1 compared to the highest
        // tree in 'next' (we only consider the highest because that's the one
        // giving the height to the tree as defined by the 'height' function).
        invariant forall i: Int :: i >= 0 && i < |current| &&
          (forall k: Int :: k >= 0 && k < |current| &&
            height(current[i]) > height(current[k])) &&
          forall j: Int :: j >= 0 && j < |next| &&
          (forall k: Int :: k >= 0 && k < |next| &&
            height(next[j]) > height(next[k]))
              ==> height(next[j]) == height(current[i]) - 1
      {
        var node : Tree := current[0]
        POP(current)
        if (isNode(getLeft(node))){
          PUSH(next, getLeft(node))
          assert false
        }
        if (isNode(getRight(node))){
          PUSH(next, getRight(node))
        }
      }
      current := next
      
    }
  }
}

define PUSH(stck, v) {
  stck := Seq(v) ++ stck
}

define POP(stck) {
  stck := stck[1..]
}