- Code refactoring.

src/cost.c

@@ -7,67 +7,12 @@
  *
  */
 #include "switches.h"
+#include "system.h"
 
 //************************************************************************
 // Private methods
 //************************************************************************
 
-//! determine whether a run is a so-called self-initiator
-int
-selfInitiator (const System sys, const int run)
-{
-  int self_initiator;
-
-  self_initiator = false;
-  if (sys->runs[run].role->initiator)
-    {
-      // An initiator
-      Termlist agents;
-      Termlist seen;
-
-      agents = sys->runs[run].rho;
-      seen = NULL;
-      while (agents != NULL)
-	{
-	  Term agent;
-
-	  agent = agents->term;
-	  if (inTermlist (seen, agent))
-	    {
-	      // This agent was already in the seen list
-	      self_initiator = true;
-	    }
-	  else
-	    {
-	      seen = termlistAdd (seen, agent);
-	    }
-	  agents = agents->next;
-	}
-      termlistDelete (seen);
-    }
-  return self_initiator;
-}
-
-//! Count the number of any self-initiators
-int
-selfInitiators (const System sys)
-{
-  int count;
-  int run;
-
-  count = 0;
-  run = 0;
-  while (run < sys->maxruns)
-    {
-      if (selfInitiator (sys, run))
-	{
-	  count++;
-	}
-      run++;
-    }
-  return count;
-}
-
 //************************************************************************
 // Public methods
 //************************************************************************

src/prune_theorems.c

@@ -210,21 +210,7 @@ prune_theorems (const System sys)
    */
   if (switches.extravert)
     {
-      int run;
+      if (selfInitiators (sys) > 0)
-
-      for (run = 0; run < sys->maxruns; run++)
-	{
-	  // Check this run only if it is an initiator role
-	  if (sys->runs[run].role->initiator)
-	    {
-	      // Check this initiator run
-	      Termlist tl;
-	      Termlist found;
-
-	      found = NULL;
-	      for (tl = sys->runs[run].rho; tl != NULL; tl = tl->next)
-		{
-		  if (inTermlist (found, tl->term))
 	{
 	  // XXX TODO
 	  // Still need to fix proof output for this
@@ -232,11 +218,6 @@ prune_theorems (const System sys)
 	  // Pruning because some agents are equal for this role.
 	  return true;
 	}
-		  found = termlistAdd (found, tl->term);
-		}
-	      termlistDelete (found);
-	    }
-	}
     }
 
   // Prune wrong agents type for initators

src/system.c

@@ -1398,3 +1398,62 @@ eventRoledef (const System sys, const int run, const int ev)
 {
   return roledef_shift (sys->runs[run].start, ev);
 }
+
+//! determine whether a run is a so-called self-initiator
+/**
+ * Alice starting a run with Bob, Charlie, Bob is also counted as self-initiation.
+ */
+int
+selfInitiator (const System sys, const int run)
+{
+  int self_initiator;
+
+  self_initiator = false;
+  if (sys->runs[run].role->initiator)
+    {
+      // An initiator
+      Termlist agents;
+      Termlist seen;
+
+      agents = sys->runs[run].rho;
+      seen = NULL;
+      while (agents != NULL)
+	{
+	  Term agent;
+
+	  agent = agents->term;
+	  if (inTermlist (seen, agent))
+	    {
+	      // This agent was already in the seen list
+	      self_initiator = true;
+	    }
+	  else
+	    {
+	      seen = termlistAdd (seen, agent);
+	    }
+	  agents = agents->next;
+	}
+      termlistDelete (seen);
+    }
+  return self_initiator;
+}
+
+//! Count the number of any self-initiators
+int
+selfInitiators (const System sys)
+{
+  int count;
+  int run;
+
+  count = 0;
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (selfInitiator (sys, run))
+	{
+	  count++;
+	}
+      run++;
+    }
+  return count;
+}

src/system.h

@@ -201,6 +201,8 @@ int iterateLocalToOther (const System sys, const int myrun,
 			 int (*callback) (Term t));
 int firstOccurrence (const System sys, const int r, Term t, int evtype);
 Roledef eventRoledef (const System sys, const int run, const int ev);
+int selfInitiator (const System sys, const int run);
+int selfInitiators (const System sys);
 
 
 //! Equality for run structure naming