- Key goals now have priority. This strategy yields complete proofs for

e.g. bke, and reduces states for NSL.

src/arachne.c

@@ -232,7 +232,7 @@ add_read_goals (const int run, const int old, const int new)
 		}
 	      termPrint (rd->message);
 	    }
-	  goal_add (rd->message, run, i);
+	  goal_add (rd->message, run, i, 0);
 	  count++;
 	}
       rd = rd->next;
@@ -489,7 +489,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	  {
 	    int keyrun;
 
-	    goal_add (tl->term, b->run_to, b->ev_to);
+	    goal_add (tl->term, b->run_to, b->ev_to, 1);
 	    tl = tl->next;
 	    keycount++;
 	  }
@@ -684,6 +684,8 @@ printSemiState ()
 /**
  * Selects the most constrained goal.
  *
+ * First selection is on level; thus, keys are selected first.
+ *
  * Because the list starts with the newest terms, and we use <= (as opposed to <), we
  * ensure that for goals with equal constraint levels, we select the oldest one.
  */
@@ -693,13 +695,14 @@ select_goal ()
   List bl;
   Binding best;
   float min_constrain;
+  int max_level;
 
   if (sys->output == PROOF)
     {
       indentPrint ();
       eprintf ("Listing open goals that might be chosen: ");
     }
-  min_constrain = 2;		// 1 is the maximum, but we want to initialize it.
+  max_level = -1;		// 0 is the minimum level
   best = NULL;
   bl = sys->bindings;
   while (bl != NULL)
@@ -719,6 +722,13 @@ select_goal ()
 
 	      if (sys->output == PROOF && best != NULL)
 		eprintf (", ");
+	      if (b->level >= max_level)
+		{
+		  if (b->level > max_level)
+		    {
+		      max_level = b->level;
+		      min_constrain = 1;	// 1 is the maximum
+		    }
 		  cons = term_constrain_level (b->term);
 		  if (cons <= min_constrain)
 		    {
@@ -727,8 +737,12 @@ select_goal ()
 		      if (sys->output == PROOF)
 			eprintf ("*");
 		    }
+		}
 	      if (sys->output == PROOF)
+		{
 		  termPrint (b->term);
+		  eprintf ("[%i]", b->level);
+		}
 	    }
 	}
       bl = bl->next;
@@ -1239,7 +1253,7 @@ add_claim_specifics (const Claimlist cl, const Roledef rd)
        * be reached (without reaching the attack).
        */
       cl->count = statesIncrease (cl->count);
-      goal_add (rd->message, 0, cl->ev);	// Assumption that all claims are in run 0
+      goal_add (rd->message, 0, cl->ev, 0);	// Assumption that all claims are in run 0
     }
 }
 

src/binding.c

@@ -40,6 +40,7 @@ binding_create (Term term, int run_to, int ev_to)
   graph = NULL;
   nodes = 0;
   b->term = term;
+  b->level = 0;
   return b;
 }
 
@@ -238,8 +239,12 @@ binding_print (const Binding b)
 
 
 //! Add a goal
+/**
+ * The int parameter 'level' is just to store additional info. Here, it stores priorities for a goal.
+ * Higher level goals will be selected first. Typically, a normal goal is level 0, a key is 1.
+ */
 void
-goal_add (Term term, const int run, const int ev)
+goal_add (Term term, const int run, const int ev, const int level)
 {
   term = deVar (term);
 #ifdef DEBUG
@@ -262,7 +267,7 @@ goal_add (Term term, const int run, const int ev)
       i = 0;
       while (i < width)
 	{
-	  goal_add (tupleProject (term, i), run, ev);
+	  goal_add (tupleProject (term, i), run, ev, level);
 	  if (i > 0)
 	    {
 	      Binding b;
@@ -278,6 +283,7 @@ goal_add (Term term, const int run, const int ev)
       Binding b;
 
       b = binding_create (term, run, ev);
+      b->level = level;
       sys->bindings = list_insert (sys->bindings, b);
     }
 }

src/binding.h

@@ -22,6 +22,7 @@ struct binding
   int nodes;
 
   Term term;
+  int level;
 };
 
 typedef struct binding *Binding;
@@ -36,7 +37,7 @@ int node_number (int run, int ev);
 
 int binding_print (Binding b);
 
-void goal_add (Term term, const int run, const int ev);
+void goal_add (Term term, const int run, const int ev, const int level);
 void goal_remove_last ();
 int goal_bind (const Binding b, const int run, const int ev);
 void goal_unbind (const Binding b);