Summary:
This makes sure we call `AbductiveDomain.summary_of_post` exactly once
per post-condition. Notice in particular in the diff:
- in Pulse.ml we remove a now-certified-useless "is_unsat_expensive"
  call
- in PulseOperations.ml we add a previously-missing call to
  `summary_of_post` (it's needed to remove local variables from the
  symbolic state + normalize)

The price to pay is ugly type annotations and down-casting peppered in a
few places, in reasonable number.

Reviewed By: da319

Differential Revision: D24078564

fbshipit-source-id: 3102cacf0