- Added a --timer=x switch to abort Arachne proofs after x seconds.

src/arachne.c

@@ -28,6 +28,7 @@
 #include "debug.h"
 #include "binding.h"
 #include "warshall.h"
+#include "timer.h"
 
 extern Term CLAIM_Secret;
 extern Term CLAIM_Nisynch;
@@ -2005,6 +2006,18 @@ prune_bounds ()
   Termlist tl;
   List bl;
 
+  /* prune for time */
+  if (passed_time_limit ())
+    {
+      // Oh no, we ran out of time!
+      if (sys->output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf ("Pruned: ran out of allowed time (-T %i switch)\n", get_time_limit () );
+	}
+      return 1;
+    }
+
   /* prune for proof depth */
   if (proofDepth > sys->switch_maxproofdepth)
     {

src/main.c

@@ -53,6 +53,7 @@ enum exittypes
 #include "symbol.h"
 #include "parser.h"
 #include "tac.h"
+#include "timer.h"
 #include "compiler.h"
 #include "latex.h"
 #include "output.h"
@@ -161,6 +162,8 @@ main (int argc, char **argv)
 					     "show summary on stdout instead of stderr");
   struct arg_lit *switch_echo =
     arg_lit0 ("E", "echo", "echo command line to stdout");
+  struct arg_int *switch_timer =
+    arg_int0 ("T", "timer", NULL, "maximum time in seconds");
 #ifdef DEBUG
   struct arg_int *switch_por_parameter =
     arg_int0 (NULL, "pp", NULL, "POR parameter");
@@ -191,6 +194,7 @@ main (int argc, char **argv)
     switch_traversal_method,
     switch_match_method,
     switch_clp,
+    switch_timer,
     switch_pruning_method,
     switch_prune_proof_depth,
     switch_prune_trace_length, switch_incremental_trace_length,
@@ -240,6 +244,7 @@ main (int argc, char **argv)
   switch_maximum_runs->ival[0] = INT_MAX;
   switch_pruning_method->ival[0] = 2;
   switch_goal_select_method->ival[0] = -1;
+  switch_timer->ival[0] = 0;
 
   /* Parse the command line as defined by argtable[] */
   nerrors = arg_parse (argc, argv, argtable);
@@ -520,6 +525,7 @@ main (int argc, char **argv)
   sys->match = switch_match_method->ival[0];
   mgu_match = sys->match;
   sys->prune = switch_pruning_method->ival[0];
+  set_time_limit (switch_timer->ival[0]);
   if (switch_progress_bar->count > 0)
     /* enable progress display */
     sys->switchS = 50000;

src/timer.c

@@ -0,0 +1,52 @@
+#include "timer.h"
+
+#include <time.h>
+#include <sys/times.h>
+
+static int time_max_seconds = 0;
+static clock_t endwait = 0;
+
+//! Set initial time limit.
+/**
+ * <= 0 means none.
+ */
+void set_time_limit (int seconds)
+{
+  if (seconds > 0)
+    {
+      time_max_seconds = seconds;
+      endwait = seconds * CLK_TCK;
+    }
+  else
+    {
+      time_max_seconds = 0;
+      endwait = 0;
+    }
+  printf ("Timer: %i\n", time_max_seconds);
+}
+
+//! Retrieve time limit
+int get_time_limit ()
+{
+  return time_max_seconds;
+}
+
+//! Check whether time limit has passed.
+int passed_time_limit ()
+{
+  if (endwait <= 0)
+    {
+      return 0;
+    }
+  else
+    {
+      struct tms t;
+
+      times(&t);
+      if (t.tms_utime > endwait)
+	  return 1;
+      else
+	  return 0;
+    }
+}
+

src/timer.h

@@ -0,0 +1,8 @@
+#ifndef TIMER
+#define TIMER
+
+void set_time_limit (int seconds);
+int get_time_limit ();
+int passed_time_limit ();
+
+#endif