- Reimplemented the weight functions for goal selection.

- Added --goal-select function, defaults to 3.

src/arachne.c

@@ -8,6 +8,7 @@
  */
 
 #include <limits.h>
+#include <float.h>
 #ifdef DEBUG
 #include <malloc.h>
 #endif
@@ -1201,6 +1202,78 @@ printSemiState ()
   eprintf ("!! - open: %i -\n", open);
 }
 
+//! Give an indication of the amount of consequences binding a term has
+/**
+ * Given a term, returns a float. 0: maximum consequences, 1: no consequences.
+ */
+float
+termBindConsequences (Term t)
+{
+  Termlist openVariables;
+
+  openVariables = termlistAddVariables(NULL, t);
+  if (openVariables == NULL)
+    {
+      // No variables, no consequences
+      return 1;
+    }
+  else
+    {
+      // For each run event in the semitrace, check whether it contains any
+      // of the open variables.
+      int totalCount;
+      int affectedCount;
+      int run;
+
+      totalCount = 0;
+      affectedCount = 0;
+      run = 0;
+      while (run < sys->maxruns)
+	{
+	  Roledef rd;
+	  int step;
+
+	  rd = sys->runs[run].start;
+	  step = 0;
+	  while (step < sys->runs[run].length)
+	    {
+	      Termlist tl;
+
+	      tl = openVariables;
+	      while (tl != NULL)
+		{
+		  if ((rd->type == READ || rd->type == SEND) && termSubTerm (rd->message, tl->term))
+		    {
+		      // This run event contains the open variable
+		      affectedCount++;
+		      tl = NULL;
+		    }
+		  else
+		    {
+		      tl = tl->next;
+		    }
+		}
+	      totalCount++;
+	      step++;
+	      rd = rd->next;
+	    }
+	  run++;
+	}
+
+      termlistDelete (openVariables);
+      if (totalCount > 0)
+	{
+	  // Valid computation
+	  return (float) (totalCount - affectedCount) / totalCount;
+	}
+      else
+	{
+	  // No consequences, ensure no division by 0
+	  return 1;
+	}
+    }
+}
+
 //------------------------------------------------------------------------
 // Larger logical componentents
 //------------------------------------------------------------------------
@@ -1213,6 +1286,11 @@ printSemiState ()
  *
  * 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.
+ *
+ * selection masks for --select-goal
+ *	1:	constrain level of term
+ * 	2:	key or not
+ * 	4:	consequences determination
  */
 Binding
 select_goal ()
@@ -1220,7 +1298,10 @@ select_goal ()
   List bl;
   Binding best;
   float min_constrain;
-  int max_level;
+  int mode;
+
+  // mode bits local storage
+  mode = sys->switchGoalSelectMethod;
 
   // Find the most constrained goal
   if (sys->output == PROOF)
@@ -1228,9 +1309,9 @@ select_goal ()
       indentPrint ();
       eprintf ("Listing open goals that might be chosen: ");
     }
-  max_level = INT_MIN;
+  min_constrain = FLT_MAX;
-  best = NULL;
   bl = sys->bindings;
