mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Java API: Make enum lookup more efficient.

Browse source 
The existing code causes an allocation of an array with all enum values
on every method call (inside the values() method),
and loops over all enum entries.
This commit is contained in:
Philipp Wendler 2016-07-22 17:28:40 +02:00
parent f325b51213
commit c3b8c15f35
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

16
scripts/mk_genfile_common.py
View file

@ -323,6 +323,9 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir):
generated_enumeration_files.append(efile.name)
efile.write('/**\n * Automatically generated file\n **/\n\n')
efile.write('package %s.enumerations;\n\n' % package_name)
efile.write('import java.util.HashMap;\n')
efile.write('import java.util.Map;\n')
efile.write('\n')
efile.write('/**\n')
efile.write(' * %s\n' % name)
@ -342,9 +345,18 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir):
efile.write(' %s(int v) {\n' % name)
efile.write(' this.intValue = v;\n')
efile.write(' }\n\n')
efile.write(' // Cannot initialize map in constructor, so need to do it lazily.\n')
efile.write(' // Easiest thread-safe way is the initialization-on-demand holder pattern.\n')
efile.write(' private static class %s_MappingHolder {\n' % name)
efile.write(' private static final Map<Integer, %s> intMapping = new HashMap<>();\n' % name)
efile.write(' static {\n')
efile.write(' for (%s k : %s.values())\n' % (name, name))
efile.write(' intMapping.put(k.toInt(), k);\n')
efile.write(' }\n')
efile.write(' }\n\n')
efile.write(' public static final %s fromInt(int v) {\n' % name)
efile.write(' for (%s k: values()) \n' % name)
efile.write(' if (k.intValue == v) return k;\n')
efile.write(' %s k = %s_MappingHolder.intMapping.get(v);\n' % (name, name))
efile.write(' if (k != null) return k;\n')
efile.write(' throw new IllegalArgumentException("Illegal value " + v + " for %s");\n' % name)
efile.write(' }\n\n')
efile.write(' public final int toInt() { return this.intValue; }\n')