Fix a bug in Simplifier

In a shared node, when merging contextes, CollectContext did not
update the mcontext array in the CollectContext-object, which is used for
collecting the contextes of the children of a shared node.
Made echo function publicly available in the Script interface.  Instead of adding a requested comment function to the Script interface or the LoggingScript, we decided to add the echo functionality instead.  Note that this function should not have any negative effect since it is mostly implemented as a no-op.  Only the LoggingScript actually does something more than returning the input.
Fixed endCheck notification

The notification was missing in all cases in DPLLEngine.solve.  This lead to bad performance and even worse interpolants in many cases.
Introduced proof rule distinctBoolEq.

This rule is used to transform a distinct term over Boolean terms into an
equality where one of the two terms gets negated.
Updated proof documentation.

The proof documentation was missing the rule :distinctBoolEq.  A presentation
of this rule was added.  To this point, no additional documentation is present
since the rule should be self-explanatory.
Merge remote-tracking branch 'christj/master'