Project 2: Boolean Expression Parser

CMSC 430, Fall 2016

Due Wed, Sep 28, 2016 @ 11:59:59pm

In this project, you will implement a front-end for the boolean constraint solver you wrote in Project 1. For example, after implementing this project, you'll be able to run the following program:

bvec x = [a, b];          # [EVar "a"; EVar "b"]
bvec y = [c, d];          # [EVar "c"; EVar "d"]
bvec z = 4;               # [EFalse; EFalse; ETrue]
bool b1 = (eq x + y, z;); # eq (add x y) z
bool b2 = (eq x + x, z;); # eq (add x x) z
sat b1;                   # are there two, two-bit numbers that sum to 4?
sat b2;                   # is there a two-bit number that, doubled, in 4?
Pretty soon you'll be ready to enter the International SAT Competition!

Here is the code skeleton for the project.

In case you didn't get project 1 fully working, you can grab compiled bytecode files boolean.cmo and boolean.cmi from /afs/ Copy those files into the _build directory after running make for the first time.

The input language to your solver is given by the following grammar, where capitalized words indicate non-terminals or the tokens ID or INT.

PROG ::= STMT*            # a program contains zero or more statements

STMT ::= bprint BEXPR;    # print an expression
       | vprint VEXPR;    # print a vector
       | bool ID = BEXPR; # bind an expression to a variable
       | bvec ID = VEXPR; # bind a vector to a variable
       | eval ASST BEXPR; # evaluate an expr under an assignment and print result
       | fv BEXPR;        # print the free variables of an expr
       | sat BEXPR;       # print the satisfiability of an expr
       | int_of VEXPR;    # print the int corresponding to a vector

BEXPR ::= 0                   # false
        | 1                   # true
        | ID                  # variable
        | BEXPR & BEXPR       # conjunction
        | BEXPR | BEXPR       # disjunction
        | !BEXPR              # negation
        | forall ID . BEXPR;  # universal quantification
        | exists ID . BEXPR;  # existential quantification
        | zero VEXPR;         # is vec equal to zero?
        | eq VEXPR, VEXPR;    # are two vecs equal?
        | (BEXPR)             # grouping

ASST ::= [ ID: (0|1), ID: (0|1), ... ] # see below

VEXPR ::= [ BEXPR, BEXPR, ... ]   # literal vector
        | ID                      # variable
        | INT                     # integer
        | VEXPR & VEXPR           # bitwise and
        | VEXPR + VEXPR           # addition
        | (VEXPR)                 # grouping
Here identifiers ID are made up of upper- and lowercase letters, digits, and underscores. They must begin with a letter or underscore. INT is made up of digits. (Note INTs must therefore be non-negative.)

The first step in building your solver is to develop a parser for the input language. Your parser will accept strings produced from PROG in the grammar above. Your parser should obey the following conventions:

Your parser should run the program as it parses it, following these rules:

Put all your code in the code skeleton we have supplied, and upload your solution to the submit server. You can either upload your solution via the web interface, or you can run java -jar submit.jar in the project directory. Your code can use any OCaml standard library functions that you like.

The Campus Senate has adopted a policy asking students to include the following statement on each assignment in every course: "I pledge on my honor that I have not given or received any unauthorized assistance on this assignment." Consequently your program is requested to contain this pledge in a comment near the top.

Please carefully read the academic honesty section of the course syllabus. Any evidence of impermissible cooperation on projects, use of disallowed materials or resources, or unauthorized use of computer accounts, will be submitted to the Student Honor Council, which could result in an XF for the course, or suspension or expulsion from the University. Be sure you understand what you are and what you are not permitted to do in regards to academic integrity when it comes to project assignments. These policies apply to all students, and the Student Honor Council does not consider lack of knowledge of the policies to be a defense for violating them. Full information is found in the course syllabus---please review it at this time.

Web Accessibility