Koen: TPTP files where we expect equinox to find a counter example
Nathan Collins
same for all .tptp files). There are three versions:
i. current code, using quantifier-based translation of case
expression. Using arithmetic [2].
ii. current code, using projection-based translation of case
expressions. Using arithmetic [2].
iii. old code, using a different quantifier-and-projection-based
translation of case expressions. Using arithmetic [3].
Equinox times out (20 seconds) for (i) and (ii), but finds a counter
model for (iii).
The new arithmetic [2] in used (i) and (ii) has nested case
expressions, whereas the old arithmetic [3] used in (iii) has
auxillary functions.
The translations in (ii) and (iii) are fairly different. I had assumed
the problem was the switch to only quantfiers in (i), but (ii) shows
that going to all projections doesn't work.
In the old version (iii) we have
fof(gt1,axiom,
(! [X,Y,ZDEF1] : ($min(f__gt(X,Y)) => ($min(X) & ((X = c_Zero) =>
(f__gt(X,Y) = c_False)))))
).
%%% implication and quantifiers for "normal" branches
fof(gt1,axiom,
(! [X,Y,ZDEF1] : ($min(f__gt(X,Y)) => ($min(X) & ((X =
c_f__Succ(ZDEF1)) => (f__gt(X,Y) = f__gtAux(ZDEF1,Y))))))
).
fof(gt1,axiom,
(! [X,Y,ZDEF1] : ($min(f__gt(X,Y)) => ($min(X) & ((X = bad) =>
(f__gt(X,Y) = bad)))))
).
%%% projection for UNR case
fof(gt1,axiom,
(! [X,Y,ZDEF1] : ($min(f__gt(X,Y)) => ($min(X) & (((X != bad) & (X !=
c_Zero) & (X != c_f__Succ('f__Succ__1'(X)))) => (f__gt(X,Y) = unr)))))
).
whereas in the new version (ii) we have
fof(dTrans__gt,
axiom,
(! [X, Y] :
($min(f__gt(X , Y))
=> ($min(X)
& (((X = bad) & (f__gt(X , Y) = bad))
| ((X = c_Zero) & (f__gt(X , Y) = c_False))
%%% projection everywhere
| ((X = c_Succ(f__p1_Succ(X)))
%%% what corresponds to gtAux in the (ii) version:
& $min(Y)
& (((Y = bad) & (f__gt(X , Y) = bad))
| ((Y = c_Zero) & (f__gt(X , Y) = c_True))
| ((Y = c_Succ(f__p1_Succ(Y)))
& (f__gt(X , Y) = f__gt(f__p1_Succ(X) , f__p1_Succ(Y))))
| ((Y != bad)
& (Y != c_Zero)
& (Y != c_Succ(f__p1_Succ(Y)))
& (f__gt(X , Y) = unr))))
%%% possibilities are enumerated / no need for excluded middle, unlike
in (iii) ?
| ((X != bad)
& (X != c_Zero)
& (X != c_Succ(f__p1_Succ(X)))
& (f__gt(X , Y) = unr))))))).
Cheers,
-nathan
[1] https://github.com/cpa/haskellcontracts-examples/blob/540d83c9f457a9e113c48115cced08a6df16608a/no/mult-gt.hs
[2] https://github.com/cpa/haskellcontracts-examples/blob/540d83c9f457a9e113c48115cced08a6df16608a/Lib/Arithmetic.hs
[3] https://github.com/cpa/haskellcontracts-examples/blob/85815c0a7296fb74ef01cbcbc3256c4e83e35794/Lib/Arithmetic.hs
p.s. The commands I ran, for future reference:
# generating the TPTP with projections and with quantifiers, using the
current code (rev 540d83c)
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7846][15:24:07]
$ ./timeout.sh 20 ../src/hcc --keep-tmps no/mult-gt.hs
Writing mult-gt.hs.mult.tptp
["mult"] are mutually recursive. Checking them altogether...
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7847][15:24:39]
$ cp mult-gt.hs.mult.tptp{,.projection}
`mult-gt.hs.mult.tptp' -> `mult-gt.hs.mult.tptp.projection'
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7848][15:24:59]
$ ./timeout.sh 20 ../src/hcc --keep-tmps no/mult-gt.hs --use-qs
Writing mult-gt.hs.mult.tptp
["mult"] are mutually recursive. Checking them altogether...
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7849][15:25:26]
$ cp mult-gt.hs.mult.tptp{,.quantifier}
`mult-gt.hs.mult.tptp' -> `mult-gt.hs.mult.tptp.quantifier'
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7850][15:25:49]
$ diff *{projection,quantifier} -U0
--- mult-gt.hs.mult.tptp.projection 2011-12-06 15:24:59.000000000 +0000
+++ mult-gt.hs.mult.tptp.quantifier 2011-12-06 15:25:49.000000000 +0000
@@ -89 +89 @@
- | ((X = c_Succ(f__p1_Succ(X))) & (f__isZero(X) = c_False))
+ | (? [X_] : ((X = c_Succ(X_)) & (f__isZero(X) = c_False)))
@@ -92 +92 @@
- & (X != c_Succ(f__p1_Succ(X)))
+ & (! [X_] : (X != c_Succ(X_)))
@@ -138,10 +138,10 @@
- | ((X = c_Succ(f__p1_Succ(X)))
- & $min(Y)
- & (((Y = bad) & (f__gt(X , Y) = bad))
- | ((Y = c_Zero) & (f__gt(X , Y) = c_True))
- | ((Y = c_Succ(f__p1_Succ(Y)))
- & (f__gt(X , Y) = f__gt(f__p1_Succ(X) ,
f__p1_Succ(Y))))
- | ((Y != bad)
- & (Y != c_Zero)
- & (Y != c_Succ(f__p1_Succ(Y)))
- & (f__gt(X , Y) = unr))))
+ | (? [X_] :
+ ((X = c_Succ(X_))
+ & $min(Y)
+ & (((Y = bad) & (f__gt(X , Y) = bad))
+ | ((Y = c_Zero) & (f__gt(X , Y) = c_True))
+ | (? [Y_] : ((Y = c_Succ(Y_)) & (f__gt(X , Y)
= f__gt(X_ , Y_))))
+ | ((Y != bad)
+ & (Y != c_Zero)
+ & (! [Y_] : (Y != c_Succ(Y_)))
+ & (f__gt(X , Y) = unr)))))
@@ -150 +150 @@
- & (X != c_Succ(f__p1_Succ(X)))
+ & (! [X_] : (X != c_Succ(X_)))
@@ -164,2 +164,2 @@
- | ((X = c_Succ(f__p1_Succ(X)))
- & (f__add(X , Y) = c_Succ(f__add(f__p1_Succ(X) , Y))))
+ | (? [X_] :
+ ((X = c_Succ(X_)) & (f__add(X , Y) =
c_Succ(f__add(X_ , Y)))))
@@ -168 +168 @@
- & (X != c_Succ(f__p1_Succ(X)))
+ & (! [X_] : (X != c_Succ(X_)))
@@ -187,2 +187,3 @@
- | ((A = c_Succ(f__p1_Succ(A)))
- & (f__mult(A , B) = f__add(B ,
f__mult_r(f__p1_Succ(A) , B))))
+ | (? [X] :
+ ((A = c_Succ(X))
+ & (f__mult(A , B) = f__add(B , f__mult_r(X , B)))))
@@ -191 +192 @@
- & (A != c_Succ(f__p1_Succ(A)))
+ & (! [X] : (A != c_Succ(X)))
# checking out the old code
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/src][%0][#7642][15:37:36]
$ git co f5fd92e
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git][%0][#7647][15:38:11]
$ cd contracts
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/contracts][%0][#7648][15:38:17]
$ make
# checking out the old examples and generating the TPTP with the old
code (the counter example is found)
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7852][15:40:32]
$ git co 85815c0a
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7855][15:41:31]
$ ./timeout.sh 20 ../contracts/Check no/mult-gt.hs -p
Writing mult-gt.hs.mult.tptp
["mult"] are mutually recursive. Checking them altogether...
Not OK :(
There's at least one contract in no/mult-gt.hs that doesn't hold.
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7856][15:41:44]
$ cp mult-gt.hs.mult.tptp{,.old}
`mult-gt.hs.mult.tptp' -> `mult-gt.hs.mult.tptp.old'
[t-nathac@cam-02-unx][/home/t-nathac/v/haskellcontracts.git/egs][%0][#7868][15:52:17]
$ equinox --modelfile mult-gt.hs.mult.tptp.old.model mult-gt.hs.mult.tptp.old
Koen Claessen
I did a quick investigation using Paradox.
I assume you expect these three files to have the same (or isomorphic)
models. They don't.
File (iii) has a model with finite domain of size 4 (as found by Paradox).
File (i) and (ii) provably have no models of size 1,2,3,4, or 5, but
does have a model of size 6! Thus, the set of models of these files is
not isomorphic; your new theories are probably stronger than the old
one.
In other words, this is not a performance regression for Equinox, but
you changed the coding.
I get the same results in Paradox when I remove that extra condition
in the selector axiom for Succ (I was just trying), so that is not the
problem.
Summary: all these files are satisfiable, but the new ones have larger
(more complicated) models.
I don't know yet as to why. It would be great if you could look at
some simpler examples of files where the old and the new coding have
discrepancies regarding model size (e.g. less function definitions and
datatypes).
Do you have a description of the new case expression translation?
Perhaps it is subtly wrong?
/Koen
Koen Claessen
functions yourself, and then still use the new translation?
If the differences disappear, then we know it is the new pattern match
translation.
If they remain, then we know it is something else, and we have simpler
formulas to look at to find out what.
/Koen
Koen Claessen
Equinox (again, alpha release).
(I had found a minor bug in the version that I put up earlier, but I
had no idea it could lead to this behavior. :-P )
Here is a latest snapshot:
http://www.cse.chalmers.se/~koen/code/
It is still interested to look at what changed in the coding though,
as it might point to a deeper problem.
/Koen
Nathan Collins
On Wed, Dec 7, 2011 at 10:11 AM, Koen Claessen <ko...@chalmers.se> wrote:
> Hi Nathan,
>
> I did a quick investigation using Paradox.
>
> I assume you expect these three files to have the same (or isomorphic)
> models. They don't.
>
> File (iii) has a model with finite domain of size 4 (as found by Paradox).
>
> File (i) and (ii) provably have no models of size 1,2,3,4, or 5, but
> does have a model of size 6! Thus, the set of models of these files is
> not isomorphic; your new theories are probably stronger than the old
> one.
Very interesting. We had not tried Paradox, altho I think you did
tell us it was better at finding models two meetings ago.
> In other words, this is not a performance regression for Equinox, but
> you changed the coding.
Right, I did not mean to assert that Equinox was at fault: all tests
in my initial email were run with the same version of Equinox, the 6
alpha.
> I get the same results in Paradox when I remove that extra condition
> in the selector axiom for Succ (I was just trying), so that is not the
> problem.
Right, I have removed this in the latest code and it does not affect
any tests.
> Summary: all these files are satisfiable, but the new ones have larger
> (more complicated) models.
>
> I don't know yet as to why. It would be great if you could look at
> some simpler examples of files where the old and the new coding have
> discrepancies regarding model size (e.g. less function definitions and
> datatypes).
I don't know any other examples where the old translation makes
Equinox converge and new translation make Equinox diverge, but I can
run Paradox on all examples where Equinox finds counter models and see
if any model sizes differ and report back.
> Do you have a description of the new case expression translation?
> Perhaps it is subtly wrong?
The 'dTrans' function [1] implements the current translation of
definitions. I will describe what I hope it does. The version (i)
with quantifiers is
-- Definition translation:
d[| f xs = ce |] := forall xs. min(f xs) -> c[| ce |] where
-- Function body (case expression) translation:
-- Recursive case. Assume the variables xsi in the patterns have
-- been alpha renamed to avoid capture / conflicts.
c[| case e of { c1 xs1 -> ce1; ... ; cn xsn -> cen } |] :=
min(e) /\ (
(e = bad /\ f xs = bad) \/
(exists xs1. e = c1 xs1 /\ c[| ce1 |]) \/
... \/
(exists xsn. e = cn xsn /\ c[| cen |]) \/ (
e /= bad /\
forall xs1. e /= c1 xs1 /\
... /\
forall xsn. e /= cn xsn /\
f xs = unr
)
)
-- Base case: 'e' is not a case expression.
c[| e |] := f xs = e
The version (ii) with projectors is
d[| f xs = ce |] := forall xs. min(f xs) -> c[| ce |] where
-- Recursive case.
c[| case e of { c1 xs1 -> ce1; ... ; cn xsn -> cen } |] :=
min(e) /\ (
(e = bad /\ f xs = bad) \/
-- We substitute the projections for the pattern variables in
-- the branch targets.
(e = c1 p11 ... p1k1 /\ c[| ce1[p11/x11,...,p1k1/xk1] |]) \/
... \/
(e = cn pn1 ... pnkn /\ c[| cen[pn1/xn1,...,pnkn/xkn] |]) \/ (
e /= bad /\
e /= c1 p11 ... p1k1 /\
... /\
e /= cn pn1 ... pnkn /\
f xs = unr
)
)
where
xsi = xi1 ... xiki
pij is the jth projector of ci applied to e,
e.g. for Nat = Zero | Succ Nat have c1 = Zero,
c2 = Succ,
n = 2
k1 = 0
k2 = 1
p21 = pred e
-- Base case: 'e' is not a case expression.
c[| e |] := f xs = e
Hopefully that makes sense, in conjunction with the examples from my
first email.
-nathan
Nathan Collins
I tried some hand-edited variations of the theories (attached). The
"hybrid" versions try to better approximate the "old" translation, but
while retaining nesting. The "hybrid-hand-edit-more-quantifier" is
supposed to be closer to "old" than 'hybrid-hand-eidt". It turns out
"Equinox, version 6.0alpha, 2011-08-19, pre-release" can find counter
models for all of these theories, even the unedited versions, but it
takes longer than 20 seconds (my arbitraty cutoff) for all new
theories. The results are:
Theory Time to find counter model
-------------------------------------------------------------------
.old 08s
.projection.hand-edit-unnest 24s
.quantifier.hand-edit-unnest 31s
.hybrid-hand-edit-unnest 39s
.hybrid-hand-edit-more-quantifier-unnest 45s
.hybrid-hand-edit 47s
.projection 49s
.quantifier 61s
.hybrid-hand-edit-more-quantifier 65s
So, keeping in mind that single timings on a shared machine are
unreliable, we see a likely significant improvement from unnesting the
case expressions, but that the nested hybrid translations are similar
to the the nested projection and quantifier translations.
Note also that Equinox actually finds the counter models more quickly
than "Paradox, version 4.0, 2010-06-29" here:
mult-gt.hs.mult.tptp.{quantifier,projection} takes {6,3} minutes. I
did not try the other theories in Paradox.
-nathan
Koen Claessen
The updated Equinox which I sent you finds models for .projection and
.quantifier in ~7 seconds for both files.
The main difference I can see between the old translation and your
nested case translation is that the latter is stating its facts
disjunctively ("either (this and this) or (that and that) or (si and
si) or (so and so)"), whereas the old translation stated its facts
conjunctively ("this or this" and "that or that" and ...). Stating
things conjunctively is more natural for clause-based theorem provers.
This might explain why the problems are more difficult, but not why
the model sizes differ. My guess is that when we find this difference,
the running times should become more closer (and in fact the nested
translation should be better).
The reason why Paradox is slower than Equinox is because the models
are more complicated and it wants to find the smallest one.
I randomly ran Paradox on some of these files, and the model size is
still 6 (as supposed to 4).
/Koen
Nathan Collins
I can probably switch to a "conjunctive" translation and/or
automatically unnest the case expressions. But I will try to find
simpler "different size models" examples first.
In the mean time, here are the new stats. Looks like your computer is
faster than ours :) Using the new Equinox:
Theory Time to find counter model
-------------------------------------------------------------------
.old 08s 05s
.projection.hand-edit-unnest 24s 13s
.quantifier.hand-edit-unnest 31s 20s
.hybrid-hand-edit-unnest 39s 21s
.hybrid-hand-edit-more-quantifier-unnest 45s 29s
.hybrid-hand-edit 47s 29s
.projection 49s 32s
.quantifier 61s 35s
.hybrid-hand-edit-more-quantifier 65s 35s
The new Equinox doesn't run on our machine, a 10.4 Ubuntu, without
help because some dynamic libs are not found. And orthogonally, are
you able to build Equinox with GHC7? I can only make GHC6 work. I
have instructions for how I build it, and how to work around the
dynamic lib problem, in the README [1]. You might want to include my
build instructions, or your better way, in your source; building
Equinox was very trial-and-error the first time around for me.
-nathan
[1] https://github.com/cpa/haskellcontracts/blob/fd4c1b84066a2bd3dbbf6de63c3e82849b8b90e5/README.md
Koen Claessen
I forgot that I was running *parallel* Equinox (try the flags +RTS -N4
-RTS for a 4-core machine for example). For this problem, I get twice
the speed-up compared to normal Equinox.
By the "new" Equinox, do you mean 6.0.1alpha? I had to rewrite a lot
when I upgraded to GHC7. (Especially, I still used Hinze-style
Data.Generics, and I was forced to re-implement my functions.) It
should now compile without problems.
Why can't you compile with GHC7?
/Koen
Nathan Collins
Here is how I fail to build Equinox with GHC 7, inside a copy (Folkung.comp)
of the Folkung dir from your tarchive:
$ make -C Haskell equinox
make: Entering directory
`/home/t-nathac/v/haskellcontracts.git/Folkung.comp/Haskell
'
ghc -optl -static -lstdc++ -I../instantiate
-I../minisat/current-base ../minisat/cur
rent-base/Solver.or ../minisat/current-base/Prop.or
../instantiate/MiniSatWrapper.or
../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2
-static -threaded -th
readed -main-is Equinox.Main.main --make Equinox.Main -o equinox
on the commandline:
Warning: -fglasgow-exts is deprecated: Use individual extensions
instead
Flags.hs:54:8:
Could not find module `CPUTime'
It is a member of the hidden package `haskell98-2.0.0.0'.
Use -v to see a list of the files searched for.
$ make -C Haskell HFLAGS="-package haskell98" equinox
make: Entering directory
`/home/t-nathac/v/haskellcontracts.git/Folkung.comp/Haskell
'
ghc -optl -static -lstdc++ -I../instantiate
-I../minisat/current-base ../minisat/cur
rent-base/Solver.or ../minisat/current-base/Prop.or
../instantiate/MiniSatWrapper.or
../instantiate/MiniSatInstantiateClause.or -package haskell98
-threaded -main-is Eq
uinox.Main.main --make Equinox.Main -o equinox
Implicit import declaration:
Ambiguous module name `Prelude':
it was found in multiple packages: base haskell98-2.0.0.0
$ make -C Haskell HFLAGS="-package haskell98 -hide-package base"
equinox
make: Entering directory
`/home/t-nathac/v/haskellcontracts.git/Folkung.comp/Haskell
'
ghc -optl -static -lstdc++ -I../instantiate
-I../minisat/current-base ../minisat/cur
rent-base/Solver.or ../minisat/current-base/Prop.or
../instantiate/MiniSatWrapper.or
../instantiate/MiniSatInstantiateClause.or -package haskell98
-hide-package base -t
hreaded -main-is Equinox.Main.main --make Equinox.Main -o equinox
Observe.hs:8:8:
Could not find module `Data.List'
It is a member of the hidden package `base'.
It is a member of the hidden package `haskell2010-1.1.0.0'.
Use -v to see a list of the files searched for.
$ make -C Haskell HFLAGS="-package haskell98 -hide-package base
-package haskell201
0" equinox
make: Entering directory
`/home/t-nathac/v/haskellcontracts.git/Folkung.comp/Haskell
'
ghc -optl -static -lstdc++ -I../instantiate
-I../minisat/current-base ../minisat/cur
rent-base/Solver.or ../minisat/current-base/Prop.or
../instantiate/MiniSatWrapper.or
../instantiate/MiniSatInstantiateClause.or -package haskell98
-hide-package base -p
ackage haskell2010 -threaded -main-is Equinox.Main.main --make
Equinox.Main -o equin
ox
Implicit import declaration:
Ambiguous module name `Prelude':
it was found in multiple packages:
haskell2010-1.1.0.0 haskell98-2.0.0.0
# This works:
$ make -C Haskell GHC=ghc6 equinox
make: Entering directory
`/home/t-nathac/v/haskellcontracts.git/Folkung.comp/Haskell
'
ghc6 -optl -static -lstdc++ -I../instantiate
-I../minisat/current-base ../minisat/cu
rrent-base/Solver.or ../minisat/current-base/Prop.or
../instantiate/MiniSatWrapper.o
r ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2
-static -threaded -t
hreaded -main-is Equinox.Main.main --make Equinox.Main -o equinox
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version
7.2.1.20110809
$ ghc6 --version
The Glorious Glasgow Haskell Compilation System, version 6.12.1
Yes, by "new" Equinox I mean 6.0.1alpha. I downloaded it yesterday.
Thanks for the RTS tip. Interestingly, I get better performance from
your precompiled Equinox and LD_LIBRARY_PATH but no +RTS, then with an
Equinox I compile and +RTS -N2 -RTS. I get an error when I try to use
+RTS with your precompiled Equinox.
$ LD_LIBRARY_PATH=/home/t-nathac/v/haskellcontracts.git/libgmp10/usr/lib:/home/t-nathac/v/haskellcontracts.git/libffi6/usr/lib/i386-linux-gnu/
../Folkung/Haskell/equinox
mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
35s
$ LD_LIBRARY_PATH=/home/t-nathac/v/haskellcontracts.git/libgmp10/usr/lib:/home/t-nathac/v/haskellcontracts.git/libffi6/usr/lib/i386-linux-gnu/
../Folkung/Haskell/equinox +RTS -N2 -RTS
mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
equinox: Most RTS options are disabled. Link with -rtsopts to enable them.
$ ../Folkung.comp/Haskell/equinox +RTS -N2 -RTS
mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
44s
$ ../Folkung.comp/Haskell/equinox
mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
63s
???
Maybe the newer libgmp10 and libffi6 are much better than whatever I
get when I compile here?
-nathan
Koen Claessen
> Could not find module `CPUTime'
> It is a member of the hidden package `haskell98-2.0.0.0'.
> Use -v to see a list of the files searched for.
Hm... I don't get this error. Does it go away when you write:
import System.CPUTime
instead of
import CPUTime?
The solution you use seems a bit excessive...
> $ LD_LIBRARY_PATH=/home/t-nathac/v/haskellcontracts.git/libgmp10/usr/lib:/home/t-nathac/v/haskellcontracts.git/libffi6/usr/lib/i386-linux-gnu/
> ../Folkung/Haskell/equinox
> mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
>
> 35s
>
> $ ../Folkung.comp/Haskell/equinox +RTS -N2 -RTS
> mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
>
> 44s
>
> $ ../Folkung.comp/Haskell/equinox
> mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
>
> 63s
I don't understand this!
/Koen
Nathan Collins
>> $ make -C Haskell equinox
>> Flags.hs:54:8:
>> Could not find module `CPUTime'
>> It is a member of the hidden package `haskell98-2.0.0.0'.
>> Use -v to see a list of the files searched for.
>
> Hm... I don't get this error. Does it go away when you write:
Are you using GHC 7.x for x < 2 by any chance? It looks like this
problem starts with GHC 7.2:
http://www.mail-archive.com/glasgow-ha...@haskell.org/msg19983.html
The "problem" is that your code mixes Haskell 98 package names and
modern package names.
Our machine has
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version
7.2.1.20110809
> import System.CPUTime
>
> instead of
>
> import CPUTime?
It's a little more involved than that :) But yes, with enough editing
of the source I can build with GHC 7. Here's a no-context diff
showing the changes I had to make to get GHC 7 to work:
$ diff -rU0 ./Folkung ./Folkung.comp | grep -v '^Binary files\|^Only
in' | tee make-
equinox-compile-with-ghc-7.U0-diff
diff -rU0 ./Folkung/Haskell/Equinox/ConSat.hs
./Folkung.comp/Haskell/Equinox/ConSat.
hs
--- ./Folkung/Haskell/Equinox/ConSat.hs 2011-10-25 16:55:00.000000000 +0100
+++ ./Folkung.comp/Haskell/Equinox/ConSat.hs 2011-12-08
14:36:42.000000000 +0000
@@ -54 +54 @@
-import IO
+import System.IO
@@ -57 +57 @@
-import List( intersperse )
+import Data.List( intersperse )
diff -rU0 ./Folkung/Haskell/Equinox/FolSat.hs
./Folkung.comp/Haskell/Equinox/FolSat.
hs
--- ./Folkung/Haskell/Equinox/FolSat.hs 2011-11-15 07:04:09.000000000 +0000
+++ ./Folkung.comp/Haskell/Equinox/FolSat.hs 2011-12-08
14:37:39.000000000 +0000
@@ -29,2 +29 @@
-import List hiding ( union, insert, delete )
-import Maybe
+import Data.List hiding ( union, insert, delete )
@@ -40 +39 @@
-import IO
+import System.IO
diff -rU0 ./Folkung/Haskell/Equinox/TermSat.hs
./Folkung.comp/Haskell/Equinox/TermSa
t.hs
--- ./Folkung/Haskell/Equinox/TermSat.hs 2011-10-25
16:55:01.000000000 +0100
+++ ./Folkung.comp/Haskell/Equinox/TermSat.hs 2011-12-08
14:36:19.000000000 +0000
@@ -60,2 +60,2 @@
-import List
-import Maybe
+import Data.List
+import Data.Maybe
@@ -64 +64 @@
-import IO
+import System.IO
diff -rU0 ./Folkung/Haskell/Flags.hs ./Folkung.comp/Haskell/Flags.hs
--- ./Folkung/Haskell/Flags.hs 2011-11-11 17:12:44.000000000 +0000
+++ ./Folkung.comp/Haskell/Flags.hs 2011-12-08 14:41:50.000000000 +0000
@@ -44 +44,4 @@
-import System
+import System.Exit
+ ( exitWith
+ , ExitCode(..)
+ )
@@ -46 +49 @@
-import List
+import Data.List
@@ -52 +55 @@
-import Char
+import Data.Char
@@ -54 +57 @@
-import CPUTime
+import System.CPUTime
diff -rU0 ./Folkung/Haskell/Main.hs ./Folkung.comp/Haskell/Main.hs
--- ./Folkung/Haskell/Main.hs 2011-11-11 17:12:01.000000000 +0000
+++ ./Folkung.comp/Haskell/Main.hs 2011-12-08 14:47:54.000000000 +0000
@@ -29 +29 @@
-import System
+import System.Exit
@@ -33 +33 @@
-import IO( hSetBuffering, stdout, BufferMode(..) )
+import System.IO( hSetBuffering, stdout, BufferMode(..) )
diff -rU0 ./Folkung/Haskell/Output.hs ./Folkung.comp/Haskell/Output.hs
--- ./Folkung/Haskell/Output.hs 2011-10-25 16:54:35.000000000 +0100
+++ ./Folkung.comp/Haskell/Output.hs 2011-12-08 14:42:19.000000000 +0000
@@ -26 +26,4 @@
-import System
+import System.Exit
+ ( exitWith
+ , ExitCode(..)
+ )
diff -rU0 ./Folkung/Haskell/Parsek.hs ./Folkung.comp/Haskell/Parsek.hs
--- ./Folkung/Haskell/Parsek.hs 2011-10-25 16:54:35.000000000 +0100
+++ ./Folkung.comp/Haskell/Parsek.hs 2011-12-08 14:39:08.000000000 +0000
@@ -104 +104 @@
-import Monad
+import Control.Monad
@@ -109 +109 @@
-import List
+import Data.List
@@ -114 +114 @@
-import Char
+import Data.Char
diff -rU0 ./Folkung/Haskell/ParseProblem.hs
./Folkung.comp/Haskell/ParseProblem.hs
--- ./Folkung/Haskell/ParseProblem.hs 2011-10-25 16:54:35.000000000 +0100
+++ ./Folkung.comp/Haskell/ParseProblem.hs 2011-12-08
14:46:49.000000000 +0000
@@ -26 +26 @@
-import System
+import System.Exit
@@ -29 +28,0 @@
- , getEnv
@@ -32 +31,5 @@
-import Char
+import System.Environment
+ ( getEnv
+ )
+
+import Data.Char
@@ -41 +44 @@
-import List
+import Data.List
@@ -48 +51 @@
-import IO
+import System.IO
@@ -51 +53,0 @@
- , try
@@ -56,0 +59 @@
+ , try
@@ -59 +62 @@
-import Monad
+import Control.Monad
@@ -77 +80 @@
- mtptp <- IO.try (getEnv "TPTP")
+ mtptp <- System.IO.Error.try (getEnv "TPTP")
@@ -119 +122 @@
- ees <- IO.try (readFile name)
+ ees <- System.IO.Error.try (readFile name)
diff -rU0 ./Folkung/Haskell/Sat.hs ./Folkung.comp/Haskell/Sat.hs
--- ./Folkung/Haskell/Sat.hs 2011-10-25 16:54:35.000000000 +0100
+++ ./Folkung.comp/Haskell/Sat.hs 2011-12-08 14:37:03.000000000 +0000
@@ -72 +72 @@
-import Random
+import System.Random
I've attached a proper (with context) diff, in case you want to apply
it as a patch.
> The solution you use seems a bit excessive...
The
make GHC=ghc6 ...
solution, or the LD_LIBRARY_PATH solution? I think both are simpler
than editing the source as above, but the LD_LIBRARY_PATH solution is
definitely complicated.
>> $ LD_LIBRARY_PATH=/home/t-nathac/v/haskellcontracts.git/libgmp10/usr/lib:/home/t-nathac/v/haskellcontracts.git/libffi6/usr/lib/i386-linux-gnu/
>> ../Folkung/Haskell/equinox
>> mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
>>
>> 35s
>>
>> $ ../Folkung.comp/Haskell/equinox +RTS -N2 -RTS
>> mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
>>
>> 44s
>>
>> $ ../Folkung.comp/Haskell/equinox
>> mult-gt.hs.mult.tptp.hybrid-hand-edit-more-quantifier
>>
>> 63s
>
> I don't understand this!
Me neither.
-nathan
Nathan Collins
Short version: I'm dumb :)
Long version: I found two differences between the old and new
translations of mult-gt.hs, in addition to the case translations. The
first is that the old translation *only* has the "extra" condition on
projections. E.g. the old .tptp has
forall x. min(pred (S x)) -> pred (S x) = x
whereas the new .tptp has
forall x. min(S x) -> pred (S x) = x.
But that doesn't matter either, for the model size.
What I think matters is the second difference: the old mult-gt.hs
doesn't even typecheck. It uses a function 'positive' that is not
defined. The new code uses 'not' and 'isZero', which are defined. I
fixed this on November 24 after adding a type checker for contracts
[1], but then forgot about it :P
In any case, the current code now has 6 different case translations: 2
choices for structure (conjunctive or disjunctive) times 3 choices for
quantifiers (projections only, hybrid, quantifiers only).
-nathan