Closed joe-hauns closed 3 months ago
Files:
> ./bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 -fdi 41 TPTP-v8.2.0//Problems/NUM/NUM930_5.p
% Running in auto input_syntax mode. Trying TPTP
Condition in file /home/jschoiss/.vampire-benchexec/build/repos/vampire/Indexing/TermSharing.cpp, line 177 violated:
_wellSortednessCheckingDisabled || SortHelper::areImmediateSortsValidPoly(t)
Value of t->toString() is: one_one(fFalse)
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b61 on 2024-03-22 08:41:08 +0000)
call stack: 0x406f0a 0x2690a99 0x40a036 0x4090a7 0x4084b1 0x407522 0x7a4c52 0x7a4ff9 0x4eca59 0x7aa92e 0x7aa6eb 0x7aa472 0x7a9efa 0x797d24 0x79a142 0x621f11 0x621a60 0x7adede 0x73ac73 0x73a9b9 0x73a532 0x56467b 0x663506 0x486d07 0x416598
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----
Files:
--decode lrs+11_5309:524288_anc=all:drc=encompass:foolp=on:gs=on:kws=precedence:nm=13:nwc=5.0321:spb=units_1
Example:
./bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 --input_syntax tptp --decode lrs+11_5309:524288_anc=all:drc=encompass:foolp=on:gs=on:kws=precedence:nm=13:nwc=5.0321:spb=units_1 --time_limit 3 /TPTP-v8.2.0//Problems/SYO/SYO500_8.008.p
(...)
% # SZS output end Saturation.
Condition in file /home/jschoiss/.vampire-benchexec/build/repos/vampire/Shell/UIHelper.cpp, line 536 violated:
!s_expecting_unsat
----- stack dump -----
Version : Vampire 4.8 (commit 23d7e9c3b61 on 2024-03-22 08:41:08 +0000)
call stack: 0x406f0a 0x2690a99 0x40a036 0x4090a7 0x4084cf 0x943bf8 0x4144e0 0x416598
(use '--traceback on' to get a human-readable stack trace)
----- end of stack dump -----
Files:
SYN/SYN000_4.p Options: --input_syntax tptp Issue: Crash in TPTP parser
Example:
/home/jschoiss/.vampire-benchexec/build/bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 --input_syntax tptp --time_limit 10 /home/jschoiss/TPTP-v8.2.0//Problems/SYN/SYN000_4.p
Condition in file /home/jschoiss/.vampire-benchexec/build/repos/vampire/Lib/Stack.hpp, line 201 violated: _stack+n < _cursor ----- stack dump ----- Version : Vampire 4.8 (commit 23d7e9c3b61 on 2024-03-22 08:41:08 +0000) call stack: 0x406f0a 0x2690a99 0x40a01d 0x942f21 0x9429c6 0x9423d1 0x96a7a3 0x96ab4c 0x97db3e 0x97e427 0x565ab1 0x564516 0x40b2d7 0x40e278 0x4144e0 0x416598 (use '--traceback on' to get a human-readable stack trace) ----- end of stack dump -----
Files:
Issue: TPTP parser fails. Options --input_syntax tptp
Example:
./bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 --input_syntax tptp --time_limit 9 TPTP-v8.2.0//Problems/SYN/SYN000_2.p
--------------------------------------------------------------------------------
Parsing Error on line 69: Unsupported unit type 'assumption' found at position 2013
Files:
Issue: TPTP parsing fails. Options --input_syntax tptp
./bin/vampire-23d7e9c3b61479bc14e1687f917c22f80dc7c8f1-Debug-z3 --input_syntax tptp --time_limit 7 TPTP-v8.2.0//Problems/LCL/LCL946_10.p
--------------------------------------------------------------------------------
Parsing Error on line 688: Failed to create predicate application for $ki_exists_in_world_$i of type 0x4967a90
The sort $i of the intended term argument X0 (at index 0) is not an instance of sort '$ki_world'
I ran the current master in default mode on all of smtlib and tptp over the weekend and here are the results:
benchmarks: 119661
solved: 58232 (48 %)
----------------------------------------------------------------------
solver master:
options:
errors: 4
assertion violation: /home/jschoiss/.vampire-benchexec/build/repos/vampire/Kernel/SortHelper.cpp@95: 88
master ITP/ITP276_4.p
master ITP/ITP210_4.p
master ITP/ITP278_4.p
master ITP/ITP217_4.p
master ITP/ITP222_4.p
master ITP/ITP236_4.p
master ITP/ITP225_4.p
master ITP/ITP259_4.p
master ITP/ITP288_4.p
master ITP/ITP231_4.p
...
assertion violation: /home/jschoiss/.vampire-benchexec/build/repos/vampire/Lib/Stack.hpp@201: 1
master SYN/SYN000_4.p
assertion violation: /home/jschoiss/.vampire-benchexec/build/repos/vampire/Parse/TPTP.cpp@1940: 49
master SWW/SWW470^3.p
master ITP/ITP216^1.p
master ITP/ITP088^1.p
master ITP/ITP198^2.p
master ITP/ITP030^2.p
master ITP/ITP089^2.p
master SEU/SEU907^5.p
master ITP/ITP094^2.p
master SWW/SWW470^2.p
master ITP/ITP039^2.p
...
parser exception: 1371
master LIN/LIN003^1.p
master SEU/SEU678^1.p
master SEU/SEU547^1.p
master SEU/SEU510^1.p
master SEU/SEU720^1.p
master SEU/SEU681^1.p
master SEU/SEU583^1.p
master GEO/GEO438^1.p
master SEU/SEU607^1.p
master SEU/SEU645^1.p
...
unsound: 0
solved: 58232
master SWC/SWC128-1.p
master SYN/SYN915-1.p
master HWV/HWV095-1.p
master HWV/HWV093-1.p
master HWV/HWV089-1.p
master COL/COL086-1.p
master COL/COL083-1.p
master COL/COL084-1.p
master COL/COL085-1.p
master ALG/ALG399-1.p
...
unique: 58232
master SWC/SWC128-1.p
master SYN/SYN915-1.p
master HWV/HWV095-1.p
master HWV/HWV093-1.p
master HWV/HWV089-1.p
master COL/COL086-1.p
master COL/COL083-1.p
master COL/COL084-1.p
master COL/COL085-1.p
master ALG/ALG399-1.p
...
I think this is the same bugs as i reported (but a bit more coarse as i didn't look into all the parser exceptions for this run. Here is the full problem list: analyse-res.txt
Bug 1 seems to result from an instance of polymorphic $let
. Minimised, it looks something like this:
tff(ty_t_List_Olist,type,
list: $tType > $tType ).
tff(sy_c_List_Olist_OCons,type,
cons:
!>[A: $tType] : ( A > fun(list(A),list(A)) ) ).
tff(sy_c_List_Oappend,type,
append:
!>[A: $tType] : ( ( list(A) * list(A) ) > list(A) ) ).
tff(sy_c_List_Osubseqs,type,
subseqs:
!>[A: $tType] : ( list(A) > list(list(A)) ) ).
tff(sy_c_List_Olist_Omap,type,
map:
!>[A: $tType,Aa: $tType] : ( ( fun(A,Aa) * list(A) ) > list(Aa) ) ).
tff(sy_c_aa,type,
aa:
!>[A: $tType,B: $tType] : ( ( fun(A,B) * A ) > B ) ).
% nth_append
tff(fact_2816_subseqs_Osimps_I2_J,axiom,
! [A: $tType,Xa: A,Xs: list(A)] :
subseqs(A,aa(list(A),list(A),cons(A,Xa),Xs)) = $let(
xss: list(list(A)),
xss:= subseqs(A,Xs),
append(list(A),map(list(A),list(A),cons(A,Xa),xss),xss) ) ).
We ask SortHelper
for the type of xss
and it fails with the assertion above, because xss
is just xss
, not xss(A)
. If you disable the assertion, it seems to go through and get clausified OK into something well-typed. @mezpusz - I think you're the expert here. Is my assessment correct? What do you think the fix should be?
The assertion seems OK for most cases, but maybe we could set a flag for let-constants like this one and skip it for those.
@MichaelRawson As far as I understand, the declaration of xss
is not well-formed, and rather it should be something like !>[A: $tType] : list(list(A))
, so that A
is not free and we can access it (at least internally). But then we would need to use xss(A)
everywhere internally. I couldn't find a good reference for polymorphic let
s, I suppose the input is correct.
Bug 4 seems to be #553 - if you add some parens to the enclosed equation it parses quite happily.
As is Bug 5 - same problem, different error.
Bug 7 doesn't reproduce for me - maybe we fixed something in the meantime?
Bug 12 seems to be bad TPTP, I've filed a bug with Geoff.
Bug 11: TPTP assumptions
are tricky because you should consider them only as intermediate lemmas to prove. We don't currently support these and it's only used in these files so I think we can consider this "won't fix" for now. We should probably maintain a blacklist of TPTP problems that we won't even attempt.
Ditto for SYN000_4
- there is some funky tuple syntax. However, we shouldn't straight-up crash, which we do - patch incoming.
Have now filed or fixed all of these. Thanks @joe-hauns !
Doing some randomized testing I ran into a couple of miscellanious crashes. Many of them are related to parsing. In some cases we just do not support what's being parsed, in some cases it's an actual crash. I decided I'll make an issue here so we can dicuss all of these crashes, and decide how to fix them, or how to exit more gracefully than crashing:
Bug 1:
Files:
Example:
Bug 2
Files:
Options:
-fda 4
Issue: Crash in function definition introduction
Example:
Bug 3
Files:
--input_syntax tptp
Issue: We return aParser Error
on valid TPTP because of a feature (HOL + Theories) that we don't support. Here we should actually return aUser Error
instead, right?Example:
Bug 4:
Files:
--input_syntax tptp
Issue: Vampire reports that the sorts of an equality do not agree during parsing. I guess this is a bug in vampire and the input files are actually valid tptp (considering how many times this issue occurrs). Example:Bug 5:
Files:
Options:
--input_syntax tptp
Issue Vampire reports that some term is not of boolean sort but used as formula. Again I reckon the TPTP is valid and there is some bug in vampire. Example:Bug 6:
Files:
Options:
-newcnf on
Issue: crash somewhere in newcnf due to some boolean term not being special.Example:
Bug 7:
Files: