diff options
| author | Guillaume Melquiond | 2016-09-29 18:59:57 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-10-01 09:07:24 +0200 |
| commit | 2e7c8893e6df7af924dba0291f70dd6fa771cb78 (patch) | |
| tree | d872a35440e85efb94133dd3e29ec0d6a5ff932d /test-suite/output/PrintModule.v | |
| parent | cc407dc4272928944af06ee141d71ff3c9622347 (diff) | |
Speed up the Search commands.
The blacklist set was converted into a string list for each item in the
environment during a search. In fact, the blacklist was checked for
each item, even if the item was already known to be ultimately discarded.
This commit fixes both performance issues. First, blacklist_filter is no
longer used directly but in two stages. Second, the boolean values are
no longer computed before calling the shortcutting operators. It seems
like someone had already noticed part of the second issue, since some (but
not all) of the boolean values were lazily computed.
The speed up becomes noticeable when the blacklist set contains more than
four elements.
Diffstat (limited to 'test-suite/output/PrintModule.v')
0 files changed, 0 insertions, 0 deletions
