NewtonCompare: Reduce the initialized memory in buddy

It was taking too long to initialize buddy. Reduced the memsize and cachesize being used.
Also made the ratio between the default values in BinRel.cpp more explicit.
BplToPds: Handle enforce clauses by asserting postcondition before return

'enforce' clauses were ignored in the BplToPds conversion.
Added the function 'instrument_enforce' in BplToPds. This function emits assert
statements before every return statement asserting the expression in enforce.
Note: The following functions *must be called in the given order*
- make_void_returns_explicit()
- instrument_enforce
- instrument_asserts

Towards this, also added a utility function to ast.h/c: expr * make_deep_copy_expr(expr *)
This makes a clean deep copy of the expression.
Define CHECK_BDDIMPLIES_WITH_SLOWER_VERSION
Change BddLessThan::operator() to const
Use a local cache for bddImplies to avoid re-evaluation

Because a BDD could look like

    a
   / \
  /   \
  b    b
 /\   / \
   \ /
    c

we don't want to re-evaluate c or we turn a linear algorithm into exponential. :-)
Merge branch 'fast-semiring-compares' into pcca-nonsense
Update to the semantics of instrument_enforce

I had assumed incorrect semantics for enforce.
The correct semantics of enforce are to assume the expression *at every point in the procedure*
This update changes how instrument_enforce replaces enforce by assume statements. Earlier, it would assume just
the post condition. Now, the assumes are put at function entry, and after every statement (except returns)
Added vim temporary file .*.swp to gitignore
Add a void return in the special error function
Fixed bug in instrument_enforce_in_stmt_list: update tail properly

BplToPds.cpp: Update the 'tl' field in the head of the list when an assume is added to the
end of the list
BplToPds: Added functions to instrument calls to non-void returning functions

When function return values, these values need to be copied to the correct
variables across a call. We accomplish this by adding special '__return_i__'
global variables (as many as the largest number of values returned
simultaneously) and copying values through these.
BplToPds: Added argument passing support using reserved global variables

(1) renamed __return_i__ to __call_return_reserved_i__
(2) Use these variables to also pass arguments to the formal parameters in functions
NewtonCompare: Fix error label reachability check

After path summary, collect all out transition from pds state with the error
label as the stack symbol then check if the combine of the weights on the *to
state* is non-zero. Earlier, the check was combine of the weights on the
transitions themselves.
Allow paths that do not end in return in functions returning values

We instrument the functions so that all such paths return non-deterministic values.
This is a safe over-approximation of the program
bp_scanner: parse T as true and F as false in boolean programs

Earlier only 1/0 were supported. Slam programs often use T/F as well.
Bug fix [BplToAst.cpp] : check for null decl list in boolean program ast when adding instrumented variables
Add Partition stuff from Aditya

(From the Duvidha repo rev #496)
WALi-ify Aditya's Partition stuff and include in build

This includes tests. WALi-ifying means add the yo emacs comments and
put in the right namespace and stuff.
Fix and turn off some warnings; fix a comment
Merge remote-tracking branch 'origin/master'