[Question][Hw2] Need more explanation on the program equivalence checker

[kingdoctor123]

I have several questions on implementing program equivalence checker part.

• Can a function return the value from Eq operation? For instance, is this function definition ok? f(x) = (x = x) If so, then should we treat result of Eq operation as having a boolean type (which is different from integer type)?
• From the definition of exp, we know type exp ::= ... | If exp * exp * exp | .... In this case, can we assume first argument of If case should be Eq? Otherwise, if the first argument evaluates to an integer value in runtime, then how do we decide which branch to take?
• Is it guaranteed that every variable and function parameter x have integer type?
• Can we assume that every given program never incurs any error in runtime (such as use of free variables)?
• I read the template code, and found that if Z3 solver says given formula is satisfiable, then our program prints the model. In this situation, it seems it also prints out the name of the variables that we used when constructing the formula. So, should we follow the naming convention provided in the problem description? (e.g., src_x, src_y, tgt_x)

Many of my questions are related to type system of the language, and it would be helpful if you clarify on these questions. Thank you in advance.

[KihongHeo]

Hi, Good point.

• Consider only integer type variables.
• Consider only well-typed and correct programs (no runtime errors, no free variables, etc).
• Use the prefixes src and tgt for variable names in source programs and target programs, repsectively.