summaryrefslogtreecommitdiff
path: root/Source/Model
diff options
context:
space:
mode:
authorGravatar Michal Moskal <michal@moskal.me>2011-10-19 15:36:14 -0700
committerGravatar Michal Moskal <michal@moskal.me>2011-10-19 15:36:14 -0700
commit39b0ec5cf8900757bb19c13cb692b2414de91475 (patch)
tree29202b260b0776fbacb13c1fd9ced136357269b8 /Source/Model
parent512562d0c48d7d71b5579476c3e07ba5c3c41817 (diff)
Performance improvements in BVD
Diffstat (limited to 'Source/Model')
-rw-r--r--Source/Model/Model.cs25
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)