[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Counterexamples timeout
From: |
Jacob L. Mandelson |
Subject: |
Re: Counterexamples timeout |
Date: |
Thu, 15 Sep 2022 10:02:57 -0700 |
User-agent: |
Mutt/1.9.4 (2018-02-28) |
On Thu, Sep 15, 2022 at 06:26:12PM +0200, Akim Demaille wrote:
> Hi Frank,
>
> > Le 29 juil. 2022 à 14:09, Frank Heckenbach <f.heckenbach@fh-soft.de> a
> > écrit :
> >
> > Hi,
> >
> > I don't know if it's something peculiar about my grammars, but it
> > seems when using "-Wcounterexamples", Bison either finds
> > counterexamples almost immediately or runs into the timeout.
> > (Or maybe 6 seconds (see below) are just so eternally long to a
> > modern CPU that there's not much between that and infinity. ;)
> > [...]
>
> I agree. Let's change that. What do you think about this proposal?
I think the English text needs a few minor edits.
> commit 6a15951030ade757de13159e545394af3cd40205
> Author: Akim Demaille <akim.demaille@gmail.com>
> Date: Tue Sep 13 08:25:59 2022 +0200
>
> cex: provide the user with a means to change the timeout
>
> Reported by Frank Heckenbach.
> https://lists.gnu.org/r/bug-bison/2022-07/msg00011.html
>
> * bootstrap.conf: Use c_strtod, so that even in French locales "1.5"
> is accepted, instead of "1,5".
> * src/counterexample.c, src/state-item.c: Use xtime_t instead of
> time_t, so that accuracy goes from seconds to nanoseconds.
> ( counterexample_init): Depend on cex.timeout rather than
> $TIME_LIMIT.
> * doc/bison.texi (%define Summary): Document cex.timeout.
>
> diff --git a/NEWS b/NEWS
> index f480cb95..32e7361a 100644
> --- a/NEWS
> +++ b/NEWS
> @@ -8,6 +8,10 @@ GNU Bison NEWS
>
> The C++ skeletons now expose copy and move operators for symbols.
>
> + The `cex.timeout` %define variable allows to control when we give up
> + finding a unifying counterexample. For instance `bison -Wcex
> + -Dcex.timeout=.5 gram.y` to give 1/2s of credit.
Is "credit" used this way elsewhere in the documentation? It feels like
an unnatural usage to me. I'd either change it to "limit" (eg, "... to
limit to 1/2s" or "... for a limit of 1/2s") or rephrase (eg, "... to
stop after 1/2s").
[...]
> +@c ================================================== cex.timeout
> +
> +@deffn Directive {%define cex.timeout} @var{duration}
> +
> +@itemize @bullet
> +@item Language(s): all
> +
> +@item Purpose:
> +Define the time credit allocated to finding unifying counterexamples.
"Define the time limit for finding unifying counterexamples."
[...]
> diff --git a/src/muscle-tab.c b/src/muscle-tab.c
> index 0945d609..40295542 100644
> --- a/src/muscle-tab.c
> +++ b/src/muscle-tab.c
> @@ -127,6 +127,9 @@ muscle_init (void)
>
> muscle_table = hash_xinitialize (HT_INITIAL_CAPACITY, NULL, hash_muscle,
> hash_compare_muscles, muscle_entry_free);
> + /* Avoid warnings if the user defined this variable, but did not
> + actually called -Wcex. */
"actually use -Wcex" or "actually call with -Wcex".
Be well,
-- Jacob