- Improved heuristics. Default is now 162 (but 99 performs equally well)

src/heuristic.c

@@ -236,6 +236,39 @@ newkeylevel (const int level)
     return 1;
 }
 
+//! count local constants
+float
+term_constcount (const System sys, Term t)
+{
+  int n, total;
+  float ratio;
+
+  int countMe (Term t)
+  {
+    if (TermRunid (t) >= 0)
+      {
+	total++;
+	if (!isTermVariable (t))
+	  {
+	    n++;
+	  }
+      }
+  }
+
+  n = 0;
+  total = 0;
+  term_iterate_deVar (t, countMe, NULL, NULL, NULL);
+  if (total == 0)
+    {
+      ratio = 1;
+    }
+  else
+    {
+      ratio = ((total - n) / total);
+    }
+  return ratio;
+}
+
 //! Determine the weight of a given goal
 /**
  * 0 to ... (lower is better)
@@ -287,11 +320,24 @@ computeGoalWeight (const System sys, const Binding b)
   // Bit 3: 8 nonce variables level (Cf. what I think is in Athena)
   erode (term_noncevariables_level (t));
 
+  // Bit 4: 16 use hidelevel (normal)
+  erode (1 * weighHidelevel (sys, t, 0.5, 0.5));
+  // Bit 5: 32 use known nonces (Athena try 2)
+  erode (term_constcount (sys, t));
+
+  // Bit 6: 64 use hidelevel (but only single-weight)
+  erode (weighHidelevel (sys, t, 0.5, 0.5));
+  // Bit 7: 128 use hidelevel (quadruple-weight)
+  erode (4 * weighHidelevel (sys, t, 0.5, 0.5));
+
+  // Bit 8: 256 use known nonces (Athena try 2), half weight
+  erode (0.5 * term_constcount (sys, t));
+
   // Define legal range
   if (smode > 0)
     error ("--heuristic mode %i is illegal", switches.heuristic);
 
-  // Return total weight
+  // Return
   return w;
 }
 

src/switches.c

@@ -49,7 +49,7 @@ switchesInit (int argc, char **argv)
   switches.maxAttacks = 0;	// no maximum default
 
   // Arachne
-  switches.heuristic = 3;	// default goal selection method
+  switches.heuristic = 162;	// default goal selection method
   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
@@ -829,7 +829,7 @@ switcher (const int process, int index, int commandline)
 	{
 	  if (switches.expert)
 	    {
-	      helptext ("    --heuristic=<int>", "use heuristic <int> [3]");
+	      helptext ("    --heuristic=<int>", "use heuristic <int> [162]");
 	    }
 	}
       else