- If we run into the time bound, report it.

This commit is contained in:
ccremers 2005-01-14 13:01:31 +00:00
parent 9df1bfed5b
commit b607b1e260
4 changed files with 17 additions and 2 deletions

View File

@ -2015,6 +2015,8 @@ prune_bounds ()
indentPrint ();
eprintf ("Pruned: ran out of allowed time (-T %i switch)\n", get_time_limit () );
}
// Pruned because of time bound!
current_claim->timebound = 1;
return 1;
}

View File

@ -548,6 +548,7 @@ commEvent (int event, Tac tc)
cl->roledef = NULL;
cl->count = 0;
cl->complete = 0;
cl->timebound = 0;
cl->failed = 0;
cl->prec = NULL;
cl->roles = NULL;

View File

@ -90,6 +90,9 @@ const char *releasetag = SVNVERSION " [modified]";
const char *releasetag = SVNVERSION;
#endif
//! The number of seconds a test is allowed to run
static int time_limit_seconds;
//! The main body, as called by the environment.
int
main (int argc, char **argv)
@ -525,6 +528,7 @@ main (int argc, char **argv)
sys->match = switch_match_method->ival[0];
mgu_match = sys->match;
sys->prune = switch_pruning_method->ival[0];
time_limit_seconds = switch_timer->ival[0];
set_time_limit (switch_timer->ival[0]);
if (switch_progress_bar->count > 0)
/* enable progress display */
@ -826,9 +830,15 @@ timersPrint (const System sys)
{
eprintf ("\tcorrect: ");
if (cl_scan->complete)
eprintf ("complete_proof");
{
eprintf ("complete_proof");
}
else
eprintf ("bounded_proof");
{
eprintf ("bounded_proof");
if (cl_scan->timebound)
eprintf ("\ttime=%i",time_limit_seconds);
}
}
}
else

View File

@ -33,6 +33,8 @@ struct claimlist
states_t failed;
//! Whether the result is complete or not (failings always are!)
int complete;
//! If we ran into the time bound (incomplete, and bad for results)
int timebound;
int r; //!< role number for mapping
int ev; //!< event index in role