Project 1: OCaml Warmup

COMP 150-AVS, Fall 2018

Due Thu, Sep 20 @ 11:59pm

This project will give you practice programming in OCaml by asking you to implement code for constructing, manipulating, and solving boolean formulae. You will then use your code to model binary numbers and solve a 3x3 magic square.

Here is the code skeleton for the project.

In this part of the project, you will develop some functions for working with boolean expressions, represented using the following type:

type bexpr =
  | ETrue
  | EVar of string
  | EAnd of bexpr * bexpr
  | EOr of bexpr * bexpr
  | ENot of bexpr
  | EForall of string * bexpr
  | EExists of string * bexpr
Here EFalse and ETrue represent the obvious values. EVar s represents the boolean variable with name s. The constructors EAnd, EOr, and ENot represent boolean conjunction, disjunction, and negation, respectively. For example, the expression (a or b) and c could be represented as And(Or(Var "a", Var "b"), Var "c"). (We'll explain Forall and Exists in a moment.)

We will use associative lists, which are just lists of pairs, to assign truth values to variables:

type asst = (string * bool) list
Here if an asst contains the pair (s, b), then that assignment gives the variable represented by the string s the value b. When working with the type asst, you will find the functions List.assoc, List.mem_assoc, and related functions helpful. See the OCaml standard library documentation for more details.

You may assume for purposes of this project that whenever you work with an asst, variables on the left override variables on the right. E.g., the assignment ["a", true; "a", false] assigns true to Var "a".

The last two expressions, EForall and EExists, represent the similarly named quantifiers. The expression EForall(x,e) is true if e is true when x is true and when x is false. Similarly, EExists(x,e) is true if e is true either when x is true or when x is false.

You can find the definitions of the above types in boolean.mli, along with type signatures for several functions you must implement in

However complex a boolean expression, it represents a single bit. In the next part of the project, you will put those bits together to represent integers using the following type:

type bvec = bexpr list (* low order bit at head of list *)
A bvec is a list of boolean expressions representing bits, with the low order bit at the head of the list. For example, we could represent the number 13 as [ETrue; EFalse; ETrue; ETrue]. Zero could be represented as [] or [EFalse] or [EFalse; EFalse], etc. An unknown 4-bit integer could be represented as [EVar "a"; EVar "b"; EVar "c"; EVar "d"].

Implement the following functions in

If you've gotten this far, you've now built a (likely very slow) solver for part of bitvector arithmetic! Suppose we have:

let x = [EVar "a"; EVar "b"]
let y = [EVar "c"; EVar "d"]
let z = [EFalse; EFalse; ETrue]  (* 4 *)
Then we can use our solver to answer questions like:
sat (eq (add x y) z)  (* are there two, two-bit numbers that sum to 4? *)
sat (eq (add x x) z)  (* is there a two-bit number that, doubled, is 4? *)
etc. Cool!

A magic square is an n-by-n grid of the numbers 1 through n^2 such that every number appears exactly once and the sum of each row, column, and diagonal is the same. For example, here is a 3x3 magic square:

In this part, you will write a function that solves the magic squares problem, using the machinery you developed in part 1. In particular, what we will do is "reduce" the problem of finding a solution to the magic squares problem to a boolean formula. We can then use the sat function to actually find a solution. Here are the functions you should write; place them in

You can try out your is_magic function by seeing if it can decide that the square above is magic. You can also try replacing one or two entries by variables, and then seeing if your code correctly finds the right numbers to fill in. However, you'll have to wait a long, long time if you try making a lot of the entries in the magic square variables, since your sat function probably takes exponential time.

Your next task is to implement a few functions related to Lambda calculus. Below is an interface file lambda.mli. You must implement the last six of the listed functions in (We've already implemented unparse for you.)

    type lexpr =
    | Var of string
    | Lam of string * lexpr
    | App of lexpr * lexpr

    val unparse : lexpr -> string

    val free_vars : lexpr -> string list
    val subst : string -> lexpr -> lexpr -> lexpr
    val beta : lexpr -> lexpr option
    val normal_form : lexpr -> lexpr
    val lexpr_of_int : int -> lexpr
    val add : lexpr -> lexpr -> lexpr
These functions should do the following:

Your last task is to write unit tests for parts 1 and 2 above, using OUnit. Put your test cases in the file, and be sure to add your test cases to the suites suite_boolean, suite_bvec, suit_magic, and suite_lambda, as appropriate.

We will grade this part of the project by running your test cases against correct and incorrect implementations. More specifically, we will create a correct implementation cor and a set of incorrect implementations Incor. Your test cases should detect that the incorrect implementations are buggy, but not just by trivially saying all implementations are buggy. Thus, you will receive credit for detection an incorrect implementation i∈Incor if at least one of your test cases both (1) flags i as incorrect and (2) passes cor as correct.

Put all your code in the code skeleton we have supplied, and upload your solution using Gradescope. Details will be posted here once we figure out what those details are.