This project is designed to be done by individuals. However, you may work in a group of two if you take on some significant "extra challenges" from the list below.
Due Tuesday, October 25
This will essentially be a symbolic executor. N-bit values should be represented as vectors of N Boolean expressions.
To execute an operation such as "c = a + b", look up the symbolic values of "a" and "b" in the current symbolic state, and do a symbolic computation of "+" that combines then into a vector of Boolean expressions (similar to Alex's description of Saturn). Then update the symbolic state to map "c" to this symbolic value.
Implement all the integer operations (including multiply, divide, and mod). (If you are using BDDs, only do multiply, divide, mod by constants.) Floating point and arrays/pointers are not required.
You will also need to unroll "for" loops. If I accidentally included code examples below with loops that don't have relatively small upper-bounds on the number of iterations, please let me know.
You do not need to build word-level expressions (although you may if you wish), but go immediately to bit level from the C abstract syntax tree.
Initial values of variables will be vectors of propositional variables.
CIL is written in ML, and is widely used to prototype program analysis applications for C. If you are more familiar with another tool, such as LLVM, go ahead and use it. Or just dive into lex and YACC if you wish. If there are trivial syntactic issues in the examples that cause problems, it is ok to edit them to work around the problems, so long as the bit-level computation remains essentially the same.
One student asked if it was ok to do the examples in Verilog. My answer is yes, if the Boolean formulas would be essentially the same as those generated by using a C front-end. The basic rule is: We don't care about syntax, but don't change the nature of the problem.
The goal of the project is to seen how to use SAT, not to write a C compiler.
http://graphics.stanford.edu/~seander/bithacks.html
There are several examples there that have several ways to compute the same function.
Prove that they are equivalent by solving the CNF formula generated using the code in part 2.
Here is a list of ones that seemed doable. I picked ones where there were several equivalent examples, or where you could easily write an equivalent naive version. I intended to skip those that involved table lookups or required floating point
Compute the minimum (min) or maximum (max) of two integers without branching Conditionally set or clear bits without branching Counting bits set, Brian Kernighan's way vs. Counting bits set in 14, 24, or 32-bit words using 64-bit instructions vs. Counting bits set, in parallel Computing parity the naive way vs. Compute parity of a byte using 64-bit multiply and modulus division vs. Compute parity of word with a multiply vs. Compute parity in parallel Swapping values the obvious way (not here). vs. Swapping values with subtraction and addition vs. Swapping values with XOR Reverse bits the obvious way vs. Reverse the bits in a byte with 3 operations (64-bit multiply and modulus division) vs. Reverse the bits in a byte with 4 operations (64-bit multiply, no division) vs Reverse the bits in a byte with 7 operations (no 64-bit)
Options: If you have already done something like this, do the same thing but use BDDs. CUDD (from Colorado) is one BDD package that can be made to work, although there are several available.