- Added keylevels to symbols. This is to help pruning the proofs, for

terms and patterns that do not originate on regular nodes.

src/compiler.c

@@ -140,6 +140,9 @@ compile (Tac tc, int maxrunsset)
   /* process the tac */
   tacProcess (tac_root);
 
+  /* Clean up keylevels */
+  symbol_fix_keylevels ();
+
   /* cleanup */
   levelDone ();
 }
@@ -402,6 +405,14 @@ commEvent (int event, Tac tc)
       msg = tacTerm (tacTuple ((trip->next->next)));
       cl = NULL;
 
+      if (event == SEND)
+	{
+	  /* set keylevels based on send events */
+	  term_set_keylevels (fromrole);
+	  term_set_keylevels (torole);
+	  term_set_keylevels (msg);
+	}
+
       break;
     case CLAIM:
       /* now parse tuple info */

src/symbol.c

@@ -1,8 +1,10 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <stdarg.h>
+#include <limits.h>
 
 #include "symbol.h"
+#include "debug.h"
 #include "memory.h"
 
 /*
@@ -79,6 +81,7 @@ get_symb (void)
       t->allocnext = symb_alloc;
       symb_alloc = t;
     }
+  t->keylevel = INT_MAX;
   return t;
 }
 
@@ -206,6 +209,44 @@ symbolSysConst (const char *str)
   return symb;
 }
 
+//! Fix all the unset keylevels
+void
+symbol_fix_keylevels (void)
+{
+  int i;
+
+  for (i = 0; i < HASHSIZE; i++)
+    {
+      Symbol sym;
+
+      sym = symbtab[i];
+      while (sym != NULL)
+	{
+#ifdef DEBUG
+	  if (DEBUGL (5))
+	    {
+	      eprintf ("Symbol ");
+	      symbolPrint (sym);
+	    }
+#endif
+	  if (sym->keylevel == INT_MAX)
+	    {
+	      // Nothing currently, this simply does not originate on a strand.
+	    }
+#ifdef DEBUG
+	  else
+	    {
+	      if (DEBUGL (5))
+		{
+		  eprintf (" has keylevel %i\n", sym->keylevel);
+		}
+	    }
+#endif
+	  sym = sym->next;
+	}
+    }
+}
+
 //! Print out according to globalError
 /**
  * Input is comparable to printf, only depends on globalError. This should be used by any function trying to do output.

src/symbol.h

@@ -20,6 +20,8 @@ struct symbol
   int type;
   //! Line number at which it occurred.
   int lineno;
+  //! Level of occurrence in role nodes. 0 for as non-key, 1 for key only, 2 for key of key only, etc..
+  int keylevel;
   //! Ascii string with name of the symbol.
   const char *text;
   //! Possible next pointer.
@@ -41,6 +43,7 @@ Symbol lookup (const char *s);
 void symbolPrint (const Symbol s);
 void symbolPrintAll (void);
 Symbol symbolSysConst (const char *str);
+void symbol_fix_keylevels (void);
 
 void eprintf (char *fmt, ...);
 

src/term.c

@@ -986,20 +986,26 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
 
 	  if (realTermTuple (term))
 	    flag = flag
-	      && (term_iterate_deVar (term->left.op1, leaf, nodel, nodem, noder));
+	      &&
+	      (term_iterate_deVar
+	       (term->left.op1, leaf, nodel, nodem, noder));
 	  else
 	    flag = flag
-	      && (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder));
+	      &&
+	      (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder));
 
 	  if (nodem != NULL)
 	    flag = flag && nodem (term);
 
 	  if (realTermTuple (term))
 	    flag = flag
-	      && (term_iterate_deVar (term->left.op1, leaf, nodel, nodem, noder));
+	      &&
+	      (term_iterate_deVar
+	       (term->left.op1, leaf, nodel, nodem, noder));
 	  else
 	    flag = flag
-	      && (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder));
+	      &&
+	      (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder));
 
 	  if (noder != NULL)
 	    flag = flag && noder (term);
@@ -1108,8 +1114,7 @@ term_constrain_level (const Term term)
   int structure;
   int flag;
 
-  void
-  tcl_iterate (Term t)
+  void tcl_iterate (Term t)
   {
     t = deVar (t);
     structure++;
@@ -1141,3 +1146,58 @@ term_constrain_level (const Term term)
   tcl_iterate (term);
   return ((float) vars / (float) structure);
 }
+
+//! Adjust the keylevels of the symbols in a term.
+/**
+ * This is used to scan the roles. For each symbol, this function does the bookkeeping of the keylevels at which they occur.
+ */
+void
+term_set_keylevels (const Term term)
+{
+  void scan_levels (int level, Term t)
+  {
+#ifdef DEBUG
+    if (DEBUGL (5))
+      {
+	int c;
+
+	c = 0;
+	while (c < level)
+	  {
+	    eprintf ("  ");
+	    c++;
+	  }
+	eprintf ("Scanning keylevel %i for term ", level);
+	termPrint (t);
+	eprintf ("\n");
+      }
+#endif
+    if (realTermLeaf (t))
+      {
+	Symbol sym;
+
+	// So, it occurs at 'level' as key. If that is less than known, store.
+	sym = t->left.symb;
+	if (level < sym->keylevel)
+	  {
+	    // New minimum level
+	    sym->keylevel = level;
+	  }
+      }
+    else
+      {
+	if (realTermTuple (t))
+	  {
+	    scan_levels (level, t->left.op1);
+	    scan_levels (level, t->right.op2);
+	  }
+	else
+	  {
+	    scan_levels (level, t->left.op);
+	    scan_levels ((level + 1), t->right.key);
+	  }
+      }
+  }
+
+  scan_levels (0, term);
+}

src/term.h

@@ -177,5 +177,6 @@ int term_iterate_open_leaves (const Term term, int (*func) ());
 void term_rolelocals_are_variables ();
 int term_encryption_level (const Term term);
 float term_constrain_level (const Term term);
+void term_set_keylevels (const Term term);
 
 #endif

src/todo.txt

@@ -1,3 +1,4 @@
+- Agent terms must have keylevel 0; enforce this!
 - './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults.
 - Select_goal should consider, for singular variables, whether their
   type can be found in M_0. If so, the goal can be ignored.