External calls to invariant generation

Added support for external calls to invariant generation.
Typical usage is explained below, see `invGenGraph.mli` for the details.

An `ignore` set is used to remind invariant generation to ignore some candidate invariants as it does not maintain any internal state. This set typically contains trivial invariants, invariants discovered and invariants received by the rest of the framework.

Examples of calls to invariant generation follow, assuming a function
```ocaml
val generate_terms : unit -> Term.t list
```
to generate some terms to mine.

```ocaml
(* Mine system for candidates if you like. *)
let system_candidates =
  mine_system
    synthesis mine_init mine_trans system
  in

let rec loop ignore =

  (* Generate some terms to mine the way you want. *)
  let terms = generate_terms () in

  (* Then, either... *)
    if you_want then

      (* ...first mine candidates... *)
      let all_candidates =
        mine_terms
        (* Mined candidates are added to [system_candidates]. *)
          system terms system_candidates
      in
      Term.TermSet.cardinal all_candidates
      |> Event.log L_info "Got %i candidate terms."
      (* ...then run invariant generation. *)
      let invariants', ignore' =
        run system ignore maxK all_candidates
      in

      (* Bla. *)
      Term.TermSet.cardinal invariants'
      |> Event.log L_info "Found %i invariants."

      loop ignore'

    else

      (* ...or just run directly. *)
      let invariants', ignore' =
        mine_terms_run
          system ignore maxK terms system_candidates
      in

      (* Bla. *)
      Term.TermSet.cardinal invariants'
      |> Event.log L_info "Found %i invariants."

      loop ignore'
in

loop Term.TermSet.empty
```

Note that you can also accumulate candidate terms:

```ocaml
let rec loop ignore candidates =
  (* Generate terms. *)
  let terms = generate_terms () in

  (* Mine them, adding to the candidate accumulator. *)
  let candidates' =
    mine_terms system terms candidates
  in

  (* Run invariant generation on all candidates. *)
  let invariants', ignore' =
    run system ignore maxK candidates'
  in

  (* Bla. *)
  Term.TermSet.cardinal invariants'
  |> Event.log L_info "Found %i invariants."

  loop ignore' candidates'
in

(* Launching on the candidates from the system. *)
mine_system
  synthesis mine_init mine_trans system
|> loop Term.TermSet.empty
```