You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I found a class of parsing errors for thf problems. Some examples of this:
> vampire --input_syntax tptp $TPTP/Problems/SYO/SYO898^9.p
User error: Undeclared type constructor mworld/0 (detected at or around line 38)
> vampire --input_syntax tptp $TPTP/Problems/SEU/SEU976^5.p
User error: Undeclared type constructor a/0 (detected at or around line 35)
> vampire --input_syntax tptp $TPTP/Problems/SEV/SEV217^5.p
User error: Undeclared type constructor c/0 (detected at or around line 38)
> vampire --input_syntax tptp $TPTP/Problems/LCL/LCL942^2.p
User error: Undeclared type constructor mworld/0 (detected at or around line 38)
> vampire --input_syntax tptp $TPTP/Problems/SYO/SYO492^6.p
User error: Undeclared type constructor mu/0 (detected at or around line 62)
> vampire --input_syntax tptp $TPTP/Problems/SWW/SWW971^5.p
User error: Undeclared type constructor mworld/0 (detected at or around line 39)
> vampire --input_syntax tptp $TPTP/Problems/SEV/SEV133^5.p
User error: Undeclared type constructor atype/0 (detected at or around line 35)
> vampire --input_syntax tptp $TPTP/Problems/SEV/SEV211^5.p
User error: Undeclared type constructor a/0 (detected at or around line 35)
> vampire --input_syntax tptp $TPTP/Problems/SYO/SYO463^3.p
User error: Undeclared type constructor mu/0 (detected at or around line 63)
> vampire --input_syntax tptp $TPTP/Problems/DAT/DAT334^21.p
User error: Undeclared type constructor mworld/0 (detected at or around line 39)
I had a look and I think the issue is the use of Signature::addFunction instead of Signature::addTypeConhere.
This could be fixed easily but there is some witchery going on in TPTP::addUninterpretedConstant which I'm not quite sure how to nicely resolve.
I will have a look at this at some point as I'm planning some more tidying and optimization of the signature in general. But that propably won't happen too soon. So if someone feels like it I'm happy if they resolve it :)
For now i'll just add this as a "known issue". Practiaclly it doesn't make any difference right now anyways because if we fix the parsing we will die with the error message This version of Vampire is not yet HOLy anyways.
The text was updated successfully, but these errors were encountered:
Thinking about it for a bit I think the special casing "vAND" & friends doesn't need to happen for type constructors anyways, so the fix should be quite simple. just pushed a branch thf-parser-fix. Does this look alright @ibnyusuf ?
This looks reasonable, but I'm still struggling to understand why this wouldn't cause many more parsing errors? If we are storing every type constructor as a function symbol, I would expect many more such errors? I'll try and look into this a little more deeply when I have some time.
I found a class of parsing errors for
thf
problems. Some examples of this:I had a look and I think the issue is the use of
Signature::addFunction
instead ofSignature::addTypeCon
here.This could be fixed easily but there is some witchery going on in
TPTP::addUninterpretedConstant
which I'm not quite sure how to nicely resolve.I will have a look at this at some point as I'm planning some more tidying and optimization of the signature in general. But that propably won't happen too soon. So if someone feels like it I'm happy if they resolve it :)
For now i'll just add this as a "known issue". Practiaclly it doesn't make any difference right now anyways because if we fix the parsing we will die with the error message
This version of Vampire is not yet HOLy
anyways.The text was updated successfully, but these errors were encountered: