Fri, 01 Aug 2014 16:07:34 +0200 beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet [Fri, 01 Aug 2014 16:07:34 +0200] rev 57758
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
Fri, 01 Aug 2014 16:07:33 +0200 tuning
blanchet [Fri, 01 Aug 2014 16:07:33 +0200] rev 57757
tuning
Fri, 01 Aug 2014 16:07:33 +0200 peek instead of joining -- is perhaps less risky
blanchet [Fri, 01 Aug 2014 16:07:33 +0200] rev 57756
peek instead of joining -- is perhaps less risky
Fri, 01 Aug 2014 14:43:57 +0200 export ML function
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57755
export ML function
Fri, 01 Aug 2014 14:43:57 +0200 compile
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57754
compile
Fri, 01 Aug 2014 14:43:57 +0200 removed 'metisFT' support in Mirabelle
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57753
removed 'metisFT' support in Mirabelle
Fri, 01 Aug 2014 14:43:57 +0200 removed Mirabelle minimization code
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57752
removed Mirabelle minimization code
Fri, 01 Aug 2014 14:43:57 +0200 modernized Mirabelle (a bit) and made it compile
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57751
modernized Mirabelle (a bit) and made it compile
Fri, 01 Aug 2014 14:43:57 +0200 restored a bit of laziness
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57750
restored a bit of laziness
Fri, 01 Aug 2014 14:43:57 +0200 reorder quantifiers to ease Z3 skolemization
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57749
reorder quantifiers to ease Z3 skolemization
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip