• Sep 24 - Added ; terminator to zero and eq to simplify parsing.
• Sep 22 - Fixed a typo: bool x=0; bprint x; should print false.
• Sep 21 - Changed production from = to eq for VEXPR

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/glue.umd.edu/class/fall2016/cmsc/430/0101/public. 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:

• &, |, and + are left-associative.
• In boolean expressions, ! binds more tightly than &, which binds more tightly than |. For example, a | !b & c should parse as a | ((!b) & c).
• In vectors, & binds more tightly than +.
• A literal vector is made up of a sequence of zero or more boolean expressions separated by commas, and is delimited by [ and ]. A trailing comma is not allowed. For example, [], [0, a, b & c], and [forall x . x | y;] are all valid literal vectors, but [a,b,] is not.
• An assignment contains zero or more comma-separated pairs of bindings of identifiers to boolean values 0 or 1, where : separates the identifier from its value. The assignment is delimited by [ and ]. Trailing commas are not allowed. For example, [] and [a:1,b:0] are valid assignments, but [a:2], [a:1,b:0,], [a:(0)], and [a:(0|1)] are not.
• Empty programs are allowed.
• Statements are terminated by semicolons. A semicolon by itself is not valid, nor can extra semicolons be added to the end of statements.
• Both forall and exists and terminated by ;. This is non-standard but will make parsing a bit easier.
• Whitespace is not significant and should be ignored.
• Comments begin with # and extend to the end of the line.

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

• In general, your solver should not print anything out except exactly what we tell you below. So be sure to remove any debugging print statements before you submit your code.
• However, you may add extra newlines before or after executing individual statements.
• Statements bprint and vprint should print out their corresponding expressions or vectors using the code we've given you in unparse.ml. Please do not modify that code as we might rely on the exact format it uses to print.
• Statements bool ID = BEXPR and bvec ID = VEXPR bind the given identifiers to a boolean expression or vector, respectively. (And these statements do not print anything.) Inside of a BEXPR, if an ID has previously been bound to a BEXPR, its binding should be substituted for the identifier. If ID has previously been bound to a VEXPR, your solver should raise an exception (any exception). If ID has not been bound, then it should be turned into an EVar node with that id. For example:
  • bool x = 0; bprint x; prints false
  • bvec x = 0; bprint x; throws an exception in evaluating the bprint statement because x is not a boolean expression.
  • bprint x; prints x
  For a VEXPR, if ID has previously been bound to a VEXPR, the previous binding is substituted for the identifier. If ID has previously been bound to a BEXPR, or if ID is not bound, your parser should raise an exception.
• Statement eval ASST BEXPR; evaluates an expression under an assignment and prints the resulting truth value as either true or false followed by a newline.
• Statement fv BEXPR; prints out a comma-separated list of the free variables of a boolean expression. For example:
  • fv x; prints x followed by newline.
  • fv x & y; prints x, y followed by newline.
  • fv 1; prints a newline.
• Statement sat BEXPR; prints out either Unsat if there is no satisfying assignment, or it prints out the satisfying assignment in the same format as ASST. For example:
  • sat 0; prints Unsat followed by a newline.
  • sat x & y; prints [x:1, y:1] followed by a newline.
• Statement int_of VEXPR; prints the integer corresponding the the VEXPR followed by a newline. Your solver should raise an exception if VEXPR contains anything other than 0's and 1's.
• (Note there are no expressions, vectors, or statements corresponding to subst for bvec.)

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.