+  best = NULL;
   while (bl != NULL)
     {
       Binding b;
@@ -1241,30 +1322,45 @@ select_goal ()
       if (!b->done && !realTermVariable (deVar (b->term)))
 	//if (!b->done)
 	{
-	  float cons;
+	  float buf_constrain;
+	  int buf_weight;
+
+	  void adapt (int w, float fl)
+	    {
+	      buf_constrain = buf_constrain + w * fl;
+	      buf_weight = buf_weight + w;
+	    }
+
+	  // buf_constrain is the addition of the factors before division by weight
+	  buf_constrain = 0;
+	  buf_weight = 0;
 
 	  if (sys->output == PROOF && best != NULL)
 	    eprintf (", ");
-	  if (b->level >= max_level)
+
+	  // Determine buf_constrain levels
+	  // Bit 0: 1 constrain level
+	  if (mode & 1) adapt (1, term_constrain_level (b->term));
+	  // Bit 1: 2 key level (inverted)
+	  if (mode & 2) adapt (2, 0.5 * (1 - b->level));
+	  // Bit 2: 4 consequence level
+	  if (mode & 4) adapt (2, termBindConsequences (b->term));
+
+	  // Weigh result
+	  if (buf_weight == 0 || buf_constrain <= min_constrain)
 	    {
-	      if (b->level > max_level)
+	      min_constrain = buf_constrain;
-		{
+	      best = b;
-		  max_level = b->level;
+	      if (sys->output == PROOF)
-		  min_constrain = 1;	// 1 is the maximum
+		eprintf ("*");
-		}
-	      cons = term_constrain_level (b->term);
-	      if (cons <= min_constrain)
-		{
-		  min_constrain = cons;
-		  best = b;
-		  if (sys->output == PROOF)
-		    eprintf ("*");
-		}
 	    }
 	  if (sys->output == PROOF)
 	    {
 	      termPrint (b->term);
-	      eprintf ("[%i]", b->level);
+	      if (mode & 2)
+		{
+	      	  eprintf ("[%i]", b->level);
+		}
 	    }
 	}
       bl = bl->next;
@@ -1279,6 +1375,7 @@ select_goal ()
 }
 
 //! Create a new intruder run to generate knowledge from m0
+
 int
 bind_goal_new_m0 (const Binding b)
 {

src/main.c

@@ -128,6 +128,8 @@ main (int argc, char **argv)
     arg_int0 ("r", "max-runs", NULL, "create at most <int> runs");
   struct arg_lit *switch_incremental_runs = arg_lit0 (NULL, "increment-runs",
 						      "incremental search using the number of runs");
+  struct arg_int *switch_goal_select_method =
+    arg_int0 (NULL, "goal-select", NULL, "use goal selection method <int> (default 0)");
   struct arg_lit *switch_latex_output =
     arg_lit0 (NULL, "latex", "output attacks in LaTeX format");
   struct arg_lit *switch_empty =
@@ -193,6 +195,7 @@ main (int argc, char **argv)
     switch_prune_proof_depth,
     switch_prune_trace_length, switch_incremental_trace_length,
     switch_maximum_runs, switch_incremental_runs,
+    switch_goal_select_method,
 
     switch_implicit_choose,
     switch_choose_first,
@@ -236,6 +239,7 @@ main (int argc, char **argv)
   switch_prune_proof_depth->ival[0] = -1;
   switch_maximum_runs->ival[0] = INT_MAX;
   switch_pruning_method->ival[0] = 2;
+  switch_goal_select_method->ival[0] = -1;
 
   /* Parse the command line as defined by argtable[] */
   nerrors = arg_parse (argc, argv, argtable);
@@ -533,6 +537,8 @@ main (int argc, char **argv)
     sys->switch_maxproofdepth = switch_prune_proof_depth->ival[0];
   if (switch_prune_trace_length->ival[0] >= 0)
     sys->switch_maxtracelength = switch_prune_trace_length->ival[0];
+  if (switch_goal_select_method->ival[0] >= 0)
+    sys->switchGoalSelectMethod = switch_goal_select_method->ival[0];
 #ifdef DEBUG
   /* in debugging mode, some extra switches */
   if (switch_debug_indent->count > 0)

src/system.c

@@ -74,6 +74,7 @@ systemInit ()
   sys->switchReduceClaims = 1;	// default remove claims from duplicate instance choosers
   sys->switchClaims = 0;	// default don't report on claims
   sys->switchClaimToCheck = NULL;	// default check all claims
+  sys->switchGoalSelectMethod = 3;	// default goal selection method
 
   /* set illegal traversal by default, to make sure it is set
      later */

src/system.h

@@ -141,6 +141,7 @@ struct system
   int switchReduceEndgame;	//!< Enable endgame cutter
   int switchReduceClaims;	//!< Symmetry reduction on claims (only works when switchAgentSymm is true)
   int switchClaims;		//!< Enable clails report
+  int switchGoalSelectMethod;	//!< Goal selection method for Arachne engine
   Term switchClaimToCheck;	//!< Which claim should be checked?
 
   //! Latex output switch.