Use Dolmen locations in recoverable/fatal errors #1284
Conversation
There was a problem hiding this comment.
Looks sensible overall.
I think we might want to have a less verbose output for errors reported in (error) where using the Emacs format doesn't make that much sense; something terser like CVC5's file:line.columns: message would be better suited. We can iterate on the error messages themselves, however the escaping issue needs to be fixed (" should be displayed as "").
tests/cram.t/run.t
Outdated
|
|
||
| unknown | ||
|
|
||
| $ echo '(set-option :produce-models true) (set-logic ALL) (check-sat) (get-objectives)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error --sat-solver Tableaux 2>/dev/null | ||
|
|
||
| unknown | ||
| (error "the selected solver does not support optimization") | ||
| (error "File "<stdin>", line 1, character 62-78: |
There was a problem hiding this comment.
It is not correct to have quotes inside strings in SMT-LIB format; they need to be replaced with double quotes "".
There was a problem hiding this comment.
I imported the function Dolmen.Std.Loc.fmt and adapted it. Yet, if the file name contains double quotes, they won't be escaped. I can write a function to handle them if you think it is important.
There was a problem hiding this comment.
Thanks! I think that since this is a format that we are using to interoperate with tools (not just users) we should be robust here -- the escaping should ideally be done generically in print_smtlib_err. I will make a separate PR.
src/lib/frontend/translate.ml
Outdated
| let rec aux acc (stmt: _ Typer_Pipe.stmt) = | ||
| let loc = Dolmen.Std.Loc.loc file stmt.loc in |
There was a problem hiding this comment.
Nit: Calling this st_loc would make it a bit less verbose to output the commands below.
src/bin/common/solving_loop.ml
Outdated
| | {contents = `Other (custom, args); loc = l; _} -> | ||
| handle_custom_statement ~loc:l custom args st |
There was a problem hiding this comment.
| | {contents = `Other (custom, args); loc = l; _} -> | |
| handle_custom_statement ~loc:l custom args st | |
| | {contents = `Other (custom, args); loc; _} -> | |
| handle_custom_statement ~loc custom args st |
There was a problem hiding this comment.
The variable st_loc already contains the location of the statement but the value Dolmen.Loc.compact is buggy (even its type is incorrect!), so we cannot transform a full location in handle_custom_statement into a compact location. Guillaume will address this issue in the next Dolmen release.
As a workaround, I passed the compact location of the statement itself here and used a different name for clarity. Actually the types are different, so shadowing wasn't that bad.
I applied your suggestion and add todo comment too.
Halbaroth
force-pushed
the
dolmen-location
branch
from
7e96cca to
f2a5e42
Compare
This PR includes two modifications:
LoctoDolmen.Std.Loc.loc.Solving_loop(when it makes sense to print such locations).