COSC 470, 2001.

The practical assignment for COSC 470 is to write a program that
reads Boolean expressions and tries to find models for them.

If you use Prolog, you can read Boolean expressions (terminated by a
full stop and new line) using the built-in operation read/1, and you
can write them out using write/1.

If you use Lisp or Scheme, you could use a syntax like
    F | T | (V num) | (NOT x) | (AND x y) | (OR x y) | (IMP x y) | (EQV x y)
and use the built-in (read ...) function to read them and the built-in
(print ...) [Lisp] or (write ...) [Scheme] to write them.

If you use Haskell, you can set up
    data BE vn
       = F
       | T
       | Var vn
       | Not (BE vn)
       | And (BE vn) (BE vn)
       | Or  (BE vn) (BE vn)
       | Imp (BE vn) (BE vn)
       | Eqv (BE vn) (BE vn)
       deriving (Eq, Read, Show)
    type BE1 = BE Int

and let the Haskell compiler figure out how to write the functions for reading
and writing such things.

What do you do if you want to write your program in C?
Turn to this directory, where you will find
    boolexpr.h
    boolexpr.c
    boolexpr.dat	(sample data)
    
    4bit.m4		used to generate the 2nd-to-last example.
    4bitf.m4		used to generate the last example.
    
In the second lecture, I defined Reduced Ordered Binary Decision Diagrams.
Binary Decision Diagram:
    0,
    1, or
    if(variable, bdd1, bdd2)

Reduced:
    1: never test a variable twice
    2: never test a variable if you don't need to
    3: store as a directed acyclic graph (typically using hash consing)
       so that there are no duplicate nodes

Ordered:
    pick an arbitrary total order on the variables, and then
    "heap order" the dag.  That is, if(v,x,y) is allowed only when
    v precedes every variable of x and y in the total order.

The code I wrote on the board converting NOT and AND to ROBDD form
can be found in

    robdd.hs			(Haskell) or
    robdd.pl			(Prolog)  or
    robdd.scm			(Scheme, a minimalist Lisp dialect)

in this directory.  The three missing functions (for OR, IMP, EQV)
are 10 lines of Haskell or 14 lines of Prolog each, following the
same pattern as the "and" example.  These codes build trees, not
DAGs, but are otherwise ordered and reduced (no redundant variable
tests).

Given an expression E, you can find its unique ROBDD R.
If R is 0, E must be false in every interpretation.
If R is 1, E must be true if every interpretation.
If R is neither 0 nor 1, E is true in some interpretations and false in others.
A path from the top of R to a 1 leaf gives you a (partial) model for E;
a path from the top of R to a 0 leaf gives you a (partial) model for NOT E.

After the assignment due date, the deleted code was restored to the models.
In 2002, I expect to put this code to a somewhat different use.