Propagation issue?

[Pieter Van Hertum]

I was testing some things with the propagation, and I have an infinite (I am of course not sure it is infinite, but very long anyway) run on this file: vocabulary V{ type T isa int a:T f(T):T b:T

} theory T:V{ a=b. a=3. f(a)=2. } structure S:V{ T={1..6} } procedure main(){ print(optimalpropagate(T,S)) }

Which is rather strange since if I change the type T={1..6} to T={1..5} it finishes in a second.

Anyone an idea?

[Pieter Van Hertum]

Okay. Let me rephrase: Anyone an idea why this is so hard? I don't think it is running infinite: the 1..6 version just ended in 10 seconds, the 1..7 version is now already running for 2 minutes. It is not hard on my memory usage.

[Bart Bogaerts]

Waarschijnlijk bdd schatters die te hard beïnvloed zijn door grootte van je type. Bij 5 doet hij het goed, bij 6 de verkeerde herschrijving.