From e0e56964d14127b19937dca680e5f6b1a1624750 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 5 Jan 2005 15:29:27 +0000 Subject: [PATCH] - Added a --timer=x switch to abort Arachne proofs after x seconds. --- src/arachne.c | 13 +++++++++++++ src/main.c | 6 ++++++ src/timer.c | 52 +++++++++++++++++++++++++++++++++++++++++++++++++++ src/timer.h | 8 ++++++++ 4 files changed, 79 insertions(+) create mode 100644 src/timer.c create mode 100644 src/timer.h diff --git a/src/arachne.c b/src/arachne.c index 3495927..e1abd21 100644 --- a/src/arachne.c +++ b/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) { diff --git a/src/main.c b/src/main.c index 7fd3f31..b87b49f 100644 --- a/src/main.c +++ b/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; diff --git a/src/timer.c b/src/timer.c new file mode 100644 index 0000000..e1fe190 --- /dev/null +++ b/src/timer.c @@ -0,0 +1,52 @@ +#include "timer.h" + +#include +#include + +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; + } +} + diff --git a/src/timer.h b/src/timer.h new file mode 100644 index 0000000..2c50c5c --- /dev/null +++ b/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