Add implication and convert to Minion

[niklasdewally]

Tracking issue: #511

Implements implication and conversion of implications to Minion.

Normalisation rules will be added in a follow up PR.

Changelog

Add Imply expression

Add the Imply expression type to represent material implication (x->y).
Implement parsing it using the JSON parser.

---

Convert implications to Minion

Convert Imply expressions to Minion.

This commit adds the following introduction rules (from Savile Row):

x -> y ~> reifyimply(y,x) if x is atomic, y is an non atomic expression
x -> y ~> ineq(x,y,0) if x is atomic, y is atomic

These are implemented together in introduce_reifyimply_ineq_from_imply.

Because the first rule uses the right hand side as a constraint,
implications cannot be flattened using flatten_generic. Implications
instead use flatten_implication, which only flattens the left hand
side.

This commit adds the following other rule changes:

• Add bool_eq_to_reify to convert boolean aux-vars to Minion.

  x =aux c ~> reify(c,x)
  x = c ~> reify(c,x)
  
  where c is a boolean constraint
  

• Flatten Not using flatten_generic

run_solver=true has been set for all implication tests except for
optimisations/implies-tautologies-cse. This test is staying disabled
for now, as it takes too long to solve with Minion in its current form.
However, this makes it ideal as a benchmark to measure the effect of
future optimisations.