2020-03-31 10:47:50 (GMT)
@Petar Vukmirovic Do you have any experimental data on which is better: unification modulo booleans or Cases?
2020-03-31 10:48:30 (GMT)
No, but I can do an evaluation today since that is an interesting question
2020-03-31 18:7:34 (GMT)
Results show that unification modulo + cases is a bit (20 probs) better than unification modulo alone
2020-03-31 19:8:18 (GMT)
What about Cases alone?
2020-03-31 19:18:28 (GMT)
That is hard to evaluate
Because when you disable ext- rules
2020-03-31 19:18:39 (GMT)
you disable also functional exctenisonality and the numbers go way down
2020-03-31 19:27:10 (GMT)
I am now testing if the situation changes with lazy cnf
2020-03-31 19:27:46 (GMT)
for the problem f(f(f(x))) = f(x) ext- version gives up
2020-03-31 19:27:55 (GMT)
and case-simp version succeeds
2020-04-01 6:41:2 (GMT)
+20 probs -- how many absolute problems?
2020-04-01 8:11:20 (GMT)
ok I was talking from memory last night
2020-04-01 8:11:28 (GMT)
now that I checked the data precisely
2020-04-01 8:11:36 (GMT)
it is 32 absolute problems
2020-04-01 8:33:24 (GMT)
Sorry, by "absolute problems", I mean how many problems do you solve without and with cases?
2020-04-01 8:33:45 (GMT)
Numbers like +20 mean nothing to me. Is it 490 vs. 510 or 49000 vs. 49020?
2020-04-01 8:36:36 (GMT)
Ok.
2020-04-01 8:37:1 (GMT)
1632 vs 1610.
2020-04-01 8:37:14 (GMT)
So it is 22, not 32 as I initially claimed (I read 1600 :)
2020-04-01 8:41:6 (GMT)
Thanks.