[isabelle-dev] AFP: PAPP_Impossibility not terminating

[Makarius]

On 18/04/2023 10:07, Manuel Eberl wrote:
> 
> I did notice at the time that the vast majority of the time was spent in 
> taking the union of the hyps of the different theorems being combined, so I 
> made sure that when I create the theorems, they all have pointer-equal hyps, 
> which sped things up phenomenally.

Did you re-invent this yourself, or did you see it here? 
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/Tools/sat.ML$348


> I should also still have a few smaller example applications of 
> that SAT solver lying around that one could use; there the difference between 
> the old and the new version would perhaps not be "2 minutes" vs 
> "non-termination" but rather something like "almost instant" and "half a 
> minute" or so, which may make debugging less painful.

It would be great to have such small benchmark examples. Please send them to 
me privately.


	Makarius