From 88e2f3d26ca0884444f6690e81ece31ac9a4418b Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Fri, 11 Mar 2005 20:41:59 +0000
Subject: [PATCH] - Added a better reverse-engineered variation of the Athena
 goal   selector. - Added an idea that might make searches somewhat faster.

---
 src/arachne.c | 100 +++++++++++++++++++++++++++++++++++++++++++++-----
 src/todo.txt  |   2 +
 2 files changed, 92 insertions(+), 10 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index 6c23a4e..dfd4f5c 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -36,6 +36,7 @@ extern Term CLAIM_Niagree;
 extern Term TERM_Agent;
 extern Term TERM_Hidden;
 extern Term TERM_Function;
+extern Term TERM_Nonce;
 
 extern int *graph;
 extern int nodes;
@@ -1676,6 +1677,71 @@ termBindConsequences (Term t)
     }
 }
 
+//! Determine whether a term is an open nonce variable
+/**
+ * Does not explore subterms
+ */
+int
+isOpenNonceVar (Term t)
+{
+  t = deVar (t);
+  if (realTermVariable (t))
+    {
+      return inTermlist (t->stype, TERM_Nonce);
+    }
+  else
+    {
+      return 0;
+    }
+}
+
+//! Count unique open variables in term
+/**
+ */
+int count_open_variables (const Term t)
+{
+  Termlist tl;
+  int n;
+
+  tl = NULL;
+  termlistAddVariables (tl, t);
+  n = 0;
+  while (tl != NULL)
+    {
+      if (!inTermlist (tl->next, t))
+	{
+	  if (isOpenNonceVar (t))
+	    {
+	      n = n + 1;
+	    }
+	}
+      tl = tl->next;
+    }
+  termlistDelete (tl);
+  return n;
+}
+
+//! Athena-like factor
+/**
+ * Lower is better (more nonce variables)
+ */
+float
+term_noncevariables_level (const Term t)
+{
+  int onv;
+  const int enough = 2;
+
+  onv = count_open_variables (t);
+  if (onv >= enough)
+    {
+      return 0;
+    }
+  else
+    {
+      return 1 - (onv/enough);
+    }
+}
+
 //------------------------------------------------------------------------
 // Larger logical componentents
 //------------------------------------------------------------------------
@@ -1785,13 +1851,23 @@ select_goal ()
 	    {
 	      float buf_constrain;
 	      int buf_weight;
+	      int smode;
 
-	      void adapt (int w, float fl)
+	      void adapt (const int w, const float fl)
 	      {
 		buf_constrain = buf_constrain + w * fl;
 		buf_weight = buf_weight + w;
 	      }
 
+	      void erode (const int w, const float fl)
+		{
+		  if (smode & 1)
+		    {
+		      adapt (w,fl);
+		    }
+		  smode = smode / 2;
+		}
+
 	      // buf_constrain is the addition of the factors before division by weight
 	      buf_constrain = 0;
 	      buf_weight = 0;
@@ -1799,19 +1875,23 @@ select_goal ()
 	      if (sys->output == PROOF && best != NULL)
 		eprintf (", ");
 
+	      // We will shift this mode variable
+	      smode = mode;
+
 	      // Determine buf_constrain levels
 	      // Bit 0: 1 constrain level
-	      if (mode & 1)
-		adapt (1, term_constrain_level (b->term));
+		erode (1, term_constrain_level (b->term));
 	      // Bit 1: 2 key level (inverted)
-	      if (mode & 2)
-		adapt (1, 0.5 * (1 - b->level));
+		erode (1, 0.5 * (1 - b->level));
 	      // Bit 2: 4 consequence level
-	      if (mode & 4)
-		adapt (1, termBindConsequences (b->term));
-	      // Bit 4: 16 single variables first
-	      if (mode & 16)
-		adapt (4, 1 - isTermVariable (b->term));
+		erode (1, termBindConsequences (b->term));
+	      // Bit 3: 8 single variables first
+		erode (1, 1 - isTermVariable (b->term));
+	      // Bit 4: 16 nonce variables level (Cf. what I think is in Athena)
+	        erode (1, term_noncevariables_level (b->term));
+	      // Define legal range
+	      if (smode > 0)
+		error ("--goal-select mode %i is illegal", mode);
 
 	      // Weigh result
 	      if (buf_weight == 0 || buf_constrain <= min_constrain)
diff --git a/src/todo.txt b/src/todo.txt
index 0e884b4..9b3b48e 100644
--- a/src/todo.txt
+++ b/src/todo.txt
@@ -1,3 +1,5 @@
 - Add something of a 'history list of bound goals', through the arachne
   engine. Then, put a limit on the amount of times some goal occurs: the
   goal selection might ignore that goal then, for further selection.
+- Maybe it helps to fix the agents of the claim run (i.e. all different
+  agents?, this restricts the attacks somewhat), make a switch for this.