diff options
| author | Alasdair | 2019-01-14 21:06:01 +0000 |
|---|---|---|
| committer | Alasdair | 2019-01-14 21:06:01 +0000 |
| commit | ef61b884cecc2c8ab11d7db1c1c593005be865e6 (patch) | |
| tree | c95eb1d920def478ad406999a581a51e3ad1b627 /src/rewriter.mli | |
| parent | 154e822f482c63b067bfe62dbbbffc565c1cc6ba (diff) | |
Add a function to perform re-writes in parallel
rewrite_defs_base_parallel j is the same as rewrite_defs_base
except it performs the re-writes in j parallel processes. Currently
only the trivial_sizeof re-write is parallelised this way with a
default of 4. This works on my machine (TM) but may fail elsewhere.
Because 2019 OCaml concurrency support is lacking, we use Unix.fork
and Marshal.to_channel to send the info from the child processes
performing the re-write back to the parent.
Also fix a missing case in pretty_print_lem
Diffstat (limited to 'src/rewriter.mli')
| -rw-r--r-- | src/rewriter.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/rewriter.mli b/src/rewriter.mli index 53b892d4..ec4e381c 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -70,6 +70,8 @@ val rewrite_defs : tannot defs -> tannot defs val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs +val rewrite_defs_base_parallel : int -> tannot rewriters -> tannot defs -> tannot defs + (* Same as rewrite_defs base but display a progress bar when verbosity >= 1 *) val rewrite_defs_base_progress : string -> tannot rewriters -> tannot defs -> tannot defs |