From 6cd8007ab016cf05e8f3b177cd0db5617479c656 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Wed, 10 Nov 2010 22:01:38 +0100
Subject: [PATCH] EFFICIENCY: New (default) heuristic.

Given that sk/pk/k are now hardcoded, we can exploit their occurrences with this
new heuristic.

The heuristic can now scan for the lowest term depth at which either sk or k occur.
This will cause the heuristic to favor looking for sk, then sk(x), and only later
other terms. In a small test this was twice as fast. For protocols based on pk only
the performance loss should be negligible.

The old heuristic was 162, now it is 162+512 = 674.
---
 src/heuristic.c | 73 +++++++++++++++++++++++++++++++++++++++++++++++++
 src/switches.c  |  4 +--
 2 files changed, 75 insertions(+), 2 deletions(-)

diff --git a/src/heuristic.c b/src/heuristic.c
index 646b4cb..179125b 100644
--- a/src/heuristic.c
+++ b/src/heuristic.c
@@ -217,6 +217,76 @@ term_constcount (const System sys, Term t)
   return ratio;
 }
 
+//! determine lowest level at which sk/sk occurs, or -1 otherwise.
+int
+lowest_skk_level (Term t)
+{
+  t = deVar (t);
+  if (t == NULL)
+    {
+      return -1;
+    }
+  if (isTermEqual (t, TERM_SK) || isTermEqual (t, TERM_K))
+    {
+      return 0;
+    }
+  if (realTermLeaf (t))
+    {
+      return -1;
+    }
+  if (realTermTuple (t))
+    {
+      int x, y;
+      x = lowest_skk_level (TermOp1 (t));
+      y = lowest_skk_level (TermOp2 (t));
+      if (x < 0)
+	return y;
+      if (y < 0)
+	return x;
+      if (y < x)
+	return y;
+      else
+	return x;
+    }
+  else
+    {
+      int x, y;
+      x = lowest_skk_level (TermOp (t));
+      y = lowest_skk_level (TermKey (t));
+      if (x < 0)
+	return y + 1;
+      if (y < 0)
+	return x + 1;
+      if (y < x)
+	return y + 1;
+      else
+	return x + 1;
+    }
+}
+
+//! count sk/k level depth
+float
+term_skk_level (const System sys, Term t)
+{
+  int l;
+
+  l = lowest_skk_level (t);
+  if (l < 0)
+    {
+      return 1.0;
+    }
+  else
+    {
+      float res;
+
+      res = l / 4;
+      if (res > 1)
+	return 1;
+      else
+	return res;
+    }
+}
+
 //! Determine the weight of a given goal
 /**
  * 0 to ... (lower is better)
@@ -281,6 +351,9 @@ computeGoalWeight (const System sys, const Binding b)
   // Bit 8: 256 use known nonces (Athena try 2), half weight
   erode (0.5 * term_constcount (sys, t));
 
+  // Bit 9: 512 do sk first (first sk, then sk occurrence level 1, etc)
+  erode (16 * term_skk_level (sys, t));
+
   // Define legal range
   if (smode > 0)
     error ("--heuristic mode %i is illegal", switches.heuristic);
diff --git a/src/switches.c b/src/switches.c
index c7884d2..ca9c82a 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -72,7 +72,7 @@ switchesInit (int argc, char **argv)
   switches.maxOfRole = 0;	// no maximum default
 
   // Arachne
-  switches.heuristic = 162;	// default goal selection method
+  switches.heuristic = 674;	// default goal selection method (used to be 162)
   switches.maxIntruderActions = INT_MAX;	// max number of encrypt/decrypt events
   switches.agentTypecheck = 1;	// default do check agent types
   switches.concrete = true;	// default removes symbols, and makes traces concrete
@@ -961,7 +961,7 @@ switcher (const int process, int index, int commandline)
 	{
 	  if (switches.expert)
 	    {
-	      helptext ("    --heuristic=<int>", "use heuristic <int> [162]");
+	      helptext ("    --heuristic=<int>", "use heuristic <int> [674]");
 	    }
 	}
       else