[Summer] Write Z3 substitution function for custom data types

[jlvargasme]

The custom refinement data types uses an alias to reference the type variable itself. e.g: type nat = {v : int | v > = 0} , in this example v is the alias used for the type variable.

This task aims to implement the vc_gen_substitute function that will take a inputs a variable and perform a Z3 substitution.

e.g: type nat = {v : int | v > = 0} let y : nat = 4 vc_gen_substitute(y) would looks for v >= 0 in nat definition and replace v with the variable y by using the Z3 Ocaml API.

The verification condition for the above example would be: y = 4 -> y >= 0

Reference:

Look for substitute function in https://z3prover.github.io/api/html/ml/Z3.Expr.html

[jchen-cs]

52

Deferring type alias implementation for now