[Integration of Porridge] Generalized POR

[LCBH]

This PR integrates the library Porridge (see companion paper) into DeepSec.

Compared to the built-in POR techniques already implemented in DeepSec, Porridge provides a new POR technique that can be applied to any process (instead of action-determinate processes) but whose reduction, in terms of removal of traces, is often much less important. Unfortunately for now, the pre-computation handled by Porridge can be impractically long for large processes. Furthermore, some syntactical conditions over the input processes mut be fulfilled (this is only for easing the integration), most of them are checked at runtime. Therefore, Porridge is opt-in: one needs to use the option -with_por_gen. All concerned options are labeled Experimental.

This PR includes:

• the library Porridge in the folder porridge/,
• an interface between processes and traces as represented in DeepSec and as represented in Porridge: Source/core_library/por.ml (some .mli had to be modified),
• an integration of the search restriction guided by Porridge: Source/subterms/equivalence*.ml*,
• new installation instructions (README.md),
• some debugging utilities have been modified/improved,
• new examples in Examples/POR_gen/ (those examples are discussed in the ESORICS'18 paper).

[LCBH]

The commit 81132537be5ba13c04a68019d343475d93ebb44d can be reversed if you actually like the output line (Stats) ---- Number of explorations [118]., even when generalized POR is disabled.

[VincentCheval]

A new version of Deepsec is coming very soon. So I'm thinking of merging Porridge for this new version.