2020-07-19 15:32:26 (GMT)
If you run zip on bool_calculi and run it with
./zipperposition.exe ~/Documents/TPTP-v7.3.0/Problems/SEU/SEU301+1.p --mode=ho-pragmatic --max-inferences=3 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=no-cases --ext-rules=off --ho-prim-enum=none --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework -q "1|const|conjecture-relative-var(1,s,f)" -q "1|prefer-processed|pnrefined(1,1,1,2,2,2,0.5)" -q "1|prefer-sos|staggered(1)" -q "2|prefer-fo|default" -q "2|defer-sos|staggered(2)" -q "2|prefer-easy-ho|conjecture-relative-struct(1.5,3.5,2,3)" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection11 --solve-formulas=true --ord=lambda_rpo --prec-gen-fun=unary_first -bt
2020-07-19 15:32:41 (GMT)
You will get the strangest error message
2020-07-19 15:33:3 (GMT)
After a lot of debugging I discovered that two terms that are syntactially the same have different hash code
2020-07-19 15:33:36 (GMT)
Those two terms are builtin terms -- the term representing type Iota
2020-07-19 15:33:40 (GMT)
And they are in TypedSTerm
2020-07-19 15:34:24 (GMT)
Is there any special hashing of types that I cannot find?
2020-07-19 16:44:18 (GMT)
first thing to do is to use --print-hashconsing-id.
2020-07-19 16:44:27 (GMT)
(hashconsing bugs are pretty annoying.)
2020-07-19 16:44:51 (GMT)
Does it also happen on combinators?
2020-07-20 10:59:52 (GMT)
OK I investigated this bug a little bit. Here is the debug output:
** hash 1 **
computed: prop=69
computed: ι=71
computed: ι=70
2020-07-20 11:0:24 (GMT)
As you can see, different calls to hash with the same object give different hash values
2020-07-20 11:2:27 (GMT)
Note that this is all on the level of TypedSTerm
2020-07-20 11:3:9 (GMT)
The bug did not appear in combinators because Equality did not have type argument by default
2020-07-20 11:3:16 (GMT)
(on the level of TypedSTerms)
2020-07-20 11:3:23 (GMT)
I made equality polymorphic everywhere
2020-07-20 13:5:47 (GMT)
2020-07-20 13:6:5 (GMT)
OK, I think this is a deeper OCaml problem, and I do not seem to fully understand this:
2020-07-20 13:15:54 (GMT)
I have put printfs in the hash function for TypedSTerm
2020-07-20 13:16:34 (GMT)
It turns out that for the pure types (e.g. TST.AppBuiltin(Term,[])) hash_rec_ does not get executed!
2020-07-20 13:16:47 (GMT)
And every time a different hash id is computed for the same type
2020-07-20 13:17:26 (GMT)
what I think happens is that somehow a default OCaml hash function is called on types, and it overrides the values of our computed hash function
2020-07-20 13:19:35 (GMT)
This is the output from the first two calls to hash on TST:
computed: ι::19[]=71
hash_value: ι:19(1006273044)
computed: ι::19[]=70
hash_value: ι:19(1006273044)
2020-07-20 13:19:46 (GMT)
computed is what is returned as result of hash_rec_
2020-07-20 13:20:5 (GMT)
hash_value is what should be the value by copying the code in hash_rec_ and executing it
2020-07-20 13:20:33 (GMT)
19 is the Builtin.as_int of Term type
2020-07-20 13:20:57 (GMT)
I have pushed the debug state to hash_bug branch
2020-07-20 13:44:58 (GMT)
OK, I think I have found a fix:
There is this concept of a Meta term (which I do not know what it is) which was confusing the hash_rec_ function.
You called hash_rec_ on t.term instead of view t.
view t dereferences Meta term, which we must do when we compute hash code.
It seems to me that you pretty much never want to deal with raw t.term?
Shoud it be hidden somehow and forbidden to be accessed even by inner interfaces? This was a particularly nasty bug, so I think we should once and for all decide when to use t.term
2020-07-20 14:17:47 (GMT)
Ah, meta is a temporary unification variable used for type inference. You just cannot hashcons these, they'll disappear.
2020-07-20 14:18:23 (GMT)
Basically when inferring types, when we don't know, we add a meta variable and make sure it gets unified with an actual type before declaring success. That's more or less Hindley-Milner type inference.
2020-07-20 14:18:47 (GMT)
Petar Vukmirovic said:
OK, I think I have found a fix:
There is this concept of a Meta term (which I do not know what it is) which was confusing thehash_rec_function.
You called hash_rec_ ont.terminstead ofview t.
view tdereferences Meta term, which we must do when we compute hash code.
It seems to me that you pretty much never want to deal with rawt.term?
Shoud it be hidden somehow and forbidden to be accessed even by inner interfaces? This was a particularly nasty bug, so I think we should once and for all decide when to uset.term
Yes, I think TypedSTerm.view is there for this exact reason :)
2020-07-20 14:19:13 (GMT)
But hashconsing TypedSTerm might be a bit complicated, really.
2020-07-20 14:23:40 (GMT)
The problem is that these metas are not resolved immediately.
You could have a mix of hashconsed/not-hashconsed terms (where not-hashconsed terms have id=-1) and have equality work modulo that, but it's tricky and error prone. Maybe we can have another AST for CNF?