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



Hi Makarius,

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?

Best!

-------------------------------------------------------------------------------------------------------------------
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": Timed out.
"spass": Timed out.
"remote_vampire": Timed out.
"z3": Timed out.
------------------------------------------------------------------
Isabelle RC1
sledgehammer_params [dont_try0] (* mandatory *)
Num. Threads = 1

lemma "[a] = [b] ==> a = b"

"cvc4": Timed out.
"remote_vampire": Try this: by (metis list.inject) (63 ms).
"z3": Try this: by (metis list.inject) (63 ms).
"spass": Try this: by (metis list.inject) (31 ms).
"e": Try this: by (metis the_elem_set) (62 ms).

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": Timed out.
"spass": Timed out.
"e": Timed out.
------------------------------------------------------------------
Isabelle RC2
sledgehammer_params [dont_try0] (* mandatory *)
Num_Threads = 1

lemma "[a] = [b] ==> a = b"

"cvc4": A prover error occurred:
Solver "cvc4" failed -- enable tracing using the "smt_trace" option for
details
"remote_vampire": Try this: by (metis list.inject) (63 ms).
"z3": Try this: by (metis list.inject) (47 ms).
"spass": Timed out.
"e": Try this: by (metis append_Cons append_Nil list.inject) (62 ms).

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": Timed out.
"spass": Timed out.
"e": Timed out.

On Sat, Apr 25, 2015 at 6:06 AM, Makarius <makarius at sketis.net> wrote:

> On Fri, 24 Apr 2015, Alfio Martini wrote:
>
>  Even with dont_try0 as a sledgehammer parameter, I get the same old
>> timeout
>> results both
>> with Isa2014 and Isa2015-RC1. I havenÂt tried with Isa2015RC2 yet,
>>
>>>
>>>> Operating System: Windows 8.1, 64-bit operating system
>>>> Ram Memory: 8GB
>>>> Processor: intel i5-3230M, 64 bit processor
>>>>
>>>
> That CPU has 2 cores and hyperthreading, i.e. 4 virtual cores.  Can you
> try this:
>
>   ML "Multithreading.max_threads_value ()"
>
> There is some chance that it gives 4, because Cygwin is not reliable in
> reporting virtual CPU cores.  Since starting external processes in parallel
> imposes an extra load on Cygwin, it might explain the timeout of the
> provers.
>
> The Isabelle/jEdit plugin options offer the possibility to set "threads"
> explicitly, e.g. to 2.  Does this change the situation?
>
>
>         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.