diff options
author | Michal Moskal <michal@moskal.me> | 2011-10-19 15:36:14 -0700 |
---|---|---|
committer | Michal Moskal <michal@moskal.me> | 2011-10-19 15:36:14 -0700 |
commit | 39b0ec5cf8900757bb19c13cb692b2414de91475 (patch) | |
tree | 29202b260b0776fbacb13c1fd9ced136357269b8 /Source/Model | |
parent | 512562d0c48d7d71b5579476c3e07ba5c3c41817 (diff) |
Performance improvements in BVD
Diffstat (limited to 'Source/Model')
-rw-r--r-- | Source/Model/Model.cs | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index f54ebbef..643a6b03 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -241,6 +241,31 @@ namespace Microsoft.Boogie /// </summary>
public Element TryEval(params Element[] args)
{
+ for (int i = 0; i < args.Length; ++i)
+ if(args[i]==null)
+ throw new ArgumentException();
+
+ if (apps.Count > 10) {
+ var best = apps;
+ for (int i = 0; i < args.Length; ++i)
+ if (args[i].references.Count < best.Count)
+ best = args[i].references;
+ if (best != apps) {
+ foreach (var tpl in best) {
+ bool same = true;
+ if (tpl.Func != this)
+ continue;
+ for (int i = 0; i < args.Length; ++i)
+ if (tpl.Args[i] != args[i]) {
+ same = false;
+ break;
+ }
+ if (same) return tpl.Result;
+ }
+ return null;
+ }
+ }
+
foreach (var tpl in apps) {
bool same = true;
for (int i = 0; i < args.Length; ++i)
|