aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/PrintModule.v
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-09-29 18:59:57 +0200
committerGuillaume Melquiond2016-10-01 09:07:24 +0200
commit2e7c8893e6df7af924dba0291f70dd6fa771cb78 (patch)
treed872a35440e85efb94133dd3e29ec0d6a5ff932d /test-suite/output/PrintModule.v
parentcc407dc4272928944af06ee141d71ff3c9622347 (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