kind2-mc/kind2 — pull request #205 by AdrienChampion (2014-12-23 21:41:48+00:00)
Title: 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
```