Re: [isabelle] Disproof methods with Word.thy and AutoCorres



Dear Scott,

Sorry for the delay in answering. I am just coming back from vacation.

> quickcheck easily finds a counterexample, but nitpick struggles with the potentially massive cardinalities of the underlying types. For example,
> 
> lemma "(x :: 8 word) = y"
> nitpick[sat_solver = MiniSat_JNI]
> 
> outputs:
> 
> Nitpicking formula... 
> Timestamp: 12:28:39. 
> Too many scopes. Skipping 95000 scopes. (Consider using "mono" or
> "merge_type_vars" to prevent this.) 
> Batch 1 of 100: Trying 50 scopes:
>  card int = 1, card nat = 1, card "4 list" = 1, card "2 list" = 1,
>    card "1 list" = 1, card "1" = 1, card unit = 1, card "8 word" = 1,
>    card "8" = 1, card "4" = 1, and card "2" = 1;
>  card int = 2, card nat = 2, card "4 list" = 2, card "2 list" = 2,
>    card "1 list" = 2, card "1" = 1, card unit = 1, card "8 word" = 2,
>    card "8" = 2, card "4" = 2, and card "2" = 2;
> …
> 
> In my experience nitpick’s recommendations do not seem to alleviate the problem. By manually constraining the cardinalities, I was however able to found a counterexample for 4 bit words, but nothing greater.

The problem here is that Nitpick has no built in support for words. It then needs to work in terms of the definition

    typedef 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
      morphisms uint Abs_word by auto

which is not fun for SAT solving.

Nitpick's underlying engine, Kodkod, has a notion of words, and it would be possible to handle them really efficiently. However, this would require quite a bit of work in Nitpick, which is not one of my main research interests right now. Sorry about that.

Regards,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.