Stream: General

Topic: blast fails with no output

Christoph Madlener (Sep 24 2021 at 12:14):

I'm trying to use blast to solve goals like the following (basically the goal follows directly from an assumption, with a lot of commutations):

theory TestComm
  imports ZF
begin

lemma "((((P58 ∨ P59) ∧ (P56 ∨ P57) ∨ (P62 ∨ P63) ∧ (P60 ∨ P61)) ∧ ((P48 ∨ P49) ∧ (P51 ∨ P50) ∨ (P55 ∨ P54) ∧ (P53 ∨ P52)) ∨
         ((P45 ∨ P44) ∧ (P46 ∨ P47) ∨ (P42 ∨ P43) ∧ (P41 ∨ P40)) ∧ ((P35 ∨ P34) ∧ (P32 ∨ P33) ∨ (P39 ∨ P38) ∧ (P37 ∨ P36))) ∧
        (((P9 ∨ P8) ∧ (P11 ∨ P10) ∨ (P14 ∨ P15) ∧ (P12 ∨ P13)) ∧ ((P3 ∨ P2) ∧ (P0 ∨ P1) ∨ (P7 ∨ P6) ∧ (P5 ∨ P4)) ∨
         ((P30 ∨ P31) ∧ (P28 ∨ P29) ∨ (P25 ∨ P24) ∧ (P27 ∨ P26)) ∧ ((P17 ∨ P16) ∧ (P18 ∨ P19) ∨ (P23 ∨ P22) ∧ (P20 ∨ P21)))) ⟹
     ((((P0 ∨ P1) ∧ (P2 ∨ P3) ∨ (P4 ∨ P5) ∧ (P6 ∨ P7)) ∧ ((P8 ∨ P9) ∧ (P10 ∨ P11) ∨ (P12 ∨ P13) ∧ (P14 ∨ P15)) ∨
         ((P16 ∨ P17) ∧ (P18 ∨ P19) ∨ (P20 ∨ P21) ∧ (P22 ∨ P23)) ∧ ((P24 ∨ P25) ∧ (P26 ∨ P27) ∨ (P28 ∨ P29) ∧ (P30 ∨ P31))) ∧
        (((P32 ∨ P33) ∧ (P34 ∨ P35) ∨ (P36 ∨ P37) ∧ (P38 ∨ P39)) ∧ ((P40 ∨ P41) ∧ (P42 ∨ P43) ∨ (P44 ∨ P45) ∧ (P46 ∨ P47)) ∨
         ((P48 ∨ P49) ∧ (P50 ∨ P51) ∨ (P52 ∨ P53) ∧ (P54 ∨ P55)) ∧ ((P56 ∨ P57) ∧ (P58 ∨ P59) ∨ (P60 ∨ P61) ∧ (P62 ∨ P63))))"
  by blast


end

When I try this blast (sometimes) fails without any output, i.e. it looks like this in jEdit:
image.png
but I get nothing in the output panel. Can anyone tell me what's going wrong here?

Mohammad Abdulaziz (Sep 24 2021 at 12:34):

It seems to me that this happens when blast detects that it won’t terminate.

Christoph Madlener (Sep 24 2021 at 12:44):

How does that detection work? Because on the above example, sometimes I get the silent failure (usually pretty quickly), or blast succeeds (after running for some time).

Mohammad Abdulaziz (Sep 24 2021 at 13:01):

Sorry, I thought this was purple. Looking closely, I see that it’s pink, which I don’t understand. It sometimes happens to me with smt calls and goes away if I refresh the theory file. I always thought it is a bug.

Manuel Eberl (Nov 08 2021 at 08:51):

My guess would be that it's more of a resource problem, i.e. it runs out of memory. I cannot answer the question of why that doesn't crash the entire Isabelle process though. This is the kind of thing that is probably best asked on the isabelle-users mailing list because Makarius will be the best person to answer it (and he refuses to use Zulip).

Last updated: Dec 21 2024 at 12:33 UTC