Added some options for the human-readable debugging output
Renamed parameter of ItemTree.addChildAndMerge
Hopefully fixed bugs concerning optimization problems with multi-level i-trees
Added weak normalization from the new SHARP
Adding empty leaves / root has now been migrated into SHARP
Removed XXX in QSAT encoding
Added fold markers to all source files
Hopefully fixed bug when merging two item tree nodes. The merged (i.e., eliminated) node's children must be informed of their new parent.
Added fold markers to ClaspCallback classes
Hopefully fixed an issue when using costs for multi-level encodings that
was caused by wrongly merging sibling item trees.

Consider these two sibling i-trees (where a,b,c are items and 1,2 are costs):

a 1
|- b 2
|- c 1

a 1
|- b 1
|- c 2

The existing D-FLAT algorithm merges them since they are equal w.r.t. item sets.
Result of this merging:

a 1    [results from merging the two roots]
|- b 1 [results from merging b 2 with b 1 -- b 1 is better and thus used]
|- c 1 [results from merging c 1 with c 2 -- c 1 is better and thus used]

This result is wrong. To see the reason, consider this i-tree as representing a game. If we play "a" in our first move on this resulting i-tree, what we actually play (in the complete game tree) is one of the (at least two) extensions of the "a" node. Depending on which of these (at least) two extensions we have played, our next move, say "c", corresponds to a move leading to cost 1 in one case, and to a move leading to cost 2 in the other case. The latter witnesses that it is wrong to associate only a cost of 1 with the "c" node of the resulting i-tree. What to do?

It seems to me that it is reasonable not to merge the original two i-trees even though they are equal w.r.t. item sets. That is, two i-trees shall only be equal if they (recursively) have equal item sets -- as before -- and additionally all nodes except possibly the root have equal costs. (Note that for sibling leaves this means that only their item sets must be equal -- the costs may be distinct.)

Note that now we are in the seemingly strange situation that the item trees "b 1" and "b 2", as well as "c 1" and "c 2" are equal, but the following are not.

a 1
|- b 2
|- c 1

a 1
|- b 1
|- c 2
Made compiler shut up about an unjustified warning
Made non-unicode item tree output more beautiful.
Switched to latest clasp version and updated INSTALL file
pulled upstream