Re: [isabelle] Difficulties with "setsum" (Alfio Martini)



Hi Makarius,

First of all, many thanks for helping me working around this problem, and
during the weekend!

>Do you have an extra virus checker that somehow delays external program
execution?
Good point. I have found some obscure McAffe internet security software in
my machine. I do not
know  how it got there. I only use Avast. Anyway, I deleted and used time
out = 60.

Now I solve the harder lemma both in Isabelle 2014 and Isabelle 2015-RC2. I
will
remove cvc4 from the provers list until that bug is corrected. Things get
much faster
without it. In any case, sledgehammer seems to solve problems a lot faster
in Isabelle
2014  than in RC2. Who would expect that?

Here are my results. Thanks a lot!


Isabelle  2014
sledgehammer_params [dont_try0] (* can't be used, otherwise
sledgehammer runs forever and can't be canceled. I had to kill
Isabelle *)

Num. Threads = 1

lemma "[a] = [b] ==> a = b"
"e": Try this: by (metis the_elem_set) (13 ms).
"spass": Timed out.
"remote_vampire": Try this: by (metis list.inject) (15 ms).
"z3": Try this: by (metis list.inject) (19 ms).

lemma aux: "m < n+1 ==> setsum f {m..n + 1} =
    setsum f {m..n} + f (n + 1 :: int)"
"e": Try this: by (metis add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int linorder_not_less set_upto
setsum.insert zle_add1_eq_le zless_add1_eq) (1.15 s).
"spass": Timed out.
"remote_vampire": Timed out.
"z3": Timed out.
 --------------------------------------------------------------------
Isabelle RC2
sledgehammer_params [dont_try0] (* mandatory *)
timeout = 60
Num_Threads = 1


lemma aux: "m < n+1 ==> setsum f {m..n + 1} =
    setsum f {m..n} + f (n + 1 :: int)"
"cvc4": A prover error occurred:
Solver "cvc4" failed -- enable tracing using the "smt_trace" option for
details
"remote_vampire": Timed out.
"z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_upto atLeastLessThanPlusOne_atLeastAtMost_int
atLeastLessThan_iff finite_atLeastAtMost_int setsum.insert) (> 1.0 s, timed
out).
"spass": Timed out.
"e": Timed out.

On Sat, Apr 25, 2015 at 5:48 PM, Makarius <makarius at sketis.net> wrote:

> On Sat, 25 Apr 2015, Alfio Martini wrote:
>
>  At least I got some progress, yet the overall situation is still far from
>> ideal.
>>
>> I got the best results with Threads=1 (instead of the default 0). "ML
>> Multithreading..." returns 4. Following your suggestions, here is the
>> summary of my tests with 2014, RC1 and RC2.
>>
>> It seems that 2014 is the best option so far. So what is next?
>>
>
> Next you can try the adhoc snapshot
> http://www4.in.tum.de/~wenzelm/unofficial/Isabelle_25-Apr-2015 -- it
> contains the change of CVC4 by Jasmin, and a checkbox to control the "try0"
> or "dont_try0" option in the Sledgehammer panel.
>
>
> Your SledgeFail.thy contains two examples:
>
> lemma "[a] = [b] â a = b"
>
> lemma "m < n + 1 â setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
> int)"
>
>
> The first works smoothly for me with or without "try methods", both on
> Linux and Windows.
>
>
> The second takes a bit longer to produce the following results (without
> "try methods").  The following is on Linux:
>
> "cvc4": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
> atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (122 ms).
> "e": Try this: by (metis add.commute atLeastAtMostPlus1_int_conv
> atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff
> finite_atLeastAtMost_int less_irrefl setsum.insert zle_add1_eq_le
> zless_add1_eq) (761 ms).
> "z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
> atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (158 ms).
> "spass": Timed out.
> "remote_vampire": Timed out.
>
>
> This is on Windows 7, with sledgehammer_timeout = 60 (see plugin options):
>
> "cvc4": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
> atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (203 ms).
> "remote_vampire": Timed out.
> "spass": Timed out.
> "z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
> atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (1.2 s).
> "e": Timed out.
>
>
> That is less than nothing, although not as smooth as on a proper Unix
> system.
>
> Do you have an extra virus checker that somehow delays external program
> execution?
>
>
>         Makarius




-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil



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