Fri, 01 Aug 2014 16:07:34 +0200 |
blanchet |
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
|
changeset |
files
|
Fri, 01 Aug 2014 16:07:33 +0200 |
blanchet |
tuning
|
changeset |
files
|
Fri, 01 Aug 2014 16:07:33 +0200 |
blanchet |
peek instead of joining -- is perhaps less risky
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
export ML function
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
compile
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed 'metisFT' support in Mirabelle
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed Mirabelle minimization code
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
modernized Mirabelle (a bit) and made it compile
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
restored a bit of laziness
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
reorder quantifiers to ease Z3 skolemization
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned order of arguments
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned name context code
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned whitespace
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
more rational unskolemizing of names
|
changeset |
files
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
added appropriate method for skolemization of Z3 steps to the mix
|
changeset |
files
|