External calls to invariant generation

Added support for external calls to invariant generation.
Typical usage is explained below, see `invGenGraph.mli` for the details.

When calling invariant generation, do call the `no_more_lsd` function to destroy the underlying lsd instance. If you don't and invGen is running when exiting, lsd will not be killed.

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
```ocaml
(* ...a function to generate terms, *)
val generate_terms : unit -> Term.t list
(* ...a bool flag for candidate term synthesis from state variables of the system, *)
val synthesis : bool
(* ...a bool flag for candidate term mining from initial predicate of the system, *)
val mine_init : bool
(* ...and a bool flag for candidate term mining from transition predicate of the system. *)
val mine_trans : bool
```

Code:
```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

    (* Bla. *)
    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
